TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Interval.Proof

Configured interval correctness #

Packing and decoding are inverse on complete endpoint encodings, including signed zeros and NaNs. Every configured operation decodes to the existing model operation. Soundness and validity are transported from Model.Interval, retaining its format and finiteness hypotheses.

In particular, arithmetic soundness starts from finite valid intervals and concludes membership in extended-real bounds: overflow is permitted. Totalized real decoding alone is not a sound interpretation of infinite or NaN endpoints.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Formats.BinaryInterchange.Model.Interval format) :
(ofModel I).toModel = I

Decoding packed bounds preserves every endpoint bit.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.ofModel_toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
ofModel I.toModel = I

Repacking decoded bounds is lossless.

source
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_injective {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
Function.Injective toModel

Model equality determines configured interval equality.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.mem_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
x ∈ I ↔ Binary.toModel x ∈ I.toModel

Membership agrees with the exact model order.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.valid_ofModel_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Formats.BinaryInterchange.Model.Interval format) :
(ofModel I).Valid ↔ I.Valid

Packing model bounds preserves finite validity.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.validExtended_ofModel_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Formats.BinaryInterchange.Model.Interval format) :
(ofModel I).ValidExtended ↔ I.ValidExtended

Packing model bounds preserves extended validity.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_point {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
(point x).toModel = Formats.BinaryInterchange.Model.Interval.point (Binary.toModel x)

Point construction commutes with decoding.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_whole {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] :
whole.toModel = Formats.BinaryInterchange.Model.Interval.whole format

The configured whole range has exactly the model's endpoints.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_ofBounds {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (lo hi : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
(ofBounds lo hi).toModel = Formats.BinaryInterchange.Model.Interval.ofBounds (Binary.toModel lo) (Binary.toModel hi)

Checked construction commutes with decoding.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_hull {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
(I.hull J).toModel = I.toModel.hull J.toModel

Configured hull decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
(I.add J).toModel = I.toModel.add J.toModel

Configured add decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
(I.sub J).toModel = I.toModel.sub J.toModel

Configured sub decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
(I.mul J).toModel = I.toModel.mul J.toModel

Configured mul decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) :
(I.div J).toModel = I.toModel.div J.toModel

Configured div decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_neg {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
I.neg.toModel = I.toModel.neg

Configured neg decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_inv {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
I.inv.toModel = I.toModel.inv

Configured inv decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_relu {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
I.relu.toModel = I.toModel.relu

Configured relu decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_abs {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
I.abs.toModel = I.toModel.abs

Configured abs decodes to the model operation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Binary.Interval.toModel_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) :
I.sqrt.toModel = I.toModel.sqrt

Configured sqrt decodes to the model operation.

source
@[reducible, inline]
abbrev FloatLib.Floats.ExecFloat.Binary.Interval.RealMem {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (x : ℝ) :
Prop

Real membership in decoded bounds; meaningful as an interval interpretation under Valid.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.ExecFloat.Binary.Interval.ERealMem {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (x : EReal) :
    Prop

    Extended-real membership, permitting infinite endpoints under ValidExtended.

    Instances For
      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.Valid.validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {I : Interval} (hI : I.Valid) :
      I.ValidExtended

      Finite validity implies extended validity.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.eRealMem_coe_iff_of_valid {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {I : Interval} (hI : I.Valid) (x : ℝ) :
      I.ERealMem ↑x ↔ I.RealMem x

      Finite endpoint interpretations agree after embedding a real number into EReal.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.valid_point_of_isFinite {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hx : isFinite x = true) :
      (point x).Valid

      A finite value gives a valid point interval.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.validExtended_point_of_isNaN_eq_false {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (x : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hx : isNaN x = false) :
      (point x).ValidExtended

      A non-NaN value gives an extended-valid point interval, including at infinity.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.validExtended_whole {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) :
      whole.ValidExtended

      The full IEEE range is extended-valid.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.eRealMem_whole {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) (x : EReal) :
      whole.ERealMem x

      The full IEEE range contains every extended real.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.validExtended_ofBounds {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (lo hi : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hformat : format.isIEEE = true) :
      (ofBounds lo hi).ValidExtended

      Checked IEEE bounds are extended-valid even when the supplied pair is unordered.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.add_sound {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) (hJ : J.Valid) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
      (I.add J).ERealMem ↑(x + y)

      Outward-rounded add encloses the exact real result, including overflow.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.add_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) :
      (I.add J).ValidExtended

      IEEE add returns ordered, non-NaN bounds, even for indeterminate input endpoints.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.sub_sound {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) (hJ : J.Valid) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
      (I.sub J).ERealMem ↑(x - y)

      Outward-rounded sub encloses the exact real result, including overflow.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.sub_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) :
      (I.sub J).ValidExtended

      IEEE sub returns ordered, non-NaN bounds, even for indeterminate input endpoints.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.mul_sound {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) (hJ : J.Valid) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
      (I.mul J).ERealMem ↑(x * y)

      Outward-rounded mul encloses the exact real result, including overflow.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.mul_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) :
      (I.mul J).ValidExtended

      IEEE mul returns ordered, non-NaN bounds, even for indeterminate input endpoints.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.div_sound {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) (hJ : J.Valid) {x y : ℝ} (hx : I.RealMem x) (hy : J.RealMem y) :
      (I.div J).ERealMem ↑(x / y)

      Outward-rounded div encloses the exact real result, including overflow.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.div_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I J : Interval) (hformat : format.isIEEE = true) :
      (I.div J).ValidExtended

      IEEE div returns ordered, non-NaN bounds, even for indeterminate input endpoints.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.neg_sound_extended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hI : I.ValidExtended) {x : ℝ} (hx : I.ERealMem ↑x) :
      I.neg.ERealMem ↑(-x)

      The neg image encloses every represented real, permitting infinite bounds.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.neg_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hI : I.ValidExtended) :
      I.neg.ValidExtended

      The neg image preserves extended validity in every format.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.relu_sound_extended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hI : I.ValidExtended) {x : ℝ} (hx : I.ERealMem ↑x) :
      I.relu.ERealMem ↑(max x 0)

      The relu image encloses every represented real, permitting infinite bounds.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.relu_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hI : I.ValidExtended) :
      I.relu.ValidExtended

      The relu image preserves extended validity in every format.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.abs_sound_extended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hI : I.ValidExtended) {x : ℝ} (hx : I.ERealMem ↑x) :
      I.abs.ERealMem ↑|x|

      The abs image encloses every represented real, permitting infinite bounds.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.abs_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hI : I.ValidExtended) :
      I.abs.ValidExtended

      The abs image preserves extended validity in every format.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.inv_sound {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) {x : ℝ} (hx : I.RealMem x) :
      I.inv.ERealMem ↑(1 / x)

      Reciprocal soundness includes zero: the whole-range fallback encloses the totalized result.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.inv_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hformat : format.isIEEE = true) :
      I.inv.ValidExtended

      IEEE reciprocal returns extended-valid bounds.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.sqrt_sound {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) (hnonnegative : 0 ≤ (Binary.toModel I.lo).toReal) {x : ℝ} (hx : I.RealMem x) :
      I.sqrt.ERealMem ↑√x

      Directed square root encloses the real square root on nonnegative finite input bounds.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.Interval.sqrt_validExtended {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (I : Interval) (hformat : format.isIEEE = true) (hI : I.Valid) (hnonnegative : 0 ≤ (Binary.toModel I.lo).toReal) :
      I.sqrt.ValidExtended

      Directed square root preserves extended validity on nonnegative finite input bounds.