Arithmetic enclosures for executable binary intervals

Read this module after IntervalSemantics.Order for the proofs behind negation, addition, subtraction, multiplication, division, and reciprocal. The four-corner arguments for products and quotients are kept with the operations that consume them. IntervalSemantics.Finite supplies the separate range-checked results for all-words-finite encodings.

IEEE binary arithmetic starts with finite valid inputs and encloses exact real results in EReal, allowing overflow at the output. Negation also accepts infinite input endpoints. The validity theorems explain which results can be passed to later interval operations; division through zero and indeterminate candidate bounds use the whole interval.

Interval.Arithmetic contains the executable definitions. IntervalSemantics.Activations builds ReLU, absolute-value, and square-root enclosures on the results here.

Exact negation

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.neg_sound_extended {fmt : FloatFormat} (A : Interval fmt) (hA : A.ValidExtended) {x : ℝ} (hx : A.ERealMem ↑x) : A.neg.ERealMem ↑(-x)

The negated interval encloses each negated real member, including with infinite endpoints.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.neg_validExtended {fmt : FloatFormat} (A : Interval fmt) (hA : A.ValidExtended) : A.neg.ValidExtended

Negation preserves ordered, non-NaN endpoints in every format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.neg_sound {fmt : FloatFormat} (A : Interval fmt) (hA : A.Valid) {x : ℝ} (hx : A.RealMem x) : A.neg.ERealMem ↑(-x)

Interval negation encloses the negation of every represented real value.

Addition

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.add_sound {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hB : B.Valid) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.add B).ERealMem ↑(x + y)

Outward-rounded interval addition encloses every sum of represented real values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.add_validExtended {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) : (A.add B).ValidExtended

Outward-rounded addition always returns ordered IEEE bounds without NaNs.

Subtraction

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sub_sound {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hB : B.Valid) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.sub B).ERealMem ↑(x - y)

Outward-rounded interval subtraction encloses every represented real difference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sub_validExtended {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) : (A.sub B).ValidExtended

Outward-rounded subtraction always returns ordered IEEE bounds without NaNs.

Four-corner enclosures

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.eRealMem_ofBounds_corners {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hB : B.Valid) (down up : Model fmt → Model fmt → Model fmt) (f : ℝ → ℝ → ℝ) {z : ℝ} (hdown : ∀ (a b : Model fmt), a.isFinite = true → b.isFinite = true → b = B.lo ∨ b = B.hi → (down a b).isNaN = false ∧ (down a b).toEReal ≤ ↑(f a.toReal b.toReal)) (hup : ∀ (a b : Model fmt), a.isFinite = true → b.isFinite = true → b = B.lo ∨ b = B.hi → (up a b).isNaN = false ∧ ↑(f a.toReal b.toReal) ≤ (up a b).toEReal) (hz : z ∈ Set.Icc (Floats.Interval.minOfFour (f A.lo.toReal B.lo.toReal) (f A.lo.toReal B.hi.toReal) (f A.hi.toReal B.lo.toReal) (f A.hi.toReal B.hi.toReal)) (Floats.Interval.maxOfFour (f A.lo.toReal B.lo.toReal) (f A.lo.toReal B.hi.toReal) (f A.hi.toReal B.lo.toReal) (f A.hi.toReal B.hi.toReal))) : (ofBounds (minOfFour (down A.lo B.lo) (down A.lo B.hi) (down A.hi B.lo) (down A.hi B.hi)) (maxOfFour (up A.lo B.lo) (up A.lo B.hi) (up A.hi B.lo) (up A.hi B.hi))).ERealMem ↑z

The checked four-corner enclosure contains every real bracketed by the exact corner values.

The corner operations down and up are applied to the endpoints of A and B. Each downward corner must lie below, and each upward corner above, the exact value f of the corresponding decoded endpoints, and neither may be a NaN. The bound hypotheses receive finiteness of both arguments and the identity of the right endpoint, so operations with a side condition on the right operand, such as a nonzero divisor, can discharge it per endpoint.

Four-corner multiplication

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mul_sound {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hB : B.Valid) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.mul B).ERealMem ↑(x * y)

Outward-rounded interval multiplication encloses every represented real product.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mul_validExtended {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) : (A.mul B).ValidExtended

Outward-rounded multiplication always returns ordered IEEE bounds without NaNs.

Division and reciprocal

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.div_sound {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hB : B.Valid) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.div B).ERealMem ↑(x / y)

Outward-rounded interval division encloses every represented real quotient.

The theorem is total in the denominator: when B contains zero the result is whole fmt, which encloses every real, and otherwise the four directed corner quotients bracket x / y. Both intervals must be Valid (finite ordered endpoints) because the directed division kernels are specified only on finite operands; an extended version with infinite endpoints would need directed-division semantics for infinite arguments, which the library does not provide.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.div_validExtended {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.isIEEE = true) : (A.div B).ValidExtended

Outward-rounded division always returns ordered IEEE bounds without NaNs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.inv_sound {fmt : FloatFormat} (B : Interval fmt) (hfmt : fmt.isIEEE = true) (hB : B.Valid) {y : ℝ} (hy : B.RealMem y) : B.inv.ERealMem ↑(1 / y)

Outward-rounded interval reciprocal encloses every represented real reciprocal.