TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Operation.Proof.Checked

Proof-indexed checked operations #

Application lemmas for operations returning Option. A refinement proof shows that represented finite inputs cannot take the failure branch, with optional scalar preconditions when required.

These lemmas connect an executable checker to a proof-indexed caller. At the raw-code level, failure remains explicit. Once the caller supplies represented finite inputs and, for the On variants, the scalar precondition, the refinement theorem proves that none is impossible and returns a value carrying its denotation proof.

Unary, binary, and ternary versions provide map_denote for the denotation equation and applyAt for constructing a proof-indexed result. The unconditional contracts also provide exists_result to recover a successful code and its denotation.

source
@[inline]
def FloatLib.Numerics.Operation.Internal.atOfCheckedResult {B : NumericalSystem} (result : Option B.Code) {value : NumericalValue B.Scalar} (hresult : Option.map B.denote result = some value) :
B.At value

Extract the successful code from a checked computation whose refinement proof rules out failure.

This is the shared implementation of the arity-specific applyAt functions below. Inlining preserves the direct checked-operation runtime path after proof erasure.

Instances For

    Checked operations with no additional precondition #

    source
    theorem FloatLib.Numerics.Operation.Checked1.map_denote {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} (hrefines : Checked1 A B run spec) {value : A.Scalar} (code : A.AtFinite value) :
    Option.map B.denote (run code.val) = some (spec value)

    Observe a checked unary operation on a proof-indexed finite input.

    source
    theorem FloatLib.Numerics.Operation.Checked1.map_denote_eq {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} {expected : NumericalValue B.Scalar} (hrefines : Checked1 A B run spec) {value : A.Scalar} (code : A.AtFinite value) (hspec : spec value = expected) :
    Option.map B.denote (run code.val) = some expected

    Observe a checked unary operation with an independently stated result.

    source
    theorem FloatLib.Numerics.Operation.Checked1.exists_result {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} (hrefines : Checked1 A B run spec) {value : A.Scalar} (code : A.AtFinite value) :
    ∃ (result : B.Code), run code.val = some result ∧ B.denote result = spec value

    A checked unary refinement succeeds on every represented finite input.

    source
    @[inline]
    def FloatLib.Numerics.Operation.Checked1.applyAt {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} (hrefines : Checked1 A B run spec) {value : A.Scalar} (code : A.AtFinite value) :
    B.At (spec value)

    Apply a checked unary refinement to a represented input, discharging the impossible failure.

    Instances For
      source
      theorem FloatLib.Numerics.Operation.Checked2.map_denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} (hrefines : Checked2 A B C run spec) {leftValue : A.Scalar} {rightValue : B.Scalar} (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) :
      Option.map C.denote (run left.val right.val) = some (spec leftValue rightValue)

      Observe a checked two-input operation on proof-indexed finite inputs.

      source
      theorem FloatLib.Numerics.Operation.Checked2.map_denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} {expected : NumericalValue C.Scalar} (hrefines : Checked2 A B C run spec) {leftValue : A.Scalar} {rightValue : B.Scalar} (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) (hspec : spec leftValue rightValue = expected) :
      Option.map C.denote (run left.val right.val) = some expected

      Observe a checked two-input operation with an independently stated result.

      source
      theorem FloatLib.Numerics.Operation.Checked2.exists_result {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} (hrefines : Checked2 A B C run spec) {leftValue : A.Scalar} {rightValue : B.Scalar} (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) :
      ∃ (result : C.Code), run left.val right.val = some result ∧ C.denote result = spec leftValue rightValue

      A checked two-input refinement succeeds on represented finite inputs.

      source
      @[inline]
      def FloatLib.Numerics.Operation.Checked2.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} (hrefines : Checked2 A B C run spec) {leftValue : A.Scalar} {rightValue : B.Scalar} (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) :
      C.At (spec leftValue rightValue)

      Apply a checked two-input refinement, discharging the impossible failure.

      Instances For
        source
        theorem FloatLib.Numerics.Operation.Checked3.map_denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} (hrefines : Checked3 A B C D run spec) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) :
        Option.map D.denote (run first.val second.val third.val) = some (spec firstValue secondValue thirdValue)

        Observe a checked three-input operation on proof-indexed finite inputs.

        source
        theorem FloatLib.Numerics.Operation.Checked3.map_denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} {expected : NumericalValue D.Scalar} (hrefines : Checked3 A B C D run spec) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) (hspec : spec firstValue secondValue thirdValue = expected) :
        Option.map D.denote (run first.val second.val third.val) = some expected

        Observe a checked three-input operation with an independently stated result.

        source
        theorem FloatLib.Numerics.Operation.Checked3.exists_result {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} (hrefines : Checked3 A B C D run spec) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) :
        ∃ (result : D.Code), run first.val second.val third.val = some result ∧ D.denote result = spec firstValue secondValue thirdValue

        A checked three-input refinement succeeds on represented finite inputs.

        source
        @[inline]
        def FloatLib.Numerics.Operation.Checked3.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} (hrefines : Checked3 A B C D run spec) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) :
        D.At (spec firstValue secondValue thirdValue)

        Apply a checked three-input refinement, discharging the impossible failure.

        Instances For

          Checked operations under a scalar precondition #

          source
          theorem FloatLib.Numerics.Operation.Checked1On.map_denote {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} {pre : A.Scalar → Prop} (hrefines : Checked1On A B run spec pre) {value : A.Scalar} (hpre : pre value) (code : A.AtFinite value) :
          Option.map B.denote (run code.val) = some (spec value)

          Observe a preconditioned checked unary operation on a proof-indexed finite input.

          source
          theorem FloatLib.Numerics.Operation.Checked1On.map_denote_eq {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} {pre : A.Scalar → Prop} {expected : NumericalValue B.Scalar} (hrefines : Checked1On A B run spec pre) {value : A.Scalar} (hpre : pre value) (code : A.AtFinite value) (hspec : spec value = expected) :
          Option.map B.denote (run code.val) = some expected

          Observe a preconditioned checked unary operation with an independent result.

          source
          @[inline]
          def FloatLib.Numerics.Operation.Checked1On.applyAt {A : NumericalSystem} {B : NumericalSystem} {run : A.Code → Option B.Code} {spec : A.Scalar → NumericalValue B.Scalar} {pre : A.Scalar → Prop} (hrefines : Checked1On A B run spec pre) {value : A.Scalar} (hpre : pre value) (code : A.AtFinite value) :
          B.At (spec value)

          Apply a preconditioned checked unary refinement to a represented input.

          Instances For
            source
            theorem FloatLib.Numerics.Operation.Checked2On.map_denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} {pre : A.Scalar → B.Scalar → Prop} (hrefines : Checked2On A B C run spec pre) {leftValue : A.Scalar} {rightValue : B.Scalar} (hpre : pre leftValue rightValue) (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) :
            Option.map C.denote (run left.val right.val) = some (spec leftValue rightValue)

            Observe a preconditioned checked two-input operation on proof-indexed finite inputs.

            source
            theorem FloatLib.Numerics.Operation.Checked2On.map_denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} {pre : A.Scalar → B.Scalar → Prop} {expected : NumericalValue C.Scalar} (hrefines : Checked2On A B C run spec pre) {leftValue : A.Scalar} {rightValue : B.Scalar} (hpre : pre leftValue rightValue) (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) (hspec : spec leftValue rightValue = expected) :
            Option.map C.denote (run left.val right.val) = some expected

            Observe a preconditioned checked two-input operation with an independent result.

            source
            @[inline]
            def FloatLib.Numerics.Operation.Checked2On.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {run : A.Code → B.Code → Option C.Code} {spec : A.Scalar → B.Scalar → NumericalValue C.Scalar} {pre : A.Scalar → B.Scalar → Prop} (hrefines : Checked2On A B C run spec pre) {leftValue : A.Scalar} {rightValue : B.Scalar} (hpre : pre leftValue rightValue) (left : A.AtFinite leftValue) (right : B.AtFinite rightValue) :
            C.At (spec leftValue rightValue)

            Apply a preconditioned checked two-input refinement to represented inputs.

            Instances For
              source
              theorem FloatLib.Numerics.Operation.Checked3On.map_denote {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} {pre : A.Scalar → B.Scalar → C.Scalar → Prop} (hrefines : Checked3On A B C D run spec pre) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (hpre : pre firstValue secondValue thirdValue) (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) :
              Option.map D.denote (run first.val second.val third.val) = some (spec firstValue secondValue thirdValue)

              Observe a preconditioned checked three-input operation on proof-indexed finite inputs.

              source
              theorem FloatLib.Numerics.Operation.Checked3On.map_denote_eq {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} {pre : A.Scalar → B.Scalar → C.Scalar → Prop} {expected : NumericalValue D.Scalar} (hrefines : Checked3On A B C D run spec pre) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (hpre : pre firstValue secondValue thirdValue) (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) (hspec : spec firstValue secondValue thirdValue = expected) :
              Option.map D.denote (run first.val second.val third.val) = some expected

              Observe a preconditioned checked three-input operation with an independent result.

              source
              @[inline]
              def FloatLib.Numerics.Operation.Checked3On.applyAt {A : NumericalSystem} {B : NumericalSystem} {C : NumericalSystem} {D : NumericalSystem} {run : A.Code → B.Code → C.Code → Option D.Code} {spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar} {pre : A.Scalar → B.Scalar → C.Scalar → Prop} (hrefines : Checked3On A B C D run spec pre) {firstValue : A.Scalar} {secondValue : B.Scalar} {thirdValue : C.Scalar} (hpre : pre firstValue secondValue thirdValue) (first : A.AtFinite firstValue) (second : B.AtFinite secondValue) (third : C.AtFinite thirdValue) :
              D.At (spec firstValue secondValue thirdValue)

              Apply a preconditioned checked three-input refinement to represented inputs.

              Instances For