Documentation

LeanCert.Tactic.IntervalAuto.Bound

Main Interval Bound Tactics #

Core interval bound proving: intervalBoundCore, certify_bound, interval_bound. Also includes shadow diagnostics for error reporting.

Diagnostic Helpers for Shadow Computation #

source
def LeanCert.Tactic.Auto.runShadowDiagnostic (boundGoal : Option BoundGoal) (_goalType : Lean.Expr) :
Lean.Elab.Tactic.TacticM Lean.MessageData

Run shadow computation to diagnose why a proof failed

Equations
Instances For

    Main Tactic Implementation #

    source
    def LeanCert.Tactic.Auto.intervalBoundCore (taylorDepth : ℕ) :
    Lean.Elab.Tactic.TacticM Unit

    The main interval_bound tactic implementation

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LeanCert.Tactic.Auto.intervalBoundCore.proveForallLe (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) :
      Lean.Elab.Tactic.TacticM Unit

      Prove ∀ x ∈ I, f x ≤ c

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def LeanCert.Tactic.Auto.intervalBoundCore.proveForallGe (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) :
        Lean.Elab.Tactic.TacticM Unit

        Prove ∀ x ∈ I, c ≤ f x

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def LeanCert.Tactic.Auto.intervalBoundCore.proveForallLt (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) :
          Lean.Elab.Tactic.TacticM Unit

          Prove ∀ x ∈ I, f x < c

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def LeanCert.Tactic.Auto.intervalBoundCore.proveForallGt (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) :
            Lean.Elab.Tactic.TacticM Unit

            Prove ∀ x ∈ I, c < f x

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Tactic Syntax #

              source
              def LeanCert.Tactic.Auto.tacticCertify_bound_ :
              Lean.ParserDescr

              The certify_bound tactic.

              Automatically proves bounds on expressions using interval arithmetic.

              Usage:

              • certify_bound - uses adaptive precision (tries depths 10, 15, 20, 25, 30)
              • certify_bound 20 - uses fixed Taylor depth of 20

              Supports goals of the form:

              • ∀ x ∈ I, f x ≤ c
              • ∀ x ∈ I, c ≤ f x
              • ∀ x ∈ I, f x < c
              • ∀ x ∈ I, c < f x

              Note: interval_bound is an alias for backward compatibility.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def LeanCert.Tactic.Auto.tacticInterval_bound_ :
                Lean.ParserDescr

                Backward-compatible alias for certify_bound

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For