编辑“︁Lean反射API”︁（章节）

= Lean反射API =

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

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

== 基础概念 ==
=== 表达式结构 ===
Lean中的表达式是通过归纳类型定义的，主要构造函数包括：
<syntaxhighlight lang="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) -- Π类型
  | ...                    -- 其他构造
</syntaxhighlight>

=== 环境交互 ===
通过环境对象可以查询全局声明：
<syntaxhighlight lang="lean">
#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"
</syntaxhighlight>
输出：<code>Found: Nat.add</code>

== 核心API方法 ==
{| class="wikitable"
|+ 常用反射API方法
! 方法 !! 描述 !! 示例
|-
| <code>inferType</code> || 推断表达式类型 || <code>inferType (mkConst ``Nat.succ)</code>
|-
| <code>whnf</code> || 弱头范式化简 || <code>whnf (mkApp (mkConst ``Nat.add) (mkNatLit 1))</code>
|-
| <code>isDefEq</code> || 定义相等判断 || <code>isDefEq (mkNatLit 1) (mkApp (mkConst ``Nat.succ) (mkNatLit 0))</code>
|}

== 实际案例 ==
=== 自动证明构造 ===
构建一个自动生成简单等式的过程：
<syntaxhighlight lang="lean">
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  -- 抛出错误
</syntaxhighlight>

=== 表达式遍历 ===
递归计算表达式中常量出现的次数：
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 高级主题 ==
=== 元编程模式 ===
<mermaid>
graph TD
    A[表面语法] -->|解析| B(Expr)
    B -->|反射API| C[元程序]
    C -->|生成| D[新Expr]
    D -->|执行| E[结果]
</mermaid>

=== 性能考虑 ===
反射操作涉及较多计算开销，关键性能优化策略包括：
* 使用<code>withReducible</code>限制化简深度
* 缓存频繁查询的环境信息
* 避免深层表达式遍历

== 数学基础 ==
反射API的理论基础是'''λ演算'''和'''类型论'''，表达式等价性遵循：
<math>
\Gamma \vdash e_1 \equiv e_2 : \alpha \quad \text{iff} \quad \text{isDefEq}(e_1, e_2) = \text{true}
</math>

== 常见问题 ==
'''Q: 反射API与普通宏有何区别？'''
A: 宏在编译时展开，而反射API提供运行时程序化访问完整表达式的能力。

'''Q: 如何处理依赖类型？'''
A: 需要使用<code>forallE</code>构造和<code>liftLooseBVars</code>等方法管理绑定变量。

== 延伸阅读 ==
* Lean官方文档中的Meta Programming章节
* 《定理证明与元编程》相关学术论文
* 反射API在代码生成器中的实际应用案例

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean元编程]]