Extended-real semantics of interval endpoint selection

IEEE minimum and maximum agree with lattice min and max on non-NaN values. This module lifts that contract through the four-corner selectors used by executable interval multiplication and division.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.toEReal_minOfFour_eq {fmt : FloatFormat} (a b c d : Model fmt) (haNaN : a.isNaN = false) (hbNaN : b.isNaN = false) (hcNaN : c.isNaN = false) (hdNaN : d.isNaN = false) : (minOfFour a b c d).toEReal = min (min a.toEReal b.toEReal) (min c.toEReal d.toEReal)

Extended-real semantics of the four-way minimum on non-NaN inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.toEReal_maxOfFour_eq {fmt : FloatFormat} (a b c d : Model fmt) (haNaN : a.isNaN = false) (hbNaN : b.isNaN = false) (hcNaN : c.isNaN = false) (hdNaN : d.isNaN = false) : (maxOfFour a b c d).toEReal = max (max a.toEReal b.toEReal) (max c.toEReal d.toEReal)

Extended-real semantics of the four-way maximum on non-NaN inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.toEReal_minOfFour_le_of_le {fmt : FloatFormat} (a b c d : Model fmt) (haNaN : a.isNaN = false) (hbNaN : b.isNaN = false) (hcNaN : c.isNaN = false) (hdNaN : d.isNaN = false) {a' b' c' d' : EReal} (ha : a.toEReal ≤ a') (hb : b.toEReal ≤ b') (hc : c.toEReal ≤ c') (hd : d.toEReal ≤ d') : (minOfFour a b c d).toEReal ≤ min (min a' b') (min c' d')

Pointwise upper bounds on four non-NaN values bound their executable four-way minimum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.le_toEReal_maxOfFour_of_le {fmt : FloatFormat} (a b c d : Model fmt) (haNaN : a.isNaN = false) (hbNaN : b.isNaN = false) (hcNaN : c.isNaN = false) (hdNaN : d.isNaN = false) {a' b' c' d' : EReal} (ha : a' ≤ a.toEReal) (hb : b' ≤ b.toEReal) (hc : c' ≤ c.toEReal) (hd : d' ≤ d.toEReal) : max (max a' b') (max c' d') ≤ (maxOfFour a b c d).toEReal

Pointwise lower bounds on four non-NaN values bound their executable four-way maximum.