NN.Floats.IEEEExec.Exec32.Compare

Comparisons for executable IEEE32 values.

The definitions here implement the ordering and classification behavior used by the executable binary32 arithmetic layer.

source

def TorchLean.Floats.IEEE754.IEEE32Exec.compare (x y : IEEE32Exec) :

Option Ordering

IEEE754 numerical comparison.

Returns none (unordered) if either operand is NaN; otherwise returns an Ordering.

Instances For

source

def TorchLean.Floats.IEEE754.IEEE32Exec.lt (x y : IEEE32Exec) :

Prop

Strict order induced by IEEE-754 comparison.

lt x y is true exactly when compare x y = some .lt. In particular, if either side is NaN then lt x y is false (because compare returns none).

Instances For

source

def TorchLean.Floats.IEEE754.IEEE32Exec.le (x y : IEEE32Exec) :

Prop

Non-strict order induced by IEEE-754 comparison.

le x y is true when compare x y returns .lt or .eq, and false otherwise (including the NaN unordered case).

Instances For

Order lemmas #

IEEE-754 comparisons treat NaNs as unordered, so in particular le x x is not true for NaNs. For the interval layer, we mainly need the basic fact that le is reflexive on finite values.

source

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.le_self_of_isFinite_eq_true (x : IEEE32Exec) (hx : x.isFinite = true) :

x.le x

IEEE32Exec.le is reflexive on finite values.

Informally: if x is a finite float32, then x ≤ x. (NaNs are excluded by the isFinite premise: for NaN, isFinite x = false and x ≤ x is false because compare returns none.)

This lemma is used by the executable interval layer to show that the "point interval" [x, x] is valid whenever x is finite.

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.le_self_of_isFinite_eq_true_imp (x : IEEE32Exec) :

x.isFinite = true → x.le x

Curried form of le_self_of_isFinite_eq_true (useful for simp).

source

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_imp_le_self_iff_true (x : IEEE32Exec) :

x.isFinite = true → x.le x ↔ True

isFinite x = true → x ≤ x is always true.

This looks a bit odd, but it's exactly the side-goal produced by simp [Valid, point] in the executable interval module (NN/Floats/Interval/IEEEExec32.lean). Registering this as a simp lemma lets that file stay a one-liner.

source