TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.IEEE754.Native.Integer.Constructors

Arbitrary integer constructors #

Lean exposes the definitions of Float.ofNat, Float.ofInt, and their binary32 counterparts on top of its logical floating-point models. The arbitrary-integer casts use these constructors, whose scientific-literal path has a small-input fast path. The proofs here cover both branches before applying the shared integer conversion specification.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.round_shiftLeft (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (n k : ℕ) (e : ℤ) (hn : n ≠ 0) :
Float.Model.UnpackedFloat.round spec sign (n <<< k) (e - ↑k) = Float.Model.UnpackedFloat.round spec sign n e

Moving exact trailing binary zeros into the exponent does not change model rounding.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofScientific_zero_eq_ofNat (spec : Float.Model.Format) (n : ℕ) :
Float.Model.UnpackedFloat.ofScientific spec n 0 = Float.Model.UnpackedFloat.ofNat spec n

A scientific literal with decimal exponent zero is the shared natural-number constructor.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_ofNat (n : ℕ) :
(ofFloat (Float.ofNat n)).toModel = Formats.BinaryInterchange.Model.roundRat Formats.BinaryInterchange.FloatFormat.binary64 false n 1

Binary64 natural construction is nearest-even rounding of a denominator-one rational.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_ofNat (n : ℕ) :
(ofFloat32 (Float32.ofNat n)).toModel = Formats.BinaryInterchange.Model.roundRat Formats.BinaryInterchange.FloatFormat.binary32 false n 1

Binary32 natural construction is nearest-even rounding of a denominator-one rational.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_ofInt (n : ℤ) :
(ofFloat (Float.ofInt n)).toModel = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary64 (Numerics.Dyadic.ofScaledInt n 0)

Binary64 integer construction uses the shared dyadic rounder, including signed overflow.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_ofInt (n : ℤ) :
(ofFloat32 (Float32.ofInt n)).toModel = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary32 (Numerics.Dyadic.ofScaledInt n 0)

Binary32 integer construction uses the shared dyadic rounder, including signed overflow.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat_intToFloat (n : ℤ) :
(ofFloat n.toFloat).toModel = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary64 (Numerics.Dyadic.ofScaledInt n 0)

Int.toFloat has the same rounding specification as Float.ofInt.

source
theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofFloat32_intToFloat32 (n : ℤ) :
(ofFloat32 n.toFloat32).toModel = Formats.BinaryInterchange.Model.roundDyadic Formats.BinaryInterchange.FloatFormat.binary32 (Numerics.Dyadic.ofScaledInt n 0)

Int.toFloat32 has the same rounding specification as Float32.ofInt.