Metaprogram for Reifying Lean Expressions to LeanCert AST

This module provides metaprogramming infrastructure to translate Lean kernel expressions (e.g., fun (x : ℝ) => x + 2) into LeanCert.Core.Expr terms (e.g., Expr.add (Expr.var 0) (Expr.const 2)).

Main definitions

• LeanCert.Meta.Context - Context tracking free variables and their de Bruijn indices
• LeanCert.Meta.TranslateM - The translation monad
• LeanCert.Meta.toLeanCertExpr - Main recursive translation function
• LeanCert.Meta.reify - Entry point that handles lambda expressions

Usage

#leancert_reflect (fun x => x * x + 1)
-- Output: Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.const 1)

theorem LeanCert.Meta.max_eq_half_add_abs_sub (a b : ℝ) : max a b = (a + b + |b + -a|) / 2

Closed-form rewrite for max on reals, used for reification via existing Expr nodes.

theorem LeanCert.Meta.min_eq_half_sub_abs_sub (a b : ℝ) : min a b = (a + b - |b + -a|) / 2

Closed-form rewrite for min on reals, used for reification via existing Expr nodes.

structure LeanCert.Meta.Context : Type

Context for the translation. Stores fvars of the lambda being traversed. vars[0] corresponds to var 0, vars[1] to var 1, etc.

• vars : Array Lean.Expr

  Array of free variables from the lambda telescope

@[reducible, inline]

abbrev LeanCert.Meta.TranslateM (α : Type) : Type

The translation monad: ReaderT over MetaM with our Context.

Equations

• LeanCert.Meta.TranslateM = ReaderT LeanCert.Meta.Context Lean.MetaM

def LeanCert.Meta.findVarIdx? (e : Lean.Expr) : TranslateM (Option ℕ)

Look up a Free Variable in the context. Returns its de Bruijn index if found.

Equations

• LeanCert.Meta.findVarIdx? e = do let ctx ← read pure (Array.findIdx? (fun (x : Lean.Expr) => x == e) ctx.vars)

Helper Functions: AST Constructors

These functions build LeanCert.Core.Expr syntax trees. They construct Lean expressions that represent LeanCert AST terms.

def LeanCert.Meta.mkExprConst (q : ℚ) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.const q for a rational number.

Equations

• LeanCert.Meta.mkExprConst q = do let ratExpr ← Lean.Meta.mkAppM `Rat.divInt #[Lean.toExpr q.num, Lean.toExpr ↑q.den] Lean.Meta.mkAppM `LeanCert.Core.Expr.const #[ratExpr]

instance LeanCert.Meta.instToExprRat_leanCert : Lean.ToExpr ℚ

ToExpr instance for ℚ (rationals)

Equations

• LeanCert.Meta.instToExprRat_leanCert = { toExpr := fun (q : ℚ) => Lean.mkApp2 (Lean.mkConst `Rat.divInt) (Lean.toExpr q.num) (Lean.toExpr ↑q.den), toTypeExpr := Lean.mkConst `Rat }

def LeanCert.Meta.mkExprVar (idx : ℕ) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.var idx for a variable index.

Equations

• LeanCert.Meta.mkExprVar idx = Lean.Meta.mkAppM `LeanCert.Core.Expr.var #[Lean.toExpr idx]

def LeanCert.Meta.mkExprAdd (e1 e2 : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.add e1 e2.

Equations

• LeanCert.Meta.mkExprAdd e1 e2 = Lean.Meta.mkAppM `LeanCert.Core.Expr.add #[e1, e2]

def LeanCert.Meta.mkExprMul (e1 e2 : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.mul e1 e2.

Equations

• LeanCert.Meta.mkExprMul e1 e2 = Lean.Meta.mkAppM `LeanCert.Core.Expr.mul #[e1, e2]

def LeanCert.Meta.mkExprNeg (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.neg e.

Equations

• LeanCert.Meta.mkExprNeg e = Lean.Meta.mkAppM `LeanCert.Core.Expr.neg #[e]

def LeanCert.Meta.mkExprSub (e1 e2 : Lean.Expr) : Lean.MetaM Lean.Expr

Build subtraction e1 - e2 as e1 + (-e2) in Expr AST.

Equations

• LeanCert.Meta.mkExprSub e1 e2 = do let __do_lift ← LeanCert.Meta.mkExprNeg e2 LeanCert.Meta.mkExprAdd e1 __do_lift

def LeanCert.Meta.mkExprInv (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.inv e.

Equations

• LeanCert.Meta.mkExprInv e = Lean.Meta.mkAppM `LeanCert.Core.Expr.inv #[e]

def LeanCert.Meta.mkExprSin (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.sin e.

Equations

• LeanCert.Meta.mkExprSin e = Lean.Meta.mkAppM `LeanCert.Core.Expr.sin #[e]

def LeanCert.Meta.mkExprCos (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.cos e.

Equations

• LeanCert.Meta.mkExprCos e = Lean.Meta.mkAppM `LeanCert.Core.Expr.cos #[e]

def LeanCert.Meta.mkExprExp (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.exp e.

Equations

• LeanCert.Meta.mkExprExp e = Lean.Meta.mkAppM `LeanCert.Core.Expr.exp #[e]

def LeanCert.Meta.mkExprLog (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.log e.

Equations

• LeanCert.Meta.mkExprLog e = Lean.Meta.mkAppM `LeanCert.Core.Expr.log #[e]

def LeanCert.Meta.mkExprAtan (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.atan e.

Equations

• LeanCert.Meta.mkExprAtan e = Lean.Meta.mkAppM `LeanCert.Core.Expr.atan #[e]

def LeanCert.Meta.mkExprArsinh (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.arsinh e.

Equations

• LeanCert.Meta.mkExprArsinh e = Lean.Meta.mkAppM `LeanCert.Core.Expr.arsinh #[e]

def LeanCert.Meta.mkExprAtanh (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.atanh e.

Equations

• LeanCert.Meta.mkExprAtanh e = Lean.Meta.mkAppM `LeanCert.Core.Expr.atanh #[e]

def LeanCert.Meta.mkExprSinc (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.sinc e.

Equations

• LeanCert.Meta.mkExprSinc e = Lean.Meta.mkAppM `LeanCert.Core.Expr.sinc #[e]

def LeanCert.Meta.mkExprErf (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.erf e.

Equations

• LeanCert.Meta.mkExprErf e = Lean.Meta.mkAppM `LeanCert.Core.Expr.erf #[e]

def LeanCert.Meta.mkExprSqrt (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.sqrt e.

Equations

• LeanCert.Meta.mkExprSqrt e = Lean.Meta.mkAppM `LeanCert.Core.Expr.sqrt #[e]

def LeanCert.Meta.mkExprAbs (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build absolute value as sqrt (e * e).

Equations

• LeanCert.Meta.mkExprAbs e = do let __do_lift ← LeanCert.Meta.mkExprMul e e LeanCert.Meta.mkExprSqrt __do_lift

def LeanCert.Meta.mkExprSinh (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.sinh e.

Equations

• LeanCert.Meta.mkExprSinh e = Lean.Meta.mkAppM `LeanCert.Core.Expr.sinh #[e]

def LeanCert.Meta.mkExprCosh (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.cosh e.

Equations

• LeanCert.Meta.mkExprCosh e = Lean.Meta.mkAppM `LeanCert.Core.Expr.cosh #[e]

def LeanCert.Meta.mkExprTanh (e : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.tanh e.

Equations

• LeanCert.Meta.mkExprTanh e = Lean.Meta.mkAppM `LeanCert.Core.Expr.tanh #[e]

def LeanCert.Meta.mkExprPi : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.pi.

Equations

• LeanCert.Meta.mkExprPi = Lean.Meta.mkAppM `LeanCert.Core.Expr.pi #[]

def LeanCert.Meta.mkExprMaxViaAbs (a b : Lean.Expr) : Lean.MetaM Lean.Expr

Build max(a,b) via (a + b + |b - a|) / 2 in existing Expr constructors.

Equations

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

def LeanCert.Meta.mkExprMinViaAbs (a b : Lean.Expr) : Lean.MetaM Lean.Expr

Build min(a,b) via (a + b - |b - a|) / 2 in existing Expr constructors.

Equations

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

Constant Extraction

Numeric parsing is shared in LeanCert.Meta.Numeral.toRat?.

Main Reification Loop

The recursive function that traverses the Lean expression tree and builds the corresponding LeanCert AST.

partial def LeanCert.Meta.toLeanCertExpr (e : Lean.Expr) : TranslateM Lean.Expr

Main recursive translation from Lean.Expr to LeanCert.Core.Expr (as Lean.Expr).

Logic:

1. Check if it's a variable in our context
2. Check if it's a constant number
3. Check if it's a known arithmetic operator (+, *, -, /)
4. Check if it's a known transcendental (sin, cos, exp, log, etc.)
5. Fail if unrecognized

partial def LeanCert.Meta.toLeanCertExpr.tryMatchExpr (e : Lean.Expr) : TranslateM (Option Lean.Expr)

Try to match the expression against known patterns.

def LeanCert.Meta.toLeanCertExpr.lookupUnary (n : Lean.Name) : Option (Lean.Expr → Lean.MetaM Lean.Expr)

Unary head-symbol handlers.

Equations

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

def LeanCert.Meta.toLeanCertExpr.lookupBinary (n : Lean.Name) : Option (Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)

Binary head-symbol handlers.

Equations

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

def LeanCert.Meta.toLeanCertExpr.unaryTable : List (Lean.Name × (Lean.Expr → Lean.MetaM Lean.Expr))

Table for unary operations.

Equations

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

def LeanCert.Meta.toLeanCertExpr.binaryTable : List (Lean.Name × (Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr))

Table for binary operations with direct AST constructors.

Equations

• LeanCert.Meta.toLeanCertExpr.binaryTable = [(`HAdd.hAdd, LeanCert.Meta.mkExprAdd), (`HMul.hMul, LeanCert.Meta.mkExprMul)]

def LeanCert.Meta.toLeanCertExpr.lastArg? (args : Array Lean.Expr) : Option Lean.Expr

Last argument of an application (if present).

Equations

• LeanCert.Meta.toLeanCertExpr.lastArg? args = if _h : args.size ≥ 1 then some args[args.size - 1]! else none

def LeanCert.Meta.toLeanCertExpr.lastTwoArgs? (args : Array Lean.Expr) : Option (Lean.Expr × Lean.Expr)

Last two arguments of an application (if present).

Equations

• LeanCert.Meta.toLeanCertExpr.lastTwoArgs? args = if _h : args.size ≥ 2 then some (args[args.size - 2]!, args[args.size - 1]!) else none

def LeanCert.Meta.toLeanCertExpr.throwUnsupported {α : Type} (e : Lean.Expr) : TranslateM α

Rich unsupported-expression diagnostics (head symbol + arity).

Equations

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

partial def LeanCert.Meta.toLeanCertExpr.mkPow (base : Lean.Expr) (k : ℕ) : Lean.MetaM Lean.Expr

Build a power expression using repeated multiplication. pow(base, k) = base * base * ... * base (k times) or 1 if k = 0.

def LeanCert.Meta.toLeanCertExpr.mkPowInt (base : Lean.Expr) (z : ℤ) : Lean.MetaM Lean.Expr

Build base ^ z for integer z using Expr.pow + Expr.inv.

Equations

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

def LeanCert.Meta.toLeanCertExpr.mkHalfIntegerPow (base : Lean.Expr) (n : ℤ) : Lean.MetaM Lean.Expr

Build base ^ (n/2) for integer numerator n (half-integers).

Equations

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

def LeanCert.Meta.toLeanCertExpr.toMaxArgs? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Try to decompose e as max a b using definitional equality. This is robust against internal projection names changing across Mathlib versions.

Equations

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

def LeanCert.Meta.toLeanCertExpr.toMinArgs? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Try to decompose e as min a b using definitional equality.

Equations

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

Entry Point

The main entry point that strips the leading lambda and initializes the context.

def LeanCert.Meta.reify (e : Lean.Expr) : Lean.MetaM Lean.Expr

Entry point: Takes a lambda fun x y ... => body and returns the LeanCert AST.

This function uses lambdaTelescope to introduce the lambda-bound variables as free variables, then translates the body with those variables tracked in the context.

Equations

• LeanCert.Meta.reify e = Lean.Meta.lambdaTelescope e fun (vars : Array Lean.Expr) (body : Lean.Expr) => have ctx := { vars := vars }; ReaderT.run (LeanCert.Meta.toLeanCertExpr body) ctx

Testing Infrastructure

def LeanCert.Meta.«command#leancert_reflect_» : Lean.ParserDescr

Elaborate a term and reify it to a LeanCert expression. Useful for debugging the reification process.

Equations

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