Lean 4 的 tactic 不是黑盒——每个 tactic 本质上是一段操作证明状态的程序。本篇拆解这套元编程基础设施：Expr 是表达式的内存表示，MVarId 标识待填充的证明目标，MetaM 和 TacticM 是承载副作用的 monad 栈。理解这三层之后，自定义 tactic 就不再是猜测 API 的过程。

Expr：表达式的内部表示

Lean 4 中一切类型、命题、证明项统一表示为 Expr。核心构造子（简化版）：

1
2
3
4
5
6
7
8
9
10
11
12
13
inductive Expr where
  | bvar   : Nat → Expr                          -- 局部绑定变量（de Bruijn index）
  | fvar   : FVarId → Expr                       -- 自由变量
  | mvar   : MVarId → Expr                       -- 元变量（待填充的洞）
  | sort   : Level → Expr                        -- Type u / Prop
  | const  : Name → List Level → Expr            -- 全局常量
  | app    : Expr → Expr → Expr                  -- 函数应用
  | lam    : Name → Expr → Expr → BinderInfo → Expr  -- λ 抽象
  | forallE: Name → Expr → Expr → BinderInfo → Expr  -- Π 类型
  | letE   : Name → Expr → Expr → Expr → Bool → Expr -- let 绑定
  | lit    : Literal → Expr                      -- 数值/字符串字面量
  | mdata  : MData → Expr → Expr                 -- 元数据注解
  | proj   : Name → Nat → Expr → Expr            -- 结构体投影

用 #check 观察具体表达式的内部结构：

1
2
3
4
5
6
7
8
#check @Nat.add
-- Nat.add : Nat → Nat → Nat

open Lean in
#eval do
  let env ← getEnv
  let some info := env.find? `Nat.add | return
  IO.println s!"{info.type}"

几个重要性质：

  • de Bruijn index：bvar n 指向从内向外第 n 层的绑定器。fun x => fun y => x 中 x 表示为 bvar 1（跳过 y 那层）。这种表示让 α-等价的表达式具有相同的结构。
  • Expr 是共享的：Lean 内部对 Expr 做了 hash-consing，相同子表达式只存一份。因此比较两个 Expr 是否结构相等通常很快。
  • 元变量 mvar：证明过程中每个未关闭的目标对应一个 MVarId。tactic 的工作就是把 mvar 替换为具体的证明项。

MVarId 与证明状态

MVarId 是一个唯一标识符，指向一个"洞"——尚未填充的证明目标。每个 MVarId 关联以下信息：

1
2
3
4
5
6
structure MetavarDecl where
  userName  : Name           -- 显示名
  lctx      : LocalContext   -- 局部上下文（假设列表）
  type      : Expr           -- 目标类型
  kind      : MetavarKind    -- natural / synthetic / syntheticOpaque
  ...

InfoView 显示的目标状态（⊢ 行）就是某个 MVarId 对应的 type 字段，上方的假设来自 lctx。

观察 tactic 执行前后的目标变化：

1
2
3
4
5
6
7
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  -- 目标: ⊢ p ∧ q
  constructor
  -- 目标 1: ⊢ p
  -- 目标 2: ⊢ q
  · exact hp
  · exact hq

constructor 做的事情：取当前 MVarId（类型为 p ∧ q），创建两个新 MVarId（类型分别为 p 和 q），然后把原始 MVarId 赋值为 And.intro ?m1 ?m2。后续 exact hp 把 ?m1 赋值为 hp。

MetaM：元编程的基础 monad

MetaM 是 Lean 4 元编程的核心 monad，提供对证明状态的读写访问：

1
abbrev MetaM := ReaderT Meta.Context (StateRefT Meta.State CoreM)

MetaM 能做的事情：

  • 创建新的元变量：mkFreshExprMVar (type : Option Expr)
  • 赋值元变量：assignExprMVar (mvarId : MVarId) (val : Expr)
  • 查询元变量声明：getMVarDecl (mvarId : MVarId)
  • 类型推断：inferType (e : Expr)
  • 判断可归约相等：isDefEq (a b : Expr)
  • 规约表达式：whnf (e : Expr)（弱头范式）
  • 实例搜索：synthInstance (type : Expr)

一段 MetaM 代码示例——检查两个表达式是否 definitionally equal：

1
2
3
4
5
6
7
8
import Lean

open Lean Meta in
#eval show MetaM Unit from do
  let a := mkConst ``Nat.zero
  let b ← mkAppM ``Nat.add #[mkConst ``Nat.zero, mkConst ``Nat.zero]
  let eq ← isDefEq a b
  IO.println s!"0 =?= 0 + 0 : {eq}"  -- true

TacticM：tactic 的执行环境

TacticM 在 MetaM 之上加了目标列表管理：

1
abbrev TacticM := ReaderT Tactic.Context (StateRefT Tactic.State MetaM)

Tactic.State 维护一个 goals : List MVarId——当前所有待证目标。一个 tactic 的典型模式：

  1. 取出主目标：getMainGoal
  2. 对主目标做操作（分解、赋值、替换）
  3. 把产生的新目标放回列表：replaceMainGoal newGoals

以下是一个最小自定义 tactic 的完整实现——my_assumption 从局部上下文中搜索类型匹配的假设：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
import Lean
import Lean.Elab.Tactic

open Lean Meta Elab Tactic in
elab "my_assumption" : tactic => do
  let goal ← getMainGoal
  let goalType ← goal.getType
  let lctx ← getLCtx
  for decl in lctx do
    if decl.isImplementationDetail then continue
    if ← isDefEq decl.type goalType then
      goal.assign decl.toExpr
      return
  throwTacticEx `my_assumption goal "no matching hypothesis found"

example (n : Nat) (h : n = 0) : n = 0 := by
  my_assumption

执行过程：getMainGoal 拿到当前目标的 MVarId，goal.getType 读取目标类型（n = 0），遍历局部上下文寻找类型相同的假设，找到后用 goal.assign 将该假设填入目标位置。

Monad 栈的层次关系

完整的 monad 栈从底到顶：

1
2
3
IO → BaseIO → CoreM → MetaM → TermElabM → TacticM
                ↑         ↑         ↑           ↑
          环境/选项   元变量状态  elaboration  目标列表

每层 monad 通过 MonadLift 实例自动提升。在 TacticM 里可以直接调用 MetaM 的函数（如 inferType、isDefEq），无需手动 lift。

CoreM 提供对环境（Environment）的只读访问和对消息/诊断的写入。MetaM 在此之上加入元变量上下文和统一变量（universe level variables）。TermElabM 再加入 elaboration 专用的状态（pending tactics、saved states 等）。

构造 Expr 的常用工具

直接用 Expr 构造子写表达式极其繁琐。Lean 4 提供了一组辅助函数：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
open Lean Meta in
-- 构造全局常量
mkConst ``Nat.succ          -- Nat.succ : Nat → Nat

-- 构造应用
mkAppM ``Nat.add #[a, b]    -- Nat.add a b

-- 构造 λ 表达式
withLocalDecl `x BinderInfo.default (mkConst ``Nat) fun x => do
  let body ← mkAppM ``Nat.succ #[x]
  mkLambdaFVars #[x] body   -- fun x : Nat => Nat.succ x

-- 构造 ∀ 类型
forallTelescope type fun xs body => do
  -- xs 是绑定变量数组，body 是去掉所有 ∀ 后的核心类型
  ...

withLocalDecl 在局部上下文中临时引入一个自由变量，回调结束后自动清理。mkLambdaFVars 把自由变量重新抽象为绑定变量（转回 de Bruijn index）。这种"先引入自由变量操作，最后抽象回去"的模式贯穿整个元编程 API。

实战：读取目标并打印上下文

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
import Lean
import Lean.Elab.Tactic

open Lean Meta Elab Tactic in
elab "show_goal" : tactic => do
  let goal ← getMainGoal
  let decl ← goal.getDecl
  let lctx := decl.lctx
  IO.println s!"Goal type: {← ppExpr decl.type}"
  IO.println "Local context:"
  for d in lctx do
    unless d.isImplementationDetail do
      IO.println s!"  {d.userName} : {← ppExpr d.type}"

example (n m : Nat) (h : n < m) : n ≤ m := by
  show_goal
  -- 输出:
  -- Goal type: n ≤ m
  -- Local context:
  --   n : Nat
  --   m : Nat
  --   h : n < m
  exact Nat.le_of_lt h

ppExpr 把内部 Expr 格式化为可读字符串，用于调试输出。实际 tactic 不需要打印——直接对 Expr 做模式匹配和变换即可。

term-mode 对照

上面的 my_assumption tactic 等价于 term-mode 下直接写出假设名：

1
2
3
4
5
-- tactic-mode
example (n : Nat) (h : n = 0) : n = 0 := by my_assumption

-- term-mode
example (n : Nat) (h : n = 0) : n = 0 := h

term-mode 直接给出证明项；tactic-mode 通过操作元变量间接构造证明项。元编程 API 暴露的正是 tactic-mode 背后的机制——tactic 是"生成 term-mode 证明项的程序"。

公理检查

1
2
3
#print axioms my_assumption
-- 'my_assumption' does not depend on any axioms
-- (它是一个 tactic 声明，不引入公理)

自定义 tactic 本身不引入公理。使用该 tactic 证明的定理是否依赖公理，取决于 tactic 内部调用了什么（如 Decidable.decide 可能引入 Classical.choice）。

练习

练习 1（基础）：编写一个 tactic my_exact，接受一个 term 参数，将其 elaborate 后赋值给当前目标。提示：使用 elabTerm 将 Syntax 转为 Expr，然后用 closeMainGoal 或 goal.assign。

练习 2（进阶）：编写一个 tactic count_hyps，在 InfoView 中显示当前局部上下文的假设数量（不含 implementation detail）。使用 logInfo 输出消息到 InfoView。

练习 3（挑战）：编写一个 tactic apply_all，依次尝试对当前目标 apply 局部上下文中每一个类型匹配的假设。如果有一个成功就停止，全部失败则报错。提示：MVarId.apply 是底层 API，接受一个 Expr 并返回新目标列表。

参考资料