第 05 篇把 STLC 升级到带 Π 与 Σ 的依值类型，量词被纳入类型系统。但要在自然数、列表、树这些数据结构上证明命题，还差一件事：归纳法。

直觉上，“自然数加法可交换"这种命题的证明依赖"对所有自然数都成立”，而自然数本身是一个归纳定义的对象。要让证明跟着数据结构走，类型系统需要支持归纳类型：用一组构造子定义一族数据，然后允许"按构造子分情况讨论"——模式匹配——作为消去规则。

本篇说清楚归纳类型怎样定义、模式匹配怎样替代逻辑里的归纳推理、为什么"归纳法"在依值类型系统里就是"良基递归"。

inductive：用构造子定义一族数据

自然数在 Lean 4 里是这样定义的：

1
2
3
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

这条 inductive 声明在做四件事：

  1. 引入一个新类型 Nat。
  2. 声明两条构造子：zero 与 succ。
  3. 自动生成一组消去规则：可以对 Nat 做模式匹配。
  4. 自动生成一条递归子（recursor）Nat.rec，它正是"自然数归纳法"在类型层的化身。

任何 Nat 的值都只能由 zero 与 succ 构造而成。这条"封闭性"是归纳类型的关键特征：它告诉类型检查器"我已经枚举完了所有可能"。

列表的归纳定义类似：

1
2
3
inductive List (α : Type) where
  | nil  : List α
  | cons : α → List α → List α

二叉树：

1
2
3
inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Tree α → α → Tree α → Tree α

每条 inductive 都是"构造子的有限枚举"，每条构造子的参数都是已知类型（包括正在定义的自身——这就是"归纳"的来源）。

模式匹配即分情况讨论

定义了 Nat 之后，对自然数做"分情况讨论"等价于对它做模式匹配：

1
2
3
def isZero : Nat → Bool
  | Nat.zero   => true
  | Nat.succ _ => false

这条函数说：

  • 输入是 Nat.zero，输出 true。
  • 输入是 Nat.succ _（succ 套一个东西），输出 false。

模式匹配的"穷尽性检查"由编译器保证：漏写任何一条构造子分支，编译就会失败。这条机制对应逻辑里"分情况讨论必须穷尽所有情形"的元规则。

涉及命题时，模式匹配同样起到分情况讨论的作用：

1
2
3
4
5
theorem isZero_zero : isZero Nat.zero = true := by
  rfl

theorem isZero_succ : ∀ n, isZero (Nat.succ n) = false := by
  intro n; rfl

rfl 在这里直接验证两种情形下的等式都按定义性归约成立。证明的"分情况"在 isZero 的定义里已经写好了。

递归即归纳法

定义加法：

1
2
3
def add : Nat → Nat → Nat
  | n, Nat.zero   => n
  | n, Nat.succ m => Nat.succ (add n m)

这条 add 看上去是递归函数，但它同时是一条"对自然数归纳法"的具体实例：

  • 基础情形：n + 0 = n。
  • 归纳情形：假设已经知道 n + m，证明 n + succ m = succ (n + m)。

Lean 4 的 inductive Nat 自动给出了一条递归子 Nat.rec，类型粗略形如：

1
2
3
4
5
Nat.rec :
  {motive : Nat → Sort u} →
  motive Nat.zero →
  (∀ k, motive k → motive (Nat.succ k)) →
  ∀ n, motive n

把 motive 当成 λ n. P n，这条 Nat.rec 正是数学归纳法的精确形式：

数学归纳法 Nat.rec 参数
要证的命题 P motive : Nat → Prop
基础情形 P 0 motive zero
归纳步骤 P k → P (k+1) ∀ k, motive k → motive (succ k)
结论 ∀ n, P n ∀ n, motive n

写一条手工归纳证明：

1
2
3
4
5
theorem zero_add : ∀ n : Nat, 0 + n = n := by
  intro n
  induction n with
  | zero => rfl
  | succ k ih => simp [Nat.add_succ, ih]

induction n with 触发的就是对 Nat.rec 的调用，给出 zero 与 succ 两个分支。ih（induction hypothesis）是"归纳假设"，类型形如 0 + k = k。整段证明严格对应数学归纳法的两步。

关键观察：写一条递归函数和写一段归纳证明，在 Lean 4 里是同一种活动。模式匹配 + 递归调用既能构造数据，也能构造证明。

良基性：递归必须终止

依值类型系统接受归纳类型的代价是：递归函数必须良基（well-founded）。否则强归一化失守，整个证明系统会一致性崩塌。

Lean 4 用结构性递归（structural recursion）默认强制良基：

1
2
3
def add : Nat → Nat → Nat
  | n, Nat.zero   => n
  | n, Nat.succ m => Nat.succ (add n m)

add n m 的递归调用作用在 m 的子结构 succ m → m 上。Lean 自动验证"m 在每次递归调用都严格变小"，因此一定终止。

如果写一个非良基函数：

1
2
def bad : Nat → Nat
  | n => bad (n + 1)

Lean 4 拒绝接受。错误信息会指出"无法证明递归良基"。

这条约束的意义重大：

  • 良基递归保证强归一化，保证类型相等性判断终止。
  • 类型检查器内核保持简单与高效。
  • "编译通过 = 定理得证"成立的前提之一就是没有任何 trick 能让一段循环把假命题"证"出来。

良基检查偶尔会过严。Lean 4 提供 termination_by 与 decreasing_by 让程序员手工提供终止性证明，但这条逃生通道仍然要求人类显式给出终止度量，不允许"我猜它会停"的写法。

互归纳类型

有些数据相互依赖。例如"奇数"与"偶数"：

1
2
3
4
5
6
7
8
mutual
  inductive IsEven : Nat → Prop where
    | zero    : IsEven 0
    | succ_of : ∀ n, IsOdd n → IsEven (n + 1)

  inductive IsOdd : Nat → Prop where
    | succ_of : ∀ n, IsEven n → IsOdd (n + 1)
end

IsEven 与 IsOdd 互相引用，但每条构造子的参数仍然是子结构（IsOdd n 的参数是 IsEven 在更小的 n 上），因此良基性成立。

互归纳是日常少见但偶尔必要的工具。比如形式化语言里的"表达式"与"语句"经常需要互归纳定义。

命题归纳：相等关系

= 在 Lean 4 里也是归纳定义的：

1
2
inductive Eq {α : Sort u} (a : α) : α → Prop where
  | refl : Eq a a

只有一条构造子：refl，要求两边相同。这条定义看上去贫弱，却足以推出：

  • 反身性 a = a。
  • 对称性 a = b → b = a。
  • 传递性 a = b → b = c → a = c。
  • 替换性 a = b → P a → P b。

所有这些都是 Eq.rec（自动生成的递归子）的实例。等号在依值类型系统里不是原始概念，而是最简单的归纳类型之一。

这条洞见的意义：Lean 不需要把"等号"作为公理引入，等号的全部性质来自一条三行的 inductive。系统的可信基底因此小一截。

把数据嵌入证明的例子

定义"列表反转"，并证明"反转两次等于原列表"：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
def reverse : List α → List α
  | []        => []
  | x :: xs   => reverse xs ++ [x]

theorem reverse_append (xs ys : List α) :
    reverse (xs ++ ys) = reverse ys ++ reverse xs := by
  induction xs with
  | nil => simp [reverse]
  | cons x xs ih => simp [reverse, ih, List.append_assoc]

theorem reverse_reverse (xs : List α) :
    reverse (reverse xs) = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [reverse, reverse_append, ih]

两条定理的证明都按列表归纳进行：nil 情形用 rfl 或 simp，cons 情形用归纳假设 ih。

写完之后：

  • reverse 是一个能跑的程序。
  • reverse_reverse 是一条命题的证明。
  • 二者都通过同一个 Lean 4 编译器的类型检查。

这正是"形式化编译器编译通过就是定理得证"在依值类型系统里的具体形态：程序与证明共用同一套语法、同一套类型检查器、同一套归一化机制。

模式提炼

模式 内容
归纳类型即数据闭包 inductive 用构造子枚举出所有可能值
模式匹配即分情况 编译器强制穷尽，对应逻辑里的"分情况讨论"
递归即归纳法 递归子 T.rec 是归纳法的类型化形式
良基强制终止 结构性递归默认良基，避免假命题被"证"
等号是归纳的 = 本身就是一条 inductive，全部等式性质从一条构造子推出

给读者的练习

  1. 给 List α 写出 length、map、append，并证 length (xs ++ ys) = length xs + length ys。
  2. 互归纳定义 IsEven / IsOdd，证明 ∀ n, IsEven n ∨ IsOdd n。
  3. 想清楚：为什么不能给 Nat 加一条构造子 inf : Nat？这会破坏什么？
  4. 拓展：试着自己手写一条 inductive 的递归子类型，对照 Lean 自动生成的 Nat.rec 看一致性。

衔接到下一篇

至此，“命题与类型对应”、“STLC 即命题逻辑”、“类型检查即证明检查”、“依值类型表达一阶逻辑”、“归纳类型支撑日常数据与归纳法”——五件事都打通了。

下一篇离开纸面，正式动手搭建 Lean 4 实验环境：装 elan，跑 lake new，写第一个 .lean 文件，让本系列的全部代码片段在读者机器上真能跑起来。再往后两篇会专门写"在 Lean 中证经典命题"和"类型检查器的可信基底"。

参考资料

  • Peter Dybjer. Inductive Families. Formal Aspects of Computing, 1994.
  • Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
  • Programming in Martin-Löf’s Type Theory. Bengt Nordström, Kent Petersson, Jan M. Smith. Oxford, 1990.
  • Lean 4 文档：https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html
  • Adam Chlipala. Certified Programming with Dependent Types. 第 3 章 “Introducing Inductive Types”.