Lean反射API[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

Lean反射API是Lean定理证明器中用于元编程的核心工具，允许程序在运行时检查和操作Lean表达式的结构。通过反射API，开发者可以动态分析、构造和修改代码，实现自动化证明生成、领域特定语言(DSL)构建等高阶功能。反射API的核心思想是将代码本身视为数据（即表达式(Expr)类型），从而在元层面进行操作。

反射API的主要组件包括：

表达式(Expr)：表示Lean语法树的原子元素（如变量、常量、应用、λ抽象等）
环境(Environment)：包含当前上下文的定义、定理等全局信息
Elaborator：将表面语法转换为完全明确的表达式

基础概念[编辑 | 编辑源代码]

表达式结构[编辑 | 编辑源代码]

Lean中的表达式是通过归纳类型定义的，主要构造函数包括：

inductive Expr where
  | var     (idx : Nat)    -- 变量（德布鲁因索引）
  | const   (name : Name)  -- 常量引用
  | app     (fn arg : Expr) -- 函数应用
  | lam     (name : Name) (type body : Expr) -- λ抽象
  | forallE (name : Name) (type body : Expr) -- Π类型
  | ...                    -- 其他构造

环境交互[编辑 | 编辑源代码]

通过环境对象可以查询全局声明：

#eval show MetaM Unit from do
  let env ← getEnv
  let decl := env.find? ``Nat.add  -- 查找Nat.add的定义
  match decl with
  | some ci => IO.println s!"Found: {ci.name}"
  | none => IO.println "Declaration not found"

输出：Found: Nat.add

核心API方法[编辑 | 编辑源代码]

常用反射API方法
方法	描述	示例
`inferType`	推断表达式类型	inferType (mkConst ``Nat.succ)
`whnf`	弱头范式化简	whnf (mkApp (mkConst ``Nat.add) (mkNatLit 1))
`isDefEq`	定义相等判断	isDefEq (mkNatLit 1) (mkApp (mkConst ``Nat.succ) (mkNatLit 0))

实际案例[编辑 | 编辑源代码]

自动证明构造[编辑 | 编辑源代码]

构建一个自动生成简单等式的过程：

def autoProve (a b : Nat) : MetaM Expr := do
  let e ← mkAppM ``Eq #[mkNatLit a, mkNatLit b]
  if a = b then
    mkAppM ``Eq.refl #[mkNatLit a]  -- 生成refl证明
  else
    throwError "Not equal"

#eval autoProve 2 2  -- 成功生成证明
#eval autoProve 1 2  -- 抛出错误

表达式遍历[编辑 | 编辑源代码]

递归计算表达式中常量出现的次数：

partial def countConsts (e : Expr) : MetaM Nat := do
  match e with
  | .const _ _ => return 1
  | .app f a => return (← countConsts f) + (← countConsts a)
  | .lam _ _ b => countConsts b
  | _ => return 0

#eval countConsts (mkApp (mkConst ``Nat.add) (mkConst ``Nat.zero)) -- 返回2