Total EReal semantics helpers for IEEE32Exec

BridgeERealTotal.lean defines toEReal? : IEEE32Exec → Option EReal, which is the canonical extended-real interpretation we use when we want to distinguish +∞ from -∞ and treat NaN as "unordered" (none).

In a few proof scripts, it is convenient to have a total function into EReal. We therefore define:

• toEReal : IEEE32Exec → EReal, which totalizes toEReal? by mapping the NaN case to 0.

Informal reading rule:

If you see a theorem stated using toEReal, it should be read under hypotheses that exclude NaNs (isNaN x = false). Under that assumption, toEReal x agrees with the intended toEReal? meaning and behaves exactly as you would expect:

• finite values map to ↑(toReal x),
• +∞/-∞ map to ⊤/⊥.

This file also collects small helper lemmas (toEReal_eq_ite, signed-zero simp facts, etc.) used by multiple IEEEExec proof modules.

toEReal (totalized) and unfolding helpers

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.toEReal (x : IEEE32Exec) : EReal

Total EReal interpretation of IEEE32Exec.

This is toEReal? with the NaN case mapped to 0.

Intended invariant: Most theorems about interval endpoints assume isNaN x = false. Under that precondition, the NaN branch is unreachable and toEReal agrees with the partial EReal semantics.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_of_toEReal? {x : IEEE32Exec} {r : EReal} (h : x.toEReal? = some r) : x.toEReal = r

If toEReal? x = some r, then toEReal x = r.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_of_toEReal?_none {x : IEEE32Exec} (h : x.toEReal? = none) : x.toEReal = 0

If toEReal? x = none, then toEReal x = 0.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_eq_ite (x : IEEE32Exec) : x.toEReal = if x.isNaN = true then 0 else if x.isInf = true then if x.signBit = true then ⊥ else ⊤ else ↑x.toReal

Convenient unfolding lemma for toEReal.

This is the form that works best with simp once you have established/assumed (non-)NaN and (non-)Inf facts.

Small finiteness helpers

These are convenience lemmas for switching between isFinite and special-value predicates in proofs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isInf_eq_false_of_isFinite_eq_true (x : IEEE32Exec) (hx : x.isFinite = true) : x.isInf = false

If x is finite, then x is not an infinity.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isNaN_eq_false_of_isFinite_eq_true (x : IEEE32Exec) (hx : x.isFinite = true) : x.isNaN = false

If x is finite, then x is not a NaN.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_eq_coe_toReal_of_isFinite (x : IEEE32Exec) (hx : x.isFinite = true) : x.toEReal = ↑x.toReal

On finite values, toEReal reduces to ↑(toReal x).

This is the lemma we use most often to turn an EReal endpoint goal into a ℝ goal.

Signed-zero simp facts

IEEE-754 has distinct bit patterns for +0 and -0, but both decode to real 0. In endpoint proofs we frequently want this fact at the toEReal level.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_signedZero (s : Bool) : (if s = true then negZero else posZero).toEReal = 0

Both signed zeros map to 0 under toEReal.

This is safe to use as a simp lemma: it is a very specific pattern and does not cause unfolding loops.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_posInf : posInf.toEReal = ⊤

toEReal interprets +∞ as ⊤.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_negInf : negInf.toEReal = ⊥

toEReal interprets -∞ as ⊥.