Documentation

LeanCert.Meta.ProveSupported

Automatic Support Proof Generation #

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

Given a reified AST e : LeanCert.Core.Expr, we can construct a proof that ExprSupportedCore e by recursively matching on the AST structure.

Main definitions #

Usage #

#check_supported (fun x => x * x + 1)
-- Output: Generated proof type: ExprSupportedCore (Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.const 1))

Design notes #

Unlike Phase 1 where we matched on Lean's math operations (HAdd.hAdd, etc.), here we match on our own AST constructors (LeanCert.Core.Expr.add, etc.).

UsesOnlyVar0 Proof Generation #

Generate proof terms of type UsesOnlyVar0 e by recursively matching on the structure of e : LeanCert.Core.Expr.

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

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

This function inspects the head constant of the AST expression and recursively builds the appropriate proof constructor.

Supported: const, var 0, add, mul, neg, sin, cos, exp, atan, arsinh Not supported: var n (n ≠ 0), inv, log, atanh

ExprSupported Proof Generation #

Generate proof terms of type ExprSupported e by recursively matching on the structure of e : LeanCert.Core.Expr.

Note: ExprSupported is a strict subset of ExprSupportedCore. ExprSupported only supports: const, var, add, mul, neg, sin, cos, exp

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

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

This function inspects the head constant of the AST expression and recursively builds the appropriate proof constructor.

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

ExprSupportedCore Proof Generation #

Generate proof terms of type ExprSupportedCore e by recursively matching on the structure of e : LeanCert.Core.Expr.

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

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

This function inspects the head constant of the AST expression and recursively builds the appropriate proof constructor.

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

ExprSupportedWithInv Proof Generation #

Generate proof terms of type ExprSupportedWithInv e by recursively matching on the structure of e : LeanCert.Core.Expr. This supports the full expression language.

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

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

This function supports all expression constructors including inv, log, atan, arsinh, and atanh.

Testing Infrastructure #

source
def LeanCert.Meta.«command#check_supported_» :
Lean.ParserDescr

Elaborate a term, reify it to a LeanCert expression, and generate an ExprSupportedCore proof. Useful for debugging.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LeanCert.Meta.«command#check_supported_inv_» :
    Lean.ParserDescr

    Similar to #check_supported but for ExprSupportedWithInv.

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

      Combined Reification and Support Proof #

      Convenience functions that combine reification and support proof generation.

      source
      def LeanCert.Meta.reifyWithSupportCore (e : Lean.Expr) :
      Lean.MetaM (Lean.Expr × Lean.Expr)

      Reify a Lean expression and generate both the AST and its ExprSupportedCore proof.

      Equations
      Instances For
        source
        def LeanCert.Meta.reifyWithSupportInv (e : Lean.Expr) :
        Lean.MetaM (Lean.Expr × Lean.Expr)

        Reify a Lean expression and generate both the AST and its ExprSupportedWithInv proof.

        Equations
        Instances For