BridgeERealTotal

Extended-real (EReal) semantics for IEEE32Exec.

We use toReal? as the main “finite-only” semantic function in TorchLean. For some statements, though, we really want to distinguish +∞ from -∞ instead of collapsing both to none.

This file packages a slightly richer view:

• toEReal? x = none exactly for NaN (unordered),
• toEReal? x = some ⊤ / some ⊥ for +∞ / -∞,
• toEReal? x = some (↑(toReal x)) for finite values.

We then prove “golden theorem”-style lemmas for core ops, where the finite branch refines to the FP32 rounding-on-ℝ model (fp32Round) and the non-finite branch preserves IEEE-754 special behavior.

Background:

• IEEE 754-2019: https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg (1991): https://doi.org/10.1145/103162.103163

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

Extended-real interpretation of IEEE32Exec (none exactly for NaN).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal?_eq_none_iff_isNaN_eq_true (x : IEEE32Exec) : x.toEReal? = none ↔ x.isNaN = true

toEReal? is none exactly on NaN.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal?_eq_none_of_isNaN_eq_true (x : IEEE32Exec) (hx : x.isNaN = true) : x.toEReal? = none

NaNs stay outside the extended-real interpretation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isNaN_eq_false_of_isInf_eq_true (x : IEEE32Exec) (hx : x.isInf = true) : x.isNaN = false

A value classified as infinity is not classified as NaN.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_eq_true_of_isNaN_eq_false_of_isInf_eq_false (x : IEEE32Exec) (hnan : x.isNaN = false) (hinf : x.isInf = false) : x.isFinite = true

A non-NaN, non-infinite value is finite.

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

Finite executable floats coerce to EReal through their real interpretation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal?_add_eq_ite (x y : IEEE32Exec) : (x.add y).toEReal? = if (x.add y).isNaN = true then none else if (x.add y).isInf = true then some (if (x.add y).signBit = true then ⊥ else ⊤) else some ↑(fp32Round (x.toReal + y.toReal))

In the finite case, executable addition agrees with rounded real addition in EReal.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal?_mul_eq_ite (x y : IEEE32Exec) : (x.mul y).toEReal? = if (x.mul y).isNaN = true then none else if (x.mul y).isInf = true then some (if (x.mul y).signBit = true then ⊥ else ⊤) else some ↑(fp32Round (x.toReal * y.toReal))

In the finite case, executable multiplication agrees with rounded real multiplication in EReal.