第 14 篇展示了 tactic 如何操作 MVarId 和 Expr。本篇向上走一层：elab 不仅能定义 tactic，还能定义 term elaborator 和顶层 command。三者共享同一套 Expr 构造工具，但触发时机和返回值语义不同。

elab 的三种角色

elab 关键字根据后缀决定 elaborator 类别：

1
2
3
elab "my_tactic"   : tactic  => ...   -- 操作目标列表，无返回值
elab "my_term"     : term    => ...   -- 返回一个 Expr（证明项或值）
elab "my_command"  : command => ...   -- 顶层副作用，无返回值

三者的 monad 环境：

类别 Monad 核心职责
tactic TacticM 消费/产生 MVarId
term TermElabM 返回 Expr，可能带约束
command CommandElabM 修改环境、输出消息

自定义 term elaborator

一个 term elaborator 需要把语法片段转为 Expr。最简单的例子——一个总是返回 42 : Nat 的 term：

1
2
3
4
5
6
7
8
import Lean

open Lean Elab Term in
elab "forty_two" : term => do
  return mkNatLit 42

#check forty_two        -- forty_two : Nat
#eval forty_two         -- 42

带参数的 term elaborator 需要先定义语法：

1
2
3
4
5
6
7
8
9
10
11
12
import Lean

open Lean Elab Term Meta in

syntax "double(" term ")" : term

elab_rules : term
  | `(double($t)) => do
    let e ← elabTerm t (some (mkConst ``Nat))
    mkAppM ``Nat.add #[e, e]

#eval double(21)    -- 42

elabTerm 把语法 t elaborate 成 Expr，第二个参数是期望类型（用于类型推断指导）。mkAppM 构造 Nat.add e e。

期望类型的传播

term elaborator 通过第二个隐式参数 expectedType? : Option Expr 接收上下文提供的类型约束：

1
2
3
4
5
6
7
8
9
10
11
12
open Lean Elab Term Meta in
elab "typed_zero" : term => do
  let some expectedType ← getExpectedType?
    | throwError "typed_zero requires an expected type"
  -- 检查期望类型是否是 Nat
  if ← isDefEq expectedType (mkConst ``Nat) then
    return mkNatLit 0
  else
    throwError "typed_zero only works for Nat"

def x : Nat := typed_zero    -- 成功，x = 0
-- def y : Int := typed_zero  -- 报错：typed_zero only works for Nat

getExpectedType? 读取调用处的期望类型。这个机制让自定义语法能参与 Lean 的双向类型推断。

自定义 command

command 在顶层执行，可以向环境添加声明、输出信息、修改属性：

1
2
3
4
5
6
7
8
9
10
11
12
import Lean

open Lean Elab Command Meta in
elab "#show_type " id:ident : command => do
  let name ← resolveGlobalConstNoOverload id
  let env ← getEnv
  let some info := env.find? name
    | throwError s!"unknown constant '{name}'"
  logInfo m!"{name} : {info.type}"

#show_type Nat.add
-- Nat.add : Nat → Nat → Nat

resolveGlobalConstNoOverload 把标识符解析为全局名称。env.find? 从环境中查找常量信息。logInfo 把消息输出到 InfoView。

一个更实际的 command——批量检查公理依赖：

1
2
3
4
5
6
7
8
9
10
11
12
import Lean

open Lean Elab Command in
elab "#check_axioms " ids:ident* : command => do
  for id in ids do
    let name ← resolveGlobalConstNoOverload id
    let env ← getEnv
    let axioms := Lean.collectAxioms env name
    if axioms.isEmpty then
      logInfo m!"{name}: axiom-free"
    else
      logWarning m!"{name} depends on: {axioms.toList}"

syntax 与 macro：语法糖层

elab 直接把语法绑定到 elaboration 逻辑。如果只是做语法变换（不需要访问 MetaM），macro 更轻量：

1
2
3
4
5
-- macro 只做语法到语法的变换
macro "assert_eq " a:term " " b:term : command =>
  `(command| #check (show $a = $b from rfl))

assert_eq 2 + 2  4    -- 通过，因为 2+2 和 4 definitionally equal

macro 在 parse 阶段展开，不进入 MetaM。elab 在 elaboration 阶段执行，能访问类型信息和环境。选择依据：能用 macro 解决的用 macro，需要类型信息时用 elab。

三件套的关系：

1
2
3
syntax  → 定义新的语法形式（parser 规则）
macro   → 把新语法展开为已有语法（纯语法变换）
elab    → 把新语法直接 elaborate 为 Expr（需要语义信息）

读取和修改环境

CommandElabM 和 TermElabM 都能通过 getEnv / modifyEnv 读写环境：

1
2
3
4
5
6
7
open Lean Elab Command in
elab "#count_defs" : command => do
  let env ← getEnv
  let mut count := 0
  for (_, info) in env.constants.map₁.toList do
    if info.isDefn then count := count + 1
  logInfo m!"Environment contains {count} definitions"

向环境添加新定义需要构造 Declaration 并调用 addDecl：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
open Lean Elab Command Meta in
elab "#add_const " name:ident " := " val:term : command => do
  let nameN := name.getId
  let expr ← runTermElabM fun _ => do
    let e ← Term.elabTerm val none
    Term.synthesizeSyntheticMVarsNoPostponing
    let e ← instantiateMVars e
    return e
  let type ← runTermElabM fun _ => Meta.inferType expr
  let decl := Declaration.defnDecl {
    name := nameN
    levelParams := []
    type := type
    value := expr
    hints := .regular 0
    safety := .safe
  }
  let env ← getEnv
  match env.addDecl {} decl with
  | .ok env' => modifyEnv fun _ => env'
  | .error e => throwError m!"addDecl failed: {e.toMessageData {}}"

#add_const myFive := 5
#check myFive    -- myFive : Nat
#eval myFive     -- 5

runTermElabM 在 command 上下文中执行 term elaboration。instantiateMVars 确保所有元变量已被赋值。Declaration.defnDecl 包装为定义声明，env.addDecl 进行内核类型检查并注册到环境。

属性注册

Lean 4 的属性系统（@[simp]、@[ext]、@[aesop] 等）也可以通过元编程操作：

1
2
3
4
5
6
7
8
9
open Lean in
-- 注册 simp 属性
addSimpTheorem simpExtension name isGlobal attrKind prio

-- 自定义属性的典型模式
initialize myAttr : TagAttribute ←
  registerTagAttribute `myTag "A custom tag attribute" fun name => do
    -- 当 @[myTag] 被添加到某个声明时执行的回调
    return ()

registerTagAttribute 注册一个无参属性。registerParametricAttribute 可以注册带参数的属性（如 @[simp] 的优先级参数）。

term-mode 与 tactic-mode 的等价性

自定义 term elaborator 返回的 Expr 和 tactic 操作 MVarId 最终产生的 Expr 是同一种东西。两种方式可以互嵌：

1
2
3
4
5
6
7
-- 在 term 位置使用 tactic
def x : Nat := by exact 42

-- 在 tactic 位置使用 term elaboration
example : 1 + 1 = 2 := by
  show 1 + 1 = 2    -- show 本质上 elaborate 一个 term 作为目标类型
  rfl

自定义 term elaborator 中可以创建元变量并让用户用 tactic 填充：

1
2
3
4
5
6
open Lean Elab Term Meta in
elab "prove_it " t:term : term => do
  let type ← elabType t
  let mvar ← mkFreshExprMVar type
  -- 这个元变量会变成一个 tactic 目标
  return mvar

练习

练习 1（基础）：编写一个 term elaborator nat_of_string("...")，接受一个字符串字面量，解析为自然数并返回对应的 Expr。例如 nat_of_string("123") 应该 elaborate 为 123 : Nat。提示：String.toNat? 做解析，mkNatLit 构造字面量。

练习 2（进阶）：编写一个 command #list_simp_lemmas，打印当前环境中所有注册为 @[simp] 的引理名称（前 20 个即可）。提示：Lean.Meta.getSimpTheorems 获取 simp 集合。

练习 3（挑战）：编写一个 command #mirror，接受一个已有定义的名称，在环境中创建一个同类型同值的新定义（名称加 _mirror 后缀）。例如 #mirror Nat.zero 应创建 Nat.zero_mirror : Nat := Nat.zero。验证：#check Nat.zero_mirror 应通过。

参考资料