simp 和 norm_num 是 Lean 4 / Mathlib4 中使用频率最高的两个自动化 tactic。simp 是一个基于重写规则集合的项化简引擎，norm_num 是一个针对数值表达式的可判定算术归一化器。理解这两个 tactic 的工作原理，对于写出既正确又可维护的 Mathlib 风格证明至关重要。

前置阅读：本系列 02 Term-mode 与 Tactic-mode 切换心法讲解了 tactic 块的基本结构；03 Universe 与类型层级实战阐述了 Prop 与 Type 的区别——这些背景在理解 simp 的化简对象范围时用得上。

simp 的重写引擎

合流重写系统

simp 的核心是一个合流项重写（confluent term rewriting）系统。给定一组重写规则，系统对当前目标反复应用规则，直到没有规则可再适用为止。"合流"意味着：无论规则的应用顺序如何，最终结果（正规形式，normal form）是唯一的。

Lean 4 中，每条重写规则形如：

1	`lhs = rhs`

simp 将目标中所有能匹配 lhs 的子项替换为 rhs，方向固定为从左到右（left-to-right）。如果一条规则被反向标记（加 ← ），simp 则从右向左替换。

重写引擎的技术实现使用了 discrimination tree（判别树）作为索引结构，以 O(1) 的代价完成规则与子项的模式匹配，这是 Mathlib4 中数千条 simp 引理能被高效查找的原因。

simp lemmas 注册

Lean 4 中，给一个定理打上 @[simp] 属性，就把它注册为 simp lemma：

1 2	`@[simp] theorem Nat.add_zero (n : ℕ) : n + 0 = n := rfl`

Mathlib4 已经注册了数千条 simp lemma。可以用 #check 确认某条引理的签名：

1 2	`#check Nat.add_zero -- Nat.add_zero : ∀ (n : ℕ), n + 0 = n`

注册后，在任何调用 simp 的上下文中，这条规则都会自动生效。对当前 simp 集合里有哪些规则感到疑惑时，可以用 simp? 的输出来查看实际用到的引理集合（详见后文）。

基础用法

1 2	`example (n : ℕ) : n + 0 = n := by simp`

InfoView 在 simp 执行后将显示 Goals accomplished 🎉，因为 Nat.add_zero 已在默认 simp 集里。

对于更复杂的目标，simp 可能需要多步才能完全化简：

1 2	`example (n m : ℕ) : n + 0 + (m + 0) = n + m := by simp`

simp 先将 n + 0 化简为 n，再将 m + 0 化简为 m，最后得到 n + m = n + m，由 rfl 关闭。

`@[simp]` 属性的取舍

何时标记 `@[simp]`

一条引理适合标记为 @[simp] 的判断标准：

规则必须将 lhs 化简到"更简单"的形式，且"更简单"对所有用户来说都适用。典型例子是算术恒等式（n + 0 = n）、构造子判别（List.length [] = 0）、以及标准的 β-规约等价。

规则应当是无条件的（unconditional），或者条件可以被 simp 自动放电。

lhs 不应是变量或元变量——如果 lhs 是一个裸变量 x，则 simp 会对任意子项尝试匹配，性能极差。

循环危险

标记 @[simp] 最常见的错误是引入循环（looping）：

-- 危险示例（不要这样做）
@[simp] theorem bad_loop (n : ℕ) : n = n + 0 := (Nat.add_zero n).symm
-- lhs 是 n，rhs 是 n + 0
-- Nat.add_zero 把 n + 0 → n
-- bad_loop 把 n → n + 0
-- 两条规则合起来让 simp 无限循环

标记一条规则之前，必须检查它的 lhs/rhs 是否与已有 simp 集中的某条规则形成环。Mathlib4 的 lint 工具 #lint 中包含 simpVarHead、simpNF 等检查，可以自动检测这类问题：

1 2	`#check @List.map_id -- 若此 lemma 已在 simp 集里，标记其逆则循环`

条件 simp 引理

条件重写规则（conditional simp lemma）形如：

1 2	`@[simp] theorem Nat.div_self {n : ℕ} (hn : 0 < n) : n / n = 1 := ...`

前置条件 hn : 0 < n 会让 simp 在尝试匹配 n / n 时，先尝试从上下文或 simp 集中关闭子目标 0 < n。若关闭失败，该规则不适用。这比无条件引理性能更差，也更难预测，应当谨慎使用。

simp 的变体

`simp only [...]`

默认 simp 使用整个 simp 集，规则多时速度慢、调试难。simp only 只使用显式列出的引理：

1 2	`example (n : ℕ) : n + 0 + 0 = n := by simp only [Nat.add_zero]`

InfoView 在执行后会显示剩余目标为 n = n，此时再由 rfl 或 simp 内部的自反性关闭。实际上 simp only [Nat.add_zero] 已经足够，因为化简后恰好得到 rfl。

simp only 是 Mathlib 代码库中最推荐的形式：证明更加稳定，不会因为 Mathlib 更新添加了新 simp 引理而意外失效（这种失效被称为 simp regression）。

`simp [lemma1, lemma2]`

在默认 simp 集的基础上，追加指定引理：

1
2
3

theorem List.length_append_eq (l₁ l₂ : List α) :
    (l₁ ++ l₂).length = l₁.length + l₂.length := by
  simp [List.length_append]

等价于 simp [List.length_append] 展开并同时运行默认 simp 集中的其他规则。

也可以用 ← 指定逆向应用：

1
2
3

example (n : ℕ) : n = n + 0 := by
  simp [← Nat.add_zero]
-- ← 让 Nat.add_zero 从右向左：n → n + 0，这里实际上没有意义，仅演示语法

实际上 ← Nat.add_zero 方向几乎不应被用——此处仅做语法说明。

`simp_all`

simp_all 比 simp 更激进：它不仅化简当前目标，还化简 context 中的所有假设，并使用已化简的假设进一步化简目标：

1
2
3

example (h : n + 0 = m) : n = m := by
  simp_all
-- simp_all 将 h 化简为 n = m，然后 exact h 关闭目标

simp_all 适用于假设需要连锁化简的情形，但同样应优先考虑 simp_all only [...] 以维持稳定性。

`simp?` 与 `exact?`：发现工具

`simp?`

simp? 执行一次完整的 simp，然后在 InfoView 中输出"最小引理集"的建议——即实际用到的那些引理：

example (n : ℕ) : n + 0 + (0 + n) = 2 * n := by
  simp?
-- InfoView 输出示例：
-- Try this: simp only [Nat.add_zero, Nat.zero_add, Nat.two_mul]

将 simp? 的建议复制为 simp only [...] 后删除 simp?，是将探索性证明固化为稳定证明的标准流程。

`exact?`

exact? 在当前类型的全局定理库中搜索能直接关闭目标的 term：

example (n : ℕ) : 0 + n = n := by
  exact?
-- InfoView 输出示例：
-- Try this: exact Nat.zero_add n

exact? 的适用场景是"目标形式固定、确信某个引理存在但不记得全名"。相较于 simp，exact? 找到的是精确匹配，不做化简步骤。

两个工具在 VS Code + Lean4 环境下都会在 InfoView 里提供可点击的"Try this"链接，点击即自动替换为建议内容。

norm_num：数值归一化

工作原理

norm_num 是一个决定过程（decision procedure），专门处理可判定的数值算术目标。它能在 ℕ、ℤ、ℚ、ℝ 及任何有相应实例的数值类型上，自动证明或否定具体的数值命题：

example : (2 : ℕ) + 3 = 5 := by norm_num

example : (7 : ℤ) * 8 = 56 := by norm_num

example : (3 : ℚ) / 4 < 1 := by norm_num

example : ¬ (2 : ℕ) = 3 := by norm_num

norm_num 背后运行的是一个反射式（reflective）的数值求值器：它在 Lean 的元语言中计算出数值结论，再将计算过程编码为一个证明 term，交由类型检查器验证。这保证了其正确性——norm_num 不是启发式的，它给出的证明是确定性正确的。

用 #print axioms 验证某条 norm_num 证明不引入额外公理：

theorem two_plus_three : (2 : ℕ) + 3 = 5 := by norm_num

#print axioms two_plus_three
-- two_plus_three depends on axioms: [propext, Classical.choice, Quot.sound]
-- 仅依赖 Lean 4 标准公理，无额外假设

与 simp 的协作

在实践中，simp 内部会调用 norm_num 处理数值子目标。单独使用时，norm_num 比 simp 更快——在纯数值目标上无需启动完整的重写引擎。

1
2
3

-- 以下两种写法等价，但 norm_num 更快
example : (100 : ℕ) * 200 = 20000 := by norm_num
example : (100 : ℕ) * 200 = 20000 := by simp

norm_num 扩展：`@[norm_num]`

Mathlib4 提供了一套扩展机制，允许向 norm_num 注册自定义求值器。例如，Mathlib 中已有针对素数判定、阶乘、二项式系数的 norm_num 扩展：

-- 需要 import Mathlib.Tactic.NormNum.Prime
example : Nat.Prime 7 := by norm_num
example : Nat.Prime 97 := by norm_num
example : ¬ Nat.Prime 100 := by norm_num

自定义扩展的注册方式（简化示意）：

-- 实际扩展需要 import Mathlib.Tactic.NormNum.Basic
-- 并实现 NormNum.NormNumExt 的 eval 方法
-- 以下是概念性伪代码，不可直接运行
@[norm_num myFunc] def myFuncExt : NormNum.NormNumExt where
  eval := fun e => do
    -- 匹配 e 的形式，计算 myFunc 的值，返回证明
    ...

扩展一旦注册，norm_num 便能自动识别对应函数并给出证明，无需用户手动展开定义。

Term mode 与 Tactic mode 对照

Nat.add_zero 既可以用 term mode 直接给出居民，也可以用 tactic mode 通过 simp 关闭：

-- 目标：∀ (n : ℕ), n + 0 = n

-- Term mode：直接给出居民
theorem add_zero_term (n : ℕ) : n + 0 = n := Nat.add_zero n

-- Tactic mode：用 simp 关闭
theorem add_zero_tactic (n : ℕ) : n + 0 = n := by
  simp [Nat.add_zero]

对于已有直接构造子的引理，term mode 更短，链接到的定义更明确。对于需要多步化简才能出现结论的目标，tactic mode（尤其是 simp）更省力。

本系列 02 Term-mode 与 Tactic-mode 切换心法对这类选择有更完整的讨论。

典型 InfoView 状态

在 VS Code 中，将光标置于 tactic 之前和之后，InfoView 分别显示前状态和后状态。以下是一个多步 simp 的典型输出：

-- 光标在 simp only [Nat.add_zero] 之前
-- InfoView:
-- ⊢ n + 0 + (m + 0) = n + m

example (n m : ℕ) : n + 0 + (m + 0) = n + m := by
  simp only [Nat.add_zero]
-- 光标在 simp only [Nat.add_zero] 之后
-- InfoView:
-- Goals accomplished 🎉

若 simp only [...] 未完全关闭目标，InfoView 会显示剩余目标，此时可追加更多引理或换用其他 tactic。

-- 示例：simp only 未完全关闭
-- 假设目标 ⊢ n * 1 + 0 = n
example (n : ℕ) : n * 1 + 0 = n := by
  simp only [Nat.mul_one]
  -- InfoView 此时显示: ⊢ n + 0 = n
  simp only [Nat.add_zero]
  -- InfoView: Goals accomplished 🎉

这种逐步逼近的方式是调试 simp 问题的标准手段。

综合示例

simp、norm_num 和 exact? 在实际证明中通常配合使用：

import Mathlib.Tactic

-- 目标：证明 List.sum [1, 2, 3, 4, 5] = 15
theorem list_sum_example : List.sum [1, 2, 3, 4, 5] = 15 := by
  norm_num [List.sum]

-- 目标：证明一个含条件的数值断言
theorem even_sum (n : ℕ) (h : n % 2 = 0) : (n + 2) % 2 = 0 := by
  omega
-- 注：此类目标更适合 omega（线性整数算术），
-- norm_num 处理具体数值，omega 处理含变量的线性关系

-- 目标：List.length 的基本性质
theorem length_cons_simp (a : α) (l : List α) :
    (a :: l).length = l.length + 1 := by
  simp [List.length_cons]

练习

练习 1

证明下列命题，禁止使用 rfl，必须用 simp only 且列出所用引理：

1
2
3

theorem ex1 (n : ℕ) : 0 + n + 0 = n := by
  -- 补全此处
  sorry

提示：Nat.zero_add、Nat.add_zero 均在 Mathlib 的默认 simp 集里。用 simp? 找出最小引理集后，替换为 simp only。

练习 2

以下引理如果被标记 @[simp] 会产生循环，指出循环原因并给出正确的处理方式：

1 2	`-- 候选引理（勿直接标记） theorem problematic (n : ℕ) : n = n + 0 - 0 := by omega`

提示：分析 lhs 和 rhs 在已有 simp 集中能被哪些规则改写，画出重写图找出环路。

练习 3

用 norm_num 证明以下命题（需 import Mathlib.Tactic.NormNum.Prime）：

1
2
3

example : Nat.Prime 1009 := by
  -- 补全此处
  sorry

验证完成后，运行 #print axioms 查看该证明依赖的公理列表。

参考资料

Mathlib4 文档：simp
Mathlib4 文档：norm_num
Lean 4 Reference Manual：Rewriting
Avigad, Jeremy et al. Theorem Proving in Lean 4，Chapter 5：Tactics
Mathlib4 源码：Mathlib/Tactic/Simp/、Mathlib/Tactic/NormNum/