Ordinary Lean instances for configured binary values

Configured binary values ExecFloat (Configured.Family format code plan) receive the ordinary Lean interfaces here, generically in the storage codec, so byte, machine-word, and wide carriers share one set of instances. Numerical literals are rounded once from exact rationals. Display, comparison, equality, and hashing operate on the exact-width model, independently of the packed carrier.

Two different notions of equality are installed:

• == (BEq) is IEEE numerical equality through ExecFloat.compareEqual: NaN == NaN is false and -0 == +0 is true when the format represents these values. List.contains, List.elem, and every other BEq-based search use this notion.
• = (DecidableEq) is structural equality of the stored interchange word: distinct signed-zero encodings are unequal and every NaN equals itself. decide (x = y), List.Nodup, Multiset, and Finset use this notion. Hashable hashes the same word, so x = y implies hash x = hash y.

These instances do not provide LawfulBEq. Using configured values as Std.HashMap or Std.HashSet keys requires an equality and hashing convention that satisfies their laws.

< and ≤ use IEEE numerical comparisons: a < b holds exactly when the numerical comparison returns some .lt, and a ≤ b when it returns some .lt or some .eq. Every comparison involving a NaN is false, so a ≤ a fails for NaN and these relations are not a Preorder. max and min are IEEE maximum and minimum: they propagate NaN and order -0 below +0, so max a b = if a ≤ b then b else a fails on NaN inputs.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instComparisonFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Comparison (Formats.BinaryInterchange.Configured.Family format code plan)

Configured binary comparison follows the descriptor's IEEE-style numerical order.

NaNs are unordered, signed zeros compare equal, and every other pair is ordered by exact value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_inj {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : toModel left = toModel right ↔ left = right

The stored word determines the value, so decoding to the model is injective.

theorem FloatLib.Floats.ExecFloat.Binary.compare_eq_compare_toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : left.compare right = (toModel left).compare (toModel right)

Comparison on configured values is comparison of their exact-width models.

theorem FloatLib.Floats.ExecFloat.Binary.compare_eq_none_of_isNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (h : isNaN left = true ∨ isNaN right = true) : left.compare right = none

Comparison against a NaN is unordered.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instInhabitedFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Inhabited (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

The default configured binary value is positive zero.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.default_eq_zero {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : default = zero

The default configured binary value is positive zero.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instDecidableEqFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : DecidableEq (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

Structural equality of the stored interchange word.

This differs from ==: distinct signed-zero encodings are unequal and a NaN equals itself. Deciding equality on the exact-width model keeps the instance independent of the packed carrier.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instHashableFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Hashable (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

Hash of the complete interchange word.

Structural equality = guarantees equal hashes. Numerical equality == alone does not, since distinct signed-zero encodings compare numerically equal.

theorem FloatLib.Floats.ExecFloat.Binary.hash_eq_hash_toNatBits {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : hash value = hash (toNatBits value)

The hash of a configured binary value is the hash of its interchange word.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instLTFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : LT (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

IEEE strict order: a < b holds when the numerical comparison returns some .lt.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instLEFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : LE (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

IEEE weak order: a ≤ b holds when the comparison returns some .lt or some .eq.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instDecidableLtFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : Decidable (left < right)

< is decided by the executable comparison.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instDecidableLeFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : Decidable (left ≤ right)

≤ is decided by the executable comparison.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instMaxFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Max (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

IEEE maximum: NaN operands propagate as a quiet NaN and max (-0) (+0) = +0.

This is not the order-theoretic maximum of ≤, since NaNs are unordered by ≤.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Binary.instMinFamily {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] : Min (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

IEEE minimum: NaN operands propagate as a quiet NaN and min (-0) (+0) = -0.

This is not the order-theoretic minimum of ≤, since NaNs are unordered by ≤.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_max {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (left ⊔ right).toModel = (toModel left).maximum (toModel right)

max decodes to IEEE maximum on the exact-width models.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_min {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (left ⊓ right).toModel = (toModel left).minimum (toModel right)

min decodes to IEEE minimum on the exact-width models.

theorem FloatLib.Floats.ExecFloat.Binary.lt_iff_compareLess {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left < right ↔ left.compareLess right = true

< is the executable strict comparison.

theorem FloatLib.Floats.ExecFloat.Binary.le_iff_compareLessEqual {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left ≤ right ↔ left.compareLessEqual right = true

≤ is the executable weak comparison.

theorem FloatLib.Floats.ExecFloat.Binary.lt_iff_compare_eq_lt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left < right ↔ (toModel left).compare (toModel right) = some Ordering.lt

< holds exactly when the model comparison returns some .lt.

theorem FloatLib.Floats.ExecFloat.Binary.lt_iff_lt_toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left < right ↔ (toModel left).lt (toModel right)

< on configured values is Model.lt on their models.

theorem FloatLib.Floats.ExecFloat.Binary.le_iff_compare_eq_lt_or_eq {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left ≤ right ↔ (toModel left).compare (toModel right) = some Ordering.lt ∨ (toModel left).compare (toModel right) = some Ordering.eq

≤ holds exactly when the model comparison returns some .lt or some .eq.

theorem FloatLib.Floats.ExecFloat.Binary.le_iff_le_toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left ≤ right ↔ (toModel left).le (toModel right)

≤ on configured values is Model.le on their models.

theorem FloatLib.Floats.ExecFloat.Binary.le_iff_lt_or_compareEqual {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} : left ≤ right ↔ left < right ∨ left.compareEqual right = true

≤ is < or numerical equality ==.

theorem FloatLib.Floats.ExecFloat.Binary.not_lt_of_isNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (h : isNaN left = true ∨ isNaN right = true) : ¬left < right

Nothing is strictly below or above a NaN.

theorem FloatLib.Floats.ExecFloat.Binary.not_le_of_isNaN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} (h : isNaN left = true ∨ isNaN right = true) : ¬left ≤ right

Nothing is weakly below or above a NaN.

theorem FloatLib.Floats.ExecFloat.Binary.lt_irrefl {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : ¬value < value

Strict order is irreflexive, for NaN because it is unordered and otherwise by equality.

theorem FloatLib.Floats.ExecFloat.Binary.le_self_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : value ≤ value ↔ isNaN value = false

≤ is reflexive exactly on non-NaN values.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instFormatDisplayFamilyOfModelCodecStoragePlanModel {format : FloatFormat} {plan : Configured.StoragePlan format} {code : Type} [codec : ExecFloat.ModelCodec plan (Model format) code] : ExecFloat.FormatDisplay (Configured.Family format code plan)

Configured binary values print their mathematical value rather than their packed carrier.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instOfNatExecFloatFamilyOfModelCodecStoragePlanModel {format : FloatFormat} {plan : Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ℕ) : OfNat (ExecFloat (Configured.Family format code plan)) value

Numeral literals are rounded once from the exact natural number into the destination format.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instOfScientificExecFloatFamilyOfModelCodecStoragePlanModel {format : FloatFormat} {plan : Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] : OfScientific (ExecFloat (Configured.Family format code plan))

Scientific and decimal literals are rounded once from their exact rational value into the destination format.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instNegExecFloatFamilyOfModelCodecStoragePlanModel {format : FloatFormat} {plan : Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] : Neg (ExecFloat (Configured.Family format code plan))

Negation follows the destination format's signed-zero and exceptional-value policy.