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 carries no 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)

#eval shows both endpoints as their values.

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

Membership using the numerical order of Model, in which 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 not valid under this finite-endpoint predicate. For finite formats, whole uses the two maximal finite endpoints and is valid.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.instDecidableValid {fmt : FloatFormat} (I : Interval fmt) : Decidable I.Valid

Validity is decided by classifying and comparing the endpoints.

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.

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.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.instDecidableValidExtended {fmt : FloatFormat} (I : Interval fmt) : Decidable I.ValidExtended

Extended validity is decided by classifying and comparing the endpoints.

@[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 [-∞, +∞], and 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, which is false for unordered comparisons.

@[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 produce NaN endpoints instead. Such endpoint calculations cannot justify a narrower bound, and for formats with infinity the fallback encloses every real number, so interval arithmetic composes.

@[inline]

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

Whether the represented endpoint range contains numerical zero.