Sterbenz exact subtraction

Sterbenz's lemma applies to the rounded-real grid of every fmt: two same-sign representable values within a factor of two have an exactly representable difference. For an IEEE descriptor, subtraction of the corresponding finite model values is finite and decodes to that exact real difference. The same-sign forms cover negative operands and zero as well.

References

• R. P. Brent and P. Zimmermann, Modern Computer Arithmetic, Theorem 3.4. https://members.loria.fr/PZimmermann/mca/mca-cup-0.5.9.pdf
• Flocq, Flocq.Prop.Sterbenz. https://flocq.gitlabpages.inria.fr/flocq/html/Flocq.Prop.Sterbenz.html

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_sub_eq_of_sterbenz (fmt : FloatFormat) {u v : ℝ} (hu : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) u) (hv : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) v) (hupos : 0 < u) (hvpos : 0 < v) (huv : u ≤ 2 * v) (hvu : v ≤ 2 * u) : roundAt fmt (u - v) = u - v

Sterbenz exactness for the rounded-real grid selected by fmt: two positive representable reals within a factor of two have a representable difference, so nearest-even rounding changes nothing.

The nonnegative and same-sign variants below also cover zero and negative operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sub_eq_of_sterbenz {fmt : FloatFormat} {x y : Model fmt} (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hxpos : 0 < x.toReal) (hypos : 0 < y.toReal) (hxy : x.toReal ≤ 2 * y.toReal) (hyx : y.toReal ≤ 2 * x.toReal) : toReal (x.sub y) = x.toReal - y.toReal

Subtraction of positive finite executable values within a factor of two has no rounding error.

The Sterbenz hypotheses also bound the exact difference by one of the finite operands, so the theorem derives finiteness of the executable result instead of assuming it.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_sub_eq_of_sterbenz_of_nonneg (fmt : FloatFormat) {u v : ℝ} (hu : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) u) (hv : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) v) (hupos : 0 ≤ u) (hvpos : 0 ≤ v) (huv : u ≤ 2 * v) (hvu : v ≤ 2 * u) : roundAt fmt (u - v) = u - v

Sterbenz exactness for nonnegative representable reals, including the zero case.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_sub_eq_of_sterbenz_of_same_sign (fmt : FloatFormat) {u v : ℝ} (hu : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) u) (hv : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) v) (hsign : 0 ≤ u * v) (huv : |u| ≤ 2 * |v|) (hvu : |v| ≤ 2 * |u|) : roundAt fmt (u - v) = u - v

Sterbenz exactness for representable reals of the same sign within a factor of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_sub_of_same_sign {fmt : FloatFormat} {x y : Model fmt} (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hsign : 0 ≤ x.toReal * y.toReal) : isFinite (x.sub y) = true

Same-sign finite subtraction cannot overflow, independently of the factor-of-two condition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sub_eq_of_sterbenz_of_same_sign {fmt : FloatFormat} {x y : Model fmt} (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hsign : 0 ≤ x.toReal * y.toReal) (hxy : |x.toReal| ≤ 2 * |y.toReal|) (hyx : |y.toReal| ≤ 2 * |x.toReal|) : toReal (x.sub y) = x.toReal - y.toReal

Subtraction of finite values of the same sign within a factor of two has the exact real difference. The real-valued statement includes both signs of zero.