# 重写与化简

> rw 的方向与位置控制、simp 的工作原理与调试、simp only 与 simp lemma 的选择。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/rewriting
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## rw：用等式替换

```lean
example (a b c : Nat) (h : a = b) : a + c = b + c := by
  rw [h]
```

`rw [h]` **把目标里所有的 `a` 换成 `b`**，然后自动试一次 `rfl`。

### 方向

```lean
example (a b : Nat) (h : a = b) : b = a := by
  rw [← h]        -- ← 是反向：把 b 换成 a
```

`←`（`\l`）**反向使用等式**。这是 `rw` 最常需要调整的地方——写错方向会报「motive is not type correct」或直接找不到可重写的位置。

### 多次重写

```lean
example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  rw [h1, h2]
```

`rw [h1, h2]` 依次执行，等价于 `rw [h1]; rw [h2]`。

### 指定位置

```lean
example (a b : Nat) (h : a = b) (hyp : a + 1 = 5) : b + 1 = 5 := by
  rw [h] at hyp
  exact hyp
```

`at hyp` 重写**假设**而不是目标。`at *` 重写所有地方。

### 只重写第一处

```lean
example (a b : Nat) (h : a = b) : a + a = b + a := by
  rw [show a = b from h]    -- 仍会全部重写
  -- 要精确控制用 conv 或 nth_rewrite
```

```lean
example (a b : Nat) (h : a = b) : a + a = b + a := by
  nth_rewrite 1 [h]
```

`nth_rewrite n [h]` 只重写第 n 处出现。

<Callout type="warn">
  **`rw` 是语法级替换，不是语义级。** 它按项的结构精确匹配——`a + b` 与 `b + a` 是不同的项，`rw` 不会自动用交换律。

  另外 `rw` **会重写所有匹配处**，这常常不是你想要的。需要精确控制时用 `nth_rewrite` 或 `conv`。
</Callout>

### rw 用 Iff

```lean
example (p q : Prop) (h : p ↔ q) (hp : p) : q := by
  rw [← h]
  exact hp
```

`↔` 可以像 `=` 一样重写命题——这是 `Iff` 最常见的用法。

## simp：自动化简

```lean
example (n : Nat) : n + 0 = n := by simp
```

`simp` 用**一组标记为 `@[simp]` 的引理**反复重写，直到无法继续。

### simp 的工作方式

```text
1. 收集所有 @[simp] 引理（库里有几万条）
2. 把它们当作【从左到右】的重写规则
3. 反复应用直到不动点
4. 尝试闭合目标（rfl / 平凡真）
```

关键点：**simp 引理是有方向的**——`@[simp] theorem foo : a = b` 表示「把 a 换成 b」，意味着 b 被认为是「更简单的形式」。

### `simp?`：看它做了什么

```lean
example (l : List Nat) : (l ++ []).length = l.length := by
  simp?
  -- Try this: simp only [List.append_nil]
```

<Callout type="info">
  **`simp?` 是排查 simp 问题的第一工具。** 它输出实际用到的引理，可以直接替换成 `simp only [...]`。

  为什么要替换：`simp only` **更快、更稳定**。`simp` 会随着库更新而改变行为（新增 simp 引理可能让原来的证明失败或变化），`simp only` 锁定了具体引理。

  **库代码里应该优先用 `simp only`**，探索时用 `simp`。
</Callout>

### 控制 simp

```lean
simp                          -- 用所有 simp 引理
simp only [foo, bar]          -- 只用这两条
simp [foo]                    -- simp 集合 + foo
simp [-foo]                   -- simp 集合但排除 foo
simp at h                     -- 化简假设
simp at *                     -- 化简所有
simp [*]                      -- 把上下文里的假设也当重写规则
simp_all                      -- 反复化简所有目标与假设
```

`simp [*]` 很有用——它会用上下文里的等式假设做重写：

```lean
example (a b : Nat) (h : a = b) : a + 0 = b := by simp [*]
```

### 声明 simp 引理

```lean
@[simp]
theorem my_lemma (n : Nat) : n * 1 = n := Nat.mul_one n
```

<Callout type="warn">
  **加 `@[simp]` 要谨慎**，两个风险：

  1. **循环**：`a = b` 和 `b = a` 都标了 simp，会无限重写。simp 有深度限制会报错，但很难查。
  2. **方向错误**：把「复杂」的一侧当成右边，会让所有目标变复杂。

  判据：**右边应该比左边更简单/更规范**。`n + 0 = n` 对（右边简单），`n = n + 0` 错。
</Callout>

## rfl vs simp vs decide

三者都能证「显然的」等式，但机制不同：

| tactic | 机制 | 适用 |
| --- | --- | --- |
| `rfl` | **定义展开后相同** | `2 + 2 = 4` |
| `simp` | **重写到不动点** | 需要引理的化简 |
| `decide` | **实际计算判定** | 可判定的具体命题 |
| `norm_num` | **数值规范化**（Mathlib） | 算术表达式 |

```lean
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 simp
```

`rfl` 对含变量的表达式常常失败——`n + 0 = n` 靠 `Nat.add` 的定义恰好能 `rfl`，但 `0 + n = n` **不行**（要归纳）。这个不对称经常让初学者困惑，原因在 `Nat.add` 是对第二个参数递归定义的。

## conv：精确定位

```lean
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 / 全称 |

```lean
example (f : Nat → Nat) (a b : Nat) (h : a = b) : f (a + 1) = f (b + 1) := by
  conv_lhs => arg 1; rw [h]
```

<Callout type="info">
  **`conv` 是最后手段**——它冗长且脆弱。先试 `nth_rewrite`、`simp only [...]`、或重新组织证明。只有在必须精确控制某一处时才用 `conv`。
</Callout>

## unfold 与 delta

```lean
def double (n : Nat) : Nat := n * 2

example (n : Nat) : double n = n * 2 := by
  unfold double
```

`unfold f` 展开定义。通常 `simp [double]` 效果一样且更灵活——把定义当 simp 引理用。

对 `def` 定义的函数，Lean 会自动生成 `double.eq_def` 等定理供重写用。

## 常见问题

### motive is not type correct

```text
motive is not type correct
```

**依值类型场景下重写失败**——被重写的项出现在其他项的类型里，替换会破坏类型。

解法：换个角度重写（先 `generalize`），或改用 `subst`、`congr`、`simp only` 试试。这是[依值类型的代价](https://daiw.org/manual/lean4/dependent-types)之一。

### 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 会做更多定义展开）。

## 实践建议

```lean
-- 探索阶段：用强力自动化
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?` 固化。** 这个流程既保持了开发效率，又让最终证明稳定可维护。

下一篇：[归纳证明](https://daiw.org/manual/lean4/induction-proofs)。