2. Lean 策略编程入门
本教程面向已经掌握 Lean 定理证明基础、也有一点编程经验，并想亲手实现自定义策略的读者。最好在 VS Code 中打开本章源文件，直接观察 Lean 的反应。读完后，你应当能把握 Lean 元编程的全貌，并写出一些简单策略。
2.1. 策略就是程序
原则上，策略就是操作证明状态的任意程序。程序可以直接写在策略证明里。下面的程序除了记录 Hello world! 什么也不做；把光标移到带蓝色下划线的 run_tac，信息视图会显示消息。暂时不用深究 Lean.logInfo 的类型，把它当作记录或打印函数即可。
〔可运行〕
namespace MetaProgrammingTutorial
example : True := ⊢ True
⊢ True
All goals completed! 🐙
要会写策略，需要回答五个问题：
-
命令式程序在 Lean 中怎样工作；
-
证明状态究竟是什么；
-
Lean 元编程围绕哪些基本数据结构展开；
-
怎样用 API 修改证明状态；
-
怎样声明新策略的语法。
2.2. 一、Lean 中的命令式程序
Lean 是纯函数式语言。与 C、Python 等命令式语言相比，它的定义不可改变，函数只依赖参数，不能自行产生副作用。不过，Haskell 等函数式语言发展出了以命令式风格编程的办法：理论基础是单子，而 do 记法替用户遮住了大部分单子细节。
这里不展开单子理论，只把单子粗略看作一种命令式程序。不同单子能访问的状态不同：
-
Lean.Elab.Tactic.TacticM是顶层策略单子，能访问证明状态的全部数据； -
Lean.Meta.MetaM只能访问元变量相关信息，暂时不必深究。这些信息只是完整证明状态的一部分，所以TacticM能调用MetaM，反向调用却不行，除非为TacticM补齐它所需的额外上下文和状态。
下面只演示 Lean 的命令式编程能力，尚未使用读取证明状态的 API。
2.2.1. do、返回值与可变局部变量
〔可运行〕
-- 参数 单子类型 返回值
-- v v v
def myCode1 (n : Nat) : Lean.Meta.MetaM Nat := do
if n = 0 then -- 在 do 记法中，这里可以省略 else
return 42
let k := n^2 -- 用 := 绑定一个值
Lean.logInfo m!"{n} -> {k}"
return k
-- 参数 单子类型 无返回值，类似 C 的 void
-- v v v
def myCode2 (n : Nat) : Lean.Elab.Tactic.TacticM Unit := do
Lean.logInfo m!"Calling myCode2 {n}"
-- Array 与 List 基本相同，但底层实现不同，可类比 C++ vector。
def myCode3 : Lean.Elab.Tactic.TacticM (Array Nat) := do
Lean.logInfo "Calling myCode3"
myCode2 7
-- Lean 变量不可变，但 do 记法允许用 let mut 获得命令式写法。
let mut a : Array Nat := #[] -- #[] 表示空 Array，而不是空 List
for i in [:5] do -- [:5]（即 [0:5]）依次遍历 0、1、2、3、4，使用 Std.Range
let res ← myCode1 i -- 用 ← 取得单子程序执行所得的值
a := a.push res -- 不带 let 的赋值只允许用于可变变量
-- 因为这里立刻以 a.push res 替换 a，Lean 的内部优化不会复制数组。
-- 给命令式程序员的提醒：单写 a.push res 不会工作；外部函数不能改变 a。
-- Lean 毕竟仍是纯函数式语言。
Lean.logInfo m!"got: {res}"
myCode2 15
return a
看看 Lean 打出的内容，确认每一条消息来自哪里。← someTactic 还可以直接嵌进表达式中执行单子程序。
〔可运行〕
example : True := ⊢ True
⊢ True
All goals completed! 🐙
这远非命令式编程的全部。后续主题还包括：单子的理论及自定义单子；Std.HashMap、foldM、IO 单子等偏编程的数据结构与函数；throwError、panic! 等不同异常；以及用 partial 绕过 Lean 的终止性检查等。
2.3. 二、证明状态是什么
在核心层面，证明是见证命题为真的项，称为证明项。证明定理时，我们随时都握有一个带孔洞的、不完整的证明项；孔洞就是元变量。大多数策略步骤会用一个子项填入一个孔洞，形式上说就是给一个元变量赋值；这个子项还可能包含新的元变量。
所有元变量都获赋值，也就是所有孔洞都填好、所有目标都关闭时，证明才完成。元变量的名字前带问号。下面证明 p → p ∧ True，并在每一步后写出当时的部分证明项。
〔可运行〕
theorem p_imp_p_true (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
-- p_imp_p_true : p → p ∧ True := ?_
p:Proph:p⊢ p ∧ True
-- p_imp_p_true : p → p ∧ True := (fun h => ?_)
p:Proph:p⊢ pp:Proph:p⊢ True
-- p_imp_p_true : p → p ∧ True := (fun h => And.intro ?left ?right)
p:Proph:p⊢ True
-- p_imp_p_true : p → p ∧ True := (fun h => And.intro h ?right)
All goals completed! 🐙
-- p_imp_p_true : p → p ∧ True := (fun h => And.intro h True.intro)
2.4. 三、元编程的基本数据结构
核心对象包括：表达式 Lean.Expr 与构造表达式的 Qq；表达式中的 Lean.Name、Lean.MVarId、Lean.FVarId；以及打印所用的 String、Format、MessageData。
2.4.1. 表达式与 Qq
Lean.Expr 表示 Lean 表达式。由于依赖类型论的性质，类型、项和证明都编码成 Lean.Expr；Lean 内核检查证明时检查的也正是它。在编辑器中按 Ctrl 并点击下面的名字，可以看库中的定义。
〔可运行〕
#check Lean.Expr
-- Qq 提供便捷记法，用来构造 Lean.Expr。
open Qq
-- Q(...) 是表达式的类型标注，q(...) 是表达式。
def t1 : Q(Prop) := q(True)
def t2 : Q(Prop) := q(∀ p : Prop, p → p ∧ True)
-- 直接写表达式可行，但比较费力。
#eval t1
#eval t2
Q(...) 的表面类型不是 Lean.Expr，但两者定义等价。Qq 也不会强制类型标注正确：可把它类比为 Python 的类型标注，能捕捉基本错误，却不是强制保证。
〔可运行〕
def t1e : Lean.Expr := t1
def t1x : Q(Nat) := t1
#check t1e
#check t1x
2.4.2. 名字与变量标识
元编程 API 基本都在 Lean 命名空间里，反复写前缀很烦，因此先打开它。Lean.Name 是另一个重要类型。单反引号写任意名字，双反引号写在当前上下文中解析过的名字。
〔可运行〕
open Lean
def n1 : Name := `Nat.blah -- 单反引号：任意名字
def n2 : Name := ``t1e -- 双反引号：在当前上下文中解析名字
#print n1
#print n2
-- Expr 对变量的处理乍看有些杂乱。
#check Expr.bvar -- 在该 Expr 内部绑定或量化的变量，以索引表示
#check Expr.fvar -- 上下文中有名字的自由变量
#check Expr.mvar -- 元变量
#check Expr.const -- 已定义的常量
#check FVarId -- 自由变量的唯一标识
#check MVarId -- 元变量的唯一标识
自由变量和元变量面向用户的名字并不是唯一标识，因为 Lean 允许多个变量同名。因此自由变量由 FVarId 标识，元变量由 MVarId 标识。这些数据类型内部也藏着名字，但 _uniq.13541 一类内部名绝不应该暴露给用户。
2.4.3. 显示与打印
基础打印函数 logInfo 比一般语言的打印函数精细。它接收的不是 String，而是 Lean.MessageData，所以显示的项支持悬停查看类型，也支持 Ctrl+点击跳转到定义。Format 则是附带良好换行信息的字符串表示。
〔可运行〕
#check MessageData -- 交互式表达式
#check String -- 标准字符列表
#check Format -- 附有换行排版信息的字符串
example : True := ⊢ True
⊢ True
All goals completed! 🐙
2.5. 四、实现四个基本策略
我们将重写下列证明使用的 intro、constructor、assumption 和 trivial。常用类型和函数藏在 Lean、Lean.Meta、Lean.Elab.Tactic 命名空间中，一并打开。
〔可运行〕
#check p_imp_p_true
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True; p:Proph:p⊢ pp:Proph:p⊢ True; p:Proph:p⊢ True; All goals completed! 🐙
open Lean Meta Elab.Tactic Qq
2.5.1. trivial：从不安全赋值开始
最容易替换的是 trivial。先取得表示当前目标的元变量，再把它赋值为 True.intro。
〔可运行〕
def runTrivial0 : TacticM Unit := do
let goal : MVarId ← getMainGoal -- 取得表示当前目标的元变量
goal.assign q(True.intro) -- 第一次尝试并不理想
-- 最好避免低层 MVarId.assign，原因马上就会看到。
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True; p:Proph:p⊢ pp:Proph:p⊢ True; p:Proph:p⊢ True
All goals completed! 🐙
-- 目标已关闭。
MVarId.assign 不做类型检查，所以这次赋值并不安全。若拿 runTrivial0 同时关闭 ?left : p 和 ?right : True，它会痛快地接受两个赋值。直到最后内核检查完整证明项时，才报一个难懂的错误：@And.intro p True 的第一个证明应当属于 p，却收到了 True.intro。
〔故意错误〕 以下是原教程要求读者亲眼观察的第一个错误；以注释隔离，避免破坏整章构建。
-- example (p : Prop) : p → p ∧ True := by -- 故意错误
-- intro h; constructor
-- run_tac runTrivial0
-- run_tac runTrivial0
#check True -- 隔离块的可构建哨兵
这种错误很难解读，因此应只在赋值类型正确时才给元变量赋值。Batteries 提供了检查能否赋值的函数；可 Ctrl+点击查看实现。
〔可运行〕
#check MVarId.assignIfDefEq
def runTrivial1 : TacticM Unit := do
let goal : MVarId ← getMainGoal
goal.assignIfDefEq q(True.intro)
现在对错误目标调用 runTrivial1，错误会在正确的位置出现。
〔故意错误〕 第二个错误同样以注释展示。
-- example (p : Prop) : p → p ∧ True := by
-- intro h; constructor
-- run_tac runTrivial1 -- 错误现在出现在该出现的位置
-- run_tac runTrivial1
#check True -- 隔离块的可构建哨兵
不过，只有一句 failed 并不实用。可以用 try ... catch _ => ... 捕获错误，再用 throwError 给出更有用的诊断。这里也修正上游文字中的函数名笔误：诊断应说 runTrivial，不是 runTrivial1。
〔可运行〕
def runTrivial : TacticM Unit := do
let goal : MVarId ← getMainGoal
try
goal.assignIfDefEq q(True.intro)
catch _ =>
let goalType ← goal.getType
throwError "tactic runTrivial failed, the goal has type `{goalType}` instead of `True`"
〔故意错误〕 第三个错误展示改进后的诊断；诊断字符串保持不译，以便与 Lean 输出逐字对照。
-- example (p : Prop) : p → p ∧ True := by
-- intro h; constructor
-- run_tac runTrivial -- 此处得到有用的错误消息
-- run_tac runTrivial
#check True -- 隔离块的可构建哨兵
2.5.2. assumption：遍历局部上下文
实现 assumption 要遍历所有假设，逐个试用。信息视图中 ⊢ 上方的假设列表叫局部上下文。一般说来，每个元变量，也就是每个目标，都有自己的局部上下文；这里可用 withMainContext 把当前主目标的局部上下文放进单子上下文，再以 getLCtx 取得它。
〔可运行〕
example (n : Nat) (hn : n > 5) : True := n:Nathn:n > 5⊢ True
n:Nathn:n > 5⊢ True
All goals completed! 🐙
def runAssumption : TacticM Unit :=
withMainContext do -- 这里必须有 do，函数开头则可以没有
let goal ← getMainGoal
let ctx ← getLCtx
for (decl : LocalDecl) in ctx do
if decl.kind != .default then continue
try
goal.assignIfDefEq (Expr.fvar decl.fvarId)
return -- 成功便结束
catch _ =>
pure () -- 忽略该异常，继续尝试
throwError "Assumption not found"
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True; p:Proph:p⊢ pp:Proph:p⊢ True
p:Proph:p⊢ True
All goals completed! 🐙
2.5.3. constructor：建立新元变量
余下两个策略需要创建元变量。通用入口如下。
〔可运行〕
#check mkFreshExprMVar
#check mkFreshExprSyntheticOpaqueMVar
通常应把目标元变量设为 syntheticOpaque，让 Lean 知道它们较重要，不要随意赋值。mkFreshExprSyntheticOpaqueMVar 就这样做；Ctrl+点击会看到，它只是以特定 kind 调用 mkFreshExprMVar。
这里只实现处理 And 目标的教学版 constructor，不尝试覆盖一般归纳类型。先写两个函数，从主目标的类型 A ∧ B 中抽出类型表达式 A 与 B。Qq 版本给 tgt 加 Q(...) 标注时必须用 have，不能用 let；~q(...) 模式只能在 MetaM 或更强的单子中匹配。
〔可运行〕
def extractAndGoals1 : TacticM (Expr × Expr) := do
let tgt ← getMainTarget -- 等价于 (← getMainGoal).getType
have quotedTgt : Q(Prop) := tgt
match quotedTgt with
| ~q($p ∧ $q) => return (p, q)
| _ => throwError "Goal {tgt} is not of the form (?_ ∧ ?_)"
-- 不用 Qq 也能手工完成。
def extractAndGoals2 : TacticM (Expr × Expr) := do
let tgt ← getMainTarget
let (`And, #[p, q]) := tgt.getAppFnArgs
| throwError "Goal {tgt} is not of the form (?_ ∧ ?_)"
return (p, q)
-- 非 Qq 版本要求项的形状匹配得更精确；匹配前有时需要下面两步。
#check instantiateMVars
#check whnf
深入这两个函数超出本教程范围。先检查两种 And 分解是否都工作。这里修正上游的日志笔误：第二条必须打印 a2、b2，而不是再次打印 a1、b1。
〔可运行〕
example (p q : Prop) (h : p ∧ q) : p ∧ q := p:Propq:Proph:p ∧ q⊢ p ∧ q
p:Propq:Proph:p ∧ q⊢ p ∧ q
All goals completed! 🐙
runConstructor 要把主目标 ?_ : A ∧ B 替换成 And.intro (?left : A) (?right : B)。新元变量的局部上下文来自单子上下文，因此需要 withMainContext。目标赋值后，活动目标列表不会自动维护，还必须用 replaceMainGoal 明确登记两个新目标。
〔可运行〕
/-- 把主目标 `?_ : A ∧ B` 替换为两个子目标。 -/
def runConstructor : TacticM Unit := do
withMainContext do -- 可试着注释掉本行，观察哪里损坏
let goal ← getMainGoal
let ((a : Q(Prop)), (b : Q(Prop))) ← extractAndGoals1
let left : Q($a) ← mkFreshExprSyntheticOpaqueMVar a (tag := `left)
let right : Q($b) ← mkFreshExprSyntheticOpaqueMVar b (tag := `right)
goal.assign q(And.intro $left $right) -- 此处敢直接用 assign 吗？
replaceMainGoal [left.mvarId!, right.mvarId!]
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True
p:Proph:p⊢ pp:Proph:p⊢ True
p:Proph:p⊢ True
All goals completed! 🐙
2.5.4. intro：操作局部上下文
intro 的实现藏着最多细节；第一次没有完全看懂也不必担心。它读取目标的 forallE 结构，分配自由变量标识，把新声明放入局部上下文，把函数体里的绑定变量实例化成自由变量，然后在新上下文中创建目标，最后以 lambda 项给旧目标赋值。
〔可运行〕
def runIntro (name : Name) : TacticM Unit :=
withMainContext do
let goal ← getMainGoal
let lctx ← getLCtx
let .forallE _ type body c ← goal.getType
| throwError "Goal not of the form `_ → _` or `∀ _, _`"
let fvarId : FVarId ← mkFreshFVarId -- 分配新自由变量
let lctx' := lctx.mkLocalDecl fvarId name type c -- 放进新上下文
let fvar : Expr := .fvar fvarId
let body := body.instantiate1 fvar -- 把 bvar 转成 fvar
withLCtx' lctx' do
-- 新元变量的局部上下文由单子上下文决定。
let newMVar ← mkFreshExprSyntheticOpaqueMVar body
let newVal ← mkLambdaFVars #[fvar] newMVar
goal.assign newVal
replaceMainGoal [newMVar.mvarId!]
-- Lean 已实现 intro，因此也有捷径。
def runIntro2 (name : Name) : TacticM Unit := do
let goal ← getMainGoal
let (_, m) ← goal.intro name
replaceMainGoal [m]
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True
p:Proph:p⊢ pp:Proph:p⊢ True
p:Proph:p⊢ True
All goals completed! 🐙
2.5.5. 自定义 have
前面的策略都围绕目标工作。下面展示怎样向局部上下文加入一个新 have。代码寻找 hab 与 ha 对应的自由变量，构造项 hab ha，推断其类型 b，再用 assert 与 intro 把 hb : b 放入上下文。这里修正上游注释笔误：t = "b" 时，e 是 hab ha，不是 hab hb。
〔可运行〕
example (a b : Prop) (ha : a) (hab : a → b) : b := a:Propb:Propha:ahab:a → b⊢ b
a:Propb:Propha:ahab:a → bhb:b⊢ b
All goals completed! 🐙
2.6. 五、声明新策略语法
前面讨论了策略内部如何工作，调用策略的语法同样重要。处理语法时使用 Lean.Syntax 与 Lean.TSyntax；Lean.Syntax 的实现相当杂乱，无须现在深究。
〔可运行〕
#check Lean.Syntax
#check Lean.TSyntax
正如 Q(...) 是带标注的 Expr，TSyntax .. 是带标注的 Syntax。这里的标注叫语法类别，本质只是一个 Name。常用类别包括：表示任意类型 Lean 表达式的 term、表示策略的 tactic、表示自然数文字的 num、表示名字或标识符文字的 ident。较次要的例子有表示顶层命令（如 def、#eval）的 command，以及表示 do 记法中命令的 doElem。
2.6.1. 构造语法与宏
可以用 `(kind| syntax) 引用构造 Syntax。这只能在类似 MetaM 的单子中工作；准确地说，要求位于 CoreM 之上。
〔可运行〕
def s1 : MetaM (TSyntax `tactic) := `(tactic| apply And.intro)
def s2 : MetaM (TSyntax `term) := `(1+2+3) -- 等价于 `(term| 1+2+3)
-- 生成的 Syntax 看起来很杂乱，但所需数据确实都在其中。
#eval s1
#eval s2
宏是在精译语法时运行的语法变换规则。下面两个宏只处理 And 与 True。把光标悬停在宏名上，还能看到文档字符串。
〔可运行〕
/-- `constructor` 的简化版，只适用于 `And` 目标。 -/
macro "my_constructor" : tactic => `(tactic| apply And.intro)
/-- 关闭 `True` 目标。 -/
macro "my_trivial" : tactic => `(tactic| exact True.intro)
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True; p:Proph:p⊢ pp:Proph:p⊢ True; p:Proph:p⊢ True; All goals completed! 🐙
2.6.2. 用 elab 连接语法与程序
intro 与 assumption 可用 elab 命令把单子程序接到相应语法上。定义语法的语法本身对空白很敏感：下面的 a:ident 中，a 与冒号之间不能加空格；前面的 `(tactic| 也最好保持这种紧凑写法。
〔可运行〕
/-- 自定义 `intro`。 -/
elab "my_intro" a:ident : tactic => do
-- a 的类型是 ``TSyntax `ident``，即标识符语法类别。
let aName : Name := a.getId
runIntro aName
/-- 自定义 `assumption`。 -/
elab "my_assumption" : tactic => do
runAssumption
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True; p:Proph:p⊢ pp:Proph:p⊢ True; p:Proph:p⊢ True; All goals completed! 🐙
还可以从其他语法类别中提取参数：str 用 getString 转为 String，num 用 getNat 转为 Nat，scientific 同时可转为精确的 Rat 和浮点 Float；原生数字语法不支持负数。项的精译依赖上下文，因此 term 应在 withMainContext 中交给 elabTerm。还有许多同类 Lean.Elab.Tactic.elab* 函数，例如 elabTermEnsuringType、elabTermWithHoles。
〔可运行〕
/-- 把字符串记录成消息。 -/
elab "echo" s:str : tactic => do
let s : String := s.getString
Lean.logInfo s
/-- 打印给定自然数的平方。 -/
elab "square_nat" n:num : tactic => do
let n : Nat := n.getNat
Lean.logInfo s!"{n^2}"
/-- 打印给定非负十进制数的平方。 -/
elab "square_float" n:scientific : tactic => do
let (m, s, e) := n.getScientific
let q : Rat := Rat.ofScientific m s e
let f : Float := Float.ofScientific m s e
Lean.logInfo s!"Rat: {q*q}, Float: {f^2}"
/-- 显示给定项的类型。 -/
elab "my_check" e:term : tactic => do
withMainContext do
let e : Expr ← elabTerm e none -- 不给期望类型，把 TSyntax `term 精译成 Expr
let t ← inferType e
Lean.logInfo m!"{e} : {t}"
example (n : Nat) : True := n:Nat⊢ True
n:Nat⊢ True
n:Nat⊢ True
n:Nat⊢ True
n:Nat⊢ True
All goals completed! 🐙
下面留下自定义 have。策略精译器本身是可运行定义，但故意抛错，具体实现由读者完成。
〔练习模板〕
elab "my_have" n:ident ":=" e:term : tactic => do
throwError "Not implemented, left as an exercise"
〔练习·故意错误〕 第四个错误是调用尚未实现的练习；仍用注释隔离。
-- example (x y : Prop) (hx : x) (hxy : x → y) : y := by
-- my_have hy := hxy hx
-- exact hy
#check True -- 隔离块的可构建哨兵
2.6.3. 拆分 syntax、macro_rules 与 elab_rules
macro 和 elab 很方便；语法复杂后，可先用 syntax 定义形状，再用 macro_rules 或 elab_rules 定义含义。
〔可运行〕
/-- `my_constructor'` 的文档字符串。 -/
syntax "my_constructor'" : tactic
syntax "my_trivial'" : tactic
syntax "my_intro'" ident : tactic
syntax "my_assumption'" : tactic
macro_rules
| `(tactic| my_constructor') => `(tactic| apply And.intro)
| `(tactic| my_trivial') => `(tactic| exact True.intro)
elab_rules : tactic
-- 匹配变量使用 `$` 反引用；也可写 `$h:ident` 显式标注语法类别。
| `(tactic| my_intro' $h:ident) => runIntro h.getId
| `(tactic| my_assumption') => runAssumption
example (p : Prop) : p → p ∧ True := p:Prop⊢ p → p ∧ True
p:Proph:p⊢ p ∧ True; p:Proph:p⊢ pp:Proph:p⊢ True; p:Proph:p⊢ True; All goals completed! 🐙
2.6.4. 语法数组：简化版 simp_rw
数组尤其适合展示这些规则。先打开 Lean.Parser.Tactic.location 所在命名空间。在 term,* 中，* 表示可空列表，换成 + 表示非空列表；逗号表示元素以逗号分隔，省略逗号则以空格分隔。在 (location)? 中，location 是 simp at h 这类指定假设位置的语法，? 表示内容可有可无。
〔可运行〕
open Parser.Tactic
syntax "my_simp_rw " "[" term,* "]" (location)? : tactic
macro_rules
-- 可选语法或语法列表用 `$[...]` 反引用：`$[...]?` 匹配可选项，
-- `$[...],*` 匹配可空的逗号分隔列表。没有 `$` 的方括号是字面符号。
-- 此处并非所有语法类别标注都必需；写出它们只是为了清楚。
| `(tactic| my_simp_rw [$e:term, $[$es:term],*] $[$loc:location]?) =>
`(tactic| simp only [$e:term] $[$loc:location]?; my_simp_rw [$[$es:term],*] $[$loc:location]?)
| `(tactic| my_simp_rw [$e:term] $[$loc:location]?) =>
`(tactic| simp only [$e:term] $[$loc:location]?)
| `(tactic| my_simp_rw [] $[$_loc:location]?) => `(tactic| skip)
example : ∀ n m : Nat, m + n + 1 - 1 = n + m := ⊢ ∀ (n m : Nat), m + n + 1 - 1 = n + m
All goals completed! 🐙
也可以用 elab_rules 直接遍历项数组，每轮构造一个 simp only 策略语法，再交给 evalTactic 执行。
〔可运行〕
syntax "my_simp_rw' " "[" term,* "]" (Parser.Tactic.location)? : tactic
elab_rules : tactic
| `(tactic| my_simp_rw' [$[$es:term],*] $[$loc:location]?) =>
for e in es do
let simpOnlyTactic ← `(tactic| simp only [$e:term] $[$loc:location]?)
evalTactic simpOnlyTactic
example : ∀ n m : Nat, m + n + 1 - 1 = n + m := ⊢ ∀ (n m : Nat), m + n + 1 - 1 = n + m
All goals completed! 🐙
语法匹配会迅速变复杂，遗憾的是没有覆盖所有细枝末节的通用指南。
2.6.5. 更进一步的语法定义
my_simp_rw 的语法还可以先拆成重写规则和规则序列。<|> 表示备选，因而箭头既可写 Unicode ←，也可写 ASCII <-。
〔源码节选〕 这段会与前面的同名 my_simp_rw 语法冲突，因此按源码展示，不参与精译。
-- syntax rwRule := ("← " <|> "<- ")? term
-- syntax rwRuleSeq := "[" rwRule,* "]"
-- syntax "my_simp_rw " rwRuleSeq (location)? : tactic
#check True -- 隔离块的可构建哨兵
也可以声明全新的语法类别。下面是玩具例子：允许用近似自然语言的方式写算术表达式。宏规则会把 language[1 plus (2 times 4)] 展开为 1 + (2 * 4)。
〔可运行〕
declare_syntax_cat my_syntax_cat
syntax my_syntax_cat " plus " my_syntax_cat : my_syntax_cat
syntax my_syntax_cat " times " my_syntax_cat : my_syntax_cat
syntax "(" my_syntax_cat ")" : my_syntax_cat
syntax num : my_syntax_cat -- num 用于 42 这样的数字文字
syntax "language[" my_syntax_cat "]" : term
macro_rules
| `(language[$a plus $b]) => `(language[$a] + language[$b])
| `(language[$a times $b]) => `(language[$a] * language[$b])
| `(language[($a)]) => `((language[$a]))
| `(language[$n:num]) => `($n:num)
#check (language[1 plus (2 times 4)] : Int)
2.7. 结束语
元编程还有很多内容。更深入的 Lean 元编程教材见 Lean 4 Metaprogramming Book；遇到难解的元编程故障时，可查 Metaprogramming gotchas；Qq 的独立资料见 quote4。
更重要的是保持好奇：对本章使用的函数按 Ctrl+点击，直接看它们在做什么。也可点击 TacticM、MetaM，乃至以后遇到的 TermElabM、CoreM、IO、MacroM、DelabM，观察它们额外携带哪些 Context 与 State，以及各自扩展了什么单子。这些状态乍看吓人，但 Lean 能支配的全部信息总得存放在某处。
〔可运行〕
end MetaProgrammingTutorial