Native values through the shared representation bridge

Lean has named NaN and infinity constants alongside its logical floating-point models, and we're glad it is making more of this model available for proofs. Here we connect those constants and the ofFloat / toFloat adapters to the same packed-model proofs used for arithmetic and integer conversion.

Every native value round-trips. In the other direction, a FloatLib word may carry a NaN payload that Lean's model does not retain, and Model.canonicalizeModel describes that change. Finite values, infinities, and both signed zeros keep their bits.

Binary32

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32 (value : Float32) : (ofFloat32 value).toModel = Formats.BinaryInterchange.Model.ofFloat32Model value.toModel

Importing a native value reads the word in its logical binary32 model.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat32_eq (value : Binary32) : (toFloat32 value).toModel = (toModel value).toFloat32Model

Exporting binary32 uses the shared packed-model conversion, including NaN normalization.

theorem FloatLib.Floats.ExecFloat.Binary.isModelCanonical_ofFloat32 (value : Float32) : (ofFloat32 value).toModel.IsModelCanonical

An imported native binary32 value already satisfies Lean's canonical-NaN invariant.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toFloat32_ofFloat32 (value : Float32) : (ofFloat32 value).toFloat32 = value

Importing and then exporting a native binary32 value gives it back.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_nan : (ofFloat32 Float32.nan).toModel = Formats.BinaryInterchange.Model.canonicalNaN Formats.BinaryInterchange.FloatFormat.binary32

Lean's binary32 NaN imports as FloatLib's canonical quiet NaN.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_inf : (ofFloat32 Float32.inf).toModel = Formats.BinaryInterchange.Model.posInf Formats.BinaryInterchange.FloatFormat.binary32

Lean's binary32 infinity imports as FloatLib's positive infinity.

Binary64

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat (value : Float) : (ofFloat value).toModel = Formats.BinaryInterchange.Model.ofFloatModel value.toModel

Importing a native value reads the word in its logical binary64 model.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_toFloat_eq (value : Binary64) : (toFloat value).toModel = (toModel value).toFloatModel

Exporting binary64 uses the shared packed-model conversion, including NaN normalization.

theorem FloatLib.Floats.ExecFloat.Binary.isModelCanonical_ofFloat (value : Float) : (ofFloat value).toModel.IsModelCanonical

An imported native binary64 value already satisfies Lean's canonical-NaN invariant.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toFloat_ofFloat (value : Float) : (ofFloat value).toFloat = value

Importing and then exporting a native binary64 value gives it back.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_nan : (ofFloat Float.nan).toModel = Formats.BinaryInterchange.Model.canonicalNaN Formats.BinaryInterchange.FloatFormat.binary64

Lean's binary64 NaN imports as FloatLib's canonical quiet NaN.

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_inf : (ofFloat Float.inf).toModel = Formats.BinaryInterchange.Model.posInf Formats.BinaryInterchange.FloatFormat.binary64

Lean's binary64 infinity imports as FloatLib's positive infinity.