Format-generic executable floating-point intervals

Closed executable intervals have Model fmt endpoints, an endpoint order, and format-independent constructors. Outward-rounded arithmetic and activation ranges live in later modules.

The executable layer is separate from soundness theorems so applications can choose an exact real, extended-real, or format-model interpretation without changing the interval representation.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Interval (fmt : FloatFormat) : Type

A closed executable interval with both endpoints in fmt.

• lo : Model fmt

  Lower endpoint.

• hi : Model fmt

  Upper endpoint.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqInterval {fmt✝ : FloatFormat} : DecidableEq (Interval fmt✝)

def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqInterval.decEq {fmt✝ : FloatFormat} (x✝ x✝¹ : Interval fmt✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprInterval {fmt✝ : FloatFormat} : Repr (Interval fmt✝)

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprInterval.repr {fmt✝ : FloatFormat} : Interval fmt✝ → ℕ → Std.Format

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mem {fmt : FloatFormat} (I : Interval fmt) (x : Model fmt) : Prop

Membership using the numerical order of Model; NaNs are unordered.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.instMembership {fmt : FloatFormat} : Membership (Model fmt) (Interval fmt)

Enable x ∈ I for format-generic executable intervals.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mem_iff {fmt : FloatFormat} (I : Interval fmt) (x : Model fmt) : x ∈ I ↔ I.lo.le x ∧ x.le I.hi

Unfold membership into lower- and upper-endpoint comparisons.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.Valid {fmt : FloatFormat} (I : Interval fmt) : Prop

An interval is valid when both endpoints are finite and ordered.

For formats with infinity, whole is intentionally not valid under this finite-endpoint predicate. For finite formats, whole uses the two maximal finite endpoints and is valid.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ValidExtended {fmt : FloatFormat} (I : Interval fmt) : Prop

An interval is extended-valid when both endpoints are non-NaN and are ordered.

Unlike Valid, this predicate permits infinite endpoints. It is the closure invariant for outward-rounded IEEE operations: a finite input interval may produce an infinite endpoint on overflow without ceasing to denote an ordered interval.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.point {fmt : FloatFormat} (x : Model fmt) : Interval fmt

Degenerate interval [x, x].

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.hull {fmt : FloatFormat} (A B : Interval fmt) : Interval fmt

Smallest endpoint hull containing both input intervals, with IEEE NaN propagation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.minOfFour {fmt : FloatFormat} (a b c d : Model fmt) : Model fmt

Minimum of four values, grouped to match the interval corner operations.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.maxOfFour {fmt : FloatFormat} (a b c d : Model fmt) : Model fmt

Maximum of four values, grouped to match the interval corner operations.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.whole (fmt : FloatFormat) : Interval fmt

Conservative interval spanning the complete numerical range of fmt.

Formats with infinity use [-∞, +∞]; formats without infinity use their two maximal finite endpoints.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.leB {fmt : FloatFormat} (x y : Model fmt) : Bool

Executable x ≤ y; unordered comparisons return false.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ofBounds {fmt : FloatFormat} (lo hi : Model fmt) : Interval fmt

Build an enclosure from ordered, non-NaN endpoints, or use the whole range.

The candidate pair is kept only when leB lo hi holds. It is replaced by whole fmt when either endpoint is a NaN (so the comparison is unordered) and also when lo > hi numerically, which can happen when a caller supplies reversed bounds. An indeterminate expression such as 0 * ∞ can instead produce NaN endpoints. Indeterminate endpoint calculations cannot justify a narrower bound; for formats with infinity the fallback encloses every real number and permits interval arithmetic to compose.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.containsZero {fmt : FloatFormat} (I : Interval fmt) : Bool

Whether the represented endpoint range contains numerical zero.