Documentation

LeanCert.Meta.ProveContinuous

Automatic Continuity Proof Generation #

This module provides metaprogramming infrastructure to automatically generate ContinuousOn proof terms for reified LeanCert expressions.

Given a reified AST e : LeanCert.Core.Expr, we construct a proof that ContinuousOn (fun x => Expr.eval (fun _ => x) e) (Set.Icc lo hi).

Main definitions #

Design #

We define ExprContinuousCore as a separate predicate from ExprSupportedCore because:

Operations in ExprContinuousCore:

source
@[reducible, inline]
abbrev LExpr :
Type
Equations
Instances For

    Continuous Expression Predicate #

    Since inv (1/x) is not continuous at 0, we define a separate predicate for expressions that are continuous everywhere. This excludes inv from ExprSupportedCore.

    source
    inductive LeanCert.Meta.ExprContinuousCore :
    LExpr → Prop

    Expressions that are continuous everywhere (excludes inv and log). This is a subset of ExprSupportedCore used for continuity proofs. Note: log is excluded because it is not continuous at 0.

    Instances For
      source
      theorem LeanCert.Meta.ExprContinuousCore.toSupported {e : LExpr} (h : ExprContinuousCore e) :
      Core.ExprSupportedCore e

      ExprContinuousCore implies ExprSupportedCore

      Base Continuity Theorem #

      This theorem proves that all ExprContinuousCore expressions evaluate to continuous functions. We prove this by induction on the structure of ExprContinuousCore.

      source
      theorem LeanCert.Meta.exprContinuousCore_continuousOn (e : LExpr) (hsupp : ExprContinuousCore e) {s : Set ℝ} :
      ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) s

      All ExprContinuousCore expressions are continuous on any set.

      This is the foundational theorem that allows automatic continuity proof generation. Since ExprContinuousCore only includes operations that are continuous everywhere (const, var, add, mul, neg, sin, cos, exp, sqrt, sinh, cosh, tanh), the result follows by structural induction.

      NOTE: inv and log are NOT included because they are not continuous at 0.

      source
      theorem LeanCert.Meta.exprContinuousCore_continuousOn_Icc (e : LExpr) (hsupp : ExprContinuousCore e) (lo hi : ℝ) :
      ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc lo hi)

      Specialized version for Icc intervals (common case for interval_roots)

      source
      theorem LeanCert.Meta.exprContinuousCore_continuousOn_interval (e : LExpr) (hsupp : ExprContinuousCore e) (I : Core.IntervalRat) :
      ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)

      Version taking IntervalRat for convenience

      Backward Compatibility: ExprSupportedCore Continuity #

      These theorems are provided for backward compatibility with code that uses ExprSupportedCore. For expressions with log, a domain validity condition is required.

      source
      def LeanCert.Meta.exprContinuousDomainValid (e : LExpr) (s : Set ℝ) :
      Prop

      Domain validity for continuity: ensures log arguments evaluate to positive values. For expressions without log, this is always True.

      Equations
      Instances For
        source
        theorem LeanCert.Meta.exprContinuousDomainValid_of_ExprSupported {e : LExpr} (hsupp : Core.ExprSupported e) {s : Set ℝ} :
        exprContinuousDomainValid e s

        Domain validity is trivially true for ExprSupported expressions (which exclude log).

        source
        theorem LeanCert.Meta.exprContinuousDomainValid_of_ExprContinuousCore {e : LExpr} (hcont : ExprContinuousCore e) {s : Set ℝ} :
        exprContinuousDomainValid e s

        Domain validity is trivially true for ExprContinuousCore expressions (no log).

        source
        theorem LeanCert.Meta.exprSupportedCore_continuousOn (e : LExpr) (hsupp : Core.ExprSupportedCore e) {s : Set ℝ} (hdom : exprContinuousDomainValid e s) :
        ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) s

        All ExprSupportedCore expressions are continuous on sets where log arguments are positive.

        This theorem exists for backward compatibility with code that uses ExprSupportedCore. For expressions with log, the domain validity condition ensures the argument evaluates to positive values on s.

        Metaprogramming: Continuity Proof Generation #

        Generate proof terms of ContinuousOn (fun x => Expr.eval (fun _ => x) e) (Set.Icc lo hi) by applying exprContinuousCore_continuousOn_Icc with an automatically generated ExprContinuousCore proof.

        Note: We use ExprContinuousCore (not ExprSupportedCore) because inv is not continuous everywhere, and ExprContinuousCore excludes inv.

        source
        partial def LeanCert.Meta.mkContinuousCoreProof (e_ast : Lean.Expr) :
        Lean.MetaM Lean.Expr

        Generate a proof of ExprContinuousCore e_ast by matching on the AST structure.

        This is similar to mkSupportedCoreProof but for the ExprContinuousCore predicate which excludes inv (since 1/x is not continuous at 0).

        Supported: const, var, add, mul, neg, sin, cos, exp, sqrt, sinh, cosh, tanh Not supported: inv, log, atan, arsinh, atanh

        source
        def LeanCert.Meta.mkContinuousOnProof (e_ast interval : Lean.Expr) :
        Lean.MetaM Lean.Expr

        Generate a ContinuousOn proof for an expression on an interval.

        Given:

        • e_ast : the AST expression (Lean.Expr representing LeanCert.Core.Expr)
        • interval : the interval expression (Lean.Expr representing IntervalRat)

        Returns a proof of: ContinuousOn (fun x => Expr.eval (fun _ => x) e) (Set.Icc I.lo I.hi)

        This works by:

        1. Generating an ExprContinuousCore proof for the AST
        2. Applying exprContinuousCore_continuousOn_interval

        Note: This will fail for expressions containing inv since 1/x is not continuous at 0.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def LeanCert.Meta.mkContinuousOnProofIcc (e_ast lo hi : Lean.Expr) :
          Lean.MetaM Lean.Expr

          Alternative: generate ContinuousOn proof with explicit lo/hi bounds

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

            Testing Infrastructure #

            source
            def LeanCert.Meta.«command#check_continuous_On_,_» :
            Lean.ParserDescr

            Debug command to test continuity proof generation

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