Correctness of binary subtraction

Subtraction is implemented as addition of the negated right operand. These theorems connect that implementation to exact real subtraction followed by one nearest-even rounding step.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_sub_of_abs_toReal_sub_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal - y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.sub y).isFinite = true

Finite operands whose exact real difference is within the destination's largest finite magnitude cannot overflow under nearest-even subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_sub_of_abs_add_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal| + |y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.sub y).isFinite = true

The triangle bound |x| + |y| ≤ maxFinite is a symbolic sufficient condition for finite nearest-even subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sub_eq_roundAt {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.sub y).isFinite = true) : (x.sub y).toReal = roundAt fmt (x.toReal - y.toReal)

Finite subtraction is exact real subtraction followed by one nearest-even format rounding.

The hypothesis hfin excludes overflow by asking that the executable difference be finite; toReal_sub_eq_roundAt_of_abs_add_le_posMaxFinite supplies it from a bound on the operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_sub_eq_roundAt_of_abs_add_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hbound : |x.toReal| + |y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.sub y).toReal = roundAt fmt (x.toReal - y.toReal)

Finite subtraction under a symbolic triangle bound is exact real subtraction followed by one nearest-even format rounding.