Lean 4 的 tactic 框架不是封闭的黑盒——整个 tactic 集合本身就是用 Lean 4 写成的，对用户完全开放扩展。syntax、macro、elab 三个关键字构成了这套元编程机制的核心，分别对应语法解析层、宏展开层、精化（elaboration）层。理解这三层的职责边界，就能在合适的抽象层次上定义自己的 tactic，而不是绕道求助 sorry 或重复编写机械的组合步骤。

本篇是"深入 Lean"系列第 08 篇。前置阅读：02 Term-mode 与 Tactic-mode 切换心法（tactic 基本操作），03 Universe 与类型层级实战（Sort/Type/Prop 区分）。

三层架构

Lean 4 的元编程体系在编译管线里分三层处理用户写下的语法片段：

1
2
3
4
5
6
7
用户源码
  ↓ 解析（parser）
语法树（Syntax）
  ↓ 宏展开（macro expansion）
展开后的语法树（Syntax）
  ↓ 精化（elaboration）
核心项（Expr）

解析层由 syntax 关键字负责，扩充 Lean 的文法，告诉解析器"这种写法合法，产生这种 Syntax 节点"。宏层由 macro / macro_rules 负责，把一种 Syntax 模式机械地变换为另一种 Syntax，不接触类型或证明状态。精化层由 elab / elab_rules 负责，接收 Syntax 并访问完整的精化上下文（当前目标、局部假设、元变量），产生核心 Expr。

选用哪一层的原则很直接：能在语法层解决的不下沉到宏层，能在宏层解决的不下沉到精化层。越深层能做的事越多，但实现也越复杂，且越难被其他宏组合。

syntax：扩充文法

syntax 声明一条新的产生式规则：

1
2
-- 在 `tactic` 语法类别里新增一种写法
syntax "trivial_nat" : tactic

执行这一行后，Lean 解析器就接受 trivial_nat 作为合法的 tactic 语法——但此时还没有语义，尝试使用它会报 elaboration function for 'trivial_nat' has not been implemented。

syntax 规则可以带参数。下面声明一个接受可选词项列表的 tactic：

1
2
-- 接受一个可选的 simp 引理列表
syntax "trivial_nat" ("[" term,* "]")? : tactic

语法类别 tactic 是 Lean 预定义的；常见类别还有 term（表达式）、command（顶层命令）、doElem（do 块元素）。定义自己的语法类别需要 declare_syntax_cat，这在构建嵌入式 DSL 时才需要用到。

macro：语法到语法的变换

macro 是给语法模式写一个展开规则，展开结果是另一段 Syntax：

1
2
-- 把 `trivial_nat` 直接展开为 `omega` 后接 `simp`
macro "trivial_nat" : tactic => `(tactic| first | omega | simp)

展开式用 `(…) 反引号语法构造新的 Syntax 节点。tactic| 前缀指定目标语法类别。

验证它能用：

1
2
example (n : Nat) : n + 0 = n := by trivial_nat
-- #check 上面这个目标：omega 处理 n + 0 = n

macro_rules 允许在同名宏下写多条模式匹配分支（类似 match）：

1
2
3
4
syntax "my_and_intro" : tactic

macro_rules
  | `(tactic| my_and_intro) => `(tactic| constructor)

带参数的宏展开：

1
2
3
4
-- 把 `rw_seq [h1, h2, h3]` 展开为依次 `rw [h1]; rw [h2]; rw [h3]`
macro "rw_seq" "[" hs:term,+ "]" : tactic => do
  let steps ← hs.getElems.mapM fun h => `(tactic| rw [$h])
  return Syntax.mkSepArray steps (mkAtom ";")

宏在展开时不能读取证明状态，只能进行语法模式匹配和重组。这意味着宏是卫生的（hygienic）——展开引入的局部名字不会意外捕获用户代码里的同名绑定，Lean 4 的宏系统内置了 hygienic 处理。

卫生宏与反卫生转义

默认的宏卫生性可防止名字冲突：

1
2
3
4
5
6
7
8
9
-- 下面的宏引入局部变量 x，不会捕获调用处的 x
macro "swap_pair" e:term : term => `(
  let x := ($e).1
  let y := ($e).2
  (y, x)
)

-- 即使调用处有一个 x，宏展开后的 x 也是独立的
def test (x : Nat × Nat) : Nat × Nat := swap_pair x

如果需要刻意插入一个能被外部访问的名字（反卫生），用 mkIdent：

1
2
3
4
open Lean in
macro "introduce_h" : tactic =>
  let h := mkIdent `h
  `(tactic| intro $h)

实际项目中很少需要反卫生转义；大多数 tactic DSL 都应保持卫生。

elab：访问证明状态

宏只能做语法变换；要读取当前目标、局部假设、或操作元变量，必须写 elab 规则。

最小 elab tactic

1
2
3
4
5
6
7
import Lean

open Lean Elab Tactic in
elab "show_goal" : tactic => do
  let goal ← getMainGoal
  let goalType ← goal.getType
  logInfo m!"当前目标类型: {goalType}"

调用时：

1
2
3
4
example (n : Nat) : n + 1 > n := by
  show_goal
  -- InfoView 消息面板输出：当前目标类型: n + 1 > n
  omega

getMainGoal 返回当前的主目标（一个 MVarId）；goal.getType 返回其类型（一个 Expr）；logInfo 把消息输出到 InfoView。

访问局部上下文

1
2
3
4
5
6
open Lean Elab Tactic Meta in
elab "list_hyps" : tactic => do
  let ctx ← getLCtx
  for decl in ctx do
    if !decl.isAuxDecl then
      logInfo m!"假设 {decl.userName} : {← ppExpr decl.type}"

getLCtx 返回当前局部上下文（LocalContext），遍历其中每个非辅助声明可以列出所有假设：

1
2
3
4
5
6
7
example (a b : Nat) (h : a + b = 10) : b + a = 10 := by
  list_hyps
  -- InfoView 输出：
  -- 假设 a : Nat
  -- 假设 b : Nat
  -- 假设 h : a + b = 10
  linarith

调用其他 tactic

elab 内部可以调用已有的 tactic，把它们组合成新的策略：

1
2
3
4
5
6
7
8
9
open Lean Elab Tactic in
elab "try_omega_then_simp" : tactic => do
  let goal ← getMainGoal
  let goalType ← goal.getType
  -- 尝试 omega，失败则回退到 simp
  try
    evalTactic (← `(tactic| omega))
  catch _ =>
    evalTactic (← `(tactic| simp))

evalTactic 接受一个 Syntax 值并在当前 tactic 状态上执行它。

逐步构建 trivial_nat tactic

目标

trivial_nat 应当自动解决关于 Nat 的简单算术目标：先尝试 omega（线性算术），再尝试 simp only [Nat.add_comm, Nat.mul_comm]（基于等式的化简），两者都失败时报出有用的错误信息。

第一步：声明语法

1
2
3
4
5
-- TrivialNat.lean
import Lean
import Mathlib.Tactic  -- 或 import Std

syntax "trivial_nat" : tactic

第二步：实现 elab 规则

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
open Lean Elab Tactic in
elab_rules : tactic
  | `(tactic| trivial_nat) => do
    let goal ← getMainGoal
    let goalType ← inferType (mkMVar goal)
    -- 只对 Prop 目标操作（排除非命题目标）
    if !(← isProp goalType) then
      throwTacticEx `trivial_nat goal
        m!"trivial_nat 只处理命题目标，当前目标不是 Prop: {goalType}"
    -- 尝试 omega
    try
      evalTactic (← `(tactic| omega))
      return
    catch _ => pure ()
    -- 尝试 simp with nat lemmas
    try
      evalTactic (← `(tactic| simp only [Nat.add_comm, Nat.add_assoc,
                                         Nat.mul_comm, Nat.zero_add,
                                         Nat.add_zero]))
      return
    catch _ => pure ()
    -- 两者都失败，给出诊断信息
    throwTacticEx `trivial_nat goal
      m!"trivial_nat 无法自动证明此目标，请手动处理: {goalType}"

第三步：测试

1
2
3
4
5
6
7
8
9
10
11
12
-- 测试 omega 路径
example (n : Nat) : n + 1 > n := by trivial_nat

-- 测试 simp 路径
example (n m : Nat) : n + m = m + n := by trivial_nat

-- 测试 0 + n = n
example (n : Nat) : 0 + n = n := by trivial_nat

-- 测试失败路径给出诊断（故意写一个 trivial_nat 无法证明的目标）
-- example (n : Nat) : n * n = n := by trivial_nat
-- 输出: trivial_nat 无法自动证明此目标，请手动处理: n * n = n

term-mode 对照

同样的证明在 term mode 下需要显式写出引理名：

1
2
3
4
5
6
-- term mode：手动引用引理
theorem add_comm_term (n m : Nat) : n + m = m + n :=
  Nat.add_comm n m

-- tactic mode with trivial_nat
theorem add_comm_tac (n m : Nat) : n + m = m + n := by trivial_nat

term mode 写法在有明确引理名时很清晰，但对于需要组合多步推理的算术目标，tactic 的迭代式目标缩减更合适。trivial_nat 把"先 omega 后 simp"这个组合策略封装为一个原子操作，减少重复代码。

InfoView 在调用 trivial_nat 之前的目标状态：

1
⊢ n + m = m + n

trivial_nat 调用 omega 失败（加法交换律不是线性算术定理），转而调用 simp only [Nat.add_comm, ...]，目标消失，InfoView 显示 No goals。

syntax 类别扩展

在更复杂的场景中，一个 tactic 的参数本身是另一种子语言。declare_syntax_cat 可以定义新的语法类别：

1
2
3
4
5
6
7
8
9
-- 定义一个"nat 算术提示"的语法类别
declare_syntax_cat natHint

syntax num        : natHint  -- 一个数字字面量
syntax ident      : natHint  -- 一个变量名
syntax natHint "+" natHint : natHint  -- 加法

-- 在 tactic 中使用这个新类别
syntax "nat_witness" natHint : tactic

这种模式出现在 Mathlib 的 norm_num 扩展框架里——norm_num 本身是一个可扩展的 tactic，第三方可以用 norm_num extension 机制为新的数字类型注册求值规则，而不必修改 norm_num 本身的代码。

Mathlib 中的实例

Mathlib 的大量 tactic 基于同样的三层机制构建：

ring tactic 的实现：ring 在 Mathlib.Tactic.Ring 中通过 elab 访问当前目标，把目标类型表示为多项式环上的等式，然后调用多项式规范化算法验证两边是否等价。它的语法只是 "ring" : tactic，整个验证逻辑都在 elab 函数里。

decide tactic：对可判定命题（Decidable 实例存在），decide 直接在编译期运行类型检查，对应一个极短的 elab 实现——本质上就是生成一个 of_decide_eq_true rfl 的 term。

omega：处理线性整数/自然数算术，也是一个纯 elab tactic。内部调用 Omega 定理证明器，把目标和假设翻译为不等式系统，求解后生成证明项。

simp 的扩展性通过 @[simp] 属性实现——这个属性把一个等式定理注册进全局 simp 引理集，下次调用 simp 时自动使用。这是属性（attribute）机制，与 macro/elab 并列为 Lean 4 元编程的第四类工具，但这里不展开。

1
2
3
-- 验证 trivial_nat 不依赖额外公理
#print axioms add_comm_tac
-- 输出: 'add_comm_tac' does not depend on any axioms

错误处理与诊断

自定义 tactic 的用户体验在很大程度上取决于错误信息的质量。Lean 4 提供两种报错机制：

throwTacticEx 把错误关联到特定目标，InfoView 会在报错的同时展示未完成的目标状态，方便用户理解卡在哪里：

1
throwTacticEx `my_tactic goal m!"无法处理类型 {goalType}，期望 Nat 相关命题"

throwError 只抛出消息，不关联目标：

1
throwError "参数数量不对，期望 2 个，得到 {args.size} 个"

对于复杂 tactic，建议在 catch 分支里同时保留原始异常信息：

1
2
3
4
5
try
  evalTactic (← `(tactic| omega))
catch e =>
  throwTacticEx `trivial_nat goal
    m!"omega 失败（{e.toMessageData}），已尝试 simp 路径"

练习

练习 1

实现一个 cases_or tactic，等价于对目标上下文中第一个 _ ∨ _ 类型的假设自动执行 cases。elab 实现需要遍历局部上下文，找到第一个 Or-headed 假设，然后调用 evalTactic (← \(tactic| cases $hyp))`。

提示：用 getLCtx 遍历，Expr.isAppOf 或模式匹配 Expr.app 判断是否是 Or 应用。

练习 2

用 macro 实现 rw_all [h]，等价于 rw [h] at *。验证以下用例能通过：

1
2
3
example (a b : Nat) (h : a = b) (h2 : a + 1 = 5) : b + 1 = 5 := by
  rw_all [h]
  exact h2

练习 3

修改本篇的 trivial_nat，使其接受一个可选的 simp 引理列表，例如 trivial_nat [my_lemma1, my_lemma2]，在 simp 阶段把用户提供的引理追加进去。语法声明：

1
syntax "trivial_nat" ("[" term,* "]")? : tactic

elab_rules 里用 Syntax.getArgs 或模式匹配提取可选部分，构造 simp only [...] 调用。

参考资料