Finite-operand helpers for directed arithmetic

Finite-operand classification facts support the format-generic directed arithmetic proofs.

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, and finite division with a nonzero divisor rounds an exact scaled rational. Exact cancellation has its own signed-zero rule. Square root in a directed mode instead rounds the appropriate endpoint of a dyadic bracket around the exact root, and both nearest modes use the nearest-even sqrt. These characterisations are shared by the enclosure, non-NaN, and finite-format proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_eq_of_toDyadic?_some {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearest) {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) : x.add y mode = if (addDyadic dx dy).significand = 0 then zeroForExactSum fmt mode dx.negative dy.negative else Internal.Directed.roundDyadic 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.mul_eq_of_toDyadic?_some {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearest) {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) : x.mul y mode = Internal.Directed.roundDyadic 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.div_eq_of_toDyadic?_some {fmt : FloatFormat} (mode : IEEERoundingMode) (hmode : mode ≠ IEEERoundingMode.nearest) {x y : Model fmt} {dx dy : Numerics.Dyadic} (hdx : x.toDyadic? = some dx) (hdy : y.toDyadic? = some dy) (hy0 : y.isZero = false) : x.div y mode = Internal.Directed.roundRatScaled 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.sqrt_of_isZero {fmt : FloatFormat} {mode : IEEERoundingMode} {x : Model fmt} (hfinite : x.isFinite = true) (hzero : x.isZero = true) : x.sqrt mode = x

Square root fixes a finite zero of either sign in every rounding direction, for every descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_down_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.sqrt IEEERoundingMode.down = roundDyadicDown fmt (sqrtDyadicBracket fmt d).lower

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_up_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.sqrt IEEERoundingMode.up = roundDyadicUp fmt (sqrtDyadicBracket fmt d).upper

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