6. 归纳法
本章介绍归纳法，这是一种适用于自然数以及整数、自然数对等其他离散类型的证明方法。我们还会介绍递归，这是一种定义数列（更一般地，定义从离散类型出发的函数）的方法；而归纳法正是证明关于递归定义对象的结果的标准方法。
在第 6.1 节到第 6.3 节中，我们只使用最传统形式的归纳法：通过把关于一个自然数的结果同关于前一个自然数的结果联系起来，来证明该结果，并使用这种归纳法的若干小变体。在第 6.4 节到第 6.7 节中，我们介绍强归纳法，以及更一般的良基归纳法。这些归纳原理更加灵活。
6.1. 引言
6.1.1. 例
问题
设 \(n\) 为自然数。证明 \(2 ^n\ge n+1\)。
解答
我们对 \(n\) 归纳证明。基例 \(2^0\geq 0+1\) 是显然的。
现在假设对某个自然数 \(k\)，有 \(2 ^k\ge k+1\)。那么
在 Lean 中，策略 simple_induction 会建立一个归纳证明。这里，在 simple_induction n with k IH 这一行之前，目标状态显示一个目标；
n : ℕ
⊢ 2 ^ n ≥ n + 1
而使用该策略之后，目标状态显示两个目标，一个对应基例，一个对应归纳步。
⊢ 2 ^ 0 ≥ 0 + 1
k : ℕ
IH : 2 ^ k ≥ k + 1
⊢ 2 ^ (k + 1) ≥ k + 1 + 1
下面是完整的 Lean 证明。
example (n : ℕ) : 2 ^ n ≥ n + 1 := by
simple_induction n with k IH
· -- base case
numbers
· -- inductive step
calc 2 ^ (k + 1) = 2 * 2 ^ k := by ring
_ ≥ 2 * (k + 1) := by rel [IH]
_ = (k + 1 + 1) + k := by ring
_ ≥ k + 1 + 1 := by extra
6.1.2. 例
定理
设 \(n\) 为自然数。那么 \(n\) 要么为偶数，要么为奇数。
（与例 3.1.9、例 4.2.9 比较。）
证明
我们对 \(n\) 归纳证明。
基例是证明 0 要么为偶数，要么为奇数。我们证明它为偶数。确实，\(0=2\cdot 0\)。
现在假设对某个自然数 \(k\)，\(k\) 要么为偶数，要么为奇数。
情形 1（\(k\) 为偶数）：则存在整数 \(x\)，使得 \(k=2x\)，于是 \(k+1 = 2x+1\)，所以 \(k+1\) 为奇数。
情形 2（\(k\) 为奇数）：则存在整数 \(x\)，使得 \(k=2x+1\)，并且
所以 \(k+1\) 为偶数。
下面是这个论证在 Lean 中的提纲。请填补各处的 sorry。
example (n : ℕ) : Even n ∨ Odd n := by
simple_induction n with k IH
· -- base case
sorry
· -- inductive step
obtain ⟨x, hx⟩ | ⟨x, hx⟩ := IH
· sorry
· sorry
6.1.3. 例
定理
设 \(a,b,d\) 为整数，并假设 \(a\equiv b \mod d\)。设 \(n\) 为自然数。则 \(a^n\equiv b ^ n \mod d\)。
这是模算术的幂规则，即引理 Int.modEq.pow，我们在例 3.3.9 中曾不加证明地陈述过它。它是组合在一起形成 rel 策略模算术能力的引理之一。
证明
我们对 \(n\) 归纳证明。
首先注意 \(a^0-b^0 = d\cdot 0\)，所以 \(d\mid a^0-b^0\)，从而 \(a^0\equiv b ^ 0 \mod d\)。这是基例。
现在设 \(k\) 为自然数，并假设 \(a^k\equiv b ^ k \mod d\)。则存在整数 \(x\)，使得 \(a^k- b ^ k =dx\)。又由假设 \(a\equiv b \mod d\)，存在整数 \(y\)，使得 \(a-b=dy\)。于是
所以 \(d\mid a^{k+1}-b^{k+1}\)，从而 \(a^{k+1}\equiv b ^ {k+1} \mod d\)。
请把这个证明写成 Lean。
example {a b d : ℤ} (h : a ≡ b [ZMOD d]) (n : ℕ) : a ^ n ≡ b ^ n [ZMOD d] := by
sorry
6.1.4. 例
问题
设 \(n\) 为自然数。证明 \(4^n\) 模 15 同余于 \(1\) 或 \(4\)。
解答
我们对 \(n\) 归纳证明。首先，\(4^0=1\)，所以 \(4^0\equiv 1\mod 15\)。
现在设 \(k\) 为自然数，并假设我们知道 \(4^k\) 模 15 同余于 \(1\) 或 \(4\)。
情形 1（\(4^k\equiv 1\mod 15\)）：那么
情形 2（\(4^k\equiv 4\mod 15\)）：那么
example (n : ℕ) : 4 ^ n ≡ 1 [ZMOD 15] ∨ 4 ^ n ≡ 4 [ZMOD 15] := by
simple_induction n with k IH
· -- base case
left
numbers
· -- inductive step
obtain hk | hk := IH
· right
calc (4:ℤ) ^ (k + 1) = 4 * 4 ^ k := by ring
_ ≡ 4 * 1 [ZMOD 15] := by rel [hk]
_ = 4 := by numbers
· left
calc (4:ℤ) ^ (k + 1) = 4 * 4 ^ k := by ring
_ ≡ 4 * 4 [ZMOD 15] := by rel [hk]
_ = 15 * 1 + 1 := by numbers
_ ≡ 1 [ZMOD 15] := by extra
6.1.5. 例
我们也可以用归纳法证明关于所有大于等于某个给定数的自然数的结果。只要从那个数开始归纳即可。
问题
设 \(n\) 为大于等于 2 的自然数。证明 \(3 ^n\ge 2^n+5\)。
解答
我们从 2 开始对 \(n\) 归纳证明。基例 \(3^2\geq 2^2+5\) 是显然的。
现在假设对某个自然数 \(k\)，有 \(3 ^k\ge 2^k+5\)。那么
在 Lean 中，策略 induction_from_starting_point 会建立一个从给定起点开始的归纳证明。
example {n : ℕ} (hn : 2 ≤ n) : (3:ℤ) ^ n ≥ 2 ^ n + 5 := by
induction_from_starting_point n, hn with k hk IH
· -- base case
numbers
· -- inductive step
calc (3:ℤ) ^ (k + 1) = 2 * 3 ^ k + 3 ^ k := by ring
_ ≥ 2 * (2 ^ k + 5) + 3 ^ k := by rel [IH]
_ = 2 ^ (k + 1) + 5 + (5 + 3 ^ k) := by ring
_ ≥ 2 ^ (k + 1) + 5 := by extra
6.1.6. 例
从非零起点开始归纳，是处理“充分大”问题时特别有用的技巧。
问题
证明：对所有充分大的自然数 \(n\)，都有 \(2^n\geq n^2\)。
解答
我们将证明它对所有自然数 \(n\geq 4\) 成立。
我们从 4 开始对 \(n\) 归纳证明。基例 \(2^4\geq 4^2\) 是显然的。
现在假设对某个自然数 \(k\geq 4\)，有 \(2 ^k\ge k^2\)。那么
下面是这个论证在 Lean 中的提纲。请填补各处的 sorry。
example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 2 := by
dsimp
use 4
intro n hn
induction_from_starting_point n, hn with k hk IH
· -- base case
sorry
· -- inductive step
sorry
6.1.7. 练习
设 \(n\) 为自然数。证明 \(3 ^n\ge n^2+n+1\)。
example (n : ℕ) : 3 ^ n ≥ n ^ 2 + n + 1 := by sorry
设 \(a\geq -1\) 为实数，设 \(n\) 为自然数。证明 \((1+a)^n\ge 1+na\)。这个事实称为 Bernoulli 不等式。
example {a : ℝ} (ha : -1 ≤ a) (n : ℕ) : (1 + a) ^ n ≥ 1 + n * a := by sorry
设 \(n\) 为自然数。证明 \(5^n\) 模 8 同余于 \(1\) 或 \(5\)。
example (n : ℕ) : 5 ^ n ≡ 1 [ZMOD 8] ∨ 5 ^ n ≡ 5 [ZMOD 8] := by sorry
设 \(n\) 为自然数。证明 \(6^n\) 模 7 同余于 \(1\) 或 \(6\)。
example (n : ℕ) : 6 ^ n ≡ 1 [ZMOD 7] ∨ 6 ^ n ≡ 6 [ZMOD 7] := by sorry
设 \(n\) 为自然数。证明 \(4^n\) 模 7 同余于 \(1\)、\(2\) 或 \(4\)。
example (n : ℕ) : 4 ^ n ≡ 1 [ZMOD 7] ∨ 4 ^ n ≡ 2 [ZMOD 7] ∨ 4 ^ n ≡ 4 [ZMOD 7] := by sorry
证明：对所有充分大的自然数 \(n\)，都有 \(3^n\geq 2^n+100\)。
example : forall_sufficiently_large n : ℕ, (3:ℤ) ^ n ≥ 2 ^ n + 100 := by dsimp sorry
证明：对所有充分大的自然数 \(n\)，都有 \(2^n\geq n^2+4\)。
example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 2 + 4 := by dsimp sorry
证明：对所有充分大的自然数 \(n\)，都有 \(2^n\geq n^3\)。
example : forall_sufficiently_large n : ℕ, 2 ^ n ≥ n ^ 3 := by dsimp sorry
设 \(a\) 为奇自然数。用归纳法证明：对所有自然数 \(n\)，自然数 \(a^n\) 为奇数。并由此推出：对所有自然数 \(a\) 和 \(n\)，若 \(a^n\) 为偶数，则 \(a\) 为偶数。（这一部分不是归纳问题。）
theorem Odd.pow {a : ℕ} (ha : Odd a) (n : ℕ) : Odd (a ^ n) := by sorry theorem Nat.even_of_pow_even {a n : ℕ} (ha : Even (a ^ n)) : Even a := by sorry
6.2. 递推关系
6.2.1. 例
数列是一个无限延伸的带指标列表。有些数列由闭公式定义。例如，\(a_n=2^n\) 定义了一个数列，即 2 的幂，其项为
在 Lean 中，我们会这样定义这个数列：
def a (n : ℕ) : ℕ := 2 ^ n
Lean 也会计算这个数列中我们想要的任意一项：
#eval a 20 -- infoview displays `1048576`
然而，许多重要数列并没有简单的闭公式。定义数列的一种更灵活方式是递归定义。例如，我们可以递归地定义一个数列 \((b_n)\)：
\[\begin{split}b_0&=3 \\ \text{for }n:\mathbb{N},\quad b_{n+1} &= b_n{}^2-2.\end{split}\]
这个数列的前几项是
在 Lean 中，我们会这样定义这个数列：
def b : ℕ → ℤ
| 0 => 3
| n + 1 => b n ^ 2 - 2
Lean 也会计算这个数列中我们想要的任意一项（在其计算能力范围内！）：
#eval b 7 -- infoview displays `316837008400094222150776738483768236006420971486980607`
当一个数列递归定义时，用归纳法研究它通常很方便。
问题
证明：对所有 \(n\)，整数 \(b_n\) 为奇数。
解答
我们对 \(n\) 归纳证明。
首先注意
所以 \(b_0\) 为奇数。
现在设 \(k\) 为自然数，并假设 \(b_k\) 为奇数。则存在整数 \(x\)，使得 \(b_k=2x+1\)。于是有
所以 \(b_{k+1}\) 也为奇数。
下面是这个解答在 Lean 中的样子；注意按需使用 rw [b] 来展开 \(b\) 的递归定义的某一部分。
example (n : ℕ) : Odd (b n) := by
simple_induction n with k hk
· -- base case
use 1
calc b 0 = 3 := by rw [b]
_ = 2 * 1 + 1 := by numbers
· -- inductive step
obtain ⟨x, hx⟩ := hk
use 2 * x ^ 2 + 2 * x - 1
calc b (k + 1) = b k ^ 2 - 2 := by rw [b]
_ = (2 * x + 1) ^ 2 - 2 := by rw [hx]
_ = 2 * (2 * x ^ 2 + 2 * x - 1) + 1 := by ring
你也可以尝试用奇偶性的模算术刻画给出另一种证明；这种做法在文字证明和 Lean 中都可行。
6.2.2. 例
下面是另一个递归定义的数列：
\[\begin{split}x_0&=5 \\ \text{for }n:\mathbb{N},\quad x_{n+1} &= 2x_n-1.\end{split}\]
在 Lean 中，该定义如下：
def x : ℕ → ℤ
| 0 => 5
| n + 1 => 2 * x n - 1
请算出这个数列的前几项（或让 Lean 替你计算）。下面是我们可以证明的关于数列 \((x_n)\) 的一个性质：
问题
证明：对所有自然数 \(n\)，都有 \(x_n\equiv 1\mod 4\)。
解答
我们对 \(n\) 归纳证明。
对于基例，观察到
对于归纳步，假设对某个自然数 \(k\) 有 \(x_k\equiv 1\mod 4\)。那么
也成立。
请把这个陈述的两部分证明写成 Lean。
example (n : ℕ) : x n ≡ 1 [ZMOD 4] := by
simple_induction n with k IH
· -- base case
sorry
· -- inductive step
sorry
6.2.3. 例
有时，递归定义的数列也可以由闭式表达式给出。前一题中的数列 \((x_n)\) 正是如此。
问题
证明：对所有自然数 \(n\)，都有 \(x_n=2^{n+2}+1\)。
解答
我们对 \(n\) 归纳证明。
对于基例，注意如所需，
对于归纳步，假设对某个自然数 \(k\) 有 \(x_k=2^{k+2}+1\)。那么
example (n : ℕ) : x n = 2 ^ (n + 2) + 1 := by
simple_induction n with k IH
· -- base case
calc x 0 = 5 := by rw [x]
_ = 2 ^ (0 + 2) + 1 := by numbers
· -- inductive step
calc x (k + 1) = 2 * x k - 1 := by rw [x]
_ = 2 * (2 ^ (k + 2) + 1) - 1 := by rw [IH]
_ = 2 ^ ((k + 1) + 2) + 1 := by ring
6.2.4. 例
下面还有一个递归定义的数列：
\[\begin{split}A_0&=0 \\ \text{for }n:\mathbb{N},\quad A_{n+1} &= A_n + (n + 1).\end{split}\]
def A : ℕ → ℚ
| 0 => 0
| n + 1 => A n + (n + 1)
我们先算出这个数列的前几项：
\[\begin{split}A_0&=0 \\ A_1&=A_0+1 \\ &=1\\ A_2&=A_1+2 \\ &=1+2\\ &=3\\ A_3&=A_2+3 \\ &=3+3\\ &=6\\ A_4&=A_3+4 \\ &=6+4\\ &=10\\ \ldots\end{split}\]
注意这个模式：先加 1，再加 2，再加 3，再加 4。因此事实上
\[\begin{split}A_1&=1 \\ A_2&=1+2 \\ A_3&=1+2+3 \\ A_4&=1+2+3+4\\ \ldots\end{split}\]
数列的项 \(A_n\) 表示从 1 到 \(n\) 的各数之和。
问题
证明：对所有自然数 \(n\)，
解答
我们对 \(n\) 归纳证明。首先注意
这就建立了基例。现在设 \(k\) 为自然数，并假设 \(A_k=\frac{k(k+1)}{2}\)。于是有
下面是在 Lean 中的写法；由于 Lean 比人更擅长代数，所以它少写了一步。
example (n : ℕ) : A n = n * (n + 1) / 2 := by
simple_induction n with k IH
· -- base case
calc A 0 = 0 := by rw [A]
_ = 0 * (0 + 1) / 2 := by numbers
· -- inductive step
calc
A (k + 1) = A k + (k + 1) := by rw [A]
_ = k * (k + 1) / 2 + (k + 1) := by rw [IH]
_ = (k + 1) * (k + 1 + 1) / 2 := by ring
6.2.5. 例
前一个数列是通过先加 1、再加 2、再加 3 等等构造出来的。如果做同样的事，但把加法换成乘法，会怎样？这给出所谓的阶乘函数，其中“\(n\) 的阶乘”记为 \(n!\)。
\[\begin{split}0!&=1 \\ \text{for }n:\mathbb{N},\quad(n+1)! &= (n + 1) ⬝ n!\end{split}\]
def factorial : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * factorial n
notation:10000 n "!" => factorial n
所以
\[\begin{split}1!&=1 \\ 2!&=2\cdot 1 \\ 3!&=3\cdot 2\cdot 1 \\ 4!&=4\cdot 3\cdot 2\cdot 1.\\ \ldots\end{split}\]
具体地，
\[\begin{split}0!&=1 \\ 1!&=1\cdot A_0 \\ &=1\cdot 1 \\ &=1\\ 2!&=2\cdot A_1 \\ &=2\cdot 1 \\ &=2\\ 3!&=3\cdot A_2 \\ &=3\cdot 2 \\ &=6\\ 4!&=4\cdot A_3 \\ &=4\cdot 6 \\ &=24\\ \ldots\end{split}\]
问题
设 \(n\) 为自然数。证明每个满足 \(1\le d\le n\) 的自然数 \(d\) 都是 \(n!\) 的因子。
解答
我们对 \(n\) 归纳证明。基例 \(n=0\) 中，陈述是空真的，因为不存在满足 \(1\le d\le 0\) 的自然数 \(d\)。
设 \(k\) 为自然数，并假设每个满足 \(1\le d\le k\) 的自然数 \(d\) 都是 \(k!\) 的因子。现在设 \(d\) 为满足 \(1\le d\le k+1\) 的自然数。我们必须证明 \(d\) 是 \((k+1)!\) 的因子。
情形 1（\(d=k+1\)）：我们有
所以 \(d\) 是 \((k+1)!\) 的因子。
情形 2（\(d<k+1\)）：则 \(d\le k\)，所以由归纳假设，\(d\) 是 \(k!\) 的因子。因此存在自然数 \(x\)，使得 \(k!=dx\)。于是有
所以 \(d\) 是 \((k+1)!\) 的因子。
下面是 Lean 中的同一个证明。我们把它记录下来，以便以后用名称 dvd_factorial 调用。
example (n : ℕ) : ∀ d, 1 ≤ d → d ≤ n → d ∣ n ! := by
simple_induction n with k IH
· -- base case
intro k hk1 hk
interval_cases k
· -- inductive step
intro d hk1 hk
obtain hk | hk : d = k + 1 ∨ d < k + 1 := eq_or_lt_of_le hk
· -- case 1: `d = k + 1`
sorry
· -- case 2: `d < k + 1`
sorry
6.2.6. 例
问题
证明：对所有自然数 \(n\)，都有 \((n+1)!\ge 2^n\)。
解答
我们对 \(n\) 归纳证明。
对于基例，
对于归纳步，假设对某个自然数 \(k\)，有 \((k+1)!\ge 2^k\)。那么
example (n : ℕ) : (n + 1)! ≥ 2 ^ n := by
sorry
6.2.7. 练习
考虑由如下递归定义的数列 \((c_n)\)：\[\begin{split}c_0&=7 \\ \text{对 }n:\mathbb{N},\quad c_{n+1} &= 3c_n-10.\end{split}\] 证明：对所有自然数 \(n\)，整数 \(c_n\) 为奇数。
\[\begin{split}c_0&=7 \\ \text{for }n:\mathbb{N},\quad c_{n+1} &= 3c_n-10.\end{split}\]def c : ℕ → ℤ | 0 => 7 | n + 1 => 3 * c n - 10 example (n : ℕ) : Odd (c n) := by sorry
设数列 \((c_n)\) 如前一题定义。证明：对所有 \(n\)，有 \(c_n=2\cdot 3^n+5\)。
example (n : ℕ) : c n = 2 * 3 ^ n + 5 := by sorry
考虑由如下递归定义的数列 \((y_n)\)：\[\begin{split}y_0&=2 \\ \text{对 }n:\mathbb{N},\quad y_{n+1} &= y_n{}^2.\end{split}\] 证明：对所有自然数 \(n\)，有 \(y_n=2^{2^n}\)。
\[\begin{split}y_0&=2 \\ \text{for }n:\mathbb{N},\quad y_{n+1} &= y_n{}^2.\end{split}\]def y : ℕ → ℕ | 0 => 2 | n + 1 => (y n) ^ 2 example (n : ℕ) : y n = 2 ^ (2 ^ n) := by sorry
考虑由如下递归定义的数列 \((B_n)\)：\[\begin{split}B_0&=0 \\ \text{对 }n:\mathbb{N},\quad B_{n+1} &= B_n+(n+1)^2.\end{split}\] 因而 \(B_n\) 表示和 \(1^2+2^2+3^2+\cdots+n^2\)。证明：对所有自然数 \(n\)，\[B_n=\frac{n(n+1)(2n+1)}{6}.\]
\[\begin{split}B_0&=0 \\ \text{for }n:\mathbb{N},\quad B_{n+1} &= B_n+(n+1)^2.\end{split}\]\[B_n=\frac{n(n+1)(2n+1)}{6}.\]def B : ℕ → ℚ | 0 => 0 | n + 1 => B n + (n + 1 : ℚ) ^ 2 example (n : ℕ) : B n = n * (n + 1) * (2 * n + 1) / 6 := by sorry
考虑由如下递归定义的数列 \((S_n)\)：\[\begin{split}S_0&=1 \\ \text{对 }n:\mathbb{N},\quad S_{n+1} &= S_n+\frac{1}{2^{n+1}}.\end{split}\] 因而 \(S_n\) 表示和 \(1+\frac{1}{2}+\frac{1}{4}+\cdots+\frac{1}{2^n}\)。证明：对所有自然数 \(n\)，\[S_n=2-\frac{1}{2^n}.\]
\[\begin{split}S_0&=1 \\ \text{for }n:\mathbb{N},\quad S_{n+1} &= S_n+\frac{1}{2^{n+1}}.\end{split}\]\[S_n=2-\frac{1}{2^n}.\]def S : ℕ → ℚ | 0 => 1 | n + 1 => S n + 1 / 2 ^ (n + 1) example (n : ℕ) : S n = 2 - 1 / 2 ^ n := by sorry
证明：对所有自然数 \(n\)，\(n!\) 严格为正。我们把它记录下来，以便以后用名称
factorial_pos调用。example (n : ℕ) : 0 < n ! := by sorry
证明：对所有 \(n\geq 2\)，\(n!\) 为偶数。请使用从起点 2 开始的归纳（见例 6.1.5）。
example {n : ℕ} (hn : 2 ≤ n) : Nat.Even (n !) := by sorry
证明：对所有自然数 \(n\)，都有 \((n+1)!\le (n+1)^n\)。（与例 6.2.6 比较。）
example (n : ℕ) : (n + 1) ! ≤ (n + 1) ^ n := by sorry
6.3. 两步归纳法
6.3.1. 例
上一节中，我们研究了每一项由前一项构造出的递归定义数列。但也可以定义依赖若干个前项的递归数列。
例如，下面是一个由前两项递归定义的数列。
注意，由于递推关系依赖前两项，我们需要给出该数列的两个具体初值（\(a_0=2\) 与 \(a_1=1\)）作为起点。
这个数列的前几项是
在 Lean 中，我们会这样定义这个数列：
def a : ℕ → ℤ
| 0 => 2
| 1 => 1
| n + 2 => a (n + 1) + 2 * a n
并且，和上一节一样，Lean 会为我们计算该数列的任意项：
#eval a 5 -- infoview displays `31`
请在纸上或借助 Lean 再算出这个数列的若干项。你会开始看出一个模式：数列的每一项都与某个 2 的幂相差 1。我们可以用归纳法证明这一模式。
问题
证明：对所有自然数 \(n\)，都有 \(a_n=2^n+(-1)^n\)。
在下面的证明中，注意有两个基例和两个归纳假设。请思考为什么。
解答
我们对 \(n\) 归纳证明。
我们有
并且
现在设 \(k\) 为自然数，并假设 \(a_k=2^k+(-1)^k\) 且 \(a_{k+1}=2^{k+1}+(-1)^{k+1}\)。那么
主要计算的前两步（使用递推关系和归纳假设）相当固定，但根据你对指数规则和心算的熟练程度，收尾部分的行数可能或多或少。Lean 可以一行完成全部！
对于这种有两个基例和两个归纳假设的归纳，我们使用 Lean 策略 two_step_induction。
example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
two_step_induction n with k IH1 IH2
. calc a 0 = 2 := by rw [a]
_ = 2 ^ 0 + (-1) ^ 0 := by numbers
. calc a 1 = 1 := by rw [a]
_ = 2 ^ 1 + (-1) ^ 1 := by numbers
calc
a (k + 2)
= a (k + 1) + 2 * a k := by rw [a]
_ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [IH1, IH2]
_ = (2 : ℤ) ^ (k + 2) + (-1) ^ (k + 2) := by ring
6.3.2. 例
问题
证明：对所有自然数 \(m\geq 1\)，\(a_m\) 模 6 同余于 1 或 5。
解答
我们将证明一个比题目陈述更精确的结果，即对所有自然数 \(n\geq 1\)，要么
- \(a_n\equiv 1\mod 6\) 且 \(a_{n+1}\equiv 5\mod 6\)，或
- \(a_n\equiv 5\mod 6\) 且 \(a_{n+1}\equiv 1\mod 6\)。
我们对 \(n\) 归纳证明。
对于基例 \(n=1\)，注意 \(a_1=1\) 且 \(a_2=5\)，所以 \(a_1\equiv 1\mod 6\) 且 \(a_2\equiv 5\mod 6\)。
对于归纳步，设 \(k\) 为自然数，并假设要么
- \(a_k\equiv 1\mod 6\) 且 \(a_{k+1}\equiv 5\mod 6\)，或
- \(a_k\equiv 5\mod 6\) 且 \(a_{k+1}\equiv 1\mod 6\)。
情形 1（\(a_k\equiv 1\mod 6\) 且 \(a_{k+1}\equiv 5\mod 6\)）：那么
情形 2（\(a_k\equiv 5\mod 6\) 且 \(a_{k+1}\equiv 1\mod 6\)）：那么
你也许还不清楚，为什么这些计算正是解决问题所需要的。这里还有相当多低层次的逻辑操作，并没有在文字中直接点明。下面的 Lean 证明可能会使其中一些逻辑操作更明显。
example {m : ℕ} (hm : 1 ≤ m) : a m ≡ 1 [ZMOD 6] ∨ a m ≡ 5 [ZMOD 6] := by
have H : ∀ n : ℕ, 1 ≤ n →
(a n ≡ 1 [ZMOD 6] ∧ a (n + 1) ≡ 5 [ZMOD 6])
∨ (a n ≡ 5 [ZMOD 6] ∧ a (n + 1) ≡ 1 [ZMOD 6])
· intro n hn
induction_from_starting_point n, hn with k hk IH
· left
constructor
calc a 1 = 1 := by rw [a]
_ ≡ 1 [ZMOD 6] := by extra
calc a (1 + 1) = 1 + 2 * 2 := by rw [a, a, a]
_ = 5 := by numbers
_ ≡ 5 [ZMOD 6] := by extra
· obtain ⟨IH1, IH2⟩ | ⟨IH1, IH2⟩ := IH
· right
constructor
· apply IH2
calc a (k + 1 + 1) = a (k + 1) + 2 * a k := by rw [a]
_ ≡ 5 + 2 * 1 [ZMOD 6] := by rel [IH1, IH2]
_ = 6 * 1 + 1 := by numbers
_ ≡ 1 [ZMOD 6] := by extra
· left
constructor
· apply IH2
calc a (k + 1 + 1) = a (k + 1) + 2 * a k := by rw [a]
_ ≡ 1 + 2 * 5 [ZMOD 6] := by rel [IH1, IH2]
_ = 6 * 1 + 5 := by numbers
_ ≡ 5 [ZMOD 6] := by extra
obtain ⟨H1, H2⟩ | ⟨H1, H2⟩ := H m hm
· left
apply H1
· right
apply H1
6.3.3. 例
以前两项递归定义的数列中，最著名的例子是 Fibonacci 数列：每一项都是前两项之和。
def F : ℕ → ℤ
| 0 => 1
| 1 => 1
| n + 2 => F (n + 1) + F n
请在纸上或借助 Lean 算出前 10 项。
问题
证明 Fibonacci 数列 \((F_n)\) 满足：对所有自然数 \(n\)，都有 \(F_n \le 2^n\)。
解答
我们对 \(n\) 归纳证明。
当 \(n=0\) 时，我们有
当 \(n=1\) 时，我们有
设 \(k\) 为自然数，并假设 \(F_k\le 2^k\) 且 \(F_{k+1}\le 2^{k+1}\)。那么
example (n : ℕ) : F n ≤ 2 ^ n := by
two_step_induction n with k IH1 IH2
· calc F 0 = 1 := by rw [F]
_ ≤ 2 ^ 0 := by numbers
· calc F 1 = 1 := by rw [F]
_ ≤ 2 ^ 1 := by numbers
· calc F (k + 2) = F (k + 1) + F k := by rw [F]
_ ≤ 2 ^ (k + 1) + 2 ^ k := by rel [IH1, IH2]
_ ≤ 2 ^ (k + 1) + 2 ^ k + 2 ^ k := by extra
_ = 2 ^ (k + 2) := by ring
6.3.4. 例
解答
我们对 \(n\) 归纳证明。首先，
现在，设 \(k\) 为自然数，并假设 \(F_{k+1}^2-F_{k+1}F_k-F_k^2=-(-1)^k\)。那么
example (n : ℕ) : F (n + 1) ^ 2 - F (n + 1) * F n - F n ^ 2 = - (-1) ^ n := by
simple_induction n with k IH
· calc F 1 ^ 2 - F 1 * F 0 - F 0 ^ 2 = 1 ^ 2 - 1 * 1 - 1 ^ 2 := by rw [F, F]
_ = - (-1) ^ 0 := by numbers
· calc F (k + 2) ^ 2 - F (k + 2) * F (k + 1) - F (k + 1) ^ 2
= (F (k + 1) + F k) ^ 2 - (F (k + 1) + F k) * F (k + 1)
- F (k + 1) ^ 2 := by rw [F]
_ = - (F (k + 1) ^ 2 - F (k + 1) * F k - F k ^ 2) := by ring
_ = - -(-1) ^ k := by rw [IH]
_ = -(-1) ^ (k + 1) := by ring
6.3.5. 例
到目前为止，我们已经见过简单归纳、从指定起点开始的归纳和两步归纳。因此你也许不会惊讶：从指定起点开始作两步归纳同样是有效的。
考虑由如下递推定义的数列 \((d_n)\)：
\[\begin{split}d_0&=3\\ d_1&=1\\ \text{for }n:\mathbb{N},\quad d_{n+2}&=3d_{n+1}+5d_n.\end{split}\]
def d : ℕ → ℤ
| 0 => 3
| 1 => 1
| k + 2 => 3 * d (k + 1) + 5 * d k
问题
证明：对所有充分大的自然数 \(n\)，都有 \(d_n \ge 4^n\)。
开始这个问题时，你可以先手算或在 Lean 中计算前几项做实验。
#eval d 2 -- infoview displays `18`
#eval d 3 -- infoview displays `59`
#eval d 4 -- infoview displays `267`
#eval d 5 -- infoview displays `1096`
#eval d 6 -- infoview displays `4623`
#eval d 7 -- infoview displays `19349`
类似地，你可以手算或在 Lean 中计算 4 的前几个幂。
#eval 4 ^ 2 -- infoview displays `16`
#eval 4 ^ 3 -- infoview displays `64`
#eval 4 ^ 4 -- infoview displays `256`
#eval 4 ^ 5 -- infoview displays `1024`
#eval 4 ^ 6 -- infoview displays `4096`
#eval 4 ^ 7 -- infoview displays `16384`
根据这个有限样本，看起来 \(d_n\) 在 \(n=4\) 时超过 \(4^n\)。所以我们尝试从 4 开始归纳。
解答
我们将证明它对所有自然数 \(n\geq 4\) 成立。
当 \(n=4\) 时，我们有
当 \(n=5\) 时，我们有
设 \(k\) 为自然数，并假设 \(d_k\ge 4^k\) 且 \(d_{k+1}\ge 4^{k+1}\)。那么我们有
在 Lean 中，我们可以对这种论证使用策略 two_step_induction_from_starting_point。
example : forall_sufficiently_large n : ℕ, d n ≥ 4 ^ n := by
dsimp
use 4
intro n hn
two_step_induction_from_starting_point n, hn with k hk IH1 IH2
· calc d 4 = 267 := by rfl
_ ≥ 4 ^ 4 := by numbers
· calc d 5 = 1096 := by rfl
_ ≥ 4 ^ 5 := by numbers
calc d (k + 2) = 3 * d (k + 1) + 5 * d k := by rw [d]
_ ≥ 3 * 4 ^ (k + 1) + 5 * 4 ^ k := by rel [IH1, IH2]
_ = 16 * 4 ^ k + 4 ^ k := by ring
_ ≥ 16 * 4 ^ k := by extra
_ = 4 ^ (k + 2) := by ring
6.3.6. 练习
考虑由如下递归定义的数列 \((b_n)\)：\[\begin{split}b_0&=0\\ b_1&=1\\ \text{对 }n:\mathbb{N},\quad b_{n+2}&=5b_{n+1}-6b_n.\end{split}\] 证明：对所有自然数 \(n\)，都有 \(b_n=3^n - 2 ^ n\)。
\[\begin{split}b_0&=0\\ b_1&=1\\ \text{for }n:\mathbb{N},\quad b_{n+2}&=5b_{n+1}-6b_n.\end{split}\]def b : ℕ → ℤ | 0 => 0 | 1 => 1 | n + 2 => 5 * b (n + 1) - 6 * b n example (n : ℕ) : b n = 3 ^ n - 2 ^ n := by sorry
考虑由如下递归定义的数列 \((c_n)\)：\[\begin{split}c_0&=3\\ c_1&=2\\ \text{对 }n:\mathbb{N},\quad c_{n+2}&=4c_n.\end{split}\] 证明：对所有自然数 \(n\)，都有 \(c_n=2\cdot 2^n+(-2)^n\)。
\[\begin{split}c_0&=3\\ c_1&=2\\ \text{for }n:\mathbb{N},\quad c_{n+2}&=4c_n.\end{split}\]def c : ℕ → ℤ | 0 => 3 | 1 => 2 | n + 2 => 4 * c n example (n : ℕ) : c n = 2 * 2 ^ n + (-2) ^ n := by sorry
考虑由如下递归定义的数列 \((t_n)\)：\[\begin{split}t_0&=5\\ t_1&=7\\ \text{对 }n:\mathbb{N},\quad t_{n+2}&=2t_{n+1}-t_n.\end{split}\] 证明：对所有自然数 \(n\)，都有 \(t_n=2n+5\)。
\[\begin{split}t_0&=5\\ t_1&=7\\ \text{for }n:\mathbb{N},\quad t_{n+2}&=2t_{n+1}-t_n.\end{split}\]def t : ℕ → ℤ | 0 => 5 | 1 => 7 | n + 2 => 2 * t (n + 1) - t n example (n : ℕ) : t n = 2 * n + 5 := by sorry
考虑由如下递归定义的数列 \((q_n)\)：\[\begin{split}q_0&=1\\ q_1&=2\\ \text{对 }n:\mathbb{N},\quad q_{n+2}&=2q_{n+1}-q_n+6n + 6.\end{split}\] 证明：对所有自然数 \(n\)，都有 \(q_n=n^3+1\)。
\[\begin{split}q_0&=1\\ q_1&=2\\ \text{for }n:\mathbb{N},\quad q_{n+2}&=2q_{n+1}-q_n+6n + 6.\end{split}\]def q : ℕ → ℤ | 0 => 1 | 1 => 2 | n + 2 => 2 * q (n + 1) - q n + 6 * n + 6 example (n : ℕ) : q n = (n:ℤ) ^ 3 + 1 := by sorry
考虑由如下递归定义的数列 \((s_n)\)：\[\begin{split}s_0&=2\\ s_1&=3\\ \text{对 }n:\mathbb{N},\quad s_{n+2}&=2s_{n+1}+3s_n.\end{split}\] 证明：对所有自然数 \(m\)，\(s_m\) 模 5 同余于 2 或 3。
\[\begin{split}s_0&=2\\ s_1&=3\\ \text{for }n:\mathbb{N},\quad s_{n+2}&=2s_{n+1}+3s_n.\end{split}\]def s : ℕ → ℤ | 0 => 2 | 1 => 3 | n + 2 => 2 * s (n + 1) + 3 * s n example (m : ℕ) : s m ≡ 2 [ZMOD 5] ∨ s m ≡ 3 [ZMOD 5] := by sorry
考虑由如下递归定义的数列 \((p_n)\)：\[\begin{split}p_0&=2\\ p_1&=3\\ \text{对 }n:\mathbb{N},\quad p_{n+2}&=6p_{n+1}-p_n.\end{split}\] 证明：对所有自然数 \(m\geq 1\)，\(p_m\) 模 7 同余于 2 或 3。
\[\begin{split}p_0&=2\\ p_1&=3\\ \text{for }n:\mathbb{N},\quad p_{n+2}&=6p_{n+1}-p_n.\end{split}\]def p : ℕ → ℤ | 0 => 2 | 1 => 3 | n + 2 => 6 * p (n + 1) - p n example (m : ℕ) : p m ≡ 2 [ZMOD 7] ∨ p m ≡ 3 [ZMOD 7] := by sorry
考虑由如下递归定义的数列 \((r_n)\)：\[\begin{split}r_0&=2\\ r_1&=0\\ \text{对 }n:\mathbb{N},\quad r_{n+2}&=2r_{n+1}+r_n.\end{split}\] 证明：对所有充分大的自然数 \(n\)，都有 \(r_n\geq 2^n\)。
\[\begin{split}r_0&=2\\ r_1&=0\\ \text{for }n:\mathbb{N},\quad r_{n+2}&=2r_{n+1}+r_n.\end{split}\]def r : ℕ → ℤ | 0 => 2 | 1 => 0 | n + 2 => 2 * r (n + 1) + r n example : forall_sufficiently_large n : ℕ, r n ≥ 2 ^ n := by sorry
证明 Fibonacci 数列 \((F_n)\) 满足：对所有充分大的自然数 \(n\)，都有 \(0.4 \cdot 1.6^n < F_n < 0.5 \cdot 1.7^n\)。
example : forall_sufficiently_large n : ℕ, (0.4:ℚ) * 1.6 ^ n < F n ∧ F n < (0.5:ℚ) * 1.7 ^ n := by sorry
脚注
- 1
- 例子改编自 Hammack，《Book of Proof》，第 10.5 节。
6.4. 强归纳法
6.4.1. 例
我们已经遇到越来越复杂的归纳原理：从例 6.1.1 中的“简单归纳”开始，最后到例 6.3.5 中相当小众的“从指定起点开始的两步归纳”。与其随着问题变得更复杂而发展越来越奇特的归纳原理，不如解释一种更一般的方法：强归纳法。这个方法让我们可以逐个证明关于自然数的命题；在每一步中，所依赖的不仅是紧前一步，而是任意先前步骤。
我们用强归纳法重新做一遍例 6.3.3。差别在 Lean 中会更明显，但我们先给出文字证明；在文字证明中，差别主要只是强调方式不同。
问题
证明：对所有自然数 \(n\)，都有 \(F_n \le 2^n\)。
解答
我们对 \(n\) 作强归纳证明。设 \(n\) 为自然数，并假设对所有自然数 \(m < n\)，都有 \(F_m \le 2^m\)。（\(\star\)）
我们按照 \(n\) 是 0、1，还是对某个自然数 \(k\) 有 \(n=k+2\) 分类讨论。
当 \(n=0\) 时，我们有
当 \(n=1\) 时，我们有
当 \(n=k+2\) 时，我们有 \(k<k+2\) 且 \(k+1<k+2\)，所以由归纳假设（\(\star\)），\(F_k\le 2^k\) 且 \(F_{k+1}\le 2^{k+1}\)。因此
在 Lean 中，强归纳法几乎可以静默地用于证明。我们建立一个定理，陈述想要用强归纳证明的结果（这里的陈述是
对所有自然数 \(n\)，\(F_n \le 2^n\)
我在 Lean 中把它命名为 F_bound）。然后在该定理的证明内部，我们可以引用这个定理本身！Lean 会尝试为我们检查：我们只把该定理用于比当前正在研究的值更小的输入值。
你可能觉得这很可疑，或者有循环论证的危险。请自己检查：如果你尝试在值 \(n\) 本身，或在更大的值如 \(n+17\) 处调用引理 F_bound，Lean 会报错。
theorem F_bound (n : ℕ) : F n ≤ 2 ^ n := by
match n with
| 0 =>
calc F 0 = 1 := by rw [F]
_ ≤ 2 ^ 0 := by numbers
| 1 =>
calc F 1 = 1 := by rw [F]
_ ≤ 2 ^ 1 := by numbers
| k + 2 =>
have IH1 := F_bound k -- first inductive hypothesis
have IH2 := F_bound (k + 1) -- second inductive hypothesis
calc F (k + 2) = F (k + 1) + F k := by rw [F]
_ ≤ 2 ^ (k + 1) + 2 ^ k := by rel [IH1, IH2]
_ ≤ 2 ^ (k + 1) + 2 ^ k + 2 ^ k := by extra
_ = 2 ^ (k + 2) := by ring
6.4.2. 例
定理
设 \(n \geq 2\) 为自然数。则存在素数 \(p\)，使得 \(p\) 是 \(n\) 的因子。
证明
我们对 \(n\) 作强归纳证明。设 \(n\) 为自然数，并假设对所有满足 \(2 \le m < n\) 的自然数 \(m\)，都存在素数 \(p\) 是 \(m\) 的因子。（\(\star\)）
如果 \(n\) 是素数，那么 \(n\) 本身就是 \(n\) 的一个素因子，证明完成。
如果 \(n\) 不是素数，那么由于 \(n \geq 2\)，存在自然数 \(m\) 满足 \(2 \le m < n\)，且 \(m\) 是 \(n\) 的因子。（这在第 5.3 节的一道练习中已经证明。）由归纳假设（\(\star\)），存在素数 \(p\) 是 \(m\) 的因子。
由于 \(m\mid n\)，存在自然数 \(x\)，使得 \(n = mx\)。由于 \(p \mid m\)，存在自然数 \(y\)，使得 \(m = py\)。于是
所以 \(p\) 也是 \(n\) 的因子。
下面是在 Lean 中的同一个证明。第 5.3 节练习中的引理在 Lean 中名为 exists_factor_of_not_prime。
注意，这又是一个强归纳证明：在 \(n\) 处实例化的定理证明内部，我们调用了同一个定理（命名为 exists_prime_factor）在 \(m\) 处的实例。此时 Lean 有一个可用假设说明 \(m<n\)，所以这是有效的。
theorem exists_prime_factor {n : ℕ} (hn2 : 2 ≤ n) : ∃ p : ℕ, Prime p ∧ p ∣ n := by
by_cases hn : Prime n
. -- case 1: `n` is prime
use n
constructor
· apply hn
· use 1
ring
. -- case 2: `n` is not prime
obtain ⟨m, hmn, _, ⟨x, hx⟩⟩ := exists_factor_of_not_prime hn hn2
have IH : ∃ p, Prime p ∧ p ∣ m := exists_prime_factor hmn -- inductive hypothesis
obtain ⟨p, hp, y, hy⟩ := IH
use p
constructor
· apply hp
· use x * y
calc n = m * x := hx
_ = (p * y) * x := by rw [hy]
_ = p * (x * y) := by ring
6.4.3. 练习
证明：对所有自然数 \(n>0\)，存在自然数 \(a\) 和 \(x\)，其中 \(x\) 为奇数，并且 \(n=2^ax\)。建议做法：先按 \(n\) 的奇偶性分类，使用引理
even_or_odd。theorem extract_pow_two (n : ℕ) (hn : 0 < n) : ∃ a x, Odd x ∧ n = 2 ^ a * x := by sorry
6.5. 帕斯卡三角形
6.5.1. 定义
考虑由如下递归定义的自然数族 \((P_{a,b})\)：
\[\begin{split}\text{for }a:\mathbb{N},\quad P_{a,0}&=1 \\ \text{for }b:\mathbb{N},\quad P_{0,b+1}&=1 \\ \text{for }a,b:\mathbb{N},\quad P_{a+1,b+1} &= P_{a+1,b}+P_{a,b+1}.\end{split}\]
这个定义是良基的，因为定义的每一步只依赖先前的项 \(P_{a,b}\)，而对这些项而言，表达式 \(a+b\) 严格更小。
下面是在 Lean 中的样子，其中良基性说明用语法 termination_by 表达。
def pascal : ℕ → ℕ → ℕ
| a, 0 => 1
| 0, b + 1 => 1
| a + 1, b + 1 => pascal (a + 1) b + pascal a (b + 1)
termination_by _ a b => a + b
照常，Lean 可以算出我们要求的任意函数值。例如，
#eval pascal 2 4 -- infoview displays `15`
下面列出 \(a\) 和 \(b\) 从 0 到 5 的所有取值。
0 |
1 |
2 |
3 |
4 |
5 |
|
|---|---|---|---|---|---|---|
0 |
1 |
1 |
1 |
1 |
1 |
1 |
1 |
1 |
2 |
3 |
4 |
5 |
6 |
2 |
1 |
3 |
6 |
10 |
15 |
21 |
3 |
1 |
4 |
10 |
20 |
35 |
56 |
4 |
1 |
5 |
15 |
35 |
70 |
126 |
5 |
1 |
6 |
21 |
56 |
126 |
252 |
请从头重新计算其中几个值，以检查你对定义的理解。
函数 pascal 的传统可视化方式，是把上表旋转后排成一个三角形。
图 6.1 Pascal 三角形（图片来源：Wikimedia Commons）
6.5.2. 例
定理
对所有自然数 \(a\) 和 \(b\)，有 \(P_{a,b} \le (a+b)!\)。
证明
我们相对于表达式 \(a+b\) 作强归纳证明。
由第 6.2 节的一道练习，阶乘总是 \(\geq 1\)，所以对所有 \(a\)，
并且对所有 \(b\)，
现在设 \(a\) 和 \(b\) 为自然数，并假设对所有满足 \(x+y<(a+1)+(b+1)\) 的 \(x\) 和 \(y\)，都有 \(P_{x,y} \le (x+y)!\)。那么特别地
所以
theorem pascal_le (a b : ℕ) : pascal a b ≤ (a + b)! := by
match a, b with
| a, 0 =>
calc pascal a 0 = 1 := by rw [pascal]
_ ≤ (a + 0)! := by apply factorial_pos
| 0, b + 1 =>
calc pascal 0 (b + 1) = 1 := by rw [pascal]
_ ≤ (0 + (b + 1))! := by apply factorial_pos
| a + 1, b + 1 =>
have IH1 := pascal_le (a + 1) b -- inductive hypothesis
have IH2 := pascal_le a (b + 1) -- inductive hypothesis
calc pascal (a + 1) (b + 1) = pascal (a + 1) b + pascal a (b + 1) := by rw [pascal]
_ ≤ (a + 1 + b) ! + (a + (b + 1)) ! := by rel [IH1, IH2]
_ ≤ (a + b) * (a + b + 1) ! + (a + 1 + b) ! + (a + (b + 1)) ! := by extra
_ = ((a + b + 1) + 1) * (a + b + 1)! := by ring
_ = ((a + b + 1) + 1)! := by rw [factorial, factorial, factorial]
_ = (a + 1 + (b + 1))! := by ring
termination_by _ a b => a + b
6.5.3. 例
通过更精细的计算，我们可以把例 6.5.2 中的上界改进为一个精确公式。
定理
对所有自然数 \(a\) 和 \(b\)，有 \(P_{a,b}\, a!\, b!= (a+b)!\)。
证明
我们相对于表达式 \(a+b\) 作强归纳证明。
对所有 \(a\)，
并且对所有 \(b\)，
现在设 \(a\) 和 \(b\) 为自然数，并假设对所有满足 \(x+y<(a+1)+(b+1)\) 的 \(x\) 和 \(y\)，都有 \(P_{x,y}\, x!\, y! = (x+y)!\)。那么特别地
所以
theorem pascal_eq (a b : ℕ) : pascal a b * a ! * b ! = (a + b)! := by
match a, b with
| a, 0 =>
calc pascal _ 0 * a ! * 0! = 1 * a ! * 0! := by rw [pascal]
_ = 1 * a ! * 1 := by rw [factorial]
_ = (a + 0)! := by ring
| 0, b + 1 =>
calc pascal 0 (b + 1) * 0 ! * (b + 1)! = 1 * 0 ! * (b + 1)! := by rw [pascal]
_ = 1 * 1 * (b + 1)! := by rw [factorial, factorial]
_ = (0 + (b + 1))! := by ring
| a + 1, b + 1 =>
have IH1 := pascal_eq (a + 1) b -- inductive hypothesis
have IH2 := pascal_eq a (b + 1) -- inductive hypothesis
calc
pascal (a + 1) (b + 1) * (a + 1)! * (b + 1)!
= (pascal (a + 1) b + pascal a (b + 1)) * (a + 1)! * (b + 1)! := by rw [pascal]
_ = pascal (a + 1) b * (a + 1)! * (b + 1)!
+ pascal a (b + 1) * (a + 1)! * (b + 1)! := by ring
_ = pascal (a + 1) b * (a + 1)! * ((b + 1) * b !)
+ pascal a (b + 1) * ((a + 1) * a !) * (b + 1)! := by rw [factorial, factorial]
_ = (b + 1) * (pascal (a + 1) b * (a + 1)! * b !)
+ (a + 1) * (pascal a (b + 1) * a ! * (b + 1)!) := by ring
_ = (b + 1) * ((a + 1) + b) !
+ (a + 1) * (a + (b + 1)) ! := by rw [IH1, IH2]
_ = ((1 + a + b) + 1) * (1 + a + b) ! := by ring
_ = ((1 + a + b) + 1) ! := by rw [factorial]
_ = ((a + 1) + (b + 1)) ! := by ring
termination_by _ a b => a + b
Corollary
对所有自然数 \(a\) 和 \(b\)，
这个事实只是上面定理的平凡重排；但由于除法问题，Lean 证明更复杂，而本书基本上避免处理除法。这里不必纠结细节，也不必纠结两个不熟悉的策略 field_simp 和 norm_cast。
example (a b : ℕ) : (pascal a b : ℚ) = (a + b)! / (a ! * b !) := by
have ha := factorial_pos a
have hb := factorial_pos b
field_simp [ha, hb]
norm_cast
calc pascal a b * (a ! * b !) = pascal a b * a ! * b ! := by ring
_ = (a + b)! := by apply pascal_eq
6.5.4. 练习
证明：对所有自然数 \(a\) 和 \(b\)，都有 \(P_{a,b} =P_{b,a}\)。
theorem pascal_symm (m n : ℕ) : pascal m n = pascal n m := by match m, n with | 0, 0 => sorry | a + 1, 0 => sorry | 0, b + 1 => sorry | a + 1, b + 1 => sorry termination_by _ a b => a + b
使用简单归纳证明：对所有自然数 \(a\)，都有 \(P_{a,1} =a+1\)。
example (a : ℕ) : pascal a 1 = a + 1 := by sorry
6.6. 带余除法定理
6.6.1. 定义
考虑递归定义在整数上的函数 \(\operatorname{mod}\) 和 \(\operatorname{div}\)：
直观上，\(\operatorname{div}\) 计算 \(n\) 除以 \(d\) 的商（小学意义上的商，即得到一个整数而不是继续写小数），而 \(\operatorname{mod}\) 计算 \(n\) 除以 \(d\) 的余数。例如，
这些定义是良基的，因为定义的每一步只依赖先前的项 \(\operatorname{mod}(n, d)\)、\(\operatorname{div}(n, d)\)，而对这些项而言，表达式 \(2n-d\) 的绝对值严格更小。（这一点并不非常明显，尽管 Lean 可以自动证明。作为可靠性检查，
它确实严格减小。）下面是在 Lean 中的样子，其中良基性说明和定义 6.5.1 一样，用语法 termination_by 表达。
def fmod (n d : ℤ) : ℤ :=
if n * d < 0 then
fmod (n + d) d
else if h2 : 0 < d * (n - d) then
fmod (n - d) d
else if h3 : n = d then
0
else
n
termination_by _ n d => 2 * n - d
def fdiv (n d : ℤ) : ℤ :=
if n * d < 0 then
fdiv (n + d) d - 1
else if 0 < d * (n - d) then
fdiv (n - d) d + 1
else if h3 : n = d then
1
else
0
termination_by _ n d => 2 * n - d
我们检查一下它们是否做了应该做的事：
#eval fmod 11 4 -- infoview displays `3`
#eval fdiv 11 4 -- infoview displays `2`
请自己计算几个例子（并用 Lean 检查），看看你是否相信 \(\operatorname{div}\) 和 \(\operatorname{mod}\) 正在产生“商”和“余数”。现在我们把这一点严谨化。
6.6.2. 例
定理
对任意整数 \(n\) 和 \(d\)，都有 \(\operatorname{mod}(n, d) + d \cdot \operatorname{div}(n, d) = n\)。
证明
我们相对于表达式 \(2n-d\) 作强归纳证明。假设对所有满足 \(|2m-c|<|2n-d|\) 的整数 \(m\) 和 \(c\)，都有 \(\operatorname{mod}(m, c) + c \cdot \operatorname{div}(m, c) = m\)。
情形 1（\(nd<0\)）：由归纳假设，
所以
情形 2（\(0<d(n-d)\)）：由归纳假设，
所以
情形 3（\(n=d\)）：那么
情形 4：在这个情形中，
theorem fmod_add_fdiv (n d : ℤ) : fmod n d + d * fdiv n d = n := by
rw [fdiv, fmod]
split_ifs with h1 h2 h3 <;> push_neg at *
· -- case `n * d < 0`
have IH := fmod_add_fdiv (n + d) d -- inductive hypothesis
calc fmod (n + d) d + d * (fdiv (n + d) d - 1)
= (fmod (n + d) d + d * fdiv (n + d) d) - d := by ring
_ = (n + d) - d := by rw [IH]
_ = n := by ring
· -- case `0 < d * (n - d)`
have IH := fmod_add_fdiv (n - d) d -- inductive hypothesis
calc fmod (n - d) d + d * (fdiv (n - d) d + 1)
= (fmod (n - d) d + d * fdiv (n - d) d) + d := by ring
_ = n := by addarith [IH]
· -- case `n = d`
calc 0 + d * 1 = d := by ring
_ = n := by rw [h3]
· -- last case
ring
termination_by _ n d => 2 * n - d
6.6.3. 例
定理
对任意整数 \(n\) 和 \(d\)，若 \(d\) 为正，则 \(\operatorname{mod}(n, d)\) 非负。
证明
我们相对于表达式 \(2n-d\) 作强归纳证明。假设对所有整数 \(m\) 和 \(c\)，若 \(c\) 为正且 \(|2m-c|<|2n-d|\)，则 \(\operatorname{mod}(m, c)\) 非负。
情形 1（\(nd<0\)）：由归纳假设，\(\operatorname{mod}(n, d)=\operatorname{mod}(n + d, d)\geq 0\)。
情形 2（\(0<d(n-d)\)）：由归纳假设，\(\operatorname{mod}(n, d)=\operatorname{mod}(n - d, d)\geq 0\)。
情形 3（\(n=d\)）：\(\operatorname{mod}(n, d)= 0\)，所以 \(\operatorname{mod}(n, d)\geq 0\)。
情形 4（\(0\le nd\le d^2\) 且 \(n\ne d\)）：由于 \(0\le nd\) 且根据假设 \(0<d\)，可得 \(\operatorname{mod}(n, d)=n\geq 0\)。
theorem fmod_nonneg_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : 0 ≤ fmod n d := by
rw [fmod]
split_ifs with h1 h2 h3 <;> push_neg at *
· -- case `n * d < 0`
have IH := fmod_nonneg_of_pos (n + d) hd -- inductive hypothesis
apply IH
· -- case `0 < d * (n - d)`
have IH := fmod_nonneg_of_pos (n - d) hd -- inductive hypothesis
apply IH
· -- case `n = d`
extra
· -- last case
cancel d at h1
termination_by _ n d hd => 2 * n - d
6.6.4. 例
定理
对任意整数 \(n\) 和 \(d\)，若 \(d\) 为正，则 \(\operatorname{mod}(n, d)<d\)。
证明
我们相对于表达式 \(2n-d\) 作强归纳证明。假设对所有整数 \(m\) 和 \(c\)，若 \(c\) 为正且 \(|2m-c|<|2n-d|\)，则 \(\operatorname{mod}(m, c)<c\)。
情形 1（\(nd<0\)）：由归纳假设，\(\operatorname{mod}(n, d)=\operatorname{mod}(n + d, d)<d\)。
情形 2（\(0<d(n-d)\)）：由归纳假设，\(\operatorname{mod}(n, d)=\operatorname{mod}(n - d, d)<d\)。
情形 3（\(n=d\)）：由假设，\(\operatorname{mod}(n, d)= 0<d\)。
情形 4（\(0\le nd\le d^2\) 且 \(n\ne d\)）：我们有 \(n-d\le 0\)，因为 \(d(n-d)\le 0\)，且由假设 \(0<d\)。因此 \(n\le d\)。又由假设，\(n\ne d\)。合在一起，得到 \(n<d\)。
theorem fmod_lt_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : fmod n d < d := by
rw [fmod]
split_ifs with h1 h2 h3 <;> push_neg at *
· -- case `n * d < 0`
have IH := fmod_lt_of_pos (n + d) hd -- inductive hypothesis
apply IH
· -- case `0 < d * (n - d)`
have IH := fmod_lt_of_pos (n - d) hd -- inductive hypothesis
apply IH
· -- case `n = d`
apply hd
· -- last case
have h4 :=
calc 0 ≤ - d * (n - d) := by addarith [h2]
_ = d * (d - n) := by ring
cancel d at h4
apply lt_of_le_of_ne
· addarith [h4]
· apply h3
termination_by _ n d hd => 2 * n - d
6.6.5. 例
把这些合在一起，我们可以证明如下定理。该定理解释了我们从例 3.4.4 起一直使用的策略 mod_cases：对于一个模正整数 \(b\) 考察的整数 \(a\)，我们只需列出有限多种可能。
定理
设 \(a\) 和 \(b\) 为整数，且 \(b\) 为正。存在整数 \(r\)，满足 \(0 \le r < b\)，并且 \(a \equiv r\mod b\)。
证明
我们证明整数 \(\operatorname{mod}(a,b)\) 具有这个性质。确实，由例 6.6.3 和例 6.6.4，\(0 \le \operatorname{mod}(a,b) < b\)；又由例 6.6.2，
所以
所以
example (a b : ℤ) (h : 0 < b) : ∃ r : ℤ, 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b] := by
use fmod a b
constructor
· apply fmod_nonneg_of_pos a h
constructor
· apply fmod_lt_of_pos a h
· use fdiv a b
have Hab : fmod a b + b * fdiv a b = a := fmod_add_fdiv a b
addarith [Hab]
6.6.6. 练习
证明例 6.6.4 对负 \(d\) 的类似结论：对任意整数 \(n\) 和 \(d\)，若 \(d\) 为负，则 \(d<\operatorname{mod}(n, d)\)。
theorem lt_fmod_of_neg (n : ℤ) {d : ℤ} (hd : d < 0) : d < fmod n d := by sorry
考虑递归定义在整数上的函数 \(T\)：\[\begin{split}T(n)= \begin{cases} T(1-n)+2n-1,&0< n\\ T(-n),&n< 0\\ 0&n=0. \end{cases}\end{split}\] 这个递归定义是良基的，因为它的自引用在 \(|3n-1|\) 上严格下降。证明：对所有整数 \(n\)，都有 \(T(n)=n^2\)。
\[\begin{split}T(n)= \begin{cases} T(1-n)+2n-1,&0< n\\ T(-n),&n< 0\\ 0&n=0. \end{cases}\end{split}\]def T (n : ℤ) : ℤ := if 0 < n then T (1 - n) + 2 * n - 1 else if 0 < - n then T (-n) else 0 termination_by T n => 3 * n - 1 theorem T_eq (n : ℤ) : T n = n ^ 2 := by sorry
设 \(a\) 和 \(b\) 为整数，且 \(b\) 为正。证明：存在唯一整数 \(r\) 位于范围 \(0 \le r < b\) 内，使得 \(a\equiv r\mod b\)。这个定理升级了例 6.6.5：它不仅断言存在性，也断言唯一性。我们在例 4.3.4 中曾不加证明地陈述它（Lean 名称为
Int.existsUnique_modEq_lt），并且每当我们从“显然不成立的同余”推出矛盾时，例如例 4.4.3 中，都在隐式使用它。建议做法：把下面的内容写成一个独立定理uniqueness并证明它，思路大致仿照例 4.3.4 中证明的特殊情形：设 \(a\) 和 \(b\) 为整数，且 \(b\) 为正。设 \(r\) 和 \(s\) 为整数，二者都在范围 \(0 \le r < b\)、\(0 \le s < b\) 中，并且都与 \(a\) 模 \(b\) 同余。证明它们相等。然后结合例 6.6.5 中的论证，把各部分合在一起。设 \(a\) 和 \(b\) 为整数，且 \(b\) 为正。设 \(r\) 和 \(s\) 为整数，二者都在范围 \(0 \le r < b\)、\(0 \le s < b\) 中，并且都与 \(a\) 模 \(b\) 同余。证明 \(r=s\)。
theorem uniqueness (a b : ℤ) (h : 0 < b) {r s : ℤ} (hr : 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b]) (hs : 0 ≤ s ∧ s < b ∧ a ≡ s [ZMOD b]) : r = s := by sorry example (a b : ℤ) (h : 0 < b) : ∃! r : ℤ, 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b] := by sorry
6.7. 欧几里得算法
6.7.1. 定义
定义
两个整数的函数 \(\operatorname{gcd}\) 递归定义如下：
\[\begin{split}\operatorname{gcd}(a,b)= \begin{cases} \operatorname{gcd}(b,\operatorname{mod}(a,b)) & 0< b\\ \operatorname{gcd}(b,\operatorname{mod}(a,-b)) & b< 0\\ a & b=0\text{ and }0\le a\\ -a & b=0\text{ and }a<0. \end{cases}\end{split}\]
我们练习计算 \(\operatorname{gcd}\) 函数。计算 \(\operatorname{gcd}(-21,15)\)：
（记住，\(\operatorname{mod}(a,b)\) 是定义 6.6.1 中定义的“余数”函数。）
和定义 6.5.1、定义 6.6.1 中一样，我们需要说明这个递归定义是良基的，也就是该过程总会终止。也和那些章节一样，我们通过给出一个随着过程推进其绝对值严格变小的表达式来做到这一点。这里的表达式是 \(b\)，即两个数中的第二个（注意在例子中 \(b\) 依次为 15、9、6、3、0，确实在减小）。
这导向下面对 \(\operatorname{gcd}\) 的 Lean 定义尝试，其中子句 termination_by _ a b => b 表示 \(b\) 是良基性的大小表达式。
def gcd (a b : ℤ) : ℤ :=
if 0 < b then
gcd b (fmod a b)
else if b < 0 then
gcd b (fmod a (-b))
else if 0 ≤ a then
a
else
-a
termination_by _ a b => b
但不同于第 6.5 节和第 6.6 节，这个定义还不完整：沿递归过程 \(b\) 在减小这一事实“足够不明显”，需要一个显式证明。
Proposition
递归定义 \(\operatorname{gcd}\) 是良基的。
证明
有两件事要检查：
- \(\underline{\text{若 }0<b\text{，则 }-b<\operatorname{mod}(a,b)<b}\)：由例 6.6.3 和例 6.6.4，\(0\le \operatorname{mod}(a,b)<b\)，这立即给出上界；下界则来自 \[\begin{split}-b&<0\\ &\le \operatorname{mod}(a,b).\end{split}\]
- \(\underline{\text{若 }b<0\text{，则 }b<\operatorname{mod}(a,-b)<-b}\)：我们有 \(0<-b\)，所以由例 6.6.3 和例 6.6.4，\(0\le \operatorname{mod}(a,-b)<-b\)，这立即给出上界；下界则来自 \[\begin{split}b&<0\\ &\le \operatorname{mod}(a,-b).\end{split}\]
在 Lean 中，我们分别陈述并证明这些事实，用属性 @[decreasing] 标记它们；这使随后的定义 gcd 能够调用它们来证明良基性。请检查：如果省略它们，定义会报错。
@[decreasing] theorem lower_bound_fmod1 (a b : ℤ) (h1 : 0 < b) : -b < fmod a b := by
have H : 0 ≤ fmod a b
· apply fmod_nonneg_of_pos
apply h1
calc -b < 0 := by addarith [h1]
_ ≤ _ := H
@[decreasing] theorem lower_bound_fmod2 (a b : ℤ) (h1 : b < 0) : b < fmod a (-b) := by
have H : 0 ≤ fmod a (-b)
· apply fmod_nonneg_of_pos
addarith [h1]
have h2 : 0 < -b := by addarith [h1]
calc b < 0 := h1
_ ≤ fmod a (-b) := H
@[decreasing] theorem upper_bound_fmod2 (a b : ℤ) (h1 : b < 0) : fmod a (-b) < -b := by
apply fmod_lt_of_pos
addarith [h1]
@[decreasing] theorem upper_bound_fmod1 (a b : ℤ) (h1 : 0 < b) : fmod a b < b := by
apply fmod_lt_of_pos
apply h1
之后，Lean 定义 gcd 就能成功通过。可靠性检查：Lean 定义是否与我们上面对 \(\operatorname{gcd}(-21,15)\) 的计算一致？
#eval gcd (-21) 15 -- infoview displays `3`
6.7.2. 例
关于 \(\operatorname{gcd}\) 的每个事实，都将使用同样的良基性理由通过强归纳来证明。
Proposition
对所有整数 \(a\) 和 \(b\)，整数 \(\operatorname{gcd}(a,b)\) 非负。
证明
我们对 \(b\) 作强归纳证明。假设对所有满足 \(|y|<|b|\) 的整数 \(x\) 和 \(y\)，都有 \(0 \le \operatorname{gcd}(x, y)\)。
情形 1（\(0<b\)）：\(\operatorname{gcd}(a,b)\) 等于 \(\operatorname{gcd}(b,\operatorname{mod}(a,b))\)，后者由归纳假设非负。
情形 2（\(b<0\)）：\(\operatorname{gcd}(a,b)\) 等于 \(\operatorname{gcd}(b,\operatorname{mod}(a,-b))\)，后者由归纳假设非负。
情形 3（\(b=0\)，\(0\le a\)）：此时 \(\operatorname{gcd}(a,b)=a\geq 0\)。
情形 4（\(b=0\)，\(a<0\)）：此时 \(\operatorname{gcd}(a,b)=-a\geq 0\)。
theorem gcd_nonneg (a b : ℤ) : 0 ≤ gcd a b := by
rw [gcd]
split_ifs with h1 h2 ha <;> push_neg at *
· -- case `0 < b`
have IH := gcd_nonneg b (fmod a b) -- inductive hypothesis
apply IH
· -- case `b < 0`
have IH := gcd_nonneg b (fmod a (-b)) -- inductive hypothesis
apply IH
· -- case `b = 0`, `0 ≤ a`
apply ha
· -- case `b = 0`, `a < 0`
addarith [ha]
termination_by _ a b => b
6.7.3. 例
Proposition
对所有整数 \(a\) 和 \(b\)，整数 \(\operatorname{gcd}(a,b)\) 同时是 \(a\) 和 \(b\) 的因子。
也就是说，\(\operatorname{gcd}(a,b)\) 是 \(a\) 和 \(b\) 的公因子。我们稍后会证明（见练习），它事实上是 \(a\) 和 \(b\) 的最大公因子，因此英文缩写为 GCD。
证明
我们对 \(b\) 作强归纳证明。假设对所有满足 \(|y|<|b|\) 的整数 \(x\) 和 \(y\)，都有 \(0 \le \operatorname{gcd}(x, y)\)。
情形 1（\(0<b\)）：令 \(q=\operatorname{div}(a,b)\)，令 \(r=\operatorname{mod}(a,b)\)，于是 \(a=r+bq\)（由例 6.6.2）。
那么由递归定义，\(\operatorname{gcd}(a,b)\) 等于 \(\operatorname{gcd}(b,r)\)；由归纳假设，它同时整除 \(b\) 和 \(r\)。我们需要证明它整除 \(b\)（这是立即的）和 \(a\)；现在转向后者。
由于 \(\operatorname{gcd}(a,b)\mid b\)，存在整数 \(k\)，使得 \(b = \operatorname{gcd}(a,b)k\)；又由于 \(\operatorname{gcd}(a,b)\mid r\)，存在整数 \(l\)，使得 \(r = \operatorname{gcd}(a,b)l\)。于是有
所以 \(\operatorname{gcd}(a,b)\mid a\)。
情形 2（\(b<0\)）：令 \(q=\operatorname{div}(a,-b)\)，令 \(r=\operatorname{mod}(a,-b)\)，于是 \(a=r+(-b)q\)（由例 6.6.2）。
那么由递归定义，\(\operatorname{gcd}(a,b)\) 等于 \(\operatorname{gcd}(b,r)\)；由归纳假设，它同时整除 \(b\) 和 \(r\)。我们需要证明它整除 \(b\)（这是立即的）和 \(a\)；现在转向后者。
由于 \(\operatorname{gcd}(a,b)\mid b\)，存在整数 \(k\)，使得 \(b = \operatorname{gcd}(a,b)k\)；又由于 \(\operatorname{gcd}(a,b)\mid r\)，存在整数 \(l\)，使得 \(r = \operatorname{gcd}(a,b)l\)。于是有
所以 \(\operatorname{gcd}(a,b)\mid a\)。
情形 3（\(b=0\)，\(0\le a\)）：此时 \(\operatorname{gcd}(a,b)=a\)，它是 \(a\) 的因子，因为 \(a\cdot 1=a\)；也是 \(b\) 的因子，因为
情形 4（\(b=0\)，\(a<0\)）：此时 \(\operatorname{gcd}(a,b)=-a\)，它是 \(a\) 的因子，因为 \(-a\cdot -1=a\)；也是 \(b\) 的因子，因为
可以在 Lean 中用一个“且”目标的结构来建立这个证明，如下所示：（其中 _ 只是用于展示基本结构的占位符。）
theorem gcd_dvd (a b : ℤ) : gcd a b ∣ b ∧ gcd a b ∣ a := by
rw [gcd]
split_ifs with h1 h2 <;> push_neg at *
· -- case `0 < b`
have IH : _ ∧ _ := gcd_dvd b (fmod a b) -- inductive hypothesis
obtain ⟨IH_right, IH_left⟩ := IH
constructor
· -- prove that `gcd a b ∣ b`
sorry
· -- prove that `gcd a b ∣ a`
sorry
· -- case `b < 0`
have IH : _ ∧ _ := gcd_dvd b (fmod a (-b)) -- inductive hypothesis
obtain ⟨IH_right, IH_left⟩ := IH
constructor
· -- prove that `gcd a b ∣ b`
sorry
· -- prove that `gcd a b ∣ a`
sorry
· -- case `b = 0`, `0 ≤ a`
constructor
· -- prove that `gcd a b ∣ b`
sorry
· -- prove that `gcd a b ∣ a`
sorry
· -- case `b = 0`, `a < 0`
constructor
· -- prove that `gcd a b ∣ b`
sorry
· -- prove that `gcd a b ∣ a`
sorry
termination_by gcd_dvd a b => b
但在任务 \(\operatorname{gcd}(a,b)\mid b\) 和任务 \(\operatorname{gcd}(a,b)\mid a\) 之间不断切换，有点难以跟踪。更优雅的设置是使用两个独立引理：一个证明 \(\operatorname{gcd}(a,b)\mid b\)，另一个证明 \(\operatorname{gcd}(a,b)\mid a\)，其结构如下：
theorem gcd_dvd_right (a b : ℤ) : gcd a b ∣ b := by
rw [gcd]
split_ifs with h1 h2 <;> push_neg at *
· -- case `0 < b`
have IH := gcd_dvd_left b (fmod a b) -- inductive hypothesis
· -- case `b < 0`
have IH := gcd_dvd_left b (fmod a (-b)) -- inductive hypothesis
· -- case `b = 0`, `0 ≤ a`
sorry
· -- case `b = 0`, `a < 0`
sorry
theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a := by
rw [gcd]
split_ifs with h1 h2 <;> push_neg at *
· -- case `0 < b`
have IH1 := gcd_dvd_left b (fmod a b) -- inductive hypothesis
have IH2 := gcd_dvd_right b (fmod a b) -- inductive hypothesis
sorry
· -- case `b < 0`
have IH1 := gcd_dvd_left b (fmod a (-b)) -- inductive hypothesis
have IH2 := gcd_dvd_right b (fmod a (-b)) -- inductive hypothesis
sorry
· -- case `b = 0`, `0 ≤ a`
sorry
· -- case `b = 0`, `a < 0`
sorry
但现在强归纳结构变复杂了：gcd_dvd_right 的证明依赖较小 \(a,b\) 值处的 gcd_dvd_left，而 gcd_dvd_left 的证明又依赖较小 \(a,b\) 值处的 gcd_dvd_right。这称为相互归纳，在 Lean 中有特殊语法：两个定理被包在一个 mutual 块中，末尾给出共同的终止性说明，如下：
mutual
theorem gcd_dvd_right (a b : ℤ) : gcd a b ∣ b := by
...
theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a := by
...
end
termination_by gcd_dvd_right a b => b ; gcd_dvd_left a b => b
下面是完整的 Lean 证明。
mutual
theorem gcd_dvd_right (a b : ℤ) : gcd a b ∣ b := by
rw [gcd]
split_ifs with h1 h2 <;> push_neg at *
· -- case `0 < b`
apply gcd_dvd_left b (fmod a b) -- inductive hypothesis
· -- case `b < 0`
apply gcd_dvd_left b (fmod a (-b)) -- inductive hypothesis
· -- case `b = 0`, `0 ≤ a`
have hb : b = 0 := le_antisymm h1 h2
use 0
calc b = 0 := hb
_ = a * 0 := by ring
· -- case `b = 0`, `a < 0`
have hb : b = 0 := le_antisymm h1 h2
use 0
calc b = 0 := hb
_ = -a * 0 := by ring
theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a := by
rw [gcd]
split_ifs with h1 h2 <;> push_neg at *
· -- case `0 < b`
have IH1 := gcd_dvd_left b (fmod a b) -- inductive hypothesis
have IH2 := gcd_dvd_right b (fmod a b) -- inductive hypothesis
obtain ⟨k, hk⟩ := IH1
obtain ⟨l, hl⟩ := IH2
have H : fmod a b + b * fdiv a b = a := fmod_add_fdiv a b
set q := fdiv a b
set r := fmod a b
use l + k * q
calc a = r + b * q := by rw [H]
_ = gcd b r * l + (gcd b r * k) * q := by rw [← hk, ← hl]
_ = gcd b r * (l + k * q) := by ring
· -- case `b < 0`
have IH1 := gcd_dvd_left b (fmod a (-b)) -- inductive hypothesis
have IH2 := gcd_dvd_right b (fmod a (-b)) -- inductive hypothesis
obtain ⟨k, hk⟩ := IH1
obtain ⟨l, hl⟩ := IH2
have H := fmod_add_fdiv a (-b)
set q := fdiv a (-b)
set r := fmod a (-b)
use l - k * q
calc a = r + (-b) * q := by rw [H]
_ = gcd b r * l + (- (gcd b r * k)) * q := by rw [← hk, ← hl]
_ = gcd b r * (l - k * q) := by ring
· -- case `b = 0`, `0 ≤ a`
use 1
ring
· -- case `b = 0`, `a < 0`
use -1
ring
end
termination_by gcd_dvd_right a b => b ; gcd_dvd_left a b => b
上面的证明中有一个新策略：set，它为一个长表达式引入短名称（通常是因为该表达式频繁出现，而你不想反复完整输入）。注意使用它前后目标状态如何变化。
6.7.4. 定义
定义 6.7.1 中描述的过程通常称为欧几里得算法。一个称为扩展欧几里得算法的过程，会在计算 \(\operatorname{gcd}(a,b)\) 的同时计算另外两个函数，我们称之为 \(L(a,b)\) 和 \(R(a,b)\)。
定义
两个整数的函数 \(L\) 和 \(R\) 相互递归定义如下：
\[\begin{split}L(a,b)&= \begin{cases} R(b,\operatorname{mod}(a,b)) & 0< b\\ R(b,\operatorname{mod}(a,-b)) & b<0\\ 1 & b=0\text{ and }0\le a\\ -1 & b=0\text{ and }a <0. \end{cases} \\ R(a,b)&= \begin{cases} L(b,\operatorname{mod}(a,b))-\operatorname{div}(a,b)R(b,\operatorname{mod}(a,b)) & 0< b\\ L(b,\operatorname{mod}(a,-b))+\operatorname{div}(a,-b)R(b,\operatorname{mod}(a,-b)) & b<0\\ 0 & b=0. \end{cases} \\\end{split}\]
我们用和定义 6.7.1 中相同的例子（\(a=-21\)，\(b=15\)），一起练习计算 \(\operatorname{gcd}(a,b)\)、\(L(a,b)\) 和 \(R(a,b)\)。
由于递归过程中同时需要 \(\operatorname{div}\) 和 \(\operatorname{mod}\)，预先一起计算它们会很方便：
（这张表简记了 \(\operatorname{div}(-21,15)=-2\)、\(\operatorname{mod}(-21,15)=9\)，等等。）我们立即得到
和以前一样。为了计算 \(L(a,b)\) 和 \(R(a,b)\)，从后往前推比较方便：
在 Lean 中，这个相互递归定义看起来类似于例 6.7.3 中的相互归纳证明；和那个例子一样，它被包在标记为 mutual 的块中。
mutual
def L (a b : ℤ) : ℤ :=
if 0 < b then
R b (fmod a b)
else if b < 0 then
R b (fmod a (-b))
else if 0 ≤ a then
1
else
-1
def R (a b : ℤ) : ℤ :=
if 0 < b then
L b (fmod a b) - (fdiv a b) * R b (fmod a b)
else if b < 0 then
L b (fmod a (-b)) + (fdiv a (-b)) * R b (fmod a (-b))
else
0
end
termination_by L a b => b ; R a b => b
可靠性检查：Lean 定义是否与我们手算的 \(L(-21,15)\) 和 \(R(-21,15)\) 一致？
#eval L (-21) 15 -- infoview displays `2`
#eval R (-21) 15 -- infoview displays `3`
6.7.5. 例
定义 \(L(a,b)\) 和 \(R(a,b)\) 的原因，是它们满足如下恒等式。
定理
对所有整数 \(a\) 和 \(b\)，
证明
我们对 \(b\) 作强归纳证明。假设对所有满足 \(|y|<|b|\) 的整数 \(x\) 和 \(y\)，都有 \(0 \le \operatorname{gcd}(x, y)\)。
情形 1（\(0<b\)）：令 \(q=\operatorname{div}(a,b)\)，令 \(r=\operatorname{mod}(a,b)\)，于是 \(a=r+bq\)（由例 6.6.2）。
于是由递推定义，
并且由归纳假设，\(L(b,r)b+R(b,r)r=\operatorname{gcd}(b,r)\)。所以
情形 2（\(b<0\)）：令 \(q=\operatorname{div}(a,-b)\)，令 \(r=\operatorname{mod}(a,-b)\)，于是 \(a=r+(-b)q\)（由例 6.6.2）。
于是由递推定义，
并且由归纳假设，\(L(b,r)b+R(b,r)r=\operatorname{gcd}(b,r)\)。所以
情形 3（\(b=0\)，\(0\le a\)）：由递推定义，\(\operatorname{gcd}(a,b)=a\)、\(L(a,b)=1\)、\(R(a,b)=0\)，所以
情形 4（\(b=0\)，\(a<0\)）：由递推定义，\(\operatorname{gcd}(a,b)=-a\)、\(L(a,b)=-1\)、\(R(a,b)=0\)，所以
下面是在 Lean 中的同一个证明。
theorem L_mul_add_R_mul (a b : ℤ) : L a b * a + R a b * b = gcd a b := by
rw [R, L, gcd]
split_ifs with h1 h2 <;> push_neg at *
· -- case `0 < b`
have IH := L_mul_add_R_mul b (fmod a b) -- inductive hypothesis
have H : fmod a b + b * fdiv a b = a := fmod_add_fdiv a b
set q := fdiv a b
set r := fmod a b
calc R b r * a + (L b r - q * R b r) * b
= R b r * (r + b * q) + (L b r - q * R b r) * b:= by rw [H]
_ = L b r * b + R b r * r := by ring
_ = gcd b r := IH
· -- case `b < 0`
have IH := L_mul_add_R_mul b (fmod a (-b)) -- inductive hypothesis
have H : fmod a (-b) + (-b) * fdiv a (-b) = a := fmod_add_fdiv a (-b)
set q := fdiv a (-b)
set r := fmod a (-b)
calc R b r * a + (L b r + q * R b r) * b
= R b r * (r + -b * q) + (L b r + q * R b r) * b := by rw [H]
_ = L b r * b + R b r * r := by ring
_ = gcd b r := IH
· -- case `b = 0`, `0 ≤ a`
ring
· -- case `b = 0`, `a < 0`
ring
termination_by L_mul_add_R_mul a b => b
6.7.6. 例
我们在例 6.7.5 中证明了：对任意整数 \(a\) 和 \(b\)，整数 \(L(a,b)\) 和 \(R(a,b)\) 满足
例如，\(L(7,5)=-2\)、\(R(7,5)=3\)，且 \(\operatorname{gcd}(7,5)=1\)，
#eval L 7 5 -- infoview displays `-2`
#eval R 7 5 -- infoview displays `3`
#eval gcd 7 5 -- infoview displays `1`
并且 \((-2) \cdot 7 + 3 \cdot 5 = 1\)。
但有趣的是，具有该性质的整数对通常并不唯一。例如，
在应用中，通常只需要这个性质，而不需要通过 \(L(a,b)\) 和 \(R(a,b)\) 的具体构造。因此我们把它单独记录下来。这个事实称为贝祖等式。
推论（贝祖等式）
设 \(a\) 和 \(b\) 为整数。则存在整数 \(x\) 和 \(y\)，使得 \(xa+yb=\operatorname{gcd}(a,b)\)。
证明
由例 6.7.5，整数 \(L(a,b)\) 和 \(R(a,b)\) 具有这个性质。
theorem bezout (a b : ℤ) : ∃ x y : ℤ, x * a + y * b = gcd a b := by
use L a b, R a b
apply L_mul_add_R_mul
6.7.7. 练习
证明 \(\operatorname{gcd}(a,b)\) 不仅是 \(a\) 和 \(b\) 的公因子（见例 6.7.3），而且是它们的最大公因子：若整数 \(d\) 同时整除 \(a\) 和 \(b\)，则它整除 \(\operatorname{gcd}(a,b)\)。本题不需要归纳；它是贝祖等式（例 6.7.6）的直接推论。
theorem gcd_maximal {d a b : ℤ} (ha : d ∣ a) (hb : d ∣ b) : d ∣ gcd a b := by sorry