4. 有结构的证明（二）
在第 2 章中，我们学习了逻辑符号 \(\lor\)、\(\land\) 和 \(\exists\)；这些符号允许我们由较简单的数学陈述构造较复杂的数学陈述。对于每一个这样的符号，我们都学习了它的“语法”：当它出现在假设中时如何使用，以及当它出现在目标中时如何使用。这套语法称为自然演绎。
本章完成第 2 章中开始的工作。我们将学习剩余逻辑符号 \(\forall\)、\(\to\) 和 \(\lnot\) 的语法。我们还将学习另外两个逻辑符号 \(\leftrightarrow\) 和 \(\exists!\) 的语法；它们不那么基本，因为它们可以用其他逻辑符号来定义。
4.1. “对所有”与蕴含
4.1.1. 例
问题
设 \(a\) 为实数，并假设对所有实数 \(x\)，都有 \(a\le x^2-2x\)。证明 \(a\le -1\)。
图 4.1 抛物线 \(y= x^2-2x\)。
像上题中的 \(a\le x^2-2x\) 那样，说明某个公式或谓词对于变量 \(x\) 的所有取值都为真，称为对变量 \(x\) 作全称量化。它用符号 ∀ 表示。
为了使用一个带全称量词的假设，你可能需要把它“特化”到某个具体变量。例如，在下面的解答中，我们使用的是假设在 \(x\) 取 1 时的特殊情形。
解答
在 Lean 中，使用 apply 策略完成这种特化。
example {a : ℝ} (h : ∀ x, a ≤ x ^ 2 - 2 * x) : a ≤ -1 :=
calc
a ≤ 1 ^ 2 - 2 * 1 := by apply h
_ = -1 := by numbers
4.1.2. 例
问题
设 \(n\) 为自然数，并且 \(n\) 是每个自然数 \(m\) 的因子。证明 \(n=1\)。
解答
因为 \(n\) 是每个自然数的因子，所以它也是 \(1\) 的因子。还要注意 \(1\) 为正。因此可以调用例 3.2.7 和例 3.2.8 中讨论过的因子大小界：\(n\le 1\) 且 \(1 \le n\)。于是 \(n=1\)。
对于 Lean 证明，我们回忆：例 3.2.7 中的界在 Lean 中名为 Nat.le_of_dvd，例 3.2.8 中的界在 Lean 中名为 Nat.pos_of_dvd_of_pos。
example {n : ℕ} (hn : ∀ m, n ∣ m) : n = 1 := by
have h1 : n ∣ 1 := by apply hn
have h2 : 0 < 1 := by numbers
apply le_antisymm
· apply Nat.le_of_dvd h2 h1
· apply Nat.pos_of_dvd_of_pos h1 h2
4.1.3. 例
问题
设 \(a\) 和 \(b\) 为实数，并假设每个实数 \(x\) 要么不小于 \(a\)，要么不大于 \(b\)。证明 \(a \le b\)。
解答
考虑实数 \(\frac {a+b}{2}\)。它要么不小于 \(a\)，要么不大于 \(b\)。
情形 1：\(\frac {a+b}{2} \geq a\)。于是
情形 2：\(\frac {a+b}{2} \leq b\)。于是
example {a b : ℝ} (h : ∀ x, x ≥ a ∨ x ≤ b) : a ≤ b := by
sorry
4.1.4. 例
问题
设 \(a\) 为实数，满足它的平方至多为 2，并且它大于等于任何平方至多为 2 的实数。1 又设 \(b\) 为另一个具有这两个性质的实数。证明 \(a=b\)。
考虑本题中的如下假设：
\(a\) 大于等于任何平方至多为 2 的实数。
其中隐含着一个全称量化（“任何实数”），也隐含着一个蕴含；因此，更啰嗦但更精确的表述是：
对所有实数 \(y\)，若 \(y^2\le 2\)，则 \(y\le a\)。
我们可以把这样的假设特化到任意一个具体的 \(y\)，只要前件 \(y^2\le 2\) 为真。
解答
因为 \(a^2\le 2\)，且 \(b\) 大于等于任何平方至多为 2 的实数，所以 \(a \le b\)。
因为 \(b^2\le 2\)，且 \(a\) 大于等于任何平方至多为 2 的实数，所以 \(b \le a\)。
因此 \(a=b\)。
在 Lean 中，蕴含用符号 → 表示。apply 策略也适用于含有蕴含的假设。在下面的证明中，执行 apply hb2 之前的目标状态是
a b: ℝ
ha1 : a ^ 2 ≤ 2
hb1 : b ^ 2 ≤ 2
ha2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ a
hb2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ b
⊢ a ≤ b
而执行之后的目标状态是
a b : ℝ
ha1 : a ^ 2 ≤ 2
hb1 : b ^ 2 ≤ 2
ha2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ a
hb2 : ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ b
⊢ a ^ 2 ≤ 2
假设 ∀ (y : ℝ), y ^ 2 ≤ 2 → y ≤ b 已经被应用到目标 a ≤ b 上，留下一个希望更容易的目标 a ^ 2 ≤ 2，也就是证明该蕴含的前件。
补全证明的第二部分。
example {a b : ℝ} (ha1 : a ^ 2 ≤ 2) (hb1 : b ^ 2 ≤ 2) (ha2 : ∀ y, y ^ 2 ≤ 2 → y ≤ a)
(hb2 : ∀ y, y ^ 2 ≤ 2 → y ≤ b) :
a = b := by
apply le_antisymm
· apply hb2
apply ha1
· sorry
4.1.5. 例
问题
证明：存在实数 \(b\)，使得对每个实数 \(x\)，都有 \(b \le x^2-2x\)。
注意，在本题中，目标里出现了一个全称量化陈述：“对每个实数 \(x\)，……”。
解答
我们证明 -1 具有这个性质。确实，设 \(x\) 为实数，则
我们通过形式化地引入一个具体但任意的实数 \(x\)（“设 \(x\) 为实数”），并为这个 \(x\) 证明所需陈述，来解决本题。在 Lean 中，这一论证由 intro 策略完成。使用该策略之前，目标状态是
⊢ ∀ (x : ℝ), -1 ≤ x ^ 2 - 2 * x
使用该策略之后，目标状态是
x : ℝ
⊢ -1 ≤ x ^ 2 - 2 * x
example : ∃ b : ℝ, ∀ x : ℝ, b ≤ x ^ 2 - 2 * x := by
use -1
intro x
calc
-1 ≤ -1 + (x - 1) ^ 2 := by extra
_ = x ^ 2 - 2 * x := by ring
4.1.6. 例
问题
证明：存在实数 \(c\)，使得对所有实数 \(x\) 和 \(y\)，若 \(x^2+y^2\le 4\)，则 \(x+y\geq c\)。
这里目标同时含有对 \(x\) 与 \(y\) 的全称量化，以及一个蕴含：“若 \(x^2+y^2\le 4\)，则……”。解题时，我们形式化地引入变量 \(x\)、\(y\)，也引入它们被假设满足的条件 \(x^2+y^2\le 4\)：
解答
我们证明 -3 具有这个性质。确实，设 \(x\) 和 \(y\) 为实数，并假设 \(x^2+y^2\le 4\)。那么
所以 \(x + y \geq -3\)（并且也有 \(x + y \leq 3\)）。
在 Lean 中，变量 \(x\)、\(y\) 以及假设 \(x^2+y^2\le 4\) 都用 intro 策略引入。若要从 \((x + y) ^ 2 \le 3 ^ 2\) 推出 \(-3 ≤ x + y\) 与 \(x + y ≤ 3\)，需要使用引理
lemma abs_le_of_sq_le_sq' (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) : -y ≤ x ∧ x ≤ y :=
我们先前在例 2.4.2 中见过这个引理。
example : ∃ c : ℝ, ∀ x y, x ^ 2 + y ^ 2 ≤ 4 → x + y ≥ c := by
sorry
4.1.7. 例
定义
一个性质对所有充分大的整数 \(n\) 成立，是指存在一个整数 \(N\)，使得该性质对所有整数 \(n\geq N\) 都成立。
有理数、实数等情形同理。
问题
证明：对所有充分大的整数 \(n\)，都有 \(n ^ 3 ≥ 4n ^ 2 + 7\)。
在下面的解答中，“对所有 \(n\geq 5\)”是“设 \(n\) 为整数并假设 \(n\geq 5\)”的简写。
解答
对所有 \(n\geq 5\)，
我提供了记号 forall_sufficiently_large，用来在 Lean 中表达这个问题以及类似问题。
example : forall_sufficiently_large n : ℤ, n ^ 3 ≥ 4 * n ^ 2 + 7 := by
dsimp
use 5
intro n hn
calc
n ^ 3 = n * n ^ 2 := by ring
_ ≥ 5 * n ^ 2 := by rel [hn]
_ = 4 * n ^ 2 + n ^ 2 := by ring
_ ≥ 4 * n ^ 2 + 5 ^ 2 := by rel [hn]
_ = 4 * n ^ 2 + 7 + 18 := by ring
_ ≥ 4 * n ^ 2 + 7 := by extra
4.1.8. 例
定义
自然数 \(p\) 称为素数，如果它至少为 \(2\)，并且 \(p\) 的因子只有 \(1\) 和 \(p\)。
def Prime (p : ℕ) : Prop :=
2 ≤ p ∧ ∀ m : ℕ, m ∣ p → m = 1 ∨ m = p
问题
证明 2 是素数。
解答
显然 \(2 \le 2\)。设 \(m\) 为 \(2\) 的因子。因为 \(2\) 为正，由例 3.2.7 和例 3.2.8 中讨论过的因子大小界，可得 \(m \le 2\) 且 \(1 \le m\)。满足 \(m \le 2\) 且 \(1 \le m\) 的自然数 \(m\) 只有 \(1\) 和 \(2\)，所以如所需，\(m=1\) 或 \(m=2\)。
这个解答使用了一个新技巧：由自然数的数值上下界（如这里的 \(m \le 2\) 与 \(1 \le m\)）看出只有有限多种可能性（这里是 \(m=1\) 或 \(m=2\)）。在 Lean 中，这类论证使用 interval_cases 策略。它也适用于整数，但不适用于有理数或实数；为什么？
example : Prime 2 := by
constructor
· numbers -- show `2 ≤ 2`
intro m hmp
have hp : 0 < 2 := by numbers
have hmp_le : m ≤ 2 := Nat.le_of_dvd hp hmp
have h1m : 1 ≤ m := Nat.pos_of_dvd_of_pos hmp hp
interval_cases m
· left
numbers -- show `1 = 1`
· right
numbers -- show `2 = 2`
这个引理以后可在 Lean 中用名称 prime_two 调用。
4.1.9. 例
你可能会问，如何证明一个自然数 \(p\) 不是素数。思路是说明它可以写成一个非平凡乘积。
问题
证明 6 不是素数。
解答
\(6=2\cdot 3\)，所以 \(2 \mid 6\)。但 \(2 \ne 1\) 且 \(2 \ne 6\)。
我们会在例 4.5.7 中仔细证明这个判据。现在可以放心使用它。在 Lean 中该引理名为 not_prime。
example : ¬ Prime 6 := by
apply not_prime 2 3
· numbers -- show `2 ≠ 1`
· numbers -- show `2 ≠ 6`
· numbers -- show `6 = 2 * 3`
4.1.10. 练习
设 \(a\) 为有理数，并假设对所有有理数 \(b\)，都有 \(a\ge -3+4b-b^2\)。证明 \(a\ge 1\)。
example {a : ℚ} (h : ∀ b : ℚ, a ≥ -3 + 4 * b - b ^ 2) : a ≥ 1 := sorry
设 \(n\) 为整数，并假设每个介于 1 与 5 之间的整数 \(m\) 都是 \(n\) 的因子。证明 15 是 \(n\) 的因子。（你可能需要复习第 3.5 节。）
example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 15 ∣ n := by sorry
证明：存在自然数 \(n\)，使得每个自然数 \(m\) 都至少为 \(n\)。
example : ∃ n : ℕ, ∀ m : ℕ, n ≤ m := by sorry
证明：存在实数 \(a\)，使得对所有实数 \(b\)，存在实数 \(c\)，满足 \(a + b < c\)。
example : ∃ a : ℝ, ∀ b : ℝ, ∃ c : ℝ, a + b < c := by sorry
证明：对所有充分大的实数 \(x\)，都有 \(x ^ 3 + 3 x ≥ 7 x ^ 2 + 12\)。
example : forall_sufficiently_large x : ℝ, x ^ 3 + 3 * x ≥ 7 * x ^ 2 + 12 := by sorry
证明 45 不是素数。你可以像例 4.1.9 中那样使用 Lean 引理
not_prime。example : ¬(Prime 45) := by sorry
脚注
- 1
- 也就是说，\(a\) 是平方至多为 2 的实数集合中的最大元。
4.2. “当且仅当”
4.2.1. 例
问题
设 \(a\) 为有理数。证明 \(3a+1\le 7\) 当且仅当 \(a\le 2\)。
短语“当且仅当”的含义正如字面所示。本题中，我们必须证明：（1）若 \(3a+1\le 7\)，则 \(a\le 2\)；（2）若 \(a\le 2\)，则 \(3a+1\le 7\)。
解答
首先，假设 \(3a+1\le 7\)。那么
反过来，假设 \(a\le 2\)。那么
在手写证明中，分别用符号 \(\Rightarrow\) 和 \(\Leftarrow\) 标注两个方向是很常见的：
解答
\(\Rightarrow\) 假设 \(3a+1\le 7\)。那么……
\(\Leftarrow\) 假设 \(a\le 2\)。那么……
这种写法适合用于作业、考试、黑板书写等场合。在更正式的写作中（例如本书中），我们省略这些符号，而使用“首先”“反过来”等词语来提示证明的不同部分。
在 Lean 中，“当且仅当”用双蕴含符号 ↔ 表示。由于在底层，“当且仅当”是一个“且”陈述，我们使用与“且”目标相同的策略：constructor。
example {a : ℚ} : 3 * a + 1 ≤ 7 ↔ a ≤ 2 := by
constructor
· intro h
calc a = ((3 * a + 1) - 1) / 3 := by ring
_ ≤ (7 - 1) / 3 := by rel [h]
_ = 2 := by numbers
· intro h
calc 3 * a + 1 ≤ 3 * 2 + 1 := by rel [h]
_ = 7 := by numbers
4.2.2. 例
我们把例 3.5.1 改写为一个当且仅当问题。现在有两件事要证明，其中一件我们以前已经证明过。
问题
设 \(n\) 为整数。证明 \(5n\) 是 \(8\) 的倍数，当且仅当 \(n\) 是 \(8\) 的倍数。
解答
假设 \(8\mid 5n\)。则存在整数 \(a\)，使得 \(5n=8a\)。所以
因此 \(8\mid n\)。
反过来，假设 \(8\mid n\)。则存在整数 \(a\)，使得 \(n=8a\)。所以
因此 \(8\mid 5n\)。
example {n : ℤ} : 8 ∣ 5 * n ↔ 8 ∣ n := by
constructor
· intro hn
obtain ⟨a, ha⟩ := hn
use -3 * a + 2 * n
calc
n = -3 * (5 * n) + 16 * n := by ring
_ = -3 * (8 * a) + 16 * n := by rw [ha]
_ = 8 * (-3 * a + 2 * n) := by ring
· intro hn
obtain ⟨a, ha⟩ := hn
use 5 * a
calc 5 * n = 5 * (8 * a) := by rw [ha]
_ = 8 * (5 * a) := by ring
4.2.3. 例
问题
证明：整数 \(n\) 为奇数，当且仅当它模 2 同余于 1。
解答
首先，假设 \(n\) 为奇数。则存在整数 \(k\)，使得 \(n=2k+1\)。因此 \(n-1=2k\)，所以 \(n-1\) 能被 2 整除，从而 \(n\equiv 1\mod 2\)。
反过来，假设 \(n\equiv 1\mod 2\)。则 \(2\mid n -1\)，所以存在整数 \(k\)，使得 \(n-1=2k\)。于是 \(n=2k+1\)，因此 \(n\) 为奇数。
我们把这个例子命名为 Int.odd_iff_modEq，以便以后使用。
theorem odd_iff_modEq (n : ℤ) : Odd n ↔ n ≡ 1 [ZMOD 2] := by
constructor
· intro h
obtain ⟨k, hk⟩ := h
dsimp [Int.ModEq]
dsimp [(· ∣ ·)]
use k
addarith [hk]
· sorry
4.2.4. 例
现在用同样方式刻画偶性。
问题
证明：整数 \(n\) 为偶数，当且仅当它模 2 同余于 0。
theorem even_iff_modEq (n : ℤ) : Even n ↔ n ≡ 0 [ZMOD 2] := by
constructor
· intro h
obtain ⟨k, hk⟩ := h
dsimp [Int.ModEq]
dsimp [(· ∣ ·)]
use k
addarith [hk]
· sorry
4.2.5. 例
高中阶段所谓“解”方程的概念，实际上对应一个“当且仅当”问题：为了解一个方程，你列出一串数，并证明它们满足该方程，而没有其他数满足该方程。
问题
设 \(x\) 为实数。证明 \(x ^ 2 + x - 6 = 0\)，当且仅当 \(x = -3\) 或 \(x = 2\)。
解答
首先，假设 \(x ^ 2 + x - 6 = 0\)。那么
所以要么 \(x+3=0\)，要么 \(x-2=0\)。若为前者，则 \(x=-3\)；若为后者，则 \(x=2\)。
反过来，若 \(x=-3\)，则
而若 \(x=2\)，则
example {x : ℝ} : x ^ 2 + x - 6 = 0 ↔ x = -3 ∨ x = 2 := by
sorry
4.2.6. 例
问题
设 \(a\) 为整数。证明 \(a^2-5a+5 \le -1\)，当且仅当 \(a\) 为 2 或 3。
解答
首先，假设 \(a^2-5a+5 \le -1\)。那么
所以 \(-1\le 2a-5\le 1\)。因此 \(2 \cdot 2 \le 2a\)，从而 \(2 \le a\)；同理 \(2a ≤ 2 \cdot 3\)，从而 \(a \le 3\)。因为 \(2\le a\le 3\)，所以 \(a\) 是 2 或 3。
反过来，若 \(a=2\)，则
而若 \(a=3\)，则
example {a : ℤ} : a ^ 2 - 5 * a + 5 ≤ -1 ↔ a = 2 ∨ a = 3 := by
sorry
4.2.7. 例
有些库引理具有“当且仅当”的形式。这很方便，因为它们可以代替两个普通引理，两个方向各对应一个。
问题
设 \(n\) 为整数，并假设 \(n ^ 2 - 10 n + 24 = 0\)。证明 \(n\) 为偶数。
解答
我们有
所以要么 \(n-4=0\)，要么 \(n-6=0\)。若为前者，则 \(n=2\cdot 2\)，所以 \(n\) 为偶数；若为后者，则 \(n=2\cdot 3\)，所以 \(n\) 为偶数。
在本题中，我们需要把事实 \((n-4)(n-6)=0\) 转化为“\(n-4=0\) 或 \(n-6=0\)”这一事实。以前（例如例 2.3.4 中），我们会在 Lean 中把这个事实直接代入引理
theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (h : a * b = 0) : a = 0 ∨ b = 0 :=
从而得到如下证明框架：
example {n : ℤ} (hn : n ^ 2 - 10 * n + 24 = 0) : Even n := by
have hn1 :=
calc (n - 4) * (n - 6) = n ^ 2 - 10 * n + 24 := by ring
_ = 0 := hn
have hn2 := eq_zero_or_eq_zero_of_mul_eq_zero hn1
sorry
（练习：完成该证明。）
但库中也有一个 ↔ 形式的引理，它把 eq_zero_or_eq_zero_of_mul_eq_zero 与该陈述的逆向（另一个方向）合并在一起：
theorem mul_eq_zero {a b : ℤ} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
在 Lean 中，我们可以用 rw 策略使用一个 ↔ 引理；它会把假设（或目标）中形如 ↔ 左边的表达式转换为形如 ↔ 右边的表达式。
example {n : ℤ} (hn : n ^ 2 - 10 * n + 24 = 0) : Even n := by
have hn1 :=
calc (n - 4) * (n - 6) = n ^ 2 - 10 * n + 24 := by ring
_ = 0 := hn
rw [mul_eq_zero] at hn1 -- `hn1 : n - 4 = 0 ∨ n - 6 = 0`
sorry
4.2.8. 例
上面在例 4.2.3 中，我们证明了一个整数是奇数当且仅当它模 2 同余于 1，并把它记录为 Int.odd_iff_modEq。现在这也是一个很方便的“当且仅当”库引理，我们可以用它通过模算术来解决奇偶性问题。举例来说，我们重新做一遍例 3.1.5 中的问题。
问题
证明：若整数 \(x\) 和 \(y\) 都为奇数，则 \(x+y+1\) 为奇数。
解答
我们将证明：若 \(x\equiv 1 \mod 2\) 且 \(y\equiv 1 \mod 2\)，则 \(x+y+1\equiv 1 \mod 2\)。确实，
example {x y : ℤ} (hx : Odd x) (hy : Odd y) : Odd (x + y + 1) := by
rw [Int.odd_iff_modEq] at *
calc x + y + 1 ≡ 1 + 1 + 1 [ZMOD 2] := by rel [hx, hy]
_ = 2 * 1 + 1 := by ring
_ ≡ 1 [ZMOD 2] := by extra
4.2.9. 例
利用奇偶性关于模算术的刻画，我们还可以证明例 3.1.9 中跳过证明的定理。
定理
每个整数不是偶数就是奇数。
证明
设 \(n\) 为整数。我们按照 \(n\) 模 2 的余数分类讨论。
若 \(n\equiv 0\mod 2\)，则 \(n\) 为偶数，证明完成。
若 \(n\equiv 1\mod 2\)，则 \(n\) 为奇数，证明完成。
使用例 4.2.3 与例 4.2.4 中的引理 Int.odd_iff_modEq 和 Int.even_iff_modEq，以及策略 mod_cases，把这个证明写成 Lean。我已经写出了开头。
example (n : ℤ) : Even n ∨ Odd n := by
mod_cases hn : n % 2
· left
rw [Int.even_iff_modEq]
apply hn
· sorry
4.2.10. 练习
设 \(x\) 为实数。证明 \(2x-1=11\) 当且仅当 \(x=6\)。
example {x : ℝ} : 2 * x - 1 = 11 ↔ x = 6 := by sorry
设 \(n\) 为整数。证明 63 是 \(n\) 的因子，当且仅当 7 和 9 都是 \(n\) 的因子。
example {n : ℤ} : 63 ∣ n ↔ 7 ∣ n ∧ 9 ∣ n := by sorry
设 \(a\) 和 \(n\) 为整数。证明 \(a\) 是 \(n\) 的倍数，当且仅当 \(a \equiv 0 \mod n\)。
theorem dvd_iff_modEq {a n : ℤ} : n ∣ a ↔ a ≡ 0 [ZMOD n] := by sorry
设 \(a\) 和 \(b\) 为整数，并假设 \(a \mid b\)。证明 \(a \mid 2b^3-b^2+3b\)。注意，这已经作为第 3.2 节中的一道练习出现过。但现在使用上一题证明的引理
Int.dvd_iff_modEq，这类问题会容易得多。example {a b : ℤ} (hab : a ∣ b) : a ∣ 2 * b ^ 3 - b ^ 2 + 3 * b := by sorry
设 \(k\) 为自然数。证明 \(k^2 \le 6\) 当且仅当 \(k\) 为 0、1 或 2。
example {k : ℕ} : k ^ 2 ≤ 6 ↔ k = 0 ∨ k = 1 ∨ k = 2 := by sorry
4.3. “存在唯一”
4.3.1. 例
问题
证明：存在唯一实数 \(a\)，使得 \(3a+1=7\)。
解答
我们将证明 2 是唯一具有这个性质的实数。
首先，我们证明 2 具有这个性质。确实，\(3\cdot 2+1=7\)。
现在，设 \(y\) 为满足 \(3y+1=7\) 的实数。那么
example : ∃! a : ℝ, 3 * a + 1 = 7 := by
use 2
dsimp
constructor
· numbers
intro y hy
calc
y = (3 * y + 1 - 1) / 3 := by ring
_ = (7 - 1) / 3 := by rw [hy]
_ = 2 := by numbers
4.3.2. 例
问题
证明：存在唯一有理数 \(x\)，使得对于每个介于 1 与 3 之间的有理数 \(a\)，都有 \((a-x)^2\le 1\)。
解答
我们将证明 2 是唯一具有这个性质的有理数。
首先，若 \(a\) 是介于 1 与 3 之间的有理数，则 \(-1 \le a-2 \le 1\)，所以由例 2.1.7 可得
现在，设 \(y\) 为有理数，并且对于每个介于 1 与 3 之间的有理数 \(a\)，都有 \((a-y)^2\le 1\)。
因为 1 介于 1 与 3 之间，所以 \((1-y)^2\le 1\)；因为 3 介于 1 与 3 之间，所以 \((3-y)^2\le 1\)。
于是
又由于平方非负，\((y - 2) ^ 2\geq 0\)。因此 \((y - 2) ^ 2= 0\)，所以 \(y - 2= 0\)，从而 \(y = 2\)。
在 Lean 中，例 2.1.7 的结果可作为引理 sq_le_sq' 使用。
example : ∃! x : ℚ, ∀ a, a ≥ 1 → a ≤ 3 → (a - x) ^ 2 ≤ 1 := by
sorry
4.3.3. 例
问题
设 \(x\) 为有理数，并假设存在唯一有理数 \(a\) 满足 \(a^2=x\)。证明 \(x=0\)。
更口语地说：唯一具有唯一平方根的有理数是 0。
解答
我们先证明 \(-a=a\)。确实，
而由于 \(a\) 是唯一满足 \(a^2=x\) 的有理数，这意味着 \(-a=a\)。
由此可得
所以也有 \(x=0\)：
example {x : ℚ} (hx : ∃! a : ℚ, a ^ 2 = x) : x = 0 := by
obtain ⟨a, ha1, ha2⟩ := hx
have h1 : -a = a
· apply ha2
calc
(-a) ^ 2 = a ^ 2 := by ring
_ = x := ha1
have h2 :=
calc
a = (a - -a) / 2 := by ring
_ = (a - a) / 2 := by rw [h1]
_ = 0 := by ring
calc
x = a ^ 2 := by rw [ha1]
_ = 0 ^ 2 := by rw [h2]
_ = 0 := by ring
4.3.4. 例
下面是一个关于整数的重要定理，我们会在本书后面第 6.6 节的练习中证明它。
定理（带余除法定理）
设 \(a\) 和 \(b\) 为整数，且 \(b\) 为正。则存在唯一整数 \(r\)，满足 \(0\le r<b\)，并且 \(a\equiv r\mod b\)。
这个引理使我们能够按照模 \(b\) 的同余类作分类讨论（Lean 策略 mod_cases）。但它实际上更强一些，因为陈述中的“唯一性”部分还提供了额外信息。
在 Lean 库中，它以下列形式可用：
lemma Int.existsUnique_modEq_lt (a b : ℤ) (h : 0 < b) :
∃! r : ℤ, 0 ≤ r ∧ r < b ∧ a ≡ r [ZMOD b] :=
为了更好地理解这个定理，我们只证明它无穷多个情形中的一个。
问题
证明：存在唯一整数 \(r\)，使得 \(0\le r < 5\) 且 \(14\equiv r\mod 5\)。
解答
我们将证明具有这个性质的唯一整数是 4。
首先，我们证明 4 具有这个性质。确实 \(0\le 4 < 5\)，并且由于 \(14 - 4 = 5 \cdot 2\)，有 \(14\equiv 4\mod 5\)。
现在，设 \(r\) 为满足 \(0\le r < 5\) 且 \(14\equiv r\mod 5\) 的整数。则存在整数 \(q\)，使得 \(14-r=5q\)。
我们有
所以由于 \(5\) 为正，\(1<q\)。类似地，我们有
所以由于 \(5\) 为正，\(q<3\)。
因此 \(q\) 必为 2，这是严格介于 1 与 3 之间的唯一整数。于是 \(r=14-5\cdot 2=4\)。
example : ∃! r : ℤ, 0 ≤ r ∧ r < 5 ∧ 14 ≡ r [ZMOD 5] := by
use 4
dsimp
constructor
· constructor
· numbers
constructor
· numbers
use 2
numbers
intro r hr
obtain ⟨hr1, hr2, q, hr3⟩ := hr
have :=
calc
5 * 1 < 14 - r := by addarith [hr2]
_ = 5 * q := by rw [hr3]
cancel 5 at this
have :=
calc
5 * q = 14 - r := by rw [hr3]
_ < 5 * 3 := by addarith [hr1]
cancel 5 at this
interval_cases q
addarith [hr3]
4.3.5. 练习
证明：存在唯一有理数 \(x\)，使得 \(4x-3=9\)。
example : ∃! x : ℚ, 4 * x - 3 = 9 := by sorry
证明：存在唯一自然数 \(n\)，使得对所有自然数 \(a\)，都有 \(n\le a\)。
example : ∃! n : ℕ, ∀ a, n ≤ a := by sorry
证明：存在唯一整数 \(r\)，使得 \(0\le r < 3\) 且 \(11\equiv r\mod 3\)。
example : ∃! r : ℤ, 0 ≤ r ∧ r < 3 ∧ 11 ≡ r [ZMOD 3] := by sorry
4.4. 矛盾的假设
4.4.1. 例
有时我们会遇到两个相互矛盾的假设。此时就不需要再证明别的东西了。两个相互矛盾的假设说明我们所假设的情形其实不可能发生。
这在分类证明中很常见。你可能把问题化为一组情形，在某些情形中证明目标，而在另外一些情形中证明它们不可能发生。
下面是这类推理的一个例子。为了把要点说清楚，我把解答写得非常细。
引理
设 \(x\) 和 \(y\) 为实数，并假设 \(0<xy\) 且 \(0 \le x\)。证明 \(0<y\)。
我们以前已经多次使用过这个事实；它是 cancel 策略背后的事实之一。
证明
我们按照 \(y\) 是否为正分两种情形讨论。
情形 1（\(y \le 0\)）：由于 \(0 \le x\)，我们有
所以 \(0<xy\) 为假。这与假设 \(0< xy\) 矛盾，因此这一情形不可能发生。
情形 2（\(0 < y\)）：这正是我们需要证明的结论，所以证明完成。
在 Lean 中，contradiction 策略通过指出两个相互矛盾的假设来结束一个证明（或子证明）。在这个例子的 Lean 翻译中，注意它使用前的目标状态是
y x : ℝ
h : 0 < x * y
hx : 0 ≤ x
hneg : y ≤ 0
this : ¬0 < x * y
⊢ 0 < y
其中含有相互矛盾的假设 h : 0 < x * y 和 this : ¬0 < x * y。（记住，¬ 是“非”的逻辑符号。如果你没有为假设命名，Lean 会把它标记为 this。）
example {y : ℝ} (x : ℝ) (h : 0 < x * y) (hx : 0 ≤ x) : 0 < y := by
obtain hneg | hpos : y ≤ 0 ∨ 0 < y := le_or_lt y 0
· -- the case `y ≤ 0`
have : ¬0 < x * y
· apply not_lt_of_ge
calc
0 = x * 0 := by ring
_ ≥ x * y := by rel [hneg]
contradiction
· -- the case `0 < y`
apply hpos
4.4.2. 例
得到矛盾的一种很常见方式，是证明若干假设推出某个“显然为假”的数值事实，而这个假的事实可以由 numbers 检查。
问题
设 \(t\) 为小于 3 的整数，并假设 \(t - 1 = 6\)。证明 \(t=13\)。
解答
我们有
但显然 \(7 <3\) 为假，矛盾。因此任何结论（包括 \(t=13\)）都为真。
你可以像前面的例子一样，直接使用 contradiction 策略把这个证明写成 Lean：
example {t : ℤ} (h2 : t < 3) (h : t - 1 = 6) : t = 13 := by
have H :=
calc
7 = t := by addarith [h]
_ < 3 := h2
have : ¬(7 : ℤ) < 3 := by numbers
contradiction
不过这一模式也足够常见，所以 Lean 中有一个简写。若 H 是一个假设，并且它的否定可以由 numbers 证明，那么写 numbers at H 就会关闭目标。
example {t : ℤ} (h2 : t < 3) (h : t - 1 = 6) : t = 13 := by
have H :=
calc
7 = t := by addarith [h]
_ < 3 := h2
numbers at H -- this is a contradiction!
4.4.3. 例
问题
证明：若 \(n^2+n+1\equiv 1\mod 3\)，则 \(n\equiv 0\mod 3\) 或 \(n\equiv 2\mod 3\)。
解答
我们按照 \(n\) 模 3 的余数分类讨论。若 \(n\equiv 0\mod 3\) 或 \(n\equiv 2\mod 3\)，则证明完成。否则 \(n\equiv 1\mod 3\)，于是
矛盾。
注意，在上面的证明中，我们多做了一点工作来得到 \(0\equiv 1\mod 3\) 作为矛盾，而不是得到更容易推出的 \(3\equiv 1\mod 3\)：
在本书中，我们只把满足 \(0 \le i<n\) 且 \(0 \le j<n\) 的同余 \(i\equiv j\mod n\) 视为“显然为真/假”。涉及更大数的同余，我们要求显式地先化简到模 \(n\) 的代表元；正如这里把 \(3=1 ^ 2 + 1 + 1\) 模 3 化为 \(0 + 3 \cdot 1\)，因而化为 \(0\)。
其数学依据是唯一性引理 Int.existsUnique_modEq_lt，见例 4.3.4。
example (n : ℤ) (hn : n ^ 2 + n + 1 ≡ 1 [ZMOD 3]) :
n ≡ 0 [ZMOD 3] ∨ n ≡ 2 [ZMOD 3] := by
mod_cases h : n % 3
· -- case 1: `n ≡ 0 [ZMOD 3]`
left
apply h
· -- case 2: `n ≡ 1 [ZMOD 3]`
have H :=
calc 0 ≡ 0 + 3 * 1 [ZMOD 3] := by extra
_ = 1 ^ 2 + 1 + 1 := by numbers
_ ≡ n ^ 2 + n + 1 [ZMOD 3] := by rel [h]
_ ≡ 1 [ZMOD 3] := hn
numbers at H -- contradiction!
· -- case 3: `n ≡ 2 [ZMOD 3]`
right
apply h
4.4.4. 例
我们在例 4.1.8 中定义了素数，并证明了 2 是素数。现在我们证明该定义的一个轻微改写版本；它在证明其他数为素数时会很方便。
引理
设 \(p\) 为大于等于 2 的自然数。假设对于所有满足 \(1<m<p\) 的自然数 \(m\)，\(m\) 不是 \(p\) 的因子。证明 \(p\) 是素数。
证明
既然已知 \(2 \le p\)，剩下要证明的是“素数”定义的第二部分：设 \(m\) 为 \(p\) 的因子（\(\star\)）；我们必须证明 \(m=1\) 或 \(m=p\)。
由于 \(m\) 是 \(p\) 的因子，我们有 \(1 \le m\)。所以要么 \(m=1\)，要么 \(1<m\)；我们相应地分类讨论。
情形 1（\(m=1\)）：这立即给出目标 \(m=1\) 或 \(m=p\)。
情形 2（\(1<m\)）：由于 \(m\) 是 \(p\) 的因子，我们有 \(m \le p\)。所以要么 \(m=p\)，要么 \(m<p\)；我们相应地分类讨论。
情形 2(i)（\(m=p\)）：这立即给出目标 \(m=1\) 或 \(m=p\)。
情形 2(ii)（\(m<p\)）：现在我们已经证明 \(1<m<p\)，由题目给出的一个事实可知，\(m\) 不是 \(p\) 的因子。这与前面的陈述（\(\star\)）矛盾。
我已经在 Lean 中填好了这个证明的大约一半；请补全其余部分，包括最后的矛盾。如果需要查找关于因子大小界的 Lean 名称，它们在例 3.2.7 和例 3.2.8 中已经证明。
example {p : ℕ} (hp : 2 ≤ p) (H : ∀ m : ℕ, 1 < m → m < p → ¬m ∣ p) : Prime p := by
constructor
· apply hp -- show that `2 ≤ p`
intro m hmp
have hp' : 0 < p := by extra
have h1m : 1 ≤ m := Nat.pos_of_dvd_of_pos hmp hp'
obtain hm | hm_left : 1 = m ∨ 1 < m := eq_or_lt_of_le h1m
· -- the case `m = 1`
left
addarith [hm]
-- the case `1 < m`
sorry
我们把它记录下来，以便以后用 Lean 名称 prime_test 调用。
下面举例说明如何使用这个素性判定引理。
问题
证明 5 是素数。
解答
显然 \(2 ≤ 5\)。设 \(m\) 为满足 \(1<m<5\) 的自然数。我们必须证明 5 不是 \(m\) 的倍数。需要检查三种情形：
情形 1（\(m=2\)）：由于 5 位于 2 的相邻倍数 \(2\cdot 2\) 与 \(2 \cdot 3\) 之间，所以 5 不是 2 的倍数。
情形 2（\(m=3\)）：由于 5 位于 3 的相邻倍数 \(3\cdot 1\) 与 \(3 \cdot 2\) 之间，所以 5 不是 3 的倍数。
情形 3（\(m=4\)）：由于 5 位于 4 的相邻倍数 \(4\cdot 1\) 与 \(4 \cdot 2\) 之间，所以 5 不是 4 的倍数。
example : Prime 5 := by
apply prime_test
· numbers
intro m hm_left hm_right
apply Nat.not_dvd_of_exists_lt_and_lt
interval_cases m
· use 2
constructor <;> numbers
· use 1
constructor <;> numbers
· use 1
constructor <;> numbers
这里 constructor <;> numbers 是如下代码的简写：
constructor
· numbers
· numbers
更一般地，<;> 连接两个策略，并把第二个策略应用到第一个策略产生的每个目标上。
4.4.5. 例
下面是一个更难的例子，它有许多情形。
问题
设 \(a\)、\(b\) 和 \(c\) 为正自然数，满足 \(a^2+b^2=c^2\)。证明 \(3 \le a\)。
满足这个方程的三个数称为一个勾股数组，因为由勾股定理可知，这意味着它们构成一个直角三角形的三边。自然数 3、4、5 满足这个方程：\(3^2+4^2=5^2\)。还有其他解，例如 5、12、13；但本题要证明 3、4、5 是最小的解。
解答
要么 \(a \le 2\)，要么 \(3 \le a\)。如果 \(3 \le a\)，则证明完成。若 \(a \le 2\)，我们将导出矛盾。
要么 \(b \le 1\)，要么 \(2 \le b\)。我们分别讨论这两种情形。
情形 1（\(b \le 1\)）：
我们有
这推出 \(c<3\)。现在我们有上界 \(a \le 2\)、\(b \le 1\)、\(c < 3\)，因此 \(a\) 为 1 或 2，\(b\) 为 1，且 \(c\) 为 1 或 2。我们可以分析所有这些情形，并检查它们都不成立：
情形 2（\(2 \le b\)）：
我们有
所以 \(b<c\)，从而 \(b+1\le c\)。但另一方面
所以 \(c<b+1\)，从而 \(b+1\le c\) 为假。这两个事实相互矛盾。
请把这个证明写成 Lean。它会比较长；我的版本有 27 行。
example {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(h_pyth : a ^ 2 + b ^ 2 = c ^ 2) : 3 ≤ a := by
sorry
4.4.6. 练习
设 \(x\) 和 \(y\) 为实数，其中 \(x\) 非负；又设 \(n\) 为正自然数。证明：若 \(y^n \le x^n\)，则 \(y\le x\)。我们以前已经使用过这个事实；它也是
cancel策略背后的引理之一。example {x y : ℝ} (n : ℕ) (hx : 0 ≤ x) (hn : 0 < n) (h : y ^ n ≤ x ^ n) : y ≤ x := by sorry
证明：若 \(n^2\equiv 4\mod 5\)，则 \(n\equiv 2\mod 5\) 或 \(n\equiv 3\mod 5\)。
example (n : ℤ) (hn : n ^ 2 ≡ 4 [ZMOD 5]) : n ≡ 2 [ZMOD 5] ∨ n ≡ 3 [ZMOD 5] := by sorry
证明 7 是素数。
example : Prime 7 := by sorry
给出第 2.1 节练习中一道题的另一种证明：设 \(x\) 为有理数，满足平方为 4，并且大于 1。证明 \(x=2\)。不要使用
cancel策略；请直接使用本节思想：分成两种情形，然后排除其中一种。（你可能会发现推出一个数值矛盾会很方便。）example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by have h3 := calc (x + 2) * (x - 2) = x ^ 2 + 2 * x - 2 * x - 4 := by ring _ = 0 := by addarith [h1] rw [mul_eq_zero] at h3 sorry
证明一个素数要么等于 2，要么为奇数。
example (p : ℕ) (h : Prime p) : p = 2 ∨ Odd p := by sorry
4.5. 反证法
4.5.1. 例
问题
证明：并非对所有实数 \(x\)，都有 \(x^2\geq x\)。
解答
假设对所有实数 \(x\)，都有 \(x^2\geq x\)。那么特别地 \(0.5^2\geq 0.5\)，但这是假的，矛盾。
example : ¬ (∀ x : ℝ, x ^ 2 ≥ x) := by
intro h
have : 0.5 ^ 2 ≥ 0.5 := h 0.5
numbers at this
4.5.2. 例
问题
证明 13 不是 3 的倍数。
过去我们曾用定理 Nat.not_dvd_of_exists_lt_and_lt 来建立不整除事实。但现在我们终于有工具从第一原理证明它。
解答
假设 13 是 3 的倍数。那么存在自然数 \(k\)，使得 \(13=3k\)。
情形 1，\(k \le 4\)：那么
矛盾。
情形 2，\(k \ge 5\)：那么
矛盾。
example : ¬ 3 ∣ 13 := by
intro H
obtain ⟨k, hk⟩ := H
obtain h4 | h5 := le_or_succ_le k 4
· have h :=
calc 13 = 3 * k := hk
_ ≤ 3 * 4 := by rel [h4]
numbers at h
· sorry
4.5.3. 例
问题
设 \(x\) 和 \(y\) 为实数，并假设 \(x+y=0\)。证明 \(x\) 与 \(y\) 不可能同时为正。
解答
假设 \(x\) 与 \(y\) 都为正。那么
矛盾。
example {x y : ℝ} (h : x + y = 0) : ¬(x > 0 ∧ y > 0) := by
intro h
obtain ⟨hx, hy⟩ := h
have H :=
calc 0 = x + y := by rw [h]
_ > 0 := by extra
numbers at H
4.5.4. 例
问题
证明：不存在自然数 \(n\)，使得 \(n^2=2\)。
（与例 2.3.2 比较。）
解答
假设存在某个整数 \(n\) 满足 \(n^2=2\)。
情形 1，\(n \le 1\)：那么
矛盾。
情形 2，\(n \ge 2\)：那么
矛盾。
example : ¬ (∃ n : ℕ, n ^ 2 = 2) := by
sorry
4.5.5. 例
引理
证明：整数 \(n\) 为偶数，当且仅当它不是奇数。
证明
首先，设 \(n\) 为偶数，并反设它也是奇数。那么 \(n\equiv 0\mod 2\)，但也有 \(n\equiv 1\mod 2\)。所以
矛盾。
现在，假设 \(n\) 不是奇数。由于 \(n\) 必须是偶数或奇数，所以它是偶数。
我们把它记录下来，供以后在 Lean 问题中用名称 Int.even_iff_not_odd 调用。
example (n : ℤ) : Int.Even n ↔ ¬ Int.Odd n := by
constructor
· intro h1 h2
rw [Int.even_iff_modEq] at h1
rw [Int.odd_iff_modEq] at h2
have h :=
calc 0 ≡ n [ZMOD 2] := by rel [h1]
_ ≡ 1 [ZMOD 2] := by rel [h2]
numbers at h -- contradiction!
· intro h
obtain h1 | h2 := Int.even_or_odd n
· apply h1
· contradiction
现在重复这个过程来刻画“非偶”。
引理
证明：整数 \(n\) 为奇数，当且仅当它不是偶数。
example (n : ℤ) : Int.Odd n ↔ ¬ Int.Even n := by
sorry
4.5.6. 例
问题
设 \(n\) 为整数。证明 \(n^2\not\equiv 2 \mod 3\)。
解答
假设 \(n^2\equiv 2 \mod 3\)。我们按照 \(n\) 模 3 的余数分类讨论。
若 \(n\equiv 0 \mod 3\)，则
矛盾。
若 \(n\equiv 1 \mod 3\)，则
矛盾。
最后，若 \(n\equiv 2 \mod 3\)，则
矛盾。
example (n : ℤ) : ¬(n ^ 2 ≡ 2 [ZMOD 3]) := by
intro h
mod_cases hn : n % 3
· have h :=
calc (0:ℤ) = 0 ^ 2 := by numbers
_ ≡ n ^ 2 [ZMOD 3] := by rel [hn]
_ ≡ 2 [ZMOD 3] := by rel [h]
numbers at h -- contradiction!
· sorry
· sorry
4.5.7. 例
现在我们可以偿还几笔账。首先，有如下定理，它最早在例 4.1.9 中提到：
定理
设 \(p\)、\(k\) 和 \(l\) 为自然数，且 \(k\ne 1\)、\(k\ne p\)、\(p=kl\)。则 \(p\) 不是素数。
证明
\(k\) 是 \(p\) 的因子。如果 \(p\) 是素数，那么根据定义，\(p\) 的任意因子 \(x\) 都满足 \(x=1\) 或 \(x=p\)，所以特别地 \(k=1\) 或 \(k=p\)。但这两者都会与假设矛盾。
example {p : ℕ} (k l : ℕ) (hk1 : k ≠ 1) (hkp : k ≠ p) (hkl : p = k * l) :
¬(Prime p) := by
have hk : k ∣ p
· use l
apply hkl
intro h
obtain ⟨h2, hfact⟩ := h
have : k = 1 ∨ k = p := hfact k hk
obtain hk1' | hkp' := this
· contradiction
· contradiction
4.5.8. 例
其次，还有如下定理，它最早在例 3.2.6 中提到：
定理
设 \(a\) 和 \(b\) 为整数。如果存在整数 \(q\)，使得 \(bq<a<b(q + 1)\)，则 \(a\) 不是 \(b\) 的倍数。
这就是我们在 Lean 中以 Int.not_dvd_of_exists_lt_and_lt 调用过的引理。
证明
为导出矛盾，假设 \(a\) 是 \(b\) 的倍数。则存在整数 \(k\)，使得 \(a=bk\)。又设 \(q\) 为满足 \(b q<a<b(q + 1)\) 的整数。
我们先注意到
现在分别从两个已知不等式出发推理。我们先观察到
因此（由于 \(b>0\)）有 \(k < q+1\)。
接着我们观察到
因此（由于 \(b>0\)）有 \(q < k\)，从而 \(q+1 \le k\)。
这两个事实相互矛盾，所以 \(a\) 终究不是 \(b\) 的倍数。
example (a b : ℤ) (h : ∃ q, b * q < a ∧ a < b * (q + 1)) : ¬b ∣ a := by
intro H
obtain ⟨k, hk⟩ := H
obtain ⟨q, hq₁, hq₂⟩ := h
have hb :=
calc 0 = a - a := by ring
_ < b * (q + 1) - b * q := by rel [hq₁, hq₂]
_ = b := by ring
have h1 :=
calc b * k = a := by rw [hk]
_ < b * (q + 1) := hq₂
cancel b at h1
sorry
4.5.9. 例
我们还建立一个素性判定，它比例 4.4.4 中的判定更高效。
定理
设 \(p\) 为至少为 2 的自然数。设 \(T\) 为另一个自然数，其平方大于 \(p\)；并假设每个满足 \(1<m<T\) 的自然数 \(m\) 都不是 \(p\) 的因子。则 \(p\) 是素数。
（注意，在例 4.4.4 的判定中，我们必须检查直到 \(p\) 的每个数都不是 \(p\) 的因子；而使用这个判定，只需检查到大约 \(p\) 的平方根为止。）
证明
由例 4.4.4 中的素性判定，只需证明每个满足 \(1<m<p\) 的自然数 \(m\) 都不是 \(p\) 的因子。设 \(m\) 为这样的自然数。若 \(m < T\)，则由假设可知 \(m\) 不是 \(p\) 的因子。
于是，假设 \(T \le m\)，并且 \(m\) 是 \(p\) 的因子。则存在自然数 \(l\)，使得 \(p= ml\)。自然数 \(l\) 也是 \(p\) 的因子。
我们断言 \(1<l\)。只需证明 \(m \cdot 1 < ml\)，而事实上
我们还断言 \(l<T\)。只需证明 \(Tl < T \cdot T\)，而事实上
既然已经证明 \(1<l<T\)，由假设可知 \(l\) 不是 \(p\) 的因子，矛盾。因此 \(m\) 终究不是 \(p\) 的因子。
example {p : ℕ} (hp : 2 ≤ p) (T : ℕ) (hTp : p < T ^ 2)
(H : ∀ (m : ℕ), 1 < m → m < T → ¬ (m ∣ p)) :
Prime p := by
apply prime_test hp
intro m hm1 hmp
obtain hmT | hmT := lt_or_le m T
· apply H m hm1 hmT
intro h_div
obtain ⟨l, hl⟩ := h_div
have : l ∣ p
· sorry
have hl1 :=
calc m * 1 = m := by ring
_ < p := hmp
_ = m * l := hl
cancel m at hl1
have hl2 : l < T
· sorry
have : ¬ l ∣ p := H l hl1 hl2
contradiction
我们把它记录下来，以便以后用 Lean 名称 better_prime_test 调用。
下面举例说明如何使用这个素性判定引理。我把后面的若干情形留给你检查。
问题
证明 79 是素数。
解答
显然 \(2 ≤ 79\)。还要注意 \(79<9^2\)。设 \(m\) 为满足 \(1<m<9\) 的自然数。我们要证明 79 不是 \(m\) 的倍数。需要检查七种情形：
情形 1（\(m=2\)）：由于 79 位于 2 的相邻倍数 \(2\cdot 39\) 与 \(2 \cdot 40\) 之间，所以 79 不是 2 的倍数。
情形 2（\(m=3\)）：由于 79 位于 3 的相邻倍数 \(3\cdot 26\) 与 \(3 \cdot 27\) 之间，所以 79 不是 3 的倍数。
情形 3（\(m=4\)）：由于 79 位于 4 的相邻倍数 \(4\cdot 19\) 与 \(4 \cdot 20\) 之间，所以 79 不是 4 的倍数。
（5、6、7、8 的情形依此类推。）
example : Prime 79 := by
apply better_prime_test (T := 9)
· numbers
· numbers
intro m hm1 hm2
apply Nat.not_dvd_of_exists_lt_and_lt
interval_cases m
· use 39
constructor <;> numbers
· use 26
constructor <;> numbers
· use 19
constructor <;> numbers
· sorry
· sorry
· sorry
· sorry
4.5.10. 练习
证明：不存在实数 \(t\)，使得 \(t \le 4\) 且 \(t\geq 5\)。
example : ¬ (∃ t : ℝ, t ≤ 4 ∧ t ≥ 5) := by sorry
证明：不存在实数 \(a\)，使得 \(a^2 \le 8\) 且 \(a^3\geq 30\)。
example : ¬ (∃ a : ℝ, a ^ 2 ≤ 8 ∧ a ^ 3 ≥ 30) := by sorry
证明 7 不是偶数。
example : ¬ Int.Even 7 := by sorry
设整数 \(n\) 满足 \(n+3=7\)。证明 \(n\) 不可能既为偶数又是方程 \(n^2=10\) 的解。
example {n : ℤ} (hn : n + 3 = 7) : ¬ (Int.Even n ∧ n ^ 2 = 10) := by sorry
设实数 \(x\) 满足 \(x^2<9\)。证明 \(x\) 不可能小于等于 -3，也不可能大于等于 3。
example {x : ℝ} (hx : x ^ 2 < 9) : ¬ (x ≤ -3 ∨ x ≥ 3) := by sorry
证明：不存在自然数 \(N\)，使得每个大于 \(N\) 的自然数都是偶数。
example : ¬ (∃ N : ℕ, ∀ k > N, Nat.Even k) := by sorry
设 \(n\) 为整数。证明 \(n^2\not\equiv 2 \mod 4\)。
example (n : ℤ) : ¬(n ^ 2 ≡ 2 [ZMOD 4]) := by sorry
证明 1 不是素数。我们把这个引理记录下来，以便以后用名称
not_prime_one调用。example : ¬ Prime 1 := by sorry
证明 97 是素数。
example : Prime 97 := by sorry