Standard interfaces for binary models

The Model fmt instances supply Lean's ordinary numeric interfaces. Arithmetic, comparisons, and constants route directly through the format-generic executable kernels.

Elementary functions, Pow, and MathFunctions are not installed here. Import FloatLib.Floats.Formats.BinaryInterchange.Transcendentals (or Configured.Transcendentals) by name. Certified sqrt and abs remain on this path.

Constants are constructed from exact integers and rounded according to the descriptor.

Natural numbers enter through NatCast, following mathlib: the map rounds, so it is not a Coe. Numerals resolve the way they do for any mathlib type with Zero, One, and NatCast: 0 is posZero fmt, 1 is posOne fmt, and 2, 3, ... are Nat.cast through mathlib's instOfNatAtLeastTwo. There is no separate OfNat instance, so (0 : Model fmt) and Zero.zero are the same term.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instNatCast {fmt : FloatFormat} : NatCast (Model fmt)

Natural numbers are converted by one nearest-even rounding in the destination format.

Numerals 2, 3, ... resolve to this cast through mathlib's instOfNatAtLeastTwo.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instZero {fmt : FloatFormat} : Zero (Model fmt)

Positive zero in the destination format.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instOne {fmt : FloatFormat} : One (Model fmt)

Exact positive one in the destination format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.natCast_def {fmt : FloatFormat} (value : ℕ) : ↑value = roundDyadic fmt { negative := false, significand := value, exponent := 0 }

Unfolding lemma for the natural-number cast.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.zero_eq_posZero {fmt : FloatFormat} : 0 = posZero fmt

The numeral 0 is the format's positive zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.one_eq_posOne {fmt : FloatFormat} : 1 = posOne fmt

The numeral 1 is the format's exact positive one.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.natCast_zero {fmt : FloatFormat} : ↑0 = 0

Casting the natural number zero rounds to positive zero, so it agrees with the numeral 0.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instNeg {fmt : FloatFormat} : Neg (Model fmt)

Negation with the descriptor's signed-zero and NaN conventions.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instAdd {fmt : FloatFormat} : Add (Model fmt)

Descriptor-aware nearest-even addition.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instSub {fmt : FloatFormat} : Sub (Model fmt)

Descriptor-aware nearest-even subtraction.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instMul {fmt : FloatFormat} : Mul (Model fmt)

Descriptor-aware nearest-even multiplication.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDiv {fmt : FloatFormat} : Div (Model fmt)

Descriptor-aware nearest-even division.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instBEq {fmt : FloatFormat} : BEq (Model fmt)

Boolean equality with IEEE NaN and signed-zero conventions.

NaNs compare unequal, the two zero encodings compare equal, and all other values compare by their exact storage bits.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instLT {fmt : FloatFormat} : LT (Model fmt)

Strict IEEE numerical order; unordered comparisons are false.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instLE {fmt : FloatFormat} : LE (Model fmt)

Non-strict IEEE numerical order; unordered comparisons are false.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableRelLt {fmt : FloatFormat} : DecidableRel fun (x1 x2 : Model fmt) => x1 < x2

Decidability of the comparison-based strict order.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableRelLe {fmt : FloatFormat} : DecidableRel fun (x1 x2 : Model fmt) => x1 ≤ x2

Decidability of the comparison-based non-strict order.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instMin {fmt : FloatFormat} : Min (Model fmt)

IEEE minimum, including signed-zero and NaN propagation rules.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instMax {fmt : FloatFormat} : Max (Model fmt)

IEEE maximum, including signed-zero and NaN propagation rules.