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 evalIntervalCore 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.Engine.evalInterval (e : Core.Expr) (ρ : 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 : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) :
    Core.Expr.eval ρ_real e ∈ evalInterval 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: evalIntervalCore 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.Engine.evalInterval1 (e : Core.Expr) (I : Core.IntervalRat) :
    Core.IntervalRat

    Noncomputable single-variable evaluation for extended expressions

    Equations
    Instances For
      source
      theorem LeanCert.Engine.evalInterval1_correct (e : Core.Expr) (hsupp : ExprSupported e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) :
      Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ evalInterval1 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.evalInterval? (e : Core.Expr) (ρ : IntervalEnv) :
          Option Core.IntervalRat
          Equations
          Instances For
            source
            theorem LeanCert.Engine.evalInterval?_correct (e : Core.Expr) (hsupp : ExprSupportedWithInv e) (ρ_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 ExprSupported 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.

            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) (hsupp : ExprSupportedWithInv e) (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) (hsupp : ExprSupportedWithInv e) (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) (hsupp : ExprSupportedWithInv e) (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