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

structure LeanCert.Meta.ReifyState : Type

Mutable bookkeeping for one reification pass.

• unfolded : Array Lean.Name

  Definitions delta-reduced while exposing supported arithmetic.

• remainingUnfoldSteps : ℕ

  Remaining delta-reduction steps. This prevents recursive wrappers from making reification diverge.

structure LeanCert.Meta.ReifyReport : Type

The result of reification together with information needed to bridge the reflected expression back to the user's original syntax.

• expr : Lean.Expr
• unfolded : Array Lean.Name

@[reducible, inline]

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

The translation monad: a read-only variable context plus bounded reification bookkeeping over MetaM.

Equations

• LeanCert.Meta.TranslateM = ReaderT LeanCert.Meta.Context (StateT LeanCert.Meta.ReifyState 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_reducible]

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 through the named Expr.sub wrapper.

Expr.sub is definitionally implemented by addition and negation, so the executable evaluator is unchanged. Preserving the wrapper until bridge normalization lets Expr.eval_sub recover the user's lhs - rhs syntax and is essential for general root goals lhs = rhs.

Equations

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

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.mkExprNamedConst (c : Lean.Expr) : Lean.MetaM Lean.Expr

Build LeanCert.Core.Expr.namedConst c.

Equations

• LeanCert.Meta.mkExprNamedConst c = Lean.Meta.mkAppM `LeanCert.Core.Expr.namedConst #[c]

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

Build LeanCert.Core.Expr.namedConst .pi.

Equations

• LeanCert.Meta.mkExprPi = LeanCert.Meta.mkExprNamedConst (Lean.mkConst `LeanCert.Core.MathConst.pi)

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

Build LeanCert.Core.Expr.namedConst .eulerMascheroni.

Equations

• LeanCert.Meta.mkExprEulerMascheroni = LeanCert.Meta.mkExprNamedConst (Lean.mkConst `LeanCert.Core.MathConst.eulerMascheroni)

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. Try to match a known operator/function (+, *, -, /, sin, cos, exp, etc.)
3. Check if it's a numeric constant (ℕ, ℤ, ℚ literals and casts)
4. Reduce with whnf and retry
5. Unfold definitions and retry

Important: Step 2 (operator matching) must come before step 3 (numeric constant). Otherwise toRat? eagerly constant-folds compound expressions like ↑(-2 : ℤ) + 3 into const(1), losing the syntactic structure needed by the bridge converter. With operators first, this reifies as add(const(-2), const(3)) which the bridge can match against the goal.

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.reifyWithReport (e : Lean.Expr) (maxUnfoldSteps : ℕ := 128) : Lean.MetaM ReifyReport

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

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

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.