# 实战：验证过的插入排序
> 从定义到规格到证明的完整流程——把前面所有内容串起来的一个真实例子。
- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/worked-example
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）
这一章把前面的全部内容串起来：**实现一个排序算法，并证明它正确**。
「排序正确」需要两个条件：
1. **有序性**——输出是升序的。
2. **置换性**——输出是输入的重排（不能丢元素或凭空造元素）。
只证第一条是不够的——`fun _ => []` 也满足有序性。
## 第一步：定义
```lean
import Mathlib
variable {α : Type} [LinearOrder α]
/-- 把 `a` 插入到已排序的列表 `l` 中的正确位置。 -/
def orderedInsert (a : α) : List α → List α
| [] => [a]
| b :: l => if a ≤ b then a :: b :: l else b :: orderedInsert a l
/-- 插入排序。 -/
def insertionSort : List α → List α
| [] => []
| b :: l => orderedInsert b (insertionSort l)
```
用到的：[归纳类型的模式匹配](https://daiw.org/manual/lean4/inductive-types)、[结构递归](https://daiw.org/manual/lean4/functions)、[类型类约束](https://daiw.org/manual/lean4/typeclasses)（`LinearOrder` 提供 `≤` 与可判定性）。
先测试：
```lean
#eval insertionSort [3, 1, 4, 1, 5, 9, 2, 6]
-- [1, 1, 2, 3, 4, 5, 6, 9]
```
**写证明之前先 `#eval` 测几个例子。** 如果实现本身有 bug，你会花很久试图证明一个假命题。这是形式化中最常见的时间浪费。
## 第二步：陈述规格
```lean
/-- 列表是升序的。 -/
def Sorted : List α → Prop
| [] => True
| [_] => True
| a :: b :: l => a ≤ b ∧ Sorted (b :: l)
```
Mathlib 里已有 `List.Sorted (· ≤ ·)`，这里自己定义是为了让证明自足。
置换性直接用 Mathlib 的 `List.Perm`（记作 `~`）。
两个目标定理：
```lean
theorem sorted_insertionSort (l : List α) : Sorted (insertionSort l) := by
sorry
theorem perm_insertionSort (l : List α) : insertionSort l ~ l := by
sorry
```
**先用 `sorry` 把骨架搭好**——这是[前面](https://daiw.org/manual/lean4/first-steps)提到的标准流程。
## 第三步：证置换性（较易）
从简单的开始。先证辅助引理：
```lean
theorem perm_orderedInsert (a : α) (l : List α) : orderedInsert a l ~ a :: l := by
induction l with
| nil => simp [orderedInsert]
| cons b l ih =>
simp only [orderedInsert]
split
· exact List.Perm.refl _
· calc b :: orderedInsert a l
~ b :: a :: l := List.Perm.cons b ih
_ ~ a :: b :: l := List.Perm.swap a b l
```
关键点：
- **`split`** 处理 `if` 的两个分支——这是对 `if` 条件做分类讨论的 tactic。
- **`calc`** 让置换的推导链清晰可读（[结构化证明](https://daiw.org/manual/lean4/structured-proofs)）。
- `ih` 是[归纳假设](https://daiw.org/manual/lean4/induction-proofs)：`orderedInsert a l ~ a :: l`。
主定理：
```lean
theorem perm_insertionSort (l : List α) : insertionSort l ~ l := by
induction l with
| nil => simp [insertionSort]
| cons b l ih =>
calc insertionSort (b :: l)
= orderedInsert b (insertionSort l) := rfl
_ ~ b :: insertionSort l := perm_orderedInsert b _
_ ~ b :: l := List.Perm.cons b ih
```
三步：展开定义、用刚证的引理、用归纳假设。**每一步的理由都写在右边**。
## 第四步：证有序性（较难）
需要一个更强的辅助引理——**插入保持有序**：
```lean
theorem sorted_orderedInsert (a : α) (l : List α) (h : Sorted l) :
Sorted (orderedInsert a l) := by
induction l with
| nil => simp [orderedInsert, Sorted]
| cons b l ih =>
simp only [orderedInsert]
split
case isTrue hab =>
-- a ≤ b，插在最前面
exact ⟨hab, h⟩
case isFalse hab =>
-- b < a，递归插入尾部
push_neg at hab
cases l with
| nil =>
simp [orderedInsert, Sorted]
exact le_of_lt hab
| cons c l' =>
obtain ⟨hbc, hrest⟩ := h
simp only [orderedInsert]
split
case isTrue hac =>
exact ⟨le_of_lt hab, hac, hrest⟩
case isFalse hac =>
push_neg at hac
have := ih hrest
simp only [orderedInsert] at this ⊢
exact ⟨hbc, this⟩
```
这个证明明显更复杂，值得逐条看用到了什么：
| 用到 | 出处 |
| --- | --- |
| `split` + `case isTrue/isFalse` | 对 `if` 分类，并命名分支 |
| `push_neg at hab` | 把 `¬(a ≤ b)` 变成 `b < a`（[逻辑](https://daiw.org/manual/lean4/logic-connectives)） |
| `obtain ⟨hbc, hrest⟩ := h` | 拆开 `Sorted` 的合取（[tactic 基础](https://daiw.org/manual/lean4/tactics-basics)） |
| `cases l with` | 再分一层情况 |
| `le_of_lt` | Mathlib 命名约定：「由 `<` 得 `≤`」（[Mathlib](https://daiw.org/manual/lean4/mathlib)） |
| `have := ih hrest` | 应用归纳假设 |
主定理：
```lean
theorem sorted_insertionSort (l : List α) : Sorted (insertionSort l) := by
induction l with
| nil => simp [insertionSort, Sorted]
| cons b l ih => exact sorted_orderedInsert b _ ih
```
有了辅助引理，主定理只有一行。**这是形式化的典型形态：难度集中在找对辅助引理，主定理往往是平凡的组合。**
## 第五步：打包成规格
```lean
/-- 插入排序是正确的：输出有序，且是输入的置换。 -/
theorem insertionSort_correct (l : List α) :
Sorted (insertionSort l) ∧ insertionSort l ~ l :=
⟨sorted_insertionSort l, perm_insertionSort l⟩
```
**这一行就是「这个排序算法正确」的完整、机器验证过的陈述。**
确认没有欠账：
```lean
#print axioms insertionSort_correct
-- 'insertionSort_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
```
只有 Mathlib 的三个标准公理，**没有 `sorryAx`**——证明是完整的。
## 用依值类型的版本
也可以把规格编码进类型（[依值类型](https://daiw.org/manual/lean4/dependent-types)）：
```lean
def sortedInsert (a : α) (l : {l : List α // Sorted l}) : {l : List α // Sorted l} :=
⟨orderedInsert a l.val, sorted_orderedInsert a l.val l.property⟩
```
返回类型 `{l : List α // Sorted l}` 保证**只可能返回有序列表**。
**但这未必更好。** 用 `Subtype` 包装后：
- 每次访问都要 `.val`，代码变啰嗦。
- 组合多个操作时要不断重新构造证明。
- 与 Mathlib 的 `List` 引理不能直接对接。
**Mathlib 的实际选择是「普通 `List` + 单独的定理」**，正如[依值类型那一章](https://daiw.org/manual/lean4/dependent-types)所说：信息放在类型里还是旁边的定理里，是工程判断。
经验：**规格复杂时用旁置定理，不变量简单且贯穿始终时才编进类型。**
## 完整流程回顾
```text
1. 定义 用 inductive / def，先跑通
2. #eval 测试 确认实现本身对
3. 陈述规格 写出 theorem，全用 sorry
4. 从易到难 先证简单的那个性质
5. 找辅助引理 卡住时问「需要什么更一般的事实」
6. 结构化 have / calc 让证明可读
7. 检查 #print axioms 确认无 sorry
```
## 从这里往哪走
练手的好素材：
| 题目 | 涉及 |
| --- | --- |
| 归并排序 + 正确性 | 强归纳、良基递归 |
| 二叉搜索树的插入/查找 | 归纳类型、不变量 |
| 列表反转两次等于原列表 | 基础归纳 |
| 欧几里得算法正确性 | 良基递归、整除 |
| 素数无穷 | Mathlib 检索、经典证明 |
社区资源：
- **Natural Number Game**——游戏化入门，强烈推荐给初学者。
- **Mathematics in Lean**——官方的形式化数学教程。
- **Theorem Proving in Lean 4**——偏类型论与语言本身。
- **Zulip** 的 `#new members` 频道。
下一篇：[收尾复盘](https://daiw.org/manual/lean4/recap)。