归纳法入门

Introduction

数学归纳法是形式化证明中最强大的武器。本关目标：**对所有自然数 n，n + 0 = n**。这看起来也太简单了？但注意：n + 0 = n 并不是「显然」的定义——在 Peano 公理体系下，加法的定义是递归的，我们必须用归纳法来证明这个等式。归纳法分两步： 1. **基础 (zero)**：证明 n=0 时成立 2. **归纳步 (succ)**：假设 n=k 时成立，证明 n=k+1 时成立 Lean 的 `induction` 策略会自动生成这两个子目标，并给你归纳假设 `ih`。

本关学到的新东西

策略 (Tactics)

induction数学归纳法。对 Nat 自动生成 zero 和 succ 两个分支

rw等式重写。用已知等式替换表达式中的一部分

rfl证明两边定义相等的等式（如 0+0=0, x=x）

概念 (Concepts)

归纳假设 (ih)在归纳步骤中，「假设对 n 成立」这个前提

Peano 公理自然数由 zero 和 succ 两种方式构成

Nat.add_succMathlib 中的引理：a + succ b = succ (a + b)

证明目标

当前目标

⊢∀ n : Nat, n + 0 = n

分步提示

1.用 `induction n with` 对 n 做归纳。会出现两个分支：`zero` 和 `succ n ih`。
2.基本情况 `zero`：目标变成 `0 + 0 = 0`。根据加法定义 `Nat.add_zero`，这可以直接用 `rfl` 证明。
3.归纳步 `succ n ih`：目标是 `(n+1) + 0 = n+1`。用 `rw [Nat.add_succ]` 把左边展开，得到 `(n + 0) + 1`。然后用 `rw [ih]` 把 `n + 0` 换成 `n`，目标变成 `n + 1 = n + 1`，用 `rfl`。
4.`Nat.add_succ` 是 Mathlib 里的引理：`a + (b+1) = (a+b) + 1`。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器