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.).

Shared AST Proof Helpers #

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: all Expr constructors, provided every variable is var 0. Not supported: var n for n ≠ 0.

ADSupported Proof Generation #

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

Note: ADSupported is a strict subset of ExprSupportedCore. ADSupported 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 ADSupported 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, named constants Not supported: inv, atan, arsinh, 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

    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
    • One or more equations did not get rendered due to their size.
    Instances For