结构化证明

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

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

have：引入中间结论

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 名字 : 类型 := 证明 把一个中间结论加进上下文。

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

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 引用）：

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

suffices：只需证明

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：计算链

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

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

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

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

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 类型类知道 ≤ 与 < 复合得到 <。

一个更实际的例子：

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

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

calc 是让证明可读的第一选择。 一段几十行的 tactic 序列，改写成 calc 链后往往能一眼看懂。

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

show：明确当前目标

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

show 有两个用途：

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

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

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

组合起来

一个完整的结构化证明：

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：

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

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

可维护证明的建议

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

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

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

constructor
· exact hp
· exact hq

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

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

用 simp? 得到具体引理列表。这能让证明在库升级后仍然工作——simp 的行为会随 simp 集合变化，simp only 不会。

四、命名有意义

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

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

五、长证明拆成引理

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

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

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

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

从探索到定稿

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

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

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

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

一个可读性对照

同一个定理的三个版本：

-- 版本 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。

本页目录