对自然数做归纳

做完这一节，你能证明“对所有自然数 n 都成立”的命题。第一节里那个看不懂的 sumTo_formula，到这一节结尾你会自己读懂。

学完你能做什么

• 说出归纳证明的两个部分
• 读懂归纳假设 ih 是什么、能用在哪
• 用 induction n with 写出完整的归纳证明

为什么需要归纳

上一节的 decide 只能算具体的数。“对所有 n”有无穷多种情况，算不完。

归纳法的办法是只证两件事：

1. n 是 0 时成立。
2. 如果对 k 成立，那么对 k + 1 也成立。

有了这两条，0 成立，于是 1 成立，于是 2 成立，一直下去，每个自然数都轮得到。像推倒一排多米诺骨牌：第一块倒，并且每一块都能推倒下一块。

在 Lean 里，这两件事对应两个分支：

induction n with
| zero => 证 n 是 0 的情况
| succ k ih => 证 n 是 k + 1 的情况，可以使用 ih

ih 就是第 2 条里的“如果对 k 成立”。它是一个假设，内容是把命题里的 n 换成 k。

动手：0 + n = n

这个命题看起来不用证。但 Lean 的加法是对第二个数一层层定义的，n + 0 能直接算出 n，0 + n 不能。试一下就知道：

example (n : Nat) : 0 + n = n := by
  rfl

is not definitionally equal to the right-hand side

所以要用归纳。你来走一遍，注意第二个分支里 ih 长什么样：

动手证第一个归纳证明：0 + n = n状态和报错由 Lean 4.35.0 生成

theorem zero_add' (n : Nat) : 0 + n = n := by
  induction n with
  | zero =>
    rfl
  | succ k ih =>
    rw [Nat.add_succ]
  rw [ih]

写成代码：

theorem zero_add' (n : Nat) : 0 + n = n := by
  induction n with
  | zero =>
    rfl
  | succ k ih =>
    rw [Nat.add_succ]
    rw [ih]

其中用到一条现成的定理，查一下它说什么：

#check @Nat.add_succ

Nat.add_succ : ∀ (n m : Nat), n + m.succ = (n + m).succ

m.succ 就是 m + 1。这条定理说：n + (m + 1) 等于 (n + m) + 1。用它改写之后，目标里出现了 0 + k，正好是 ih 的左边，于是可以用 ih 再改写一次。

归纳证明的套路就是这样：把 k + 1 的情况整理成能看见 k 的情况的样子，然后用归纳假设。

• 我在练习里证完了 zero_add'
• 我能说出 ih 在这个证明里的内容：0 + k = k

回到求和公式

第一节的函数和定理：

def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => sumTo n + (n + 1)

theorem sumTo_formula (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero =>
    rfl
  | succ k ih =>
    simp [sumTo]
    rw [Nat.mul_add, ih]
    simp [Nat.mul_add, Nat.add_mul]
    omega

现在能读了：

• induction n with：对 n 归纳。
• zero 分支：n 是 0，两边都算出 0，rfl。
• succ k ih 分支：ih 是 2 * sumTo k = k * (k + 1)。
  • simp [sumTo]：按定义把 sumTo (k + 1) 展开成 sumTo k + (k + 1)。
  • rw [Nat.mul_add, ih]：把 2 乘进括号，出现 2 * sumTo k，用 ih 换掉。
  • 最后两行：剩下的是纯算术，展开乘法，交给 omega。

套路没变：展开定义，让 k 的情况露出来，用 ih，剩下的交给自动策略。

• 我能指出 sumTo_formula 里哪一步用了归纳假设

考考你在 succ k ih 分支里，归纳假设 ih 说的是什么？

检查点

• 我能说出归纳证明的两个部分：0 的情况，从 k 到 k + 1
• 我能写出 induction n with | zero => … | succ k ih => … 的结构
• 我知道 ih 是假设不是目标
• 我读懂了 sumTo_formula 的每一行在做什么

没成功？

succ 分支里不知道下一步干什么。 看目标里有没有出现 ih 的左边。没有，就先展开定义或改写，直到它出现。

分支名字写错。 自然数的两个分支固定叫 zero 和 succ。k 和 ih 是你起的名字。

下一节

归纳不只能用在数上。下一节对列表做归纳，并且第一次遇到“证不下去，需要先证一个帮手”的情况。