# 结构化证明

> have/suffices/calc/show 写出可读的证明，以及「可维护的证明」应该长什么样。

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

一串 `simp`、`omega` 能证出定理，但半年后没人（包括你）看得懂。**结构化证明**让证明的推理链条显式可读。

## have：引入中间结论

```lean
theorem example_have (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  have step : a ≤ b := h1
  exact Nat.le_trans step h2
```

`have 名字 : 类型 := 证明` 把一个中间结论加进上下文。

更常见的是**先声明后证明**：

```lean
theorem example_have2 (n : Nat) : n * 2 = n + n := by
  have key : ∀ m : Nat, m * 2 = m + m := by
    intro m
    omega
  exact key n
```

`have` 是**降低单步复杂度**的主要手段：把一个大跳跃拆成若干小步，每步都能被读懂。

匿名 `have`（用 `this` 引用）：

```lean
example (a b : Nat) (h : a = b) : b = a := by
  have := h.symm
  exact this
```

## suffices：只需证明

```lean
theorem example_suffices (n : Nat) (h : n > 0) : n ≥ 1 := by
  suffices key : n ≠ 0 by omega
  omega
```

`suffices h : T by tac` 读作「**有了 T 就能用 `tac` 完成，所以只需证 T**」。

与 `have` 的区别是**顺序**：

| | `have` | `suffices` |
| --- | --- | --- |
| 先写 | 中间结论的**证明** | 中间结论**怎么用** |
| 适合 | 自底向上（从已知推） | **自顶向下**（从目标倒推） |

数学写作里常见的「只需证明……」就是 `suffices`。它让读者先看到「为什么这个引理够用」，再看引理本身的证明。

## calc：计算链

**这是结构化证明最有价值的工具**：

```lean
theorem calc_example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c :=
  calc a = b := h1
    _    = c := h2
```

每一行是一步，`_` 代表上一行的右端。

不限于等式——任何有传递性的关系都行：

```lean
theorem calc_le (a b c d : Nat) (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) : a < d :=
  calc a ≤ b := h1
    _    < c := h2
    _    ≤ d := h3
```

**混用 `≤` 与 `<` 是允许的**，Lean 通过 `Trans` 类型类知道 `≤` 与 `<` 复合得到 `<`。

一个更实际的例子：

```lean
example (a b : Nat) (h : a = 2 * b) : a + a = 4 * b :=
  calc a + a = 2 * a       := by omega
    _        = 2 * (2 * b) := by rw [h]
    _        = 4 * b       := by ring
```

**每一步的理由写在右边**——读者可以逐步验证，不必在脑子里模拟整个推导。

<Callout type="info">
  **`calc` 是让证明可读的第一选择。** 一段几十行的 tactic 序列，改写成 calc 链后往往能一眼看懂。

  写论文/教材式的形式化时，`calc` 应该是主力——它最接近人类数学写作的形式。
</Callout>

## show：明确当前目标

```lean
example (n : Nat) : n + 0 = n := by
  show n + 0 = n     -- 显式写出，读者不必去猜
  simp
```

`show` 有两个用途：

1. **文档作用**——在长证明中间提醒读者「现在要证什么」。
2. **改写目标**——可以换成**定义等价**的形式：

```lean
def isEven (n : Nat) : Prop := n % 2 = 0

example : isEven 4 := by
  show 4 % 2 = 0      -- 展开定义
  rfl
```

## 组合起来

一个完整的结构化证明：

```lean
theorem sum_first_n (n : Nat) : 2 * (List.range (n + 1)).sum = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    have h_range : (List.range (k + 2)).sum = (List.range (k + 1)).sum + (k + 1) := by
      simp [List.range_succ]
    calc 2 * (List.range (k + 2)).sum
        = 2 * ((List.range (k + 1)).sum + (k + 1)) := by rw [h_range]
      _ = 2 * (List.range (k + 1)).sum + 2 * (k + 1) := by ring
      _ = k * (k + 1) + 2 * (k + 1) := by rw [ih]
      _ = (k + 1) * (k + 2) := by ring
```

对比同样的证明写成一串 tactic：

```lean
-- 能过，但没人看得懂
theorem sum_first_n' (n : Nat) : 2 * (List.range (n + 1)).sum = n * (n + 1) := by
  induction n <;> simp [List.range_succ, *] <;> ring
```

**两者产生的项是等价的，可读性天差地别。**

## 可维护证明的建议

### 一、显式声明中间结论的类型

```lean
have key : a ≤ b := by omega        -- ✅ 类型写出来
have key := by omega                -- ❌ 读者不知道 key 是什么
```

### 二、用 `·` 聚焦每个目标

```lean
constructor
· exact hp
· exact hq
```

不用 `·` 的话，多目标时 tactic 的作用范围不明确，改动一处会连锁破坏。

### 三、定稿时把 `simp` 换成 `simp only`

用 [`simp?`](https://daiw.org/manual/lean4/rewriting) 得到具体引理列表。**这能让证明在库升级后仍然工作**——`simp` 的行为会随 simp 集合变化，`simp only` 不会。

### 四、命名有意义

```lean
have h_pos : 0 < n := ...           -- ✅
have h1 : 0 < n := ...              -- ❌ 十行之后没人记得 h1 是什么
```

Mathlib 的命名惯例是描述性的：`h_pos`、`hab`、`key`、`main`。

### 五、长证明拆成引理

超过 30 行的证明基本都该拆。**每个引理有自己的名字和陈述，就是最好的文档**。

```lean
private theorem helper_step (n : Nat) : ... := ...

theorem main_result (n : Nat) : ... := by
  ...
  exact helper_step n
```

`private` 表示只在本文件可见，不污染全局命名空间。

## 从探索到定稿

实际写证明的流程通常是：

```text
1. 探索：sorry 搭骨架，大量试 simp / omega / exact?
2. 打通：能过就行，不管好不好看
3. 重构：拆 have、改 calc、simp → simp only
4. 命名：给中间结论起有意义的名字
5. 检查：#print axioms 确认没有 sorry
```

<Callout type="warn">
  **不要跳过第 3 步。** 「能过就不管了」的证明会在下一次库升级时崩掉，而那时你已经忘了它在干什么。

  Mathlib 对贡献的证明有明确的可读性要求，正是因为形式化数学的价值不只在「机器验证通过」，还在**人能读懂并复用**。
</Callout>

## 一个可读性对照

同一个定理的三个版本：

```lean
-- 版本 1：能过，不可读
example (a b : Nat) (h : a ≤ b) : a * 2 ≤ b * 2 + 1 := by omega

-- 版本 2：显式但啰嗦
example (a b : Nat) (h : a ≤ b) : a * 2 ≤ b * 2 + 1 := by
  have h1 : a * 2 ≤ b * 2 := Nat.mul_le_mul_right 2 h
  have h2 : b * 2 ≤ b * 2 + 1 := Nat.le_succ _
  exact Nat.le_trans h1 h2

-- 版本 3：calc，兼顾可读与简洁
example (a b : Nat) (h : a ≤ b) : a * 2 ≤ b * 2 + 1 :=
  calc a * 2 ≤ b * 2     := Nat.mul_le_mul_right 2 h
    _        ≤ b * 2 + 1 := Nat.le_succ _
```

**版本 1 适合琐碎的算术，版本 3 适合承载真正的推理**。判断标准是：**这一步是否包含读者需要理解的内容**。是的话就写出来。

下一篇：[自动化 tactic](https://daiw.org/manual/lean4/automation)。