实战：验证过的插入排序

从定义到规格到证明的完整流程——把前面所有内容串起来的一个真实例子。

这一章把前面的全部内容串起来：实现一个排序算法，并证明它正确。

「排序正确」需要两个条件：

有序性——输出是升序的。
置换性——输出是输入的重排（不能丢元素或凭空造元素）。

只证第一条是不够的——fun _ => [] 也满足有序性。

第一步：定义

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)

用到的：归纳类型的模式匹配、结构递归、类型类约束（LinearOrder 提供 ≤ 与可判定性）。

先测试：

#eval insertionSort [3, 1, 4, 1, 5, 9, 2, 6]
-- [1, 1, 2, 3, 4, 5, 6, 9]

写证明之前先 #eval 测几个例子。 如果实现本身有 bug，你会花很久试图证明一个假命题。这是形式化中最常见的时间浪费。

第二步：陈述规格

/-- 列表是升序的。 -/
def Sorted : List α → Prop
  | [] => True
  | [_] => True
  | a :: b :: l => a ≤ b ∧ Sorted (b :: l)

Mathlib 里已有 List.Sorted (· ≤ ·)，这里自己定义是为了让证明自足。

置换性直接用 Mathlib 的 List.Perm（记作 ~）。

两个目标定理：

theorem sorted_insertionSort (l : List α) : Sorted (insertionSort l) := by
  sorry

theorem perm_insertionSort (l : List α) : insertionSort l ~ l := by
  sorry

先用 sorry 把骨架搭好——这是前面提到的标准流程。

第三步：证置换性（较易）

从简单的开始。先证辅助引理：

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 让置换的推导链清晰可读（结构化证明）。
ih 是归纳假设：orderedInsert a l ~ a :: l。

主定理：

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

三步：展开定义、用刚证的引理、用归纳假设。每一步的理由都写在右边。

第四步：证有序性（较难）

需要一个更强的辅助引理——插入保持有序：

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`（逻辑）
`obtain ⟨hbc, hrest⟩ := h`	拆开 `Sorted` 的合取（tactic 基础）
`cases l with`	再分一层情况
`le_of_lt`	Mathlib 命名约定：「由 `<` 得 `≤`」（Mathlib）
`have := ih hrest`	应用归纳假设

主定理：

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

有了辅助引理，主定理只有一行。这是形式化的典型形态：难度集中在找对辅助引理，主定理往往是平凡的组合。

第五步：打包成规格

/-- 插入排序是正确的：输出有序，且是输入的置换。 -/
theorem insertionSort_correct (l : List α) :
    Sorted (insertionSort l) ∧ insertionSort l ~ l :=
  ⟨sorted_insertionSort l, perm_insertionSort l⟩

这一行就是「这个排序算法正确」的完整、机器验证过的陈述。

确认没有欠账：

#print axioms insertionSort_correct
-- 'insertionSort_correct' depends on axioms: [propext, Classical.choice, Quot.sound]

只有 Mathlib 的三个标准公理，没有 sorryAx——证明是完整的。

用依值类型的版本

也可以把规格编码进类型（依值类型）：

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 + 单独的定理」，正如依值类型那一章所说：信息放在类型里还是旁边的定理里，是工程判断。

经验：规格复杂时用旁置定理，不变量简单且贯穿始终时才编进类型。

完整流程回顾

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 频道。

下一篇：收尾复盘。

本页目录