Documentation

LeanCert.Engine.Eval.Extended

Extended (Noncomputable) Interval Evaluation #

This file implements the noncomputable interval evaluator for LeanCert.Core.Expr, supporting exp with floor/ceil bounds and partial evaluation for inv/log.

Main definitions #

Design notes #

The extended evaluator uses Real.exp with floor/ceil bounds, which requires noncomputability. For computability, use LeanCert.Internal.Rational.evalTotalCore instead.

The partial evaluator evalInterval? returns none when:

When it returns some I, correctness is guaranteed.

Extended interval evaluation (noncomputable, supports exp) #

source
noncomputable def LeanCert.Internal.Rational.evalUnchecked (e : Core.Expr) (ρ : Engine.IntervalEnv) :
Core.IntervalRat

Noncomputable interval evaluator supporting exp.

For supported expressions (const, var, add, mul, neg, sin, cos, exp), this computes correct interval bounds with a fully-verified proof.

For unsupported expressions (inv, log), returns a default interval. Do not rely on results for expressions containing inv or log. Use evalInterval? for partial functions like inv and log.

This evaluator is NONCOMPUTABLE due to exp using Real.exp with floor/ceil.

Equations
Instances For
    source
    theorem LeanCert.Engine.evalInterval_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) :
    Core.Expr.eval ρ_real e ∈ Internal.Rational.evalUnchecked e ρ_int

    Fundamental correctness theorem for extended evaluation.

    This theorem is FULLY PROVED (no sorry, no axioms) for supported expressions. The hsupp hypothesis ensures we only consider expressions in the verified subset.

    Convenience functions #

    Note: LeanCert.Internal.Rational.evalTotalCore now uses Taylor series for exp/sin/cos, which gives different (often tighter) intervals than evalInterval's floor/ceil bounds. Both are correct, but they are not necessarily equal.

    For purely algebraic expressions (const, var, add, mul, neg), both evaluators give identical results.

    source
    noncomputable def LeanCert.Internal.Rational.evalUnchecked1 (e : Core.Expr) (I : Core.IntervalRat) :
    Core.IntervalRat

    Internal single-variable wrapper around evalUnchecked.

    Equations
    Instances For
      source
      theorem LeanCert.Engine.evalInterval1_correct (e : Core.Expr) (hsupp : ADSupported e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) :
      Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ Internal.Rational.evalUnchecked1 e I

      Correctness for single-variable extended evaluation

      Partial interval evaluation with inv support #

      source
      def LeanCert.Engine.evalIntervalLogDepth :
      ℕ

      Partial (Option-returning) interval evaluator supporting inv.

      For expressions with inv, this evaluator returns none if the denominator interval contains zero, and some I with a correct enclosure otherwise.

      This allows safe interval evaluation of expressions like 1/x when we can verify the denominator is bounded away from zero.

      For expressions without inv, this always returns some with the same result as evalInterval.

      Equations
      Instances For
        source
        def LeanCert.Engine.evalIntervalExpDepth :
        ℕ
        Equations
        Instances For
          source
          def LeanCert.Engine.evalIntervalAtanhDepth :
          ℕ

          Taylor depth used by the strict atanh evaluator.

          Equations
          Instances For
            source
            def LeanCert.Engine.evalInterval? (e : Core.Expr) (ρ : IntervalEnv) :
            Option Core.IntervalRat
            Equations
            Instances For
              source
              theorem LeanCert.Engine.evalInterval?_correct (e : Core.Expr) (ρ_int : IntervalEnv) (I : Core.IntervalRat) (hsome : evalInterval? e ρ_int = some I) (ρ_real : ℕ → ℝ) (hρ : envMem ρ_real ρ_int) :
              Core.Expr.eval ρ_real e ∈ I

              Main correctness theorem for evalInterval? (approach 1 from plan).

              When evalInterval? returns some I:

              1. The expression evaluates to a value in I for all ρ_real ∈ ρ_int
              2. All inv denominators along the evaluation are guaranteed nonzero (because their intervals don't contain zero)

              This follows your suggestion to keep ADSupported syntactic and add separate semantic hypotheses. The key insight is that if evalInterval? succeeds (returns Some), the interval arithmetic has already verified that no denominator interval contains zero.

              Checked API with diagnostics #

              source
              @[irreducible]
              def LeanCert.Engine.diagnoseEvalIntervalFailure (e : Core.Expr) (ρ : IntervalEnv) :
              EvalError

              Diagnose the first partial-domain failure after evalInterval? returned none. This function is deliberately separate from the trusted computation: soundness depends only on successful evalInterval?, while diagnostics may be refined without changing the correctness theorem.

              Equations
              Instances For
                source
                def LeanCert.Engine.evalIntervalChecked (e : Core.Expr) (ρ : IntervalEnv) :
                EvalResult Core.IntervalRat

                Checked rational evaluator. Every successful result is a certified finite enclosure; domain-invalid expressions return a structured error.

                Equations
                Instances For
                  source
                  theorem LeanCert.Engine.evalIntervalChecked_correct (e : Core.Expr) (ρ_int : IntervalEnv) (I : Core.IntervalRat) (hsuccess : evalIntervalChecked e ρ_int = Except.ok I) (ρ_real : ℕ → ℝ) (hρ : envMem ρ_real ρ_int) :
                  Core.Expr.eval ρ_real e ∈ I

                  Success of evalIntervalChecked is sufficient for enclosure correctness for every expression constructor.

                  source
                  def LeanCert.Engine.evalIntervalTightChecked (e : Core.Expr) (ρ : IntervalEnv) (cfg : EvalConfig := { }) :
                  EvalResult Core.IntervalRat

                  Checked Rational evaluation with a tight path for the verified computable core. Unsupported syntax or a failed core-domain check falls back to the general checked evaluator, preserving its structured domain errors.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem LeanCert.Engine.evalIntervalTightChecked_correct (e : Core.Expr) (ρ_int : IntervalEnv) (cfg : EvalConfig) (I : Core.IntervalRat) (hsuccess : evalIntervalTightChecked e ρ_int cfg = Except.ok I) (ρ_real : ℕ → ℝ) (hρ : envMem ρ_real ρ_int) :
                    Core.Expr.eval ρ_real e ∈ I

                    Every successful tight checked Rational evaluation encloses the expression value. The core branch uses the core correctness theorem; the fallback uses the general checked evaluator theorem.

                    source
                    def LeanCert.Engine.evalInterval?1 (e : Core.Expr) (I : Core.IntervalRat) :
                    Option Core.IntervalRat

                    Single-variable version of evalInterval?

                    Equations
                    Instances For
                      source
                      theorem LeanCert.Engine.evalInterval?1_correct (e : Core.Expr) (I J : Core.IntervalRat) (hsome : evalInterval?1 e I = some J) (x : ℝ) (hx : x ∈ I) :
                      Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ J

                      Correctness for single-variable partial evaluation

                      source
                      theorem LeanCert.Engine.evalInterval?_le_of_hi (e : Core.Expr) (I J : Core.IntervalRat) (c : ℚ) (hsome : evalInterval?1 e I = some J) (hhi : J.hi ≤ c) (x : ℝ) :
                      x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

                      When evalInterval? succeeds, we get bounds

                      source
                      theorem LeanCert.Engine.evalInterval?_ge_of_lo (e : Core.Expr) (I J : Core.IntervalRat) (c : ℚ) (hsome : evalInterval?1 e I = some J) (hlo : c ≤ J.lo) (x : ℝ) :
                      x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

                      When evalInterval? succeeds, we get lower bounds