2. 有结构的证明

第 1 章中的计算式证明，从某种角度看，全都是一步证明。本章逐渐引入多步证明的组成部分。这些组成部分包括：建立之后会再次引用的“中间”事实；调用由你自己或他人先前证明过的具名引理；以及拆解由较简单陈述通过逻辑符号 \(\lor\)、\(\land\) 和 \(\exists\) 组合而成的复杂数学陈述。

本章还介绍 Lean 语言的关键交互功能：实时更新的 infoview，它会跟踪你当前的假设和目标。

本章的工作会在中间插入一章之后，于 第 4 章继续。

2.1. 中间步骤

2.1.1. 例

到目前为止，我们见过的每个证明都是单个计算。不过，更典型的证明会有更复杂的结构：有些事实在早期建立，但并不立即使用，而是在后面被调入。

例如，下面是 例 1.3.3 中的代数问题。

问题

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

我们先前用一个很长的单次计算解决了它，

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

但还有另一种表达解答的方式，也许更自然，也更接近你在高中学过的解方程方法：先解出 \(b\)，然后把它代入以帮助解出 \(a\)。

解答

由于 \(b+2=3\)，所以 \(b=1\)。因此

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

这是我们第一次看到带文字的证明。句子

由于 \(b+2=3\)，所以 \(b=1\)。

用到了 第 1.5 节讨论的推理：事实 \(b=1\) 是从假设 \(b+2=3\) 通过在心里两边同时减去 2 推出的；这被认为足够明显，所以除了指出调用了哪个假设之外，不再解释推理。

现在，我们把一个新事实 \(b=1\) 加入了本题的已知事实列表，并进行一个使用该事实的计算式证明（在步骤 \((a - 5b) + 5b = 4 + 5 \cdot 1\) 中，它与 \(a-5b=4\) 一起被代换）。词语“因此”（同义词：“于是”“所以”）引入这个计算式证明；它的含义是，刚刚证明的事实将在后续推理中使用。

下面是在 Lean 中表示这个论证的方式。我们用关键字 have hb 陈述 \(b=1\)。紧接着给出证明这个事实的理由：从本题中名为 h2 的假设 \(b+2=3\) 出发，加减某个量。然后照常给出一个计算式证明，其中事实 \(b=1\)（名为 hb）会在某处被使用。

example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 := by
  have hb : b = 1 := by addarith [h2]
  calc
    a = a - 5 * b + 5 * b := by ring
    _ = 4 + 5 * 1 := by rw [h1, hb]
    _ = 9 := by ring

逐步阅读 Lean 代码并不难理解这个证明。但 Lean 实际上提供了一个强大的工具来帮助我们理解多步证明：Lean Infoview 窗口。现在我们第一次使用它。让我们随着这个问题的推进，看 infoview 能告诉我们什么。

1. 把光标放在 have hb : b = 1 这一行的开头，并查看 Lean Infoview 窗口。我们会看到：

   have hb : b = 1
   

   这只是我们起始问题的竖排显示版本：它列出题目给出的所有变量和假设，并在符号 ⊢ 旁显示我们的目标：证明 a = 9。

   a b : ℝ
   h1 : a - 5 * b = 4
   h2 : b + 2 = 3
   ⊢ a = 9
   

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

2. 接下来，把光标移动到如下几行的开头：

   calc
     a = (a - 5 * b) + 5 * b := by ring
   

   新证明的事实 hb，即 b = 1，已经加入 infoview 的假设列表。

   a b : ℝ
   h1 : a - 5 * b = 4
   h2 : b + 2 = 3
   hb : b = 1
   ⊢ a = 9
   

3. 最后，把光标移动到最后一行代码之后、下一行的开头：

   _ = 9 := by ring
   

   infoview 现在不再显示任何任务，而是显示信息 No goals，这在视觉上确认了 calc 块已经解决目标，从而完成了问题。

   No goals
   

2.1.2. 例

下面是另一个在主证明之前先建立中间陈述的推理例子。

问题

设 \(m\) 和 \(n\) 为整数，并且假设 \(m+3\le 2n-1\)、\(n\le 5\)。证明 \(m\le 6\)。

解答

我们有

\[\begin{split}m+3&\le 2n-1\\ &\le 2\cdot 5-1\\ &= 9,\end{split}\]

所以 \(m \le 6\)。

这里，中间步骤是事实 \(m+3\le 9\)。这可以通过查看文字之后的计算式证明读出：

我们有

计算左上角的表达式是 \(m+3\)，右下角的表达式是 \(9\)，中间步骤中的关系序列 \(\le\)、\(\le\)、\(=\) 共同建立了 \(m+3\) 与 \(9\) 之间的关系 \(\le\)。

我们在 例 2.1.1 中讨论过“因此”/“于是”/“所以”的含义。这里的文字

所以 \(m \le 6\)。

告诉我们，刚刚证明的事实（\(m+3\le 9\)）蕴含 \(m \le 6\)，而这个证明太直接，不需要更多细节；在本例中，它又是 第 1.5 节讨论的“两边同加减”推理。

下面是同一个证明的 Lean 写法。用于建立中间步骤的计算块由 have 引入并命名：

example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
  have h3 :=
  calc
    m + 3 ≤ 2 * n - 1 := by rel [h1]
    _ ≤ 2 * 5 - 1 := by rel [h2]
    _ = 9 := by numbers
  addarith [h3]

注意，在最后一行一开始，

addarith [h3]

目标状态（如 infoview 所显示）是

m n : ℤ
h1 : m + 3 ≤ 2 * n - 1
h2 : n ≤ 5
h3 : m + 3 ≤ 9
⊢ m ≤ 6

事实 \(m + 3 ≤ 9\) 由 calc 块建立，并命名为 h3；它现在可以作为一个额外事实供后续步骤使用，并且确实在下一步（addarith [h3]）中被使用。

2.1.3. 例

让我们重做另一个例子，这次是 例 1.4.2。问题是：

问题

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

我们之前用一个巧妙的单次计算解决了它；但下面这个解答虽然更长，却可能更容易想出来。

解答

由 \(s + 3 \geq r\) 得 \(r \leq 3 + s\)，由 \(s + r \leq 3\) 得 \(r \leq 3 - s\)。因此

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

本题有两个中间步骤：证明 \(r \leq 3 + s\)，以及证明 \(r \leq 3 - s\)。

练习：下面是本题的 Lean 框架，其中列出了所陈述的中间步骤（尚未证明），并把所陈述的计算式证明轮廓作为最后一步。请补全所有 sorry。另请试着预测 infoview 在证明中每个位置会显示什么，再与实际情况比较。

example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by
  have h3 : r ≤ 3 + s := by sorry -- justify with one tactic
  have h4 : r ≤ 3 - s := by sorry -- justify with one tactic
  calc
    r = (r + r) / 2 := by sorry -- justify with one tactic
    _ ≤ (3 - s + (3 + s)) / 2 := by sorry -- justify with one tactic
    _ = 3 := by sorry -- justify with one tactic

2.1.4. 例

下一个问题包含一种新的推理形式。

问题

设 \(t\) 为实数，并且假设 \(t^2=3t\)、\(t \geq 1\)。证明事实上 \(t\geq 2\)。

解答

我们有

\[\begin{split}t\cdot t&=t^2\\ &=3t,\end{split}\]

所以 \(t=3\)。于是 \(t\geq 2\)。

这个证明的第一步是一个计算，它建立中间陈述 \(t\cdot t=3t\)。然后，借助短语

所以 \(t=3\)

我们通过从 \(t\cdot t=3t\) 的左右两边消去 \(t\)，建立另一个中间陈述 \(t=3\)。最后推出目标 \(t=3\)。

在 Lean 中，消去推理由 cancel 策略完成。在下面的证明中，你会看到，在 cancel t at h3 这一行之前，目标状态含有假设

h3 : t * t = 3 * t

而在这一行之后，它已经被修改为

h3 : t = 3

下面是 Lean 中的完整证明。

example {t : ℝ} (h1 : t ^ 2 = 3 * t) (h2 : t ≥ 1) : t ≥ 2 := by
  have h3 :=
  calc t * t = t ^ 2 := by ring
    _ = 3 * t := by rw [h1]
  cancel t at h3
  addarith [h3]

这里有一个数学上的细微点。只有当公共因子已知非零时，才能从等式两边消去这个公共因子。在本题中，Lean 能推出公共因子 \(t\) 非零。为什么？

2.1.5. 例

下面还有一个先建立中间事实再化简的例子。

问题

设 \(a\) 和 \(b\) 为实数，并且假设 \(a ^ 2 = b ^ 2 + 1\)，且 \(a\) 非负。证明 \(a \geq 1\)。

解答

我们有

\[\begin{split}a ^ 2&= b^2 +1\\ &\geq 1\\ &=1^2,\end{split}\]

所以 \(a\geq 1\)。

从 \(a ^ 2 \geq 1 ^ 2\) 推出 \(a \geq 1\)，也可以由 cancel 策略完成。注意，Lean 正在静默检查这一步成立的条件（即 \(a\geq 0\)）。请检查：如果删除假设 h2 : a ≥ 0，则 Lean 中的消去步骤会失败。

example {a b : ℝ} (h1 : a ^ 2 = b ^ 2 + 1) (h2 : a ≥ 0) : a ≥ 1 := by
  have h3 :=
  calc
    a ^ 2 = b ^ 2 + 1 := by rw [h1]
    _ ≥ 1 := by extra
    _ = 1 ^ 2 := by ring
  cancel 2 at h3

2.1.6. 例

本节最后给出一些练习，把文字证明翻译成 Lean 证明。这些问题的难点在于：从文本中辨认出中间陈述是什么。

首先，我们再重做一个例子，这次是 例 1.4.1。问题是：

问题

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

下面是一个使用中间步骤的解答。

解答

由于 \(x + 3 \le 2\)，所以 \(x \leq -1\)。于是

\[\begin{split}y&\geq 3-2x\\ &\geq 3-2\cdot -1\\ &>3.\end{split}\]

练习：找出中间步骤，并在 Lean 中表示这个解答。

example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 := by
  sorry

2.1.7. 例

下一个问题在数学上稍难一些。

问题

设 \(a\) 和 \(b\) 为实数，并且假设 \(-b \le a \le b\)。证明 \(a ^ 2 \le b ^ 2\)。

解答

由假设的第一部分可得 \(0 \le b + a\)，由假设的第二部分可得 \(0 \le b - a\)。

因此 \((b + a)(b - a)\) 非负，所以

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

练习：找出两个中间步骤，并在 Lean 中表示这个解答。（注意，这里 Lean 比人类读者稍微更强大：你不需要给出下面这一步的任何 Lean 翻译：

因此 \((b + a)(b - a)\) 非负，

Lean 会在需要这一点的位置自行推出它。）

example (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
  sorry

2.1.8. 例

问题

设 \(a\) 和 \(b\) 为实数，并且假设 \(a \le b\)。证明 \(a ^ 3 \le b ^ 3\)。

注意，我们并未假设 \(a\) 和 \(b\) 为正，因此那些关于不等式在乘法或乘方下行为的较简单技巧并不适用。

解答

由于 \(a \le b\)，所以 \(0 \le b - a\)。

因此 \(\frac{(b - a)\left[(b - a)^2+3(b+a)^2\right]}{4}\) 非负，所以

\[\begin{split}a ^ 3 &\le a ^ 3 + \frac{(b - a)\left[(b - a)^2+3(b+a)^2\right]}{4}\\ &= b ^ 3.\end{split}\]

练习：找出中间步骤，并在 Lean 中表示这个解答。

example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by
  sorry

2.1.9. 练习

1. 设 \(x\) 为有理数，且它的平方为 4，并且它大于 1。证明 \(x=2\)。

   建议步骤：证明 \(x(x+2)=2(x+2)\)，然后消去以推出 \(x=2\)。

   example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
     sorry
   

2. 设整数 \(n\) 满足 \(n^2+4=4n\)。证明 \(n=2\)。

   建议步骤：证明 \((n-2)^2=0\)，消去平方以推出 \(n-2=0\)，然后完成证明。

   example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by
     sorry
   

3. 设 \(x\) 和 \(y\) 为有理数，并且假设 \(xy=1\)、\(x \ge 1\)。证明 \(y \le 1\)。

   建议步骤：证明 \(0

   example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
     sorry
   

2.2. 调用引理

2.2.1. 例

下面是一种我们还没有见过的问题类型：目标是不等式意义下的“不相等”，\(x\ne 1\)，而不是等式（\(=\)）或不等式（\(\le\)、\(<\)、\(\ge\)、\(>\)）。

问题

设 \(x\) 为有理数，并且假设 \(3x=2\)。证明 \(x\ne 1\)。

解答

只需证明 \(x<1\)。事实上，

\[\begin{split}x &= (3x)/3 \\ &=2/3 \\ &< 1.\end{split}\]

这个问题中发生了什么？我们使用了一条“一般知识”：如果一个数严格小于另一个数，那么它们不可能相等。或者至少这感觉像一般知识，像常识一样！但实际上它是一个引理：一个已经由我们或他人证明过、并且允许我们在证明中调用的事实。1

在 Lean 中工作时，如果想这样调用一个引理，就需要按名称说出它。此前有人在庞大的 Lean 数学库中证明了这个事实，并把它命名为 ne_of_lt：2

lemma ne_of_lt {a b : ℚ} (h : a < b) : a ≠ b :=

我们可以使用 Lean 的 apply 策略在本题中调用这个引理。在开始处理本题时，

example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by

我们的目标状态如下：

x : ℚ
hx : 3 * x = 2
⊢ x ≠ 1

当我们应用这个引理，并把光标放在这一行末尾时，

example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
  apply ne_of_lt

目标状态变成了这样：

x : ℚ
hx : 3 * x = 2
⊢ x < 1

因此，apply ne_of_lt（只）改变目标：它把目标 x ≠ 1 变成目标 x < 1，然后我们可以用处理不等式的常规方法解决它。

example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
  apply ne_of_lt
  calc
    x = 3 * x / 3 := by ring
    _ = 2 / 3 := by rw [hx]
    _ < 1 := by numbers

比较文字证明和 Lean 证明，你会注意到调用引理时的措辞很不一样。在文字中，我说：

只需证明 \(x<1\)。事实上，……

也就是说，我实际上说明了新目标会是什么，并让读者自行判断我用了哪条一般知识来改变目标。在 Lean 中，我不需要说明新目标是什么，因为读者可以通过查看目标状态自行得知。但我确实需要显式提到引理的名称，

apply ne_of_lt

因为“这是一般知识！”并不是足够精确、能让 Lean 找到它的理由。

2.2.2. 例

下面是一个类似问题；我将通过说明左边更大，而不是像上题那样说明左边更小，来证明一个不等式意义下的不相等。

问题

设 \(y\) 为实数。证明 \(y ^ 2 + 1\ne 0\)。

解答

只需证明 \(0 < y ^ 2 + 1\)，这由平方非负显然成立。

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

example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
  sorry

使用引理 ne_of_gt：

lemma ne_of_gt {a b : ℝ} (h : a > b) : a ≠ b :=

2.2.3. 例

问题

设 \(a\) 和 \(b\) 为实数，并且假设 \(a^2+b^2=0\)。证明 \(a ^ 2 = 0\)。

解答

只需同时证明 \(a ^ 2 \le 0\) 和 \(a ^ 2 \ge 0\)。第二个结论由平方非负显然成立。至于第一个，

\[\begin{split}a ^ 2 &\le a ^ 2 + b ^ 2\\ &=0.\end{split}\]

在 Lean 中使用这个引理，即 \(\le\) 关系的“反对称性”：

lemma le_antisymm {a b : α} (h1 : a ≤ b) (h2 : b ≤ a) : a = b :=

下面是 Lean 中的完整证明。

example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a ^ 2 = 0 := by
  apply le_antisymm
  calc
    a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
    _ = 0 := h1
  extra

注意，应用这个引理之后，infoview 显示了两个目标！

2 goals

a b : ℝ
h1 : a ^ 2 + b ^ 2 = 0
⊢ a ^ 2 ≤ 0

a b : ℝ
h1 : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a ^ 2

从数学上说，这并不奇怪，因为该引理有两个前提，我们都需要证明。不管怎样，Lean 中完全可以同时有多个目标：任一时刻可以有许多目标，机制很简单，你写的任何代码都会作用于列表中的第一个目标（直到它被解决，然后工作转到第二个目标，依此类推）。

2.2.4. 练习

1. 设 \(m\) 为满足 \(m + 1=5\) 的整数。证明 \(3m\ne 6\)。

   你可能会想用这样一个事实：若第一个数大于第二个数，则这两个数不相等（你会需要引理 ne_of_gt，如 例 2.2.2）。

   example {m : ℤ} (hm : m + 1 = 5) : 3 * m ≠ 6 := by
     sorry
   

2. 设 \(s\) 为有理数，且 \(3s \le -6\)、\(2s \ge -4\)。证明 \(s=-2\)。

   你很可能会使用引理 le_antisymm，它说明若 \(x\le y\) 且 \(x\ge y\)，则 \(x = y\)。

   example {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by
     sorry
   

脚注

1

在这个例子中，这是有理数上关系 \(<\) 的定义的结果。

2

这里 ne 表示 “not equal”，lt 表示 “less than”，而 of 表示我们从一个 lt 陈述推出一个 ne 陈述。Lean 标准数学库有许多这样的命名约定，但你不必遵守它们；你自己的引理愿意叫 foo 或 banana 都可以。

2.3. “或”与分类证明

2.3.1. 例

在数学中，“或”（作为逻辑符号记为 \(\lor\)）可以连接两个陈述。例如，下面的问题中，假设就是一个“或”陈述。

问题

设 \(x\) 和 \(y\) 为实数，并且假设 \(x=1\) 或 \(y=-1\)。证明 \(xy+x=y+1\)。

假设

\(x=1\) 或 \(y=-1\)

告诉我们，备选项 \(x=1\)、\(y=-1\) 中至少有一个成立（也可能两者都成立，但这不需要特殊处理）。因此，本题解答只需依次考虑这两个备选项。这称为分类证明。

解答

如果 \(x=1\)，则

\[\begin{split}xy+x&=1\cdot y+1\\ &= y+1,\end{split}\]

而如果 \(y=-1\)，则

\[\begin{split}xy+x&=x\cdot -1+x\\ &=-1+1\\ &=y+1.\end{split}\]

在 Lean 中，“或”陈述用逻辑符号 ∨ 表示。在本题开始时，infoview 显示一个任务，其中 h 是“或”陈述假设，目标是证明 \(xy+x=y+1\)。

x y : ℝ
h : x = 1 ∨ y = -1
⊢ x * y + x = y + 1

为了依次考虑“或”陈述表示的两个情形，我们使用策略 obtain。应用这个策略之后，infoview 现在显示两个更简单的任务。每个任务中的目标仍然是证明 \(xy+x=y+1\)，但假设已经改变：第一个任务中是左侧备选项 x = 1，第二个任务中是右侧备选项 y = -1。

x y : ℝ
hx : x = 1
⊢ x * y + x = y + 1

x y : ℝ
hy : y = -1
⊢ x * y + x = y + 1

然后我们可以逐一解决这些较简单的任务，分别给出计算式证明。

example {x y : ℝ} (h : x = 1 ∨ y = -1) : x * y + x = y + 1 := by
  obtain hx | hy := h
  calc
    x * y + x = 1 * y + 1 := by rw [hx]
    _ = y + 1 := by ring
  calc
    x * y + x = x * -1 + x := by rw [hy]
    _ = -1 + 1 := by ring
    _ = y + 1 := by rw [hy]

2.3.2. 例

更常见的是，你会在没有直接呈现为“或”陈述的假设时进行分类证明。此时，你需要自己创造这样一个假设：建立并证明一个作为“或”陈述的中间陈述。

问题

设 \(n\) 为任意自然数。证明 \(n ^ 2 \ne 2\)。

在这个问题中，我们将对下面这个“或”陈述分类讨论：

\(n \le 1\) 或 \(2 \le n\)。

在纸上，这可以不加证明地陈述；不过严格说来，它来自关于自然数的一个引理：一般而言，\(n\) 要么小于等于某个自然数，要么大于等于下一个自然数。完成这个分类之后，题目的解答就很容易。

解答

我们分别考虑 \(n \le 1\) 和 \(2 \le n\) 两种情形。

情形 1（\(n \le 1\)）：只需证明 \(n ^ 2 < 2\)。事实上，

\[\begin{split}n ^ 2 & \le 1 ^ 2\\ &<2.\end{split}\]

情形 2（\(2 \le n\)）：只需证明 \(n ^ 2 > 2\)。事实上，

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

在 Lean 中，我们把这个“或”陈述显式建立为一个中间事实，即某个引理的应用，

lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a :=

我们此前还没有以这种方式调用引理。语法使用 have，

have hn := le_or_succ_le n 1

而在这行代码之后，infoview 显示出我们想要的“或”陈述：

hn : n ≤ 1 ∨ 2 ≤ n

建立这个中间事实之后，我们对该事实分类讨论，于是留下两个任务，对应两个情形：

n : ℕ
hn : n ≤ 1
⊢ n ^ 2 ≠ 2

n : ℕ
hn : 2 ≤ n
⊢ n ^ 2 ≠ 2

练习：第一个情形已经用 Lean 写出。请补全第二个情形的细节。

example {n : ℕ} : n ^ 2 ≠ 2 := by
  have hn := le_or_succ_le n 1
  obtain hn | hn := hn
  apply ne_of_lt
  calc
    n ^ 2 ≤ 1 ^ 2 := by rel [hn]
    _ < 2 := by numbers
  sorry

2.3.3. 例

到目前为止，我们讨论的是如何处理出现在假设中的“或”陈述。现在转向如何处理出现在目标中的“或”陈述。这很容易：你必须证明这个“或”陈述中的某一个备选项，所以只需宣布你预期哪个备选项可行，然后证明它。

问题

设 \(x\) 为满足 \(2x+1=5\) 的实数。证明 \(x=1\) 或 \(x=2\)。

解答

我们将证明 \(x=2\)。事实上，

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

在 Lean 中，使用策略 right 来宣布你将证明目标的右侧备选项（证明左侧则用 left）。这会改变 infoview 中显示的目标：从

⊢ x = 1 ∨ x = 2

在应用策略之前，变为

⊢ x = 2

让我们做一个同时包含这两种逻辑推理风格的例子。我们解一个二次方程；这是一种经典情形，其结论中会出现“或”。我们将得到一个“或”陈述作为中间事实，分类讨论，然后在每个情形中选择目标中的一侧。

example {x : ℝ} (hx : 2 * x + 1 = 5) : x = 1 ∨ x = 2 := by
  right
  calc
    x = (2 * x + 1 - 1) / 2 := by ring
    _ = (5 - 1) / 2 := by rw [hx]
    _ = 2 := by numbers

2.3.4. 例

让我们做一个同时包含这两种逻辑推理风格的例子。我们解一个二次方程；这是一种经典情形，其结论中会出现“或”。我们将得到一个“或”陈述作为中间事实，分类讨论，然后在每个情形中选择目标中的一侧。

问题

设 \(x\) 为满足 \(x^2-3x+2=0\) 的实数。证明 \(x=1\) 或 \(x=2\)。

解答

我们有

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

在这个解答中，分类讨论写得比前面的例子略随意。短语“若 \(x-1=0\)”和“若 \(x-2=0\)”悄悄引入了两个情形，并把我们现在要在该情形下证明的目标交给读者来推断。

我已经完成了 Lean 论证的第一部分：写出证明 \((x-1)(x-2)=0\) 的计算，然后调用引理 eq_zero_or_eq_zero_of_mul_eq_zero，把它转化为一个“或”陈述。

练习：补全该论证的 Lean 版本。

在 例 2.3.2 中，我们证明了没有自然数的平方等于 2。没有整数的平方等于 2 也是真的；不过由于负数参与时序关系法则更复杂，Lean 论证会复杂得多。

我已经完成了 Lean 论证的第一部分：写出证明 \((x-1)(x-2)=0\) 的计算，然后调用引理 eq_zero_or_eq_zero_of_mul_eq_zero，把它转化为一个“或”陈述。

x : ℝ
hx : x ^ 2 - 3 * x + 2 = 0
h1 : (x - 1) * (x - 2) = 0
h2 : x - 1 = 0 ∨ x - 2 = 0
⊢ x = 1 ∨ x = 2

设 \(n\) 为任意整数。证明 \(n ^ 2 \ne 2\)。

example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 :=
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  sorry

2.3.5. 例

在 例 2.3.2 中，我们证明了没有自然数的平方等于 2。没有整数的平方等于 2 也是真的；不过由于负数参与时序关系法则更复杂，Lean 论证会复杂得多。

问题

情形 1（\(n \le 0\)）：在这个情形中，有 \(0 \le -n\)。我们再分别考虑 \(-n \le 1\) 与 \(2 \le -n\) 两种情形。

解答

情形 1(ii)（\(2 \le -n\)）：只需证明 \(n ^ 2 > 2\)。事实上，

情形 2（\(1 \le n\)）：我们分别考虑 \(n \le 1\) 与 \(2 \le n\) 两种情形。

情形 2(i)（\(n \le 1\)）：只需证明 \(n ^ 2 < 2\)。事实上，

\[\begin{split}n ^ 2 &= (-n) ^ 2\\ & \le 1 ^ 2\\ &<2.\end{split}\]

情形 2(ii)（\(2 \le n\)）：只需证明 \(n ^ 2 > 2\)。事实上，

\[\begin{split}2 &< 2 ^ 2\\ &\le (-n) ^ 2\\ & = n ^ 2.\end{split}\]

当一个证明变得这样复杂时，你可能会发现，用符号 · 标记每个新子证明的开始很有帮助，如下所示。

我们把这个定理记下来，供以后使用，名称为 sq_ne_two。

\[\begin{split}n ^ 2 & \le 1 ^ 2\\ &<2.\end{split}\]

在数学中，“且”（作为逻辑符号记为 \(\land\)）和“或”一样，也可以连接两个陈述。例如，下面的问题中，假设就是一个“且”陈述。

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

当一个证明变得这样复杂时，你可能会发现，用符号 · 标记每个新子证明的开始很有帮助，如下所示。

example {n : ℤ} : n ^ 2 ≠ 2 := by
  have hn0 := le_or_succ_le n 0
  obtain hn0 | hn0 := hn0
  · have : 0 ≤ -n := by addarith [hn0]
    have hn := le_or_succ_le (-n) 1
    obtain hn | hn := hn
    · apply ne_of_lt
      calc
        n ^ 2 = (-n) ^ 2 := by ring
        _ ≤ 1 ^ 2 := by rel [hn]
        _ < 2 := by numbers
    · apply ne_of_gt
      calc
        (2:ℤ) < 2 ^ 2 := by numbers
        _ ≤ (-n) ^ 2 := by rel [hn]
        _ = n ^ 2 := by ring
  · have hn := le_or_succ_le n 1
    obtain hn | hn := hn
    · apply ne_of_lt
      calc
        n ^ 2 ≤ 1 ^ 2 := by rel [hn]
        _ < 2 := by numbers
    · apply ne_of_gt
      calc
        (2:ℤ) < 2 ^ 2 := by numbers
        _ ≤ n ^ 2 := by rel [hn]

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

2.3.6. 练习

1. 设 \(x\) 为有理数，并且假设 \(x=4\) 或 \(x=-4\)。证明 \(x^2+1=17\)。

   example {x : ℚ} (h : x = 4 ∨ x = -4) : x ^ 2 + 1 = 17 := by
     sorry
   

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

   example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by
     sorry
   

3. 设 \(t\) 为有理数，并且假设 \(t=-2\) 或 \(t=3\)。证明 \(t^2-t-6=0\)。

   example {t : ℚ} (h : t = -2 ∨ t = 3) : t ^ 2 - t - 6 = 0 := by
     sorry
   

4. 设 \(x\) 和 \(y\) 为实数，并且假设 \(x=2\) 或 \(y=-2\)。证明 \(x^2+2x=2y+4\)。

   example {x y : ℝ} (h : x = 2 ∨ y = -2) : x * y + 2 * x = 2 * y + 4 := by
     sorry
   

5. 设 \(s\) 和 \(t\) 为满足 \(s = 3 - t\) 的有理数。证明 \(s + t = 3\) 或 \(s + t = 5\)。

   example {s t : ℚ} (h : s = 3 - t) : s + t = 3 ∨ s + t = 5 := by
     sorry
   

6. 设 \(a\) 和 \(b\) 为满足 \(a + 2b < 0\) 的有理数。证明 \(b < a / 2\) 或 \(b < -a/2\)。

   example {a b : ℚ} (h : a + 2 * b < 0) : b < a / 2 ∨ b < - a / 2 := by
     sorry
   

7. 设 \(x\) 和 \(y\) 为满足 \(y = 2x+1\) 的实数。证明 \(xy/2\)。

   example {x y : ℝ} (h : y = 2 * x + 1) : x < y / 2 ∨ x > y / 2 := by
     sorry
   

8. 设 \(x\) 为满足 \(x^2+2x-3=0\) 的实数。证明 \(x=-3\) 或 \(x=1\)。

   你很可能会使用与 例 2.3.4 中相同的引理。

   example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
     sorry
   

9. 设 \(a\) 和 \(b\) 为满足 \(a^2+2b^2=3ab\) 的实数。证明 \(a=b\) 或 \(a=2b\)。

   你很可能会使用与 例 2.3.4 中相同的引理。

   example {a b : ℝ} (hab : a ^ 2 + 2 * b ^ 2 = 3 * a * b) : a = b ∨ a = 2 * b := by
     sorry
   

10. 设 \(t\) 为满足 \(t^3=t^2\) 的实数。证明 \(t=1\) 或 \(t=0\)。

    你很可能会使用与 例 2.3.4 中相同的引理，以及 cancel 策略。

    example {t : ℝ} (ht : t ^ 3 = t ^ 2) : t = 1 ∨ t = 0 := by
      sorry
    

11. 设 \(n\) 为任意自然数。证明 \(n ^ 2 \ne 7\)。

    你很可能会使用与 例 2.3.2 中相同的引理。

    example {n : ℕ} : n ^ 2 ≠ 7 := by
      sorry
    

12. 设 \(x\) 为任意整数。证明 \(2x \ne 3\)。

    你很可能会使用与 例 2.3.2 中相同的引理。

    example {x : ℤ} : 2 * x ≠ 3 := by
      sorry
    

13. 设 \(t\) 为任意整数。证明 \(5t \ne 18\)。

    你很可能会使用与 例 2.3.2 中相同的引理。

    example {t : ℤ} : 5 * t ≠ 18 := by
      sorry
    

14. 设 \(m\) 为任意自然数。证明 \(m ^ 2 +4m\ne 46\)。

    你很可能会使用与 例 2.3.2 中相同的引理。

    example {m : ℕ} : m ^ 2 + 4 * m ≠ 46 := by
      sorry
    

2.4. “且”

2.4.1. 例

在数学中，“且”（作为逻辑符号记为 \(\land\)）和“或”一样，也可以连接两个陈述。例如，下面的问题中，假设就是一个“且”陈述。

问题

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

事实上，我们以前研究过这个问题，即 例 1.3.6。当时，我们把这个问题看作有两个独立假设：

• \(2x-y=4\)

• \(y-x+1=2\)

但现在，为了讨论方便，我们把它看作只有一个假设：

• \(2x-y=4\) 且 \(y-x+1=2\)。

这个区分相当吹毛求疵，在文字中看不出来。在 Lean 中它更明显：我们可能会遇到一个显式含有 ∧ 符号的假设，例如

x y : ℤ
h : 2 * x - y = 4 ∧ y - x + 1 = 2
⊢ x = 5

在这种情况下，策略 obtain 会把一个“且”假设拆成它的组成部分，

x y : ℤ
h1 : 2 * x - y = 4
h2 : y - x + 1 = 2
⊢ x = 5

然后我们就可以按需分别访问这些部分来解决问题。在本例中，我们实际上把问题带回了 例 1.3.6 的设定。

example {x y : ℤ} (h : 2 * x - y = 4 ∧ y - x + 1 = 2) : x = 5 := by
  obtain ⟨h1, h2⟩ := h
  calc
    x = 2 * x - y + (y - x + 1) - 1 := by ring
    _ = 4 + 2 - 1 := by rw [h1, h2]
    _ = 5 := by ring

2.4.2. 例

“且”假设在实际问题中相对少见。它可能出现的一种情形是：某个单一假设有两个自然的推论，而某个引理把这两个推论配对给出。下面是一个例子。

问题

设 \(p\) 为满足 \(p^2\le 8\) 的有理数。证明 \(p\ge -5\)。

解答

我们有

\[\begin{split}p^2&\le 9\\ &= 3^2,\end{split}\]

且 3 为正，所以 \(-3\le p\le 3\)。于是

\[\begin{split}p&\ge -3\\ &\ge -5.\end{split}\]

在 Lean 中，我们使用引理 abs_le_of_sq_le_sq' 进行这个论证。这个引理由 Fordham 学生 Ben Davidson 加入 Lean 库。请注意该引理结论中的 ∧。

theorem abs_le_of_sq_le_sq' {x y : ℚ} (h1 : x ^ 2 ≤ y ^ 2) (h2 : 0 ≤ y) :
    -y ≤ x ∧ x ≤ y :=

练习：我已经用 Lean 写出了证明中得到中间事实 \(hp' : -3 \le p \land p \le 3\) 的部分。请处理这个“且”假设，然后完成 Lean 中的证明。

example {p : ℚ} (hp : p ^ 2 ≤ 8) : p ≥ -5 := by
  have hp' : -3 ≤ p ∧ p ≤ 3
  · apply abs_le_of_sq_le_sq'
    calc
      p ^ 2 ≤ 9 := by addarith [hp]
      _ = 3 ^ 2 := by numbers
    numbers
  sorry

请注意上面证明中一段新的 Lean 语法：像这样一行

have hp' : -3 ≤ p ∧ p ≤ 3

如果没有理由，会使 Lean 要求你给出该理由，也就是说，会出现一个新目标：证明该陈述。

2 goals

p : ℚ
hp : p ^ 2 ≤ 8
⊢ -3 ≤ p ∧ p ≤ 3

p : ℚ
hp : p ^ 2 ≤ 8
hp' : -3 ≤ p ∧ p ≤ 3
⊢ p ≥ -5

当你完成证明之后（如我这里所做），你会回到先前的位置，只不过事实 \(hp'\) 现在已经是一个完全证明过的中间事实，可以供使用。

2.4.3. 例

有时，一个问题的目标也会含有“且”陈述。例如，你可能会得到一个联立方程组，并被要求确定所有出现变量的值。下面是我们在 例 1.3.3 中见过的联立方程组，但题目陈述被调整为要求我们同时求出 \(a\) 和 \(b\) 的值。

问题

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

解决这种问题的一种方法，是完全独立地建立所要求的两个事实：

解答

我们有，

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

又因为 \(b+2=3\)，所以 \(b=1\)。

在 Lean 中，我们使用 constructor 策略书写这个证明；它会接受一个目标为“且”陈述的问题，

a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ a = 9 ∧ b = 1

并把它化为两个更简单的任务，分别对应“且”的两个部分。

a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ a = 9

a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ b = 1

然后我们依次写出这两个任务的 Lean 证明。

example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
  constructor
  · calc
      a = 4 + 5 * b := by addarith [h1]
      _ = -6 + 5 * (b + 2) := by ring
      _ = -6 + 5 * 3 := by rw [h2]
      _ = 9 := by ring
  · addarith [h2]

另一种情况是，你可能想记录一个中间事实，然后在证明的两个部分中都使用它。例如，你可能想先解出 \(b\)，然后用它缩短解出 \(a\) 的工作。

解答

由于 \(b+2=3\)，所以 \(b=1\)。因此

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

通常要留给读者检查：所需目标的两个部分 \(a=9\) 与 \(b=1\) 都已经在某处被建立。

下面是这个证明在 Lean 中的样子。重要观察是：如果有某个东西要在证明的两个部分中使用（这里是事实 \(b=1\)），那么它必须在使用 constructor 策略之前建立。当使用 constructor 策略时，到目前为止建立的所有事实，都会在产生的两个任务中都可用：

a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
hb : b = 1
⊢ a = 9

a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
hb : b = 1
⊢ b = 1

example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
  have hb : b = 1 := by addarith [h2]
  constructor
  · calc
      a = 4 + 5 * b := by addarith [h1]
      _ = 4 + 5 * 1 := by rw [hb]
      _ = 9 := by ring
  · apply hb

2.4.4. 例

再看一个目标中含有“且”的例子。

问题

设 \(a\) 和 \(b\) 为实数，并且假设 \(a^2+b^2=0\)。证明 \(a=0\) 且 \(b=0\)。

解答

我们先证明 \(a^2=0\)。\((\star)\) 事实上，

\[\begin{split}a ^ 2 &\le a ^ 2 + b ^ 2\\ &=0.\end{split}\]

并且由于平方非负，还有 \(a^2\geq 0\)。

由 \((\star)\)，\(a=0\)。同样由 \((\star)\)，

\[\begin{split}b ^ 2 &= a ^ 2 + b ^ 2\\ &=0,\end{split}\]

所以 \(b=0\)。

这个问题的一部分可能让你觉得熟悉。中间目标 \(a^2=0\) 的证明重复了 例 2.2.3。

下面是 Lean 中的问题陈述，以及从 例 2.2.3 复制来的中间目标 \(a^2=0\) 的证明。请补全余下证明。策略 cancel 有助于在已知平方为零时推出量本身为零。

example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a = 0 ∧ b = 0 := by
  have h2 : a ^ 2 = 0
  · apply le_antisymm
    calc
      a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
      _ = 0 := by rw [h1]
    extra
  sorry

2.4.5. 练习

1. 设 \(a\) 和 \(b\) 为有理数，并且假设 \(a \le 1\) 且 \(a + b \le 3\)。证明 \(2a+b \le 4\)。

   example {a b : ℚ} (H : a ≤ 1 ∧ a + b ≤ 3) : 2 * a + b ≤ 4 := by
     sorry
   

2. 设 \(r\) 和 \(s\) 为实数，并且假设 \(r + s \le 1\) 且 \(r - s \le 5\)。证明 \(2r \le 6\)。

   example {r s : ℝ} (H : r + s ≤ 1 ∧ r - s ≤ 5) : 2 * r ≤ 6 := by
     sorry
   

3. 设 \(m\) 和 \(n\) 为整数，并且假设 \(n \le 8\) 且 \(m + 5 \le n\)。证明 \(m \le 3\)。

   example {m n : ℤ} (H : n ≤ 8 ∧ m + 5 ≤ n) : m ≤ 3 := by
     sorry
   

4. 设 \(p\) 为整数，并且假设 \(p + 2 \ge 9\)。证明 \(p^2\geq 49\) 且 \(7 \le p\)。

   example {p : ℤ} (hp : p + 2 ≥ 9) : p ^ 2 ≥ 49 ∧ 7 ≤ p := by
     sorry
   

5. 设 \(a\) 为有理数，并且假设 \(a - 1 \ge 5\)。证明 \(a \ge 6\) 且 \(3a \ge 10\)。

   example {a : ℚ} (h : a - 1 ≥ 5) : a ≥ 6 ∧ 3 * a ≥ 10 := by
     sorry
   

6. 设 \(x\) 和 \(y\) 为有理数，并且假设 \(x + y = 5\) 且 \(x + 2y = 7\)。证明 \(x=3\) 且 \(y=2\)。

   example {x y : ℚ} (h : x + y = 5 ∧ x + 2 * y = 7) : x = 3 ∧ y = 2 := by
     sorry
   

7. 设 \(a\) 和 \(b\) 为实数，并且假设 \(ab=a=b\)。证明 \(a=b=0\) 或 \(a=b=1\)。

   你很可能需要使用 例 2.3.4 中证明的引理 eq_zero_or_eq_zero_of_mul_eq_zero。

   example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
       a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by
     sorry
   

2.5. 存在性证明

2.5.1. 例

本节讨论存在量词，即英文中表达为如下形式的逻辑概念：

存在……使得……。

例如，下面的问题中，假设含有一个存在量词。

问题

设 \(a\) 为有理数，并且假设存在有理数 \(b\)，使得 \(a=b^2+1\)。证明 \(a>0\)。

假设“存在有理数 \(b\)，使得 \(a=b^2+1\)”可以立即拆开，从而真正取得这个存在命题的见证：一个满足 \(a=b^2+1\) 的有理数 \(b\)（也许不止一个，但这里只会选择一个见证）。然后我们就能做一个涉及见证 \(b\) 的普通计算式证明。

解答

设 \(b\) 为满足 \(a=b^2+1\) 的有理数。我们有，

\[\begin{split}a &=b^2+1\\ &>0.\end{split}\]

存在命题的逻辑符号是 \(\exists\)。在 Lean 中，策略 obtain 用来把存在性假设拆成一个见证和一个关于该见证的假设。语法与拆开“且”相同（见 第 2.4 节）。

example {a : ℚ} (h : ∃ b : ℚ, a = b ^ 2 + 1) : a > 0 := by
  obtain ⟨b, hb⟩ := h
  calc
    a = b ^ 2 + 1 := hb
    _ > 0 := by extra

在这个问题中，目标视图最初是

a : ℚ
h : ∃ b, a = b ^ 2 + 1
⊢ a > 0

使用 obtain 策略之后，存在命题被拆开，于是见证单独出现在变量列表中，并可在后续证明中访问：

a b : ℚ
hb : a = b ^ 2 + 1
⊢ a > 0

2.5.2. 例

下面是另一个带有存在性假设的问题：“存在实数 \(a\)，使得 \(at<0\)”。和前面一样，我们先拆开它，然后沿用先前方法。

问题

设 \(t\) 为实数，并且假设存在实数 \(a\)，使得 \(at<0\)。证明 \(t\ne 0\)。

解答

设 \(x\) 为满足 \(xt<0\) 的实数。我们分别考虑 \(x\le 0\) 和 \(0<x\) 两种情形。

情形 1（\(x \le 0\)）：我们有 \(0<(-x)t\) 且 \(0 \le -x\)，所以有 \(0 < t\)，从而 \(t\ne 0\)。

情形 2（\(0<x\)）：我们有

\[\begin{split}0&<-xt\\ &=x(-t)\end{split}\]

且 \(0 \le x\)，所以 \(0 < -t\)，于是 \(t<0\)，从而 \(t\ne 0\)，

下面是 Lean 中的一个部分解答（第一步用 obtain 拆开存在命题，稍后又用它进行分类讨论）。情形 2 缺失；请你完成它。

example {t : ℝ} (h : ∃ a : ℝ, a * t < 0) : t ≠ 0 := by
  obtain ⟨x, hxt⟩ := h
  have H := le_or_gt x 0
  obtain hx | hx := H
  · have hxt' : 0 < (-x) * t := by addarith [hxt]
    have hx' : 0 ≤ -x := by addarith [hx]
    cancel -x at hxt'
    apply ne_of_gt
    apply hxt'
  · sorry

2.5.3. 例

要证明目标中含有存在量词的问题，你需要自己提供一个见证，然后验证你提出的见证确实有效。

问题

证明：存在整数 \(n\)，使得 \(12n=84\)。

解答

整数 \(7\) 具有这个性质。事实上，\(12 \cdot 7=84\)。

在 Lean 中，策略 use 用来说明你选取了什么见证。

example : ∃ n : ℤ, 12 * n = 84 := by
  use 7
  numbers

在这个问题中，目标最初是

⊢ ∃ n : ℤ, 12 * n = 84

但在策略 use 7 之后，目标变成检查所提出的见证 7 是否有效。

⊢ 12 * 7 = 84

这正是 numbers 所检查的内容。

2.5.4. 例

通常，要想出存在性目标的见证需要一些创造性。本节余下部分是寻找见证的练习。

问题

设 \(x\) 为实数。证明存在实数 \(y\)，使得 \(y>x\)。

解答

实数 \(x + 1\) 具有这个性质。事实上，\(x+1>x\)。

example (x : ℝ) : ∃ y : ℝ, y > x := by
  use x + 1
  extra

2.5.5. 例

问题

证明：存在整数 \(m\) 和 \(n\)，使得 \(m^2-n^2=11\)。

解答

可取 \(m=6\)、\(n=5\)。事实上，

\[\begin{split}6^2-5^2&=36-25\\ &=11.\end{split}\]

example : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 11 := by
  sorry

2.5.6. 例

有时，你可能希望省略明确说明见证是什么的句子“可取……”。这种情况下，你应当格外细致地验证所需性质正是按题目陈述的形式成立。

问题

设 \(a\) 为整数。证明存在整数 \(m\) 和 \(n\)，使得 \(m^2-n^2=2a+1\)。

解答

\[(a+1)^2-a^2=2a+1.\]

在 Lean 中，你仍然必须使用 use 来说明见证。

example (a : ℤ) : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 2 * a + 1 := by
  sorry

2.5.7. 例

问题

设 \(p\) 和 \(q\) 为实数，并假设 \(p<q\)。证明存在实数 \(x\)，使得 \(p<x<q\)。

解答

我们将证明 \(\frac{p+q}{2}\) 具有这个性质。事实上，

\[\begin{split}p&=\frac{p+p}{2}\\ &<\frac{p+q}{2},\end{split}\]

并且

\[\begin{split}\frac{p+q}{2} &<\frac{q+q}{2}\\ &=q.\end{split}\]

example {p q : ℝ} (h : p < q) : ∃ x, p < x ∧ x < q := by
  sorry

2.5.8. 例

我记得有一次去看望他 [Ramanujan]，当时他病卧在 Putney。我乘坐的出租车号码是 1729，我说这个数在我看来相当乏味，并希望它不是一个不祥之兆。“不，”他回答说，“这是一个非常有趣的数；它是能以两种不同方式表示为两个立方数之和的最小数。”

——G. H. Hardy，《拉马努金：由其生平与工作启发的十二讲》

问题

证明：存在自然数 \(a\)、\(b\)、\(c\) 和 \(d\)，使得 \(a^3+b^3=1729=c^3+d^3\)，但 \(a\ne c\) 且 \(a\ne d\)。3

解答

\(1^3+12^3=1729=9^3+10^3\)，但 \(1\ne 9\) 且 \(1\ne 10\)。

example : ∃ a b c d : ℕ,
    a ^ 3 + b ^ 3 = 1729 ∧ c ^ 3 + d ^ 3 = 1729 ∧ a ≠ c ∧ a ≠ d := by
  use 1, 12, 9, 10
  constructor
  numbers
  constructor
  numbers
  constructor
  numbers
  numbers

2.5.9. 练习

1. 证明：存在有理数 \(t\)，使得 \(t^2=1.69\)。

   example : ∃ t : ℚ, t ^ 2 = 1.69 := by
     sorry
   

2. 证明：存在整数 \(m\) 和 \(n\)，使得 \(m^2+n^2=85\)。

   example : ∃ m n : ℤ, m ^ 2 + n ^ 2 = 85 := by
     sorry
   

3. 证明：存在实数 \(x\)，使得 \(x<0\) 且 \(x^2<1\)。

   example : ∃ x : ℝ, x < 0 ∧ x ^ 2 < 1 := by
     sorry
   

4. 证明：存在自然数 \(a\) 和 \(b\)，使得 \(2 ^ a = 5b+1\)。

   example : ∃ a b : ℕ, 2 ^ a = 5 * b + 1 := by
     sorry
   

5. 设 \(x\) 为有理数。证明存在有理数 \(y\)，使得 \(y^2>x\)。

   example (x : ℚ) : ∃ y : ℚ, y ^ 2 > x := by
     sorry
   

6. 设 \(t\) 为实数，并且假设存在实数 \(a\)，使得 \(at+1

   和 例 2.5.2 中一样，我使用了引理 le_or_gt，它说明若 \(s\) 和 \(t\) 为实数，则要么 \(s \le t\)，要么 \(t < s\)；它可以作为一种有用的分类讨论。

   example {t : ℝ} (h : ∃ a : ℝ, a * t + 1 < a + t) : t ≠ 1 := by
     sorry
   

7. 设 \(m\) 为整数，并且假设存在整数 \(a\)，使得 \(2a=m\)。证明 \(m\ne 5\)。

   example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by
     sorry
   

8. 设 \(n\) 为整数。证明存在整数 \(a\)，使得 \(2a^3 \ge na+7\)。

   example {n : ℤ} : ∃ a, 2 * a ^ 3 ≥ n * a + 7 := by
     sorry
   

9. 设 \(a\)、\(b\) 和 \(c\) 为实数，并且假设 \(a\le b+c\)、\(b\le a+c\)、\(c\le a+b\)。证明存在非负实数 \(x\)、\(y\) 和 \(z\)，使得 \(a=y+z\)、\(b=x+z\)、\(c=x+y\)。

   example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) :
       ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by
     sorry
   

脚注

3

例子改编自 Hammack，《Book of Proof》，第 7.3 节。