1. 计算式证明

本书从熟悉的数的世界开始：\(\mathbb{N}\)，即自然数（本书中包含 0）；\(\mathbb{Z}\)，即整数；\(\mathbb{Q}\)，即有理数；以及 \(\mathbb{R}\)，即实数。我们要解决一些很接近高中代数的问题：从已有等式或不等式推出新的等式或不等式。不过，我们使用的技巧通常并不在高中代数中讲授：构造一条单一的表达式链，把左边与右边连接起来。

1.1. 证明等式

1.1.1. 例

我们从等式的证明开始。下面是上述技巧的一个典型例子。

问题

设 \(a\) 和 \(b\) 为有理数，并且假设 \(a - b = 4\)、\(ab=1\)。证明 \((a+b)^2=20\)。

解答

\[\begin{split}(a+b)^2 &=(a-b)^2+4ab\\ &=4^2+4\cdot 1\\ &=20.\end{split}\]

我们称上面的证明为计算式证明。目标是证明 \((a+b)^2=20\)；为此，我们写出一串等式，从表达式 \((a+b)^2\)（左上）开始，到 \(20\)（右下）结束。这个证明隐含地包含三个步骤：

1. \(\underline{\text{证明 }(a+b)^2=(a-b)^2+4ab}\)：这是纯粹的代数重排；展开并化简后，两边都是同一个量 \(a^2+2ab+b^2\)。

2. \(\underline{\text{证明 }(a-b)^2+4ab=4^2+4\cdot 1}\)：这是纯粹的代换步骤，使用已知事实 \(a-b=4\) 和 \(ab=1\)。

3. \(\underline{\text{证明 }4^2+4\cdot 1=20}\)：这是另一个纯粹的代数步骤。

这是高等数学教材和数学研究中呈现等式证明的最常见方式。这里有一个取舍：对于证明的书写者来说，把证明组织成这种形式通常需要更多工作；但得到的证明短小且易于检查，这对读者是体贴的。

在第 1.3 节中，我们会讨论怎样想出这种风格的证明。现在先关注如何理解它们。

1.1.2. 例

问题

设 \(r\) 和 \(s\) 为实数，并且假设 \(r + 2s = -1\)、\(s = 3\)。证明 \(r = -7\)。

解答

\[\begin{split}r &= (r + 2s) - 2s \\ &= -1 - 2s\\ &= -1 - 2 \cdot 3 \\ &= - 7.\end{split}\]

这个证明隐含地包含四个步骤，它们依次把左边 \(r\) 变换为右边 \(-7\)：

1. \(\underline{\text{证明 }r=(r+2s)-2s}\)：纯粹的代数重排。

2. \(\underline{\text{证明 }(r+2s)-2s=-1 - 2s}\)：这是纯粹的代换步骤，使用已知事实 \(r + 2s = -1\)。

2. \(\underline{\text{证明 }-1-2s=-1 - 2 \cdot 3}\)：这是纯粹的代换步骤，使用已知事实 \(s = 3\)。

4. \(\underline{\text{证明 }-1 - 2 \cdot 3=-7}\)：这是另一个纯粹的代数步骤。

你也许会问，以这种风格呈现证明时有多大的灵活性。常见做法是把证明中的每个表达式单独放在一行，这样第一个表达式就不会孤零零地留在左边。这当然可以；如果涉及的表达式很长、确实需要额外空间，这也很有用。

解答

\[\begin{split}&r \\ &= (r + 2s) - 2s \\ &= -1 - 2s\\ &= -1 - 2 \cdot 3 \\ &= - 7.\end{split}\]

有时学生会想省略等号，或者把等号放在右边。这非常不合惯例；不要这样做！

最后，请注意这些计算以句号结束。整段计算被视为一个句子，而句号结束这个句子。

1.1.3. 例

下一个例子仍然遵循“代数、代换、代数”的模式。请在心里检查每一步。

问题

设 \(a\)、\(b\)、\(m\) 和 \(n\) 为整数，并且假设 \(b^2=2a^2\)、\(am+bn=1\)。证明 \((2an+bm)^2=2\)。

解答

\[\begin{split}(2an + bm) ^ 2 &= 2(am + bn) ^ 2 + (m ^ 2 - 2n ^ 2) (b ^ 2 - 2 a ^ 2) \\ &= 2 \cdot 1 ^ 2 + (m ^ 2 - 2n ^ 2) (2a ^ 2 - 2a ^ 2) \\ & = 2.\end{split}\]

在这个例子中，第一步所需的代数计算

\[(2an + bm) ^ 2= 2(am + bn) ^ 2 + (m ^ 2 - 2n ^ 2) (b ^ 2 - 2 a ^ 2),\]

相当繁重。（这个事实称为 Brahmagupta 恒等式，以约公元 628 年发现它的印度数学家命名。）你也可以选择帮助读者，给出若干中间步骤；其中每一步都能用较简单的代数计算来检查。

解答

\[\begin{split}(2an + bm) ^ 2 &=4a^2n^2+4anbm+b^2m^2\\ &=2(a^2m^2+2anbm+b^2n^2)+(4a^2n^2+b^2m^2-2a^2m^2-2b^2n^2)\\ &= 2(am + bn) ^ 2 + (m ^ 2 - 2n ^ 2) (b ^ 2 - 2 a ^ 2) \\ &= 2 \cdot 1 ^ 2 + (m ^ 2 - 2n ^ 2) (2a ^ 2 - 2a ^ 2) \\ & = 2.\end{split}\]

1.1.4. 例

再看一个例子。仍请在心里检查每一步。注意，你也许会想从“解出” \(a\) 和 \(f\) 开始，即令 \(a=bc/d\)、\(f = de/c\)。但这实际上会让解答更复杂，因为它引入了依赖于 \(d=0\) 与 \(c=0\) 是否成立的不必要分类。直接计算式证明避免了这些分类。

问题

设 \(a\)、\(b\)、\(c\)、\(d\)、\(e\) 和 \(f\) 为整数，并且假设 \(ad = bc\)、\(cf=de\)。证明 \(d(af - be) = 0\)。

解答

\[\begin{split}d(af - be) &= (ad) f - dbe \\ &= (bc) f - dbe \\ &= b (cf) - dbe \\ &= b (d e) - dbe \\ &= 0.\end{split}\]

1.2. 在 Lean 中证明等式

在本书中，我们会用两种方式书写每个证明：一种是文字方式，也就是人类几千年来一直使用的方式；另一种是在一种称为证明助理的计算机系统中书写，这种方法在 20 世纪 60 年代首次被尝试，至今仍相当少见。我们将使用证明助理 Lean 4，它自 2014 年以来由 Leonardo de Moura 领导的团队在 Microsoft Research 等机构开发；同时使用它的标准数学库 Mathlib。

从本节以及后续所有章节开始，每一节都有一个对应的 Lean 文件；阅读时，你应当同时打开它来实验。现在请前往 GitHub 仓库 https://github.com/hrmacbeth/math2001，查看如何把这些代码下载到自己的计算机，或在 Gitpod 云端打开。对初学者推荐使用 Gitpod：只需创建账号即可开始，不必安装 Lean。

Lean 代码被设计为在交互式开发环境（IDE）中编写，这样你在工作时会得到即时反馈。本书假定你使用的 IDE 是 Visual Studio Code；启动 Gitpod 时它会自动打开。

要开始，请在 Visual Studio Code 中转到对应本节的文件 Math2001/01_Proofs_by_Calculation/02_Proving_Equalities_in_Lean。打开这个文件时，你可能会看到一个名为 “Lean Infoview” 的第二面板弹出。现在可以忽略它，甚至关闭它。我们会从第 2 章开始使用 Lean Infoview。

1.2.1. 例

文件中前两行重要代码如下：

example {a b : ℚ} (h1 : a - b = 4) (h2 : a * b = 1) : (a + b) ^ 2 = 20 :=

这是例 1.1.1 的 Lean 表示：

问题

设 \(a\) 和 \(b\) 为有理数，并且假设 \(a - b = 4\)、\(ab=1\)。证明 \((a+b)^2=20\)。

代码 {a b : ℚ} 引入两个变量 a 和 b，它们的类型是 ℚ，也就是有理数的标准数学记号（助记：quotients）。

代码 (h1 : a - b = 4) (h2 : a * b = 1) 引入两个假设，对应题设给出的两个事实 \(a - b = 4\) 与 \(ab=1\)。Lean 中的假设有名称，这里是 h1 和 h2，这样以后可以引用它们。注意，乘法必须用符号 * 显式写出；而在纸上，像 \(ab\) 这样把两个变量相邻书写就表示乘法。

冒号 : 之后是目标，也就是要求我们证明的陈述：(a + b) ^ 2 = 20，即 \((a+b)^2=20\)。Lean 中用符号 ^ 表示乘方。

Lean 的关键特性是：它会在你书写证明时检查证明，并即时反馈证明是否正确。我们在上一节写出的这个问题的解答，是一个单独的计算：

\[\begin{split}(a+b)^2 &=(a-b)^2+4ab\\ &=4^2+4\cdot 1\\ &=20.\end{split}\]

这可以在 Lean 中用关键字 calc 表示为一个“计算块”。计算的各个步骤会逐行写出，类似纸上写法。每一行末尾给出这一行推理为何有效的理由。上一节已经讨论过这三步推理为何有效：

1. \(\underline{\text{证明 }(a+b)^2=(a-b)^2+4ab}\)：代数重排

2. \(\underline{\text{证明 }(a-b)^2+4ab=4^2+4\cdot 1}\)：代换，使用已知事实 \(a-b=4\) 和 \(ab=1\)。

3. \(\underline{\text{证明 }4^2+4\cdot 1=20}\)：代数重排

在 Lean 中，代数重排用策略 ring 表示，代换用策略 rw（rewrite 的缩写）表示。进行代换时，必须按名称指出你正在代入哪些假设。

example {a b : ℚ} (h1 : a - b = 4) (h2 : a * b = 1) : (a + b) ^ 2 = 20 :=
  calc
    (a + b) ^ 2 = (a - b) ^ 2 + 4 * (a * b) := by ring
    _ = 4 ^ 2 + 4 * 1 := by rw [h1, h2]
    _ = 20 := by ring

1.2.2. 例

下面是例 1.1.2 及其证明的 Lean 表示；它在纸上是这样写的：

\[\begin{split}r &= (r + 2s) - 2s \\ &= -1 - 2s\\ &= -1 - 2 \cdot 3 \\ &= - 7.\end{split}\]

在四个标有 Lean 标准占位符 sorry 的位置，各填入适当的 Lean 理由（要么是 ring，要么是带有若干假设的 rw）。1

example {r s : ℝ} (h1 : s = 3) (h2 : r + 2 * s = -1) : r = -7 :=
  calc
    r = r + 2 * s - 2 * s := by sorry
    _ = -1 - 2 * s := by sorry
    _ = -1 - 2 * 3 := by sorry
    _ = -7 := by sorry

在填写这些理由时，你大概已经发现 Lean 中出错会发生什么：某处会出现红色下划线。例如，下面每种写法都会在某处产生红色下划线。请试试看！

拼写错误，例如把 ring 写成 rin
标点错误，例如写成 rw [h2 而不是 rw [h2]
理由中使用了错误的策略，例如应该用 rw 时却写了 ring
为理由中的策略提供了错误信息，例如实际代换的是 h1，却写成 rw [h2]
计算中的数学错误，例如写成 \(1 - 2 * s\) 而不是 \(-1 - 2 * s\)

如果没有任何红色下划线，那么你的证明就是正确的。有时红色下划线很小，所以要仔细看。你还可以查看 VS Code 底部的蓝色状态栏来再次确认。符号 “⊗” 旁边的数字表示文件中有多少个错误；如果没有错误，还会显示一个对勾。

1.2.3. 例

下面是例 1.1.3 及其证明的 Lean 表示；它在纸上是这样写的：

\[\begin{split}(2an + bm) ^ 2 &= 2(am + bn) ^ 2 + (m ^ 2 - 2n ^ 2) (b ^ 2 - 2 a ^ 2) \\ &= 2 \cdot 1 ^ 2 + (m ^ 2 - 2n ^ 2) (2a ^ 2 - 2a ^ 2) \\ & = 2.\end{split}\]

和前面一样，在三个标有占位符 sorry 的位置，填入适当的 Lean 理由。

example {a b m n : ℤ} (h1 : a * m + b * n = 1) (h2 : b ^ 2 = 2 * a ^ 2) :
    (2 * a * n + b * m) ^ 2 = 2 :=
  calc
    (2 * a * n + b * m) ^ 2
      = 2 * (a * m + b * n) ^ 2 + (m ^ 2 - 2 * n ^ 2) * (b ^ 2 - 2 * a ^ 2) := by sorry
    _ = 2 * 1 ^ 2 + (m ^ 2 - 2 * n ^ 2) * (2 * a ^ 2 - 2 * a ^ 2) := by sorry
    _ = 2 := by sorry

1.2.4. 例

最后，下面是例 1.1.4 的 Lean 表示。它在纸上的证明如下：

\[\begin{split}d(af - be) &= (ad) f - dbe \\ &= (bc) f - dbe \\ &= b (cf) - dbe \\ &= b (d e) - dbe \\ &= 0.\end{split}\]

请在 Lean 中完整写出这个证明，并补全每一步的理由。注意，Lean 对运算顺序非常敏感。例如，(x * y) * z、x * (y * z) 和 (y * x) * z 在 Lean 中都表示不同的东西。2 因此，请仔细查看纸上证明的每一步；在重写时，要确保括号精确包住你想要进行代换的那个小表达式。

example {a b c d e f : ℤ} (h1 : a * d = b * c) (h2 : c * f = d * e) :
    d * (a * f - b * e) = 0 :=
  sorry

1.2.5. 练习

下一节，即第 1.3 节，包含许多计算式证明的例子。先不细读那一节的数学内容，请按照书中给出的纸上证明，把其中一些例子输入到 Lean 中。下一节对应的 Lean 文件是 Math2001/01_Proofs_by_Calculation/03_Tips_and_Tricks。

脚注

1: 你是在向 Lean 表示歉意：你还没有为这个断言提供证明！
2: 如果没有括号，例如 x * y * z，那么 Lean 会把表达式尽可能向前结合地加括号，也就是 (x * y) * z。

1.3. 提示与技巧

1.3.1. 例

本节介绍一些实际想出计算式证明的提示与技巧。

问题

设 \(a\) 和 \(b\) 为整数，并且假设 \(a = 2b + 5\)、\(b = 3\)。证明 \(a = 11\)。

由于本题目标是证明 \(a=11\)，我们已经知道解答大致会长成这样：

\[\begin{split}a&=\ldots\\ &=\ldots\\ &=11.\end{split}\]

四处寻找思路时，我们看到一个假设 \(a = 2b + 5\) 的左边正好是 \(a\)。于是把它作为计算的第一步，余下步骤便自然写出。

解答

\[\begin{split}a &= 2b + 5 \\ &= 2 \cdot 3 + 5 \\ &= 11.\end{split}\]

example {a b : ℤ} (h1 : a = 2 * b + 5) (h2 : b = 3) : a = 11 :=
  sorry

1.3.2. 例

更常见的情况是，没有任何假设的左边或右边会精确出现在目标中。下面是一个例子。

问题

设 \(x\) 为整数，并且假设 \(x+4=2\)。证明 \(x=-2\)。

由于本题目标是证明 \(x=-2\)，我们已经知道解答大致会长成这样：

\[\begin{split}x&=\ldots\\ &=\ldots\\ &=-2.\end{split}\]

唯一假设的左边是 \(x+4\)，所以我们通过在 \(x\) 中加上再减去 \(4\)，在目标中制造出一个 \(x+4\)：\(x=(x+4)-4\)。之后证明的其余部分就很容易完成。

解答

\[\begin{split}x&=(x+4)-4\\ &=2-4\\ &=-2.\end{split}\]

example {x : ℤ} (h1 : x + 4 = 2) : x = -2 :=
  sorry

1.3.3. 例

有时，我们需要不止一次执行这种在目标中“制造”某个假设一侧的过程。

问题

设 \(a\) 和 \(b\) 为实数，并且假设 \(a-5b=4\)、\(b+2=3\)。证明 \(a=9\)。

在解答的第一步，我们“制造”出一个 \(a-5b\)；后来在第三步，我们又“制造”出一个 \(b+2\)。

解答

\[\begin{split}a &= (a - 5b) + 5b\\ &= 4 + 5b \\ &= -6 + 5(b + 2) \\ &= -6 + 5 \cdot 3 \\ &= 9.\end{split}\]

example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 :=
  sorry

1.3.4. 例

我们也许需要同时使用加减法和乘除法来“制造”假设的一侧。

问题

设 \(w\) 为有理数，并且假设 \(3w+1=4\)。证明 \(w=1\)。

解答

\[\begin{split}w&=\frac{3w+1}{3}-\frac{1}{3}\\ &=\frac{4}{3}-\frac{1}{3}\\ &=1.\end{split}\]

example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 :=
  sorry

1.3.5. 例

这种技巧也适用于经典的 Algebra I 风格方程。考虑下面的问题：

问题

设 \(x\) 为整数，并且假设 \(2x + 3 = x\)。证明 \(x=-3\)。

你也许学过通过移项和整理来解这种方程，类似这样：

\[\begin{split}2x+3&=x\\ 2x+3-x&=x-x\\ x + 3&= 0\\ x &=-3.\end{split}\]

但这个解答也可以通过“制造”一个 \(2x+3\)，呈现为计算式证明。

解答

\[\begin{split}x&=(2x+3)-x-3\\ &=x-x-3\\ &=-3.\end{split}\]

example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 :=
  sorry

1.3.6. 例

类似地，你可能以前见过如下的联立方程组：

问题

设 \(x\) 和 \(y\) 为整数，并且假设 \(2x-y=4\)、\(y-x+1=2\)。证明 \(x=5\)。

你也许学过通过相加或相减方程来消去不关心的变量，然后解剩下的单变量方程。

\[ \begin{align}\begin{aligned}2x-y&=4 & \hspace{1cm}&(1)\\y-x+1&=2 & \hspace{1cm}&(2)\\(2x-y)+(y-x+1)&=4+2 & \hspace{1cm}&\text{by adding (1) and (2)}\\x +1&=6 & \hspace{1cm}&\\x&=5 & \hspace{1cm}&\end{aligned}\end{align} \]

但这个论证也可以呈现为计算式证明；这样做的好处是，不会出现需要读者自行追踪的神秘一行“把 (1) 与 (2) 相加”。

解答

\[\begin{split}x &=(2x-y)+(y-x+1)-1\\ &=4+2-1\\ &= 5.\end{split}\]

example {x y : ℤ} (h1 : 2 * x - y = 4) (h2 : y - x + 1 = 2) : x = 5 :=
  sorry

1.3.7. 例

下面是另一个通过构造假设的巧妙组合来解联立方程组的例子。

问题

设 \(u\) 和 \(v\) 为有理数，并且假设 \(u+2v=4\)、\(u-2v=6\)。证明 \(u=5\)。

解答

\[\begin{split}u &= \frac{(u+2v)+(u-2v)}{2}\\ &=\frac{4+6}{2}\\ &=5.\end{split}\]

example {u v : ℚ} (h1 : u + 2 * v = 4) (h2 : u - 2 * v = 6) : u = 5 :=
  sorry

1.3.8. 例

再看一个例子。这一次我们必须结合前两个例子的技巧：取假设的不同倍数来消去 \(y\)，然后除以剩下的 \(x\) 的倍数。

问题

设 \(x\) 和 \(y\) 为实数，并且假设 \(x + y = 4\)、\(5x-3y=4\)。证明 \(x=2\)。

解答

\[\begin{split}x &= \frac{3(x+y)+(5x-3y)}{8}\\ &=\frac{3\cdot 4+4}{8}\\ &=2.\end{split}\]

example {x y : ℝ} (h1 : x + y = 4) (h2 : 5 * x - 3 * y = 4) : x = 2 :=
  sorry

1.3.9. 例

最后，我们做几个含有次数大于一的方程的例子。

问题

设 \(a\) 和 \(b\) 为有理数，并且假设 \(a-3=2b\)。证明 \(a ^ 2 - a + 3 = 4 b ^ 2 + 10 b + 9\)。

解答

\[\begin{split}a ^ 2 - a + 3 &=\left[(a-3)^2+6a-9\right]-a+3\\ &=(a-3)^2+5a-6\\ &=(a-3)^2+5[(a-3)+3]-6\\ &=(a-3)^2+5(a-3)+9\\ &=(2b)^2+5(2b)+9\\ &=4b^2+10b+9.\end{split}\]

上面的证明比必要步骤多一些，是为了说明你可能怎样想出这个证明：先通过引入 \((a-3)^2\) 并加减多出来的项来处理 \(a^2\) 项；然后化简；再处理 \(a\) 项；再化简；最后代换并再次化简。它可以缩短为一个尽量简洁的证明：一步大的代数计算、一步代换，再加最后一步代数计算。

解答

\[\begin{split}a ^ 2 - a + 3 &=(a-3)^2+5(a-3)+9\\ &=(2b)^2+5(2b)+9\\ &=4b^2+10b+9.\end{split}\]

example {a b : ℚ} (h1 : a - 3 = 2 * b) : a ^ 2 - a + 3 = 4 * b ^ 2 + 10 * b + 9 :=
  sorry

1.3.10. 例

下面是另一个含有次数大于一的项的例子。

问题

设 \(z\) 为实数，并且假设 \(z^2-2=0\)。证明 \(z ^ 4 - z ^ 3 - z ^ 2 + 2 z + 1=3\)。

解答

\[\begin{split}z ^ 4 - z ^ 3 - z ^ 2 + 2 z + 1 &=(z ^ 2 - z + 1) (z ^ 2 - 2)+3\\ &=(z^2-z+1)\cdot 0+3\\ &=3.\end{split}\]

这看起来几乎太巧了，对吧？在草稿中，我是用你也许学过的多项式长除法想出这个解答的：用 \(z^2-2\) 除 \(z ^ 4 - z ^ 3 - z ^ 2 + 2 z + 1\)，商为 \(z ^ 2 - z + 1\)，余数为 \(3\)。但在证明中，用什么方法发现下列事实并不重要：

\[z ^ 4 - z ^ 3 - z ^ 2 + 2 z + 1=(z ^ 2 - z + 1) (z ^ 2 - 2)+3.\]

这是一个纯粹的代数恒等式，可以通过展开并化简轻松检查，因此你可以直接陈述这个结果，而不必写出发现它的方法。

example {z : ℝ} (h1 : z ^ 2 - 2 = 0) : z ^ 4 - z ^ 3 - z ^ 2 + 2 * z + 1 = 3 :=
  sorry

1.3.11. 练习

为下列各题给出计算式证明。

设 \(x\) 和 \(y\) 为实数，并且假设 \(x = 3\)、\(y = 4x - 3\)。证明 \(y = 9\)。

example {x y : ℝ} (h1 : x = 3) (h2 : y = 4 * x - 3) : y = 9 :=
  sorry

设 \(a\) 和 \(b\) 为整数，并且假设 \(a-b=0\)。证明 \(a=b\)。

example {a b : ℤ} (h : a - b = 0) : a = b :=
  sorry

设 \(x\) 和 \(y\) 为整数，并且假设 \(x-3y=5\)、\(y=3\)。证明 \(x=14\)。

example {x y : ℤ} (h1 : x - 3 * y = 5) (h2 : y = 3) : x = 14 :=
  sorry

设 \(p\) 和 \(q\) 为有理数，并且假设 \(p-2q=1\)、\(q=-1\)。证明 \(p=-1\)。

example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
  sorry

设 \(x\) 和 \(y\) 为有理数，并且假设 \(y+1=3\)、\(x+2y=3\)。证明 \(x=-1\)。

example {x y : ℚ} (h1 : y + 1 = 3) (h2 : x + 2 * y = 3) : x = -1 :=
  sorry

设 \(p\) 和 \(q\) 为整数，并且假设 \(p+4q=1\)、\(q-1=2\)。证明 \(p=-11\)。

example {p q : ℤ} (h1 : p + 4 * q = 1) (h2 : q - 1 = 2) : p = -11 :=
  sorry

设 \(a\)、\(b\) 和 \(c\) 为实数，并且假设 \(a+2b+3c=7\)、\(b+2c=3\)、\(c=1\)。证明 \(a=2\)。

example {a b c : ℝ} (h1 : a + 2 * b + 3 * c = 7) (h2 : b + 2 * c = 3)
    (h3 : c = 1) : a = 2 :=
  sorry

设 \(u\) 和 \(v\) 为有理数，并且假设 \(4u+v=3\)、\(v=2\)。证明 \(u=1/4\)。

example {u v : ℚ} (h1 : 4 * u + v = 3) (h2 : v = 2) : u = 1 / 4 :=
  sorry

设 \(c\) 为有理数，并且假设 \(4c + 1 = 3c - 2\)。证明 \(c = -3\)。

example {c : ℚ} (h1 : 4 * c + 1 = 3 * c - 2) : c = -3 :=
  sorry

设 \(p\) 为实数，并且假设 \(5p - 3 = 3p + 1\)。证明 \(p = 2\)。

example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 :=
  sorry

设 \(x\) 和 \(y\) 为整数，并且假设 \(2x+y=4\)、\(x+y=1\)。证明 \(x=3\)。

example {x y : ℤ} (h1 : 2 * x + y = 4) (h2 : x + y = 1) : x = 3 :=
  sorry

设 \(a\) 和 \(b\) 为实数，并且假设 \(a + 2b = 4\)、\(a - b = 1\)。证明 \(a = 2\)。

example {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 :=
  sorry

设 \(u\) 和 \(v\) 为实数，并且假设 \(u+1=v\)。证明 \(u^2+3u+1=v^2+v-1\)。

example {u v : ℝ} (h1 : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 :=
  sorry

设 \(t\) 为有理数，并且假设 \(t^2-4=0\)。证明 \(t^4 + 3t^3 - 3t^2 - 2t - 2 = 10t+2\)。

example {t : ℚ} (ht : t ^ 2 - 4 = 0) :
    t ^ 4 + 3 * t ^ 3 - 3 * t ^ 2 - 2 * t - 2 = 10 * t + 2 :=
  sorry

\(\!\!\!\!{^*}\) 设 \(x\) 和 \(y\) 为实数，并且假设 \(x + 3 = 5\)、\(2x - yx = 0\)。证明 \(y = 2\)。
```
example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  sorry
```

\(\!\!\!\!{^*}\) 设 \(p\)、\(q\) 和 \(r\) 为有理数，并且假设 \(p + q + r = 0\)、\(pq + pr + qr = 2\)。证明 \(p ^ 2 + q ^ 2 + r ^ 2 = -4\)。

example {p q r : ℚ} (h1 : p + q + r = 0) (h2 : p * q + p * r + q * r = 2) :
    p ^ 2 + q ^ 2 + r ^ 2 = -4 :=
  sorry

1.4. 证明不等式

1.4.1. 例

计算式证明也很适合证明不等式，也就是含有 \(<\)、\(\le\)、\(>\) 或 \(\ge\) 的事实。考虑下面这个完整例子：

问题

设 \(x\) 和 \(y\) 为整数，并且假设 \(x + 3 \le 2\)、\(y + 2x\geq 3\)。证明 \(y>3\)。

解答

\[\begin{split}y&=(y+2x)-2x\\ &\geq 3 - 2x\\ &=9 - 2(x+3)\\ &\geq 9 - 2 \cdot 2\\ &> 3.\end{split}\]

目标是证明 \(y>3\)，我们通过写出一串不等式来完成证明；这串不等式从表达式 \(y\)（左上）开始，到 \(3\)（右下）结束。这个证明隐含地包含五个步骤：

1. \(\underline{\text{证明 }y=(y+2x)-2x}\)：代数重排。

2. \(\underline{\text{证明 }(y+2x)-2x\geq 3-2x}\)：这使用给定事实 \(y + 2x\geq 3\)，以及不等式在减去同一个量时保持方向的一般规则（\(A\geq B\) 蕴含 \(A-C\geq B-C\)）。

3. \(\underline{\text{证明 }3-2x=9-2(x+3)}\)：代数重排

4. \(\underline{\text{证明 }9-2(x+3)\geq 9-2\cdot 2}\)：这使用给定事实 \(x + 3 \le 2\)，以及两条一般规则：不等式在乘以正数时保持方向（若 \(C\geq 0\)，则 \(A\geq B\) 蕴含 \(CA\geq CB\)），并且在作减法时方向反转（\(A\geq B\) 蕴含 \(C-B\geq C-A\)）。

5. \(\underline{\text{证明 }9-2\cdot 2>3}\)：这是一个数值事实，可由直接计算和比较证明。

请仔细思考第 2 步和第 4 步。它们很像等式的计算式证明中我们称为“代换步骤”的那些步骤（在 Lean 中是 rw）。例如，

第 2 步看起来像是把不等式 \(y + 2x\geq 3\) “代入”表达式 \((y+2x)-2x\)，得到 \((y+2x)-2x\geq 3-2x\)；
第 4 步看起来像是把不等式 \(x + 3 \le 2\) “代入”表达式 \(9-2(x+3)\)，得到 \(9-2(x+3)\geq 9-2\cdot 2\)。

但它们并不是直接代换；相反，它们使用的是前面提到的关于不等式在减法、乘法等运算下保持或反转方向的规则。有些情况下并不存在相关规则。例如，由 \(x \le y\) 通常既不能推出 \(\sin x \le \sin y\)，也不能推出 \(\sin x \ge \sin y\)。

还要仔细看每一步标出的关系。第一步是 \(=\)，第二步是 \(\geq\)，第三步是 \(=\)，第四步是 \(\geq\)，最后一步是 \(>\)。每一种关系都反映了该步所用的具体推理。最终结果是 \(>\)，因为可以说 \(>\) 优先于 \(\geq\) 和 \(=\)（而且 \(\geq\) 又优先于 \(=\)）。也就是说，如果你知道 \(A\geq B\) 且 \(B>C\)，那么它们可以传递地合成为 \(>\) 关系：\(A>C\)。

现在我们在 Lean 中解同一道题。

代数重排步骤和前面一样，用 ring 说明理由。
“类似代换”的步骤用策略 rel 说明理由，并指出正在“代入”的不等式；但要注意，如果相关运算下不存在保持或反转不等式方向的规则，那么在这种情况下使用它会失败。
“数值事实”用策略 numbers 说明理由。（这个策略也可以说明关于等式的“数值事实”，例如 \(4^2+4\cdot 1=20\)；我们之前对此使用的是 ring 策略。）

example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 :=
  calc
    y = y + 2 * x - 2 * x := by ring
    _ ≥ 3 - 2 * x := by rel [hy]
    _ = 9 - 2 * (x + 3) := by ring
    _ ≥ 9 - 2 * 2 := by rel [hx]
    _ > 3 := by numbers

1.4.2. 例

下面是另一个不等式计算式证明的完整例子。

问题

设 \(r\) 和 \(s\) 为有理数，并且假设 \(s+3\geq r\)、\(s+r \leq 3\)。证明 \(r\leq 3\)。

解答

\[\begin{split}r&=\frac{(s+r)+r-s}{2}\\ &\leq \frac{3+(s+3)-s}{2}\\ &=3.\end{split}\]

目标是证明 \(r\leq 3\)，该证明隐含地包含三个步骤：

1. \(\underline{\text{证明 }r=\frac{(s+r)+r-s}{2}}\)：代数重排。

2. \(\underline{\text{证明 }\frac{(s+r)+r-s}{2}\leq \frac{3+(s+3)-s}{2}}\)：这里是在“代入”给定事实 \(s+3\geq r\) 和 \(s+r \leq 3\)，使用的是不等式在加法下、以及在除以正数下保持方向的规则（并且还隐含地使用了 2 为正）。

3. \(\underline{\text{证明 }\frac{3+(s+3)-s}{2}=3}\)：代数重排。

这一次，第一步的关系是 \(=\)，第二步是 \(\leq\)，第三步是 \(=\)，而“净结果”就是关系 \(\leq\)。

练习：补全下面这个 Lean 解答中的 sorry。

example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 :=
  calc
    r = (s + r + r - s) / 2 := by sorry
    _ ≤ (3 + (s + 3) - s) / 2 := by sorry
    _ = 3 := by sorry

1.4.3. 例

再看一个类似的问题：

问题

设 \(x\) 和 \(y\) 为实数，并且假设 \(y\leq x+5\)、\(x\leq -2\)。证明 \(x+y<2\)。

解答

\[\begin{split}x + y &\leq x + (x + 5)\\ &= 2x+5 \\ &\leq 2\cdot -2 +5\\ &< 2.\end{split}\]

练习：在 Lean 中表示这个问题的解答。

example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 :=
  sorry

1.4.4. 例

在下面的问题中，请注意 \(0<A\leq 1\) 和 \(x,y\leq B\) 等简写，它们用来简洁地表达若干相关不等式。你可以查看后面的 Lean 陈述，看看这些简写更明确地表示什么。

问题

设 \(u, v, x, y, A\) 和 \(B\) 为实数。假设已知 \(0<A\leq 1, B\geq 1, x,y\leq B, 0\leq u<A\) 且 \(0\leq v<A\)。证明 \(uy+vx+uv<3AB\)。

解答

\[\begin{split}uy+vx+uv&\leq uB+vB+uv\\ &\leq AB+AB+Av\\ &\leq AB+AB+1\cdot v\\ &\leq AB+AB+Bv\\ &<AB+AB+BA \vphantom{>}\\ &=3AB.\end{split}\]

在这个计算中，多次使用了关于不等式在乘法下保持方向的规则。例如，在第一步 \(uy+vx+uv\leq uB+vB+uv\) 中，使用给定事实 \(x\leq B\) 和 \(y\leq B\)，并结合规则：不等式 \(≤\) 在乘以非负常数时保持方向（这里的常数是 \(u\)）。在第二步 \(uB+vB+uv\leq AB+AB+Av\) 中，给定事实 \(u< A\) 和 \(v< A\) 分别乘以非负常数 \(B\) 和 \(v\)。

重要的是，如果某个非负性证明是“显然”的，那么通常可以省略对你所乘常数非负性的形式证明。例如在这个例子中，\(B\) 的非负性来自给定假设 \(B\geq 1\)。Lean 策略 rel 也被设置为能推断这些“显然”的正性和非负性证明。

练习：补全下面这个 Lean 解答中的 sorry。你需要判断每一步使用了九个假设中的哪一个。

example {u v x y A B : ℝ} (h1 : 0 < A) (h2 : A ≤ 1) (h3 : 1 ≤ B) (h4 : x ≤ B)
    (h5 : y ≤ B) (h6 : 0 ≤ u) (h7 : 0 ≤ v) (h8 : u < A) (h9 : v < A) :
    u * y + v * x + u * v < 3 * A * B :=
  calc
    u * y + v * x + u * v
      ≤ u * B + v * B + u * v := by sorry
    _ ≤ A * B + A * B + A * v := by sorry
    _ ≤ A * B + A * B + 1 * v := by sorry
    _ ≤ A * B + A * B + B * v := by sorry
    _ < A * B + A * B + B * A := by sorry
    _ = 3 * A * B := by sorry

1.4.5. 例

下面是一个有一点微妙之处的例子。

问题

证明：若 \(t\) 为实数且 \(t\geq 10\)，则 \(t^2-3t+17\geq 5\)。

看到假设 \(t\geq 10\) 时，你也许会想把它直接“代入”表达式 \(t^2-3t+17\)。

这不是一个有效解答！由 \(t\geq 10\) 可以推出 \(t^2\geq 10^2\)（有一般规则：平方保持非负数之间的不等式），也可以推出 \(3t\geq 3\cdot 10\)（把不等式乘以非负常数）。但第二个不等式在取负时会反向，得到 \(-3t\leq -3\cdot 10\)，因此我们无法判断 \(t^2-3t+17\) 与 \(10^2-3\cdot 10+17\) 的相对大小。

下面是本题的一个有效解答。我们不是立即从 \(t^2\) 降到 \(10^2\)，而是“降到一半”，到 \(10t\)。这样它就能抵消 \(-3t\) 项，与其合并成 \(7t\)；这个项的系数为正而非负，从而允许对给定事实 \(t\geq 10\) 作有效的进一步代换。

解答

\[\begin{split}t^2-3t+17&=t\cdot t-3t+17\\ &\geq 10t-3t+17\\ &=7t+17\\ &\geq 7\cdot 10+17\\ &\geq 5.\end{split}\]

练习：补全下面这个 Lean 解答中的 sorry。也请试着在 Lean 中写出那个错误解答，并检查 Lean 是否会报错。

example {t : ℚ} (ht : t ≥ 10) : t ^ 2 - 3 * t - 17 ≥ 5 :=
  calc
    t ^ 2 - 3 * t - 17
      = t * t - 3 * t - 17 := by sorry
    _ ≥ 10 * t - 3 * t - 17 := by sorry
    _ = 7 * t - 17 := by sorry
    _ ≥ 7 * 10 - 17 := by sorry
    _ ≥ 5 := by sorry

1.4.6. 例

下面还有一个容易出错的问题。

问题

设 \(n\geq 5\) 为整数。证明 \(n ^ 2 > 2n + 11\)。

注意，“设 \(n\geq 5\) 为整数”（如上题所用）是常见简写，意思是“设 \(n\) 为整数，并假设 \(n\geq 5\)”。

下面是本题一个错误的“代换”解答：

\[\begin{split}n^2&\geq 5^2\\ &> 2 \cdot 5+11\\ &\leq 2n+11.\end{split}\]

错在哪里？每一个单独的推理都是有效的：

\(n^2\geq 5^2\)
\(5^2> 2 \cdot 5+11\)
\(2 \cdot 5+11\leq 2n+11\)

但是符号序列 \(\geq\)、\(>\)、\(\leq\) 不能传递地合并。（如果 \(A>B\) 且 \(B\leq C\)，我们无法得出 \(A\) 与 \(C\) 相对大小的结论。）

下面是本题的正确解答。技巧仍然是在第一步更细致一些：先只从 \(n^2\) 降到 \(5n\)，而不是降到 \(5^2\)。

解答

\[\begin{split}n^2&=n\cdot n\\ &\geq 5n\\ &=2n+3n\\ &\geq 2n + 3 \cdot 5\\ &= 2n + 11 + 4\\ &>2n+11.\end{split}\]

练习：在 Lean 中表示这个问题的解答。也请试着在 Lean 中写出那个错误解答，并检查 Lean 是否会报错。

example {n : ℤ} (hn : n ≥ 5) : n ^ 2 > 2 * n + 11 :=
  sorry

事实上，在写出正确解答时，你可能会发现最后一步很难说明理由。学完下一个例子后，再回来看那一步。

1.4.7. 例

下一个例子包含一个新技巧。

问题

设 \(m\) 和 \(n\) 为整数，并且假设 \(m ^ 2 + n \le 2\)。证明 \(n \le 2\)。

我们通过观察平方为正来解决这个问题，所以 \(n\) 必定小于 \(m ^ 2 + n\)。（严格地说，是“小于或等于”。）因此，既然 \(m ^ 2 + n\) 有上界 2，这个上界也必定适用于更小的数 \(n\)。

解答

\[\begin{split}n&\le m ^ 2 + n\\ &\le 2.\end{split}\]

Lean 知道平方为正，并能默默处理这种论证。

example {m n : ℤ} (h : m ^ 2 + n ≤ 2) : n ≤ 2 :=
  calc
    n ≤ m ^ 2 + n := by extra
    _ ≤ 2 := by rel [h]

1.4.8. 例

利用平方非负是证明不等式的一种非常常见的方法。下面是另一个例子，在其中要想出恰好应该加上的平方 \((x-y)^2\)，需要一点巧思。

问题

设 \(x\) 和 \(y\) 为实数，并且假设 \(x ^ 2 + y ^ 2 \le 1\)。证明 \((x + y) ^ 2 < 3\)。

解答

\[\begin{split}(x + y) ^ 2 &\le (x + y) ^ 2 + (x - y) ^ 2\\ &= 2 (x ^ 2 + y ^ 2)\\ &\le 2 \cdot 1\\ &< 3.\end{split}\]

练习：补全下面这个 Lean 解答中的 sorry。

example {x y : ℝ} (h : x ^ 2 + y ^ 2 ≤ 1) : (x + y) ^ 2 < 3 :=
  calc
    (x + y) ^ 2 ≤ (x + y) ^ 2 + (x - y) ^ 2 := by sorry
    _ = 2 * (x ^ 2 + y ^ 2) := by sorry
    _ ≤ 2 * 1 := by sorry
    _ < 3 := by sorry

1.4.9. 例

同一个技巧再来一次……

问题

设 \(a\) 和 \(b\) 为非负有理数，并且假设 \(a+b\leq 8\)。证明 \(3ab+a \leq 7b+72\)。

解答

\[\begin{split}3ab+a&\leq 2b^2+a^2+(3ab+a)\\ &=2(a+b)b+(a+b)a+a\\ &\leq 2\cdot 8b+8a+a\\ &=7b+9(a+b)\\ &\leq 7b+9\cdot 8\\ &=7b+72.\end{split}\]

练习：补全下面这个 Lean 解答中的 sorry。

example {a b : ℚ} (h1 : a ≥ 0) (h2 : b ≥ 0) (h3 : a + b ≤ 8) :
    3 * a * b + a ≤ 7 * b + 72 :=
  calc
    3 * a * b + a
      ≤ 2 * b ^ 2 + a ^ 2 + (3 * a * b + a) := by sorry
    _ = 2 * ((a + b) * b) + (a + b) * a + a := by sorry
    _ ≤ 2 * (8 * b) + 8 * a + a := by sorry
    _ = 7 * b + 9 * (a + b) := by sorry
    _ ≤ 7 * b + 9 * 8 := by sorry
    _ = 7 * b + 72 := by sorry

1.4.10. 例

最后，这是这个技巧的一个特别惊人的例子3，它调用了三个不同平方的非负性：\((a ^ 2 (b ^ 2 - c ^ 2)) ^ 2\)、\((b ^ 4 - c ^ 4) ^ 2\) 和 \((a ^ 2 b c - b ^ 2 c ^ 2) ^ 2\)。

问题

设 \(a\)、\(b\) 和 \(c\) 为实数。证明 \(a ^ 2 (a ^ 6 + 8 b ^ 3 c ^ 3) ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2\)。

解答

\[\begin{split}&a ^ 2 (a ^ 6 + 8 b ^ 3 c ^ 3)\\ &\le 2 (a ^ 2 (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 + 4(a ^ 2 b c - b ^ 2 c ^ 2) ^ 2 + a ^ 2 (a ^ 6 + 8 b ^ 3 c ^ 3) \\ &=(a ^ 4 + b ^ 4 + c ^ 4) ^ 2.\end{split}\]

example {a b c : ℝ} :
    a ^ 2 * (a ^ 6 + 8 * b ^ 3 * c ^ 3) ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 :=
  calc
    a ^ 2 * (a ^ 6 + 8 * b ^ 3 * c ^ 3)
      ≤ 2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2
          + 4 * (a ^ 2 * b * c - b ^ 2 * c ^ 2) ^ 2
          + a ^ 2 * (a ^ 6 + 8 * b ^ 3 * c ^ 3) := by extra
    _ = (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 := by ring

1.4.11. 练习

设 \(x\) 和 \(y\) 为整数，并且假设 \(x+3 \geq 2y\)、\(1 \le y\)。证明 \(x \geq -1\)。

example {x y : ℤ} (h1 : x + 3 ≥ 2 * y) (h2 : 1 ≤ y) : x ≥ -1 :=
  sorry

设 \(a\) 和 \(b\) 为有理数，并且假设 \(3 \leq a\)、\(a+2b\geq 4\)。证明 \(a+b\geq 3\)。

example {a b : ℚ} (h1 : 3 ≤ a) (h2 : a + 2 * b ≥ 4) : a + b ≥ 3 :=
  sorry

设 \(x\) 为整数，且 \(x\geq 9\)。证明 \(x ^ 3 - 8x ^ 2 + 2x \geq 3\)。

example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 :=
  sorry

设 \(n\geq 10\) 为整数。证明 \(n ^ 4 - 2n ^ 2 > 3n ^ 3\)。

example {n : ℤ} (hn : n ≥ 10) : n ^ 4 - 2 * n ^ 2 > 3 * n ^ 3 :=
  sorry

设 \(n\geq 5\) 为整数。证明 \(n ^ 2 - 2n + 3 > 14\)。

example {n : ℤ} (h1 : n ≥ 5) : n ^ 2 - 2 * n + 3 > 14 :=
  sorry

设 \(x\) 为有理数。证明 \(x ^ 2 - 2x \ge -1\)。

example {x : ℚ} : x ^ 2 - 2 * x ≥ -1 :=
  sorry

设 \(a\) 和 \(b\) 为实数。证明 \(a ^ 2 + b ^ 2 \ge 2ab\)。

example (a b : ℝ) : a ^ 2 + b ^ 2 ≥ 2 * a * b :=
  sorry

脚注

3: 改编自 IMO 2001，第 2 题。

1.5. 一种简便写法

我们已经解决的一些问题，其实一眼就能看出答案。比如例 1.3.2：

问题

设 \(x\) 为整数，并且假设 \(x+4=2\)。证明 \(x=-2\)。

我们用如下计算解决了它：

\[\begin{split}x&=(x+4)-4\\ &=2-4\\ &=-2,\end{split}\]

但说实话，这似乎有点小题大做。

在本书中，我们按如下方式划线：如果一个事实能仅仅通过在两边加减项（不涉及乘法、除法等）从另一个事实推出，那么就不需要写出完整的计算式证明。

为了在 Lean 中使用，我提供了一个策略 addarith，它会执行这种简单推导。下面是在上例中的用法：

example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := by addarith [h1]

下面还有一些只涉及加减项的推导；因此，对这些推导我们也不要求写出显式的计算式证明：

若 \(a-2b=1\)，则 \(a=2b+1\)。

example {a b : ℤ} (ha : a - 2 * b = 1) : a = 2 * b + 1 := by addarith [ha]

若 \(x=2\) 且 \(y ^ 2 = -7\)，则 \(x+y^2=-5\)。

example {x y : ℚ} (hx : x = 2) (hy : y ^ 2 = -7) : x + y ^ 2 = -5 :=
  calc
    x + y ^ 2 = x - 7 := by addarith [hy]
    _ = -5 := by addarith [hx]

对于不等式也可以这样做，只要不等式推导中涉及的全部只是加减项。例如：

若 \(t=4-st\)，则 \(t+st>0\)。

example {s t : ℝ} (h : t = 4 - s * t) : t + s * t > 0 := by addarith [h]

若 \(m \le 8 - n\)，则 \(10>m+n\)。

example {m n : ℝ} (h1 : m ≤ 8 - n) : 10 > m + n := by addarith [h1]

但在例 1.3.4 中，有一个推导需要除法，而不只是加法和减法：若 \(3w+1=4\)，则 \(w=1\)。

\[\begin{split}w&=\frac{3w+1}{3}-\frac{1}{3}\\ &=\frac{4}{3}-\frac{1}{3}\\ &=1.\end{split}\]

我们仍然要求这种证明完整写出。

请检查 addarith 不能验证这个推导。

example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 := sorry