Native addition and subtraction

These theorems relate FloatLib's addition and subtraction to the logical floating-point model shipped with Lean. Finite inputs include both signed zeros. The result is unrestricted, so cancellation, subnormal rounding and overflow to infinity are covered, and the equations hold on the complete packed word through the native adapters.

The finite-input hypotheses exclude NaNs and infinities, because FloatLib preserves NaN details that Lean canonicalizes and its subtraction also negates the right operand's NaN sign. These model equalities do not verify the machine instructions used by compiled native code.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_eq_ofModel_add_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x y : Model fmt) (hx : x.toModel.isFinite = true) (hy : y.toModel.isFinite = true) : x.add y = ofModel fmt (Float.Model.UnpackedFloat.add fmt.toModel x.toModel y.toModel)

For finite operands, including signed zeros, dispatched addition gives the word that Lean's unpacked model gets by adding and packing. The result may overflow to infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toModel_neg_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) (hx : x.toModel.isFinite = true) : x.neg.toModel = x.toModel.neg

Negation preserves the complete finite unpacked value, including the sign of zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sub_eq_ofModel_sub_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x y : Model fmt) (hx : x.toModel.isFinite = true) (hy : y.toModel.isFinite = true) : x.sub y = ofModel fmt (Float.Model.UnpackedFloat.sub fmt.toModel x.toModel y.toModel)

For finite operands, including signed zeros, dispatched subtraction agrees with Lean's unpacked subtraction and packing. There is no restriction on the rounded result.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_add_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : (ofFloat32 (x + y)).toModel = (ofFloat32 x).toModel.add (ofFloat32 y).toModel

Native binary32 addition commutes with the import adapter on finite inputs.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_sub_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : (ofFloat32 (x - y)).toModel = (ofFloat32 x).toModel.sub (ofFloat32 y).toModel

Native binary32 subtraction commutes with the import adapter, including signed-zero inputs.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_add_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : (ofFloat (x + y)).toModel = (ofFloat x).toModel.add (ofFloat y).toModel

Native binary64 addition commutes with the import adapter on finite inputs.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_sub_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : (ofFloat (x - y)).toModel = (ofFloat x).toModel.sub (ofFloat y).toModel

Native binary64 subtraction commutes with the import adapter, including signed-zero inputs.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat32_add_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat32 (x + y) = ofFloat32 x + ofFloat32 y

Importing the native sum equals adding the imported binary32 operands with the installed certified software operation. Finite inputs may produce zero, a subnormal, or infinity.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat32_sub_of_isFinite (x y : Float32) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat32 (x - y) = ofFloat32 x - ofFloat32 y

Importing a native binary32 difference equals certified software subtraction of the imports.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat_add_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat (x + y) = ofFloat x + ofFloat y

Importing the native sum equals adding the imported binary64 operands with the installed certified software operation, including cancellation and overflow.

theorem FloatLib.Floats.ExecFloat.Binary.ofFloat_sub_of_isFinite (x y : Float) (hx : x.isFinite = true) (hy : y.isFinite = true) : ofFloat (x - y) = ofFloat x - ofFloat y

Importing a native binary64 difference equals certified software subtraction of the imports.