Finite-operand helpers for directed arithmetic

Finite-operand classification facts support the format-generic directed arithmetic proofs. Keeping these facts separate lets each arithmetic module focus on its exact intermediate and rounding argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN1_none_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : x.chooseNaN1 = none

Unary NaN selection is inactive for a finite operand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.chooseNaN2_none_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.chooseNaN2 y = none

NaN selection is inactive when both operands are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significand_ne_zero_of_toDyadic?_some_of_isZero_eq_false {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hzero : x.isZero = false) : d.significand ≠ 0

A finite nonzero value decodes to a dyadic with nonzero significand.

Exact intermediates of finite operands

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_addDyadic_of_toDyadic?_some {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) : (addDyadic dx dy).toReal = x.toReal + y.toReal

The exact dyadic sum of two finite values denotes their real sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_mulDyadic_of_toDyadic?_some {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) : { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }.toReal = x.toReal * y.toReal

The exact dyadic product of two finite values denotes their real product.

Signed zero of an exactly cancelling sum

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_zeroForExactSum (fmt : FloatFormat) (mode : IEEERoundingMode) (leftSign rightSign : Bool) : (zeroForExactSum fmt mode leftSign rightSign).toReal = 0

The signed zero chosen for an exactly cancelling sum denotes zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_zeroForExactSum_eq_false (fmt : FloatFormat) (mode : IEEERoundingMode) (leftSign rightSign : Bool) : (zeroForExactSum fmt mode leftSign rightSign).isNaN = false

The signed zero chosen for an exactly cancelling sum is not a NaN.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_zeroForExactSum (fmt : FloatFormat) (mode : IEEERoundingMode) (leftSign rightSign : Bool) : (zeroForExactSum fmt mode leftSign rightSign).toEReal = 0

The signed zero chosen for an exactly cancelling sum denotes zero in the extended reals.

Directed operations on finite operands

For modes other than nearest-even, finite addition and multiplication reduce to rounding an exact dyadic intermediate; finite division with a nonzero divisor rounds an exact scaled rational. Exact cancellation has a separate signed-zero rule. Square root instead rounds the appropriate endpoint of a dyadic bracket around the exact root. These characterisations are shared by the enclosure, non-NaN, and finite-format proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addWithRounding_eq_of_toDyadic?_some {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearestEven) {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) : addWithRounding mode x y = if (addDyadic dx dy).significand = 0 then zeroForExactSum fmt mode dx.negative dy.negative else roundDyadicWithRounding fmt mode (addDyadic dx dy)

For finite operands, a directed addition is the directed rounding of the exact dyadic sum, or the rounding direction's signed zero when the sum cancels exactly.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulWithRounding_eq_of_toDyadic?_some {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearestEven) {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) : mulWithRounding mode x y = roundDyadicWithRounding fmt mode { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }

For finite operands, a directed multiplication rounds the exact dyadic product.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.divWithRounding_eq_of_toDyadic?_some {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearestEven) {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) (hy0 : y.isZero = false) : divWithRounding mode x y = roundRatWithRoundingScaled fmt mode (dx.negative ^^ dy.negative) dx.significand dy.significand (dx.exponent - dy.exponent)

For a finite dividend and a finite nonzero divisor, a directed division rounds the exact scaled rational quotient.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtWithRounding_eq_self_of_isZero {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearestEven) {x : Model fmt} (hfinite : x.isFinite = true) (hzero : x.isZero = true) : sqrtWithRounding mode x = x

Every directed square root fixes a finite zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtDown_eq_roundDyadicDown_of_toDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hsign : x.signBit = false) (hzero : x.isZero = false) : x.sqrtDown = roundDyadicDown fmt (sqrtDyadicBracket fmt d).lower

On a finite positive operand, sqrtDown rounds the lower square-root bracket downward.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtUp_eq_roundDyadicUp_of_toDyadic?_some {fmt : FloatFormat} {x : Model fmt} {d : Numerics.Dyadic} (hd : x.toDyadic? = some d) (hsign : x.signBit = false) (hzero : x.isZero = false) : x.sqrtUp = roundDyadicUp fmt (sqrtDyadicBracket fmt d).upper

On a finite positive operand, sqrtUp rounds the upper square-root bracket upward.