Standard posit comparisons and finite enumeration

The Posit Standard (2022) defines comparisons by regarding the complete encoded words as two's-complement signed integers. In particular, NaR compares as the least encoded value and two NaR words compare equal. This is an ordering of posit values, including NaR; it is deliberately not presented as an order embedding into Rat or Real, because NaR has no real denotation.

This module transports Lean's proved BitVec.toInt order to Model format. It also exposes the exact equivalence with BitVec format.bits and derives Mathlib's FinEnum/Fintype infrastructure from that equivalence. Exhaustive proofs can therefore enumerate the model without maintaining a second list of encodings.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Section 5.3, https://posithub.org/docs/posit_standard-2.pdf.

def FloatLib.Floats.Formats.Posit.Model.bitsEquiv (format : Format) : Model format ≃ BitVec format.bits

Representation-preserving equivalence between a posit model and its complete encoded word.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instFinEnum {format : Format} : FinEnum (Model format)

Canonical finite enumeration inherited from exact-width bit vectors.

The enumeration is by unsigned word, which is useful for encoding tables and exhaustive conformance checks. The LinearOrder below is separately the standard's signed comparison order.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.finEnum_card (format : Format) : FinEnum.card (Model format) = 2 ^ format.bits

The number of posit words is exactly 2 ^ format.bits, including zero and NaR.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.signedCode {format : Format} (value : Model format) : ℤ

Interpret the complete posit word as a two's-complement signed integer.

theorem FloatLib.Floats.Formats.Posit.Model.signedCode_injective {format : Format} : Function.Injective signedCode

Signed-code interpretation is injective at a fixed width.

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Model.instLinearOrder {format : Format} : LinearOrder (Model format)

The standard total order on posit words.

This instance makes ordinary Lean notation (<, ≤, min, max, sorting, intervals) agree with Posit Standard comparisons. NaR is included as the least word; numerical theorems that must exclude NaR should state that premise explicitly or use toRat?.

The order is transported along signedCode, but the DecidableEq field reuses the derived instance so that the model has a single decidable equality.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.compareEqual {format : Format} (left right : Model format) : Bool

Standard equality comparison.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.compareNotEqual {format : Format} (left right : Model format) : Bool

Standard inequality comparison.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.compareLess {format : Format} (left right : Model format) : Bool

Standard strict-less comparison, executed directly on the encoded words.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.compareLessEqual {format : Format} (left right : Model format) : Bool

Standard less-or-equal comparison, executed directly on the encoded words.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.compareGreater {format : Format} (left right : Model format) : Bool

Standard strict-greater comparison, executed by reversing strict-less.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.compareGreaterEqual {format : Format} (left right : Model format) : Bool

Standard greater-or-equal comparison, executed by reversing less-or-equal.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareEqual_eq_true_iff {format : Format} (left right : Model format) : left.compareEqual right = true ↔ left = right

Boolean equality agrees exactly with equality in the posit model.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareNotEqual_eq_true_iff {format : Format} (left right : Model format) : left.compareNotEqual right = true ↔ left ≠ right

Boolean inequality agrees exactly with inequality in the posit model.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareLess_eq_true_iff {format : Format} (left right : Model format) : left.compareLess right = true ↔ left < right

Encoded strict-less comparison agrees with the standard signed-word order.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareLessEqual_eq_true_iff {format : Format} (left right : Model format) : left.compareLessEqual right = true ↔ left ≤ right

Encoded less-or-equal comparison agrees with the standard signed-word order.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareGreater_eq_true_iff {format : Format} (left right : Model format) : left.compareGreater right = true ↔ left > right

Encoded strict-greater comparison agrees with the standard signed-word order.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareGreaterEqual_eq_true_iff {format : Format} (left right : Model format) : left.compareGreaterEqual right = true ↔ left ≥ right

Encoded greater-or-equal comparison agrees with the standard signed-word order.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compareEqual_nar_nar (format : Format) : (nar format).compareEqual (nar format) = true

Equality of NaR with itself follows the standard's encoded comparison rule.