Ordered numerical semantics and exception guarantees of decimal comparisons

Decimal comparison agrees with exact extended-rational order, treats either NaN as unordered, and respects cohorts. Quiet predicates raise invalid exactly for signaling NaNs; signaling predicates raise it for any NaN.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.numericValue?_eq_none_iff (x : Datum) : x.numericValue? = none ↔ x.isNaN = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_numericValue? {x y : Datum} (h : x.SameCohort y) : x.numericValue? = y.numericValue?

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_eq_none_iff (x y : Datum) : relation x y = none ↔ x.isNaN = true ∨ y.isNaN = true

Exactly the pairs containing a NaN are unordered.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_eq_lt_iff (x y : Datum) : relation x y = some Ordering.lt ↔ ∃ (a : NumericValue) (b : NumericValue), x.numericValue? = some a ∧ y.numericValue? = some b ∧ a < b

A less-than result means strict order in the exact extended rationals.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_eq_eq_iff (x y : Datum) : relation x y = some Ordering.eq ↔ ∃ (a : NumericValue), x.numericValue? = some a ∧ y.numericValue? = some a

Equality compares exact numerical values, rather than stored cohorts.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_eq_gt_iff (x y : Datum) : relation x y = some Ordering.gt ↔ ∃ (a : NumericValue) (b : NumericValue), x.numericValue? = some a ∧ y.numericValue? = some b ∧ b < a

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_finite_lt_iff (s t : Bool) (c d : ℕ) (q r : ℤ) : relation (Datum.finite s c q) (Datum.finite t d r) = some Ordering.lt ↔ Datum.finiteValue s c q < Datum.finiteValue t d r

Every finite comparison agrees with exact signed rational comparison.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_finite_eq_iff (s t : Bool) (c d : ℕ) (q r : ℤ) : relation (Datum.finite s c q) (Datum.finite t d r) = some Ordering.eq ↔ Datum.finiteValue s c q = Datum.finiteValue t d r

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_zero_zero (s t : Bool) (q r : ℤ) : relation (Datum.finite s 0 q) (Datum.finite t 0 r) = some Ordering.eq

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation_sameCohort {x x' y y' : Datum} (hx : x.SameCohort x') (hy : y.SameCohort y') : relation x y = relation x' y'

Replacing either operand by a member of its cohort preserves comparison.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.quiet_invalid_iff (p : Predicate) (x y : Datum) : (quiet p x y).status.invalid = true ↔ x.isSignaling = true ∨ y.isSignaling = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.signaling_invalid_iff (p : Predicate) (x y : Datum) : (signaling p x y).status.invalid = true ↔ x.isNaN = true ∨ y.isNaN = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.quiet_value_eq_signaling (p : Predicate) (x y : Datum) : (quiet p x y).value = (signaling p x y).value

Quiet and signaling variants have identical truth values, including on NaNs.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.quiet_value_iff (p : Predicate) (x y : Datum) : (quiet p x y).value = true ↔ Numerics.IEEEComparison.Predicate.accepts p none = true ∧ (x.isNaN = true ∨ y.isNaN = true) ∨ (Numerics.IEEEComparison.Predicate.accepts p (some Ordering.lt) = true ∧ ∃ (a : NumericValue) (b : NumericValue), x.numericValue? = some a ∧ y.numericValue? = some b ∧ a < b) ∨ (Numerics.IEEEComparison.Predicate.accepts p (some Ordering.eq) = true ∧ ∃ (a : NumericValue), x.numericValue? = some a ∧ y.numericValue? = some a) ∨ Numerics.IEEEComparison.Predicate.accepts p (some Ordering.gt) = true ∧ ∃ (a : NumericValue) (b : NumericValue), x.numericValue? = some a ∧ y.numericValue? = some b ∧ b < a

Complete truth-set specification, stated in terms of exact ordered values and unordered NaN operands. Together with the status theorems this covers all 22 named comparison entry points.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.quiet_status (p : Predicate) (x y : Datum) : (quiet p x y).status = { invalid := x.isSignaling || y.isSignaling }

Comparison never raises numerical range, division, or inexact exceptions.

theorem FloatLib.Floats.Formats.DecimalInterchange.Comparison.signaling_status (p : Predicate) (x y : Datum) : (signaling p x y).status = { invalid := x.isNaN || y.isNaN }