Decimal datums and cohorts

A finite datum stores a sign, an integer coefficient, and a quantum exponent: its value is (-1)^sign * coefficient * 10^quantum. Trailing coefficient zeros are meaningful representation information. For example, 1 × 10^0 and 10 × 10^-1 are different datums in the same cohort.

This representation layer implements IEEE 754-2019 §§3.3 and 3.5. It supplies neither decimal arithmetic nor its rounding, preferred-exponent, or exception rules.

inductive FloatLib.Floats.Formats.DecimalInterchange.Datum : Type

A decimal datum before selecting an interchange width. signaling = true represents a signaling NaN.

• finite (negative : Bool) (coefficient : ℕ) (quantum : ℤ) : Datum
• infinity (negative : Bool) : Datum
• nan (negative signaling : Bool) (payload : ℕ) : Datum

def FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqDatum.decEq (x✝ x✝¹ : Datum) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqDatum : DecidableEq Datum

def FloatLib.Floats.Formats.DecimalInterchange.Datum.display : Datum → String

Text of a datum with its coefficient and quantum: plain notation such as 1.50 or 120 when the quantum is not positive and the leading digit is at most six places after the point, otherwise one leading digit and an e exponent, such as 1.2e4 for coefficient 12 and quantum 3. Both read back as the same coefficient and quantum. Infinities print as inf and -inf, NaNs as nan.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Datum.instToString : ToString Datum

Datums print with their coefficient and quantum, as display writes them.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Datum.instRepr : Repr Datum

#eval and repr show the same text, parenthesized when negative inside an argument.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.Valid (f : Format) : Datum → Prop

Representability at the selected precision and quantum range. NaN payloads have one fewer decimal digit than finite coefficients.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Datum.instDecidableValid (f : Format) (d : Datum) : Decidable (Valid f d)

def FloatLib.Floats.Formats.DecimalInterchange.Datum.toRat? : Datum → Option ℚ

The rational value of a finite datum, or none for infinities and NaNs. Signed zeros remain distinct datums even though both map to zero. Zero bypasses the radix power, so its quantum does not determine the size of an intermediate integer.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.toRat?_eq (d : Datum) : d.toRat? = match d with | finite s c q => some ((if s = true then -1 else 1) * ↑c * 10 ^ q) | infinity negative => none | nan negative signaling payload => none

The zero shortcut preserves the usual coefficient-times-radix-power interpretation.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.SameCohort : Datum → Datum → Prop

Cohort relation of IEEE 754-2019 §§2.1 and 3.5.1: equal value and equal sign, including the sign of zero. Each infinity forms a singleton cohort. NaNs have no cohort. Width-specific cohorts restrict this relation to datums satisfying Valid.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.ofBiased (f : Format) (s : Bool) (c e : ℕ) : Datum

Finite datum from a coefficient and a biased exponent, as either decoder rebuilds it.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.ofBiased_valid (f : Format) (s : Bool) (c e : ℕ) : Valid f (ofBiased f s c e) ↔ c < f.coefficientBound ∧ e < f.exponentBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.valid_quantum_iff (f : Format) (s : Bool) (c : ℕ) (q : ℤ) : Valid f (finite s c q) ↔ c < f.coefficientBound ∧ f.minQuantum ≤ q ∧ q ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_symm {a b : Datum} (h : a.SameCohort b) : b.SameCohort a

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_trans {a b c : Datum} (hab : a.SameCohort b) (hbc : b.SameCohort c) : a.SameCohort c