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)

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.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.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 #[]

Constant Extraction

Lean stores numbers as complex hierarchies of type classes (OfNat.ofNat, Rat.cast, etc.). We need a pattern matcher that digs out the actual number.

partial def LeanCert.Meta.toRat? (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Attempt to parse a Lean Expr as a constant rational number. Handles various encodings: Nat literals, Int literals, OfNat, Neg, etc.

partial def LeanCert.Meta.toRat?.tryMatchNumeric (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Try to match a numeric expression.

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.

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.

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.