重写与化简
rw 的方向与位置控制、simp 的工作原理与调试、simp only 与 simp lemma 的选择。
rw：用等式替换
example (a b c : Nat) (h : a = b) : a + c = b + c := by
rw [h]rw [h] 把目标里所有的 a 换成 b，然后自动试一次 rfl。
方向
example (a b : Nat) (h : a = b) : b = a := by
rw [← h] -- ← 是反向：把 b 换成 a←（\l）反向使用等式。这是 rw 最常需要调整的地方——写错方向会报「motive is not type correct」或直接找不到可重写的位置。
多次重写
example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
rw [h1, h2]rw [h1, h2] 依次执行，等价于 rw [h1]; rw [h2]。
指定位置
example (a b : Nat) (h : a = b) (hyp : a + 1 = 5) : b + 1 = 5 := by
rw [h] at hyp
exact hypat hyp 重写假设而不是目标。at * 重写所有地方。
只重写第一处
example (a b : Nat) (h : a = b) : a + a = b + a := by
rw [show a = b from h] -- 仍会全部重写
-- 要精确控制用 conv 或 nth_rewriteexample (a b : Nat) (h : a = b) : a + a = b + a := by
nth_rewrite 1 [h]nth_rewrite n [h] 只重写第 n 处出现。
rw 是语法级替换，不是语义级。 它按项的结构精确匹配——a + b 与 b + a 是不同的项，rw 不会自动用交换律。
另外 rw 会重写所有匹配处，这常常不是你想要的。需要精确控制时用 nth_rewrite 或 conv。
rw 用 Iff
example (p q : Prop) (h : p ↔ q) (hp : p) : q := by
rw [← h]
exact hp↔ 可以像 = 一样重写命题——这是 Iff 最常见的用法。
simp：自动化简
example (n : Nat) : n + 0 = n := by simpsimp 用一组标记为 @[simp] 的引理反复重写，直到无法继续。
simp 的工作方式
1. 收集所有 @[simp] 引理（库里有几万条）
2. 把它们当作【从左到右】的重写规则
3. 反复应用直到不动点
4. 尝试闭合目标（rfl / 平凡真）关键点：simp 引理是有方向的——@[simp] theorem foo : a = b 表示「把 a 换成 b」，意味着 b 被认为是「更简单的形式」。
simp?：看它做了什么
example (l : List Nat) : (l ++ []).length = l.length := by
simp?
-- Try this: simp only [List.append_nil]simp? 是排查 simp 问题的第一工具。 它输出实际用到的引理，可以直接替换成 simp only [...]。
为什么要替换：simp only 更快、更稳定。simp 会随着库更新而改变行为（新增 simp 引理可能让原来的证明失败或变化），simp only 锁定了具体引理。
库代码里应该优先用 simp only，探索时用 simp。
控制 simp
simp -- 用所有 simp 引理
simp only [foo, bar] -- 只用这两条
simp [foo] -- simp 集合 + foo
simp [-foo] -- simp 集合但排除 foo
simp at h -- 化简假设
simp at * -- 化简所有
simp [*] -- 把上下文里的假设也当重写规则
simp_all -- 反复化简所有目标与假设simp [*] 很有用——它会用上下文里的等式假设做重写：
example (a b : Nat) (h : a = b) : a + 0 = b := by simp [*]声明 simp 引理
@[simp]
theorem my_lemma (n : Nat) : n * 1 = n := Nat.mul_one n加 @[simp] 要谨慎，两个风险：
- 循环：
a = b和b = a都标了 simp，会无限重写。simp 有深度限制会报错，但很难查。 - 方向错误：把「复杂」的一侧当成右边，会让所有目标变复杂。
判据：右边应该比左边更简单/更规范。n + 0 = n 对（右边简单），n = n + 0 错。
rfl vs simp vs decide
三者都能证「显然的」等式，但机制不同：
| tactic | 机制 | 适用 |
|---|---|---|
rfl | 定义展开后相同 | 2 + 2 = 4 |
simp | 重写到不动点 | 需要引理的化简 |
decide | 实际计算判定 | 可判定的具体命题 |
norm_num | 数值规范化（Mathlib） | 算术表达式 |
example : 2 + 2 = 4 := by rfl
example : (2 : Nat) + 2 = 4 := by decide
example : (37 : Nat) * 41 = 1517 := by norm_num
example (n : Nat) : n + 0 = n := by simprfl 对含变量的表达式常常失败——n + 0 = n 靠 Nat.add 的定义恰好能 rfl，但 0 + n = n 不行（要归纳）。这个不对称经常让初学者困惑，原因在 Nat.add 是对第二个参数递归定义的。
conv：精确定位
example (a b c : Nat) (h : a = b) : a + c = b + c := by
conv_lhs => rw [h]conv 进入「导航模式」，可以精确定位到表达式的某一部分再重写：
| conv 命令 | 定位 |
|---|---|
conv_lhs | 等式左边 |
conv_rhs | 等式右边 |
conv in pat => ... | 匹配某个模式的地方 |
lhs / rhs | 进一步深入 |
arg n | 第 n 个参数 |
ext x | 进入 lambda / 全称 |
example (f : Nat → Nat) (a b : Nat) (h : a = b) : f (a + 1) = f (b + 1) := by
conv_lhs => arg 1; rw [h]conv 是最后手段——它冗长且脆弱。先试 nth_rewrite、simp only [...]、或重新组织证明。只有在必须精确控制某一处时才用 conv。
unfold 与 delta
def double (n : Nat) : Nat := n * 2
example (n : Nat) : double n = n * 2 := by
unfold doubleunfold f 展开定义。通常 simp [double] 效果一样且更灵活——把定义当 simp 引理用。
对 def 定义的函数，Lean 会自动生成 double.eq_def 等定理供重写用。
常见问题
motive is not type correct
motive is not type correct依值类型场景下重写失败——被重写的项出现在其他项的类型里，替换会破坏类型。
解法：换个角度重写（先 generalize），或改用 subst、congr、simp only 试试。这是依值类型的代价之一。
simp made no progress
simp 找不到任何可应用的引理。检查：目标形式是不是你以为的（看 Infoview）；需要的引理有没有 import；是不是该先 intro/obtain 展开。
maximum recursion depth
simp 陷入循环。用 simp? 或 set_option maxRecDepth 定位，通常是某条 simp 引理方向有问题。
rw 之后目标没变
rw 只做语法匹配。目标里的 a 可能实际是 id a 或某个定义展开后的形式。用 show 先把目标改写成期望的形式，或用 simp only [h] 代替（simp 会做更多定义展开）。
实践建议
-- 探索阶段：用强力自动化
example (l : List Nat) : (l ++ []).length = l.length := by simp
-- 定稿阶段：换成显式版本，用 simp? 得到
example (l : List Nat) : (l ++ []).length = l.length := by
simp only [List.append_nil]先用 simp 探路，再用 simp? 固化。 这个流程既保持了开发效率，又让最终证明稳定可维护。
下一篇：归纳证明。