3. 逻辑

上一节中，我们处理了等式、不等式和类似与“ \(x\) 整除 \(y\) ”这样的命题。复杂的数学命题是由简单的命题通过逻辑连接词组装起来的，例如“且”、“或”、“非”、“如果……那么……”、“所有……”和“存在……”。本章我们会处理这些使用到逻辑的命题。

3.1. 蕴含和全称量词

考察 #check 后面的语句：

#check ∀ x : ℝ, 0 ≤ x → |x| = x

自然语言表述为 “对于每个实数 x ，若 0 ≤ x ，则 x 的绝对值等于 x ”。我们还可以有更复杂的语句，例如：

#check ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

自然语言表述为 “对于任意的 x, y, 以及 ε ，若 0 < ε ≤ 1, x 的绝对值小于 ε, 且 y 的绝对值小于 ε, 则 x * y 的绝对值小于 ε.” 在 Lean 中，蕴含是右结合的。所以上述表达式的意思是 “若 0 < ε, 则若 ε ≤ 1, 则若 |x| < ε …” 因此，表达式表示所有假设组合在一起导出结论。

尽管这个语句中全称量词的取值范围是对象，而蕴涵箭头引入的是假设，但 Lean 处理这两者的方式非常相似。如果你已经证明了这种形式的定理，你就可以用同样的方法把它应用于对象和假设。让我们以它为例，稍后会证明这个例子。

theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)

#check my_lemma a b δ
#check my_lemma a b δ h₀ h₁
#check my_lemma a b δ h₀ h₁ ha hb

end

Lean 中，当被量词限定的变量可以从后面的假设中推断出来时，常常使用花括号将其设为隐式，这样一来我们就可以直接将引理应用到假设中，而无需提及对象。

theorem my_lemma2 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)

#check my_lemma2 h₀ h₁ ha hb

end

如果使用 apply 策略将 my_lemma 应用于形如 |a * b| < δ 的目标，就会把引理的每个假设作为新的目标。

要证明引理，需使用 intro 策略。

theorem my_lemma3 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  sorry

引入被全称量词限定的变量时可以使用任何名字，并非一定要是 x, y 和 ε 。隐式变量也必须被引入，因为隐式变量的意思是，当我们 使用 my_lemma 时可以不写它们，但证明时还得写，因为它组成了待证命题。下面将看到为什么有时候有必要在证明开始之后引入变量和假设。

你来证明后边的部分。提示：可能会用到 abs_mul, mul_le_mul, abs_nonneg, mul_lt_mul_right 和 one_mul 。另外回忆知识点：你可以使用 .mp 和 .mpr 或者 .1 和 .2 来提取一个当且仅当语句的两个方向。

theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := sorry
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := sorry

全称量词通常隐藏在定义中，Lean 会在必要时展开定义以暴露它们。例如，让我们定义两个谓词，FnUb f a 和 FnLb f a, 其中 f 是一个从实数到实数的函数，而 a 是一个实数。第一个谓词是说 a 是 f 的值的一个上界，而第二个是说 a 是 f 的值的一个下界。

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

在下一个例子中， fun x ↦ f x + g x 是把 x 映射到 `` f x + g x`` 的函数。从表达式 f x + g x 构造这个函数的过程在类型论中称为 lambda 抽象 （lambda abstraction）。

example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by
  intro x
  dsimp
  apply add_le_add
  apply hfa
  apply hgb

把 intro 应用于目标 FnUb (fun x ↦ f x + g x) (a + b) 迫使 Lean 展开 FnUb 的定义并从全称量词中引入 x 。 此时目标为 (fun (x : ℝ) ↦ f x + g x) x ≤ a + b 。把 (fun x ↦ f x + g x) 应用到 x 上（apply func to var，类型论常用话术，指的就是把 var 代入 func 表达式）的结果应该是 f x + g x ， dsimp 命令执行了这个化简（或者说代入取值）。（其中 “d” 是指 “定义性的”）其实你可以删除这个命令，证明仍然有效；Lean 将不得不自行执行化简，才能使下一个 apply 有意义。dsimp 命令有更好的可读性。另一种选择是使用 change 策略，通过输入 change f x + g x ≤ a + b 。这也有助于提高证明的可读性，并让你对目标的转换方式有更多的控制。

证明的其余部分都是例行公事。最后两条 apply 命令迫使 Lean 展开假设中 FnUb 的定义。请尝试进行类似的证明：

example (hfa : FnLb f a) (hgb : FnLb g b) : FnLb (fun x ↦ f x + g x) (a + b) :=
  sorry

example (nnf : FnLb f 0) (nng : FnLb g 0) : FnLb (fun x ↦ f x * g x) 0 :=
  sorry

example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
    FnUb (fun x ↦ f x * g x) (a * b) :=
  sorry

虽然我们已对从实数到实数的函数定义了 FnUb 和 FnLb ，但这些定义和证明完全可推广到对任何两个有序结构的类型之间的函数。检查定理 add_le_add 的类型，发现它对任何是“有序加法交换幺半群”的结构成立；你可以不在乎它具体是什么，但自然数、整数、有理数和实数都属于这种情况。因此，如果我们能在如此广泛的东西上证明定理 fnUb_add ，那么它将可用于所有这些实例中。

variable {α : Type*} {R : Type*} [OrderedCancelAddCommMonoid R]

#check add_le_add

def FnUb' (f : α → R) (a : R) : Prop :=
  ∀ x, f x ≤ a

theorem fnUb_add {f g : α → R} {a b : R} (hfa : FnUb' f a) (hgb : FnUb' g b) :
    FnUb' (fun x ↦ f x + g x) (a + b) := fun x ↦ add_le_add (hfa x) (hgb x)

你在 Section 2.2 中已经看到过像这样的方括号，但我们仍未解释它们的含义。为了具体性，在我们的大多数例子中，我们专注于实数，但 Mathlib 包含一些具有更通用的定义和定理。

再举一个隐藏全称量词的例子， Mathlib 定义了一个谓词 Monotone ，表示函数相对于参数是非递减的：

example (f : ℝ → ℝ) (h : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b :=
  @h

性质 Monotone f 的定义完全就是冒号后的表达式。我们需要在 h 之前输入 @ 符号，不然 Lean 会展开 h 的隐式参数并插入占位符。

证明有关单调性的语句需要使用 intro 引入两个变量，例如 a 和 b, 以及假设 a ≤ b 。

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by
  intro a b aleb
  apply add_le_add
  apply mf aleb
  apply mg aleb

用证明项给出简短的证明往往更方便。描述一个临时引入对象 a 和 b 以及假设 aleb 的证明时，Lean 使用符号 fun a b aleb ↦ ... 。这类似于用 fun x ↦ x^2 这样的表达式来描述一个函数时，先暂时命名一个对象 x, 然后用它来描述函数的值。因此，上一个证明中的 intro 命令对应于下一个证明项中的 lambda 抽象。apply 命令则对应于构建定理对其参数的应用。

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x :=
  fun a b aleb ↦ add_le_add (mf aleb) (mg aleb)

技巧：如果在开始编写证明项 fun a b aleb ↦ _ 时，在表达式的其余部分使用下划线，Lean 就会提示错误，表明它无法猜测该表达式的值。如果你检查 VS Code 中的 Lean 目标窗口或把鼠标悬停在标着波浪线的错误标识符上，Lean 会向你显示剩余的表达式需要解决的目标。

尝试用策略或证明项证明它们：

example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
  sorry

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) :=
  sorry

其他例子。一个从 \(\Bbb R\) 到 \(\Bbb R\) 的函数 \(f\) ，如果对每个 \(x\), 有 \(f(-x) = f(x)\) 则称为 偶函数，如果对每个 \(x\), 有 \(f(-x) = -f(x)\) 则称为 奇函数。下面的例子形式化地定义了这两个概念，证明了一条性质。你来证明其他性质。

def FnEven (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

def FnOdd (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = -f (-x)

example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
  intro x
  calc
    (fun x ↦ f x + g x) x = f x + g x := rfl
    _ = f (-x) + g (-x) := by rw [ef, eg]


example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
  sorry

通过使用 dsimp 或 change 化简 lambda 抽象，可以缩短第一个证明。但你可以验证，除非我们准确地消除 lambda 抽象，否则接下来的 rw 不会生效，因为此时它无法在表达式中找到模式 f x 和 g x 。和其他一些策略不同， rw 作用于语法层次，它不会为你展开定义或应用还原（它有一个变种称为 erw ，在这个方向上会努力一点，但也不会努力太多）。

到处都能找到隐式全称量词，只要你知道如何发现它们。

Mathlib 包含一个用于操作集合的优秀的库。回想一下，Lean 并不使用基于集合论的基础，我们在此使用朴素的集合含义，即某个给定类型 α 的数学对象的汇集。如果 x 具有类型 α, 而 s 具有类型 Set α, 则 x ∈ s 是一个命题，它断言 x 是 s 的一个元素。若 y 具有另一个类型 β 则表达式 y ∈ s 无意义。这里“无意义”的含义是“没有类型因此 Lean 不认可它是一个形式良好的语句”。这与 Zermelo-Fraenkel 集合论不同，例如其中对于每个数学对象 a 和 b, a ∈ b 都是形式良好的语句。例如， sin ∈ cos 是 ZF 中一个形式良好的语句。集合论基础的这一缺陷是证明助手中不使用它的一个重要原因，因为证明助手的目的是帮助我们检出无意义的表达式。在 Lean 中， sin 具有类型 ℝ → ℝ, 而 cos 具有类型 ℝ → ℝ ，它不等于 Set (ℝ → ℝ), 即使在展开定义以后也不相等，因此语句 sin ∈ cos 无意义。我们还可以利用 Lean 来研究集合论本身。例如，连续统假设与 Zermelo-Fraenkel 公理的独立性就在 Lean 中得到了形式化。但这种集合论的元理论完全超出了本书的范围。

若 s 和 t 具有类型 Set α ，那么子集关系 s ⊆ t 被定义为 ∀ {x : α}, x ∈ s → x ∈ t 。量词中的变量被标记为隐式，因此给出 h : s ⊆ t 和 h' : x ∈ s ，我们可以把 h h' 作为 x ∈ t 的证明。下面的例子使用策略证明和证明项，证明了子集关系的反身性，你来类似地证明传递性。

variable {α : Type*} (r s t : Set α)

example : s ⊆ s := by
  intro x xs
  exact xs

theorem Subset.refl : s ⊆ s := fun x xs ↦ xs

theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
  sorry

就像我们对函数定义了 FnUb 一样，假设 s 是一个由某类型的元素组成的集合，且它具有一个与之关联的序。我们可以定义 SetUb s a, 意为 a 是集合 s 的一个上界。在下一个例子中，证明如果 a 是 s 的一个上界，且 a ≤ b ，则 b 也是 s 的一个上界。

variable {α : Type*} [PartialOrder α]
variable (s : Set α) (a b : α)

def SetUb (s : Set α) (a : α) :=
  ∀ x, x ∈ s → x ≤ a

example (h : SetUb s a) (h' : a ≤ b) : SetUb s b :=
  sorry

最后，我们以一个重要的例子来结束本节。函数 \(f\) 称为 单射, 若对每个 \(x_1\) 和 \(x_2\) ，如果 \(f(x_1) = f(x_2)\), 那么 \(x_1 = x_2\) 。Mathlib 定义了 Function.Injective f, 其中 x₁ 和 x₂ 是隐式的。下一个例子表明，在实数上，任何由自变量加上非零常数得到的函数都是单射。然后，你可以利用示例中的引理名称作为灵感来源，证明非零常数乘法也是单射的。

open Function

example (c : ℝ) : Injective fun x ↦ x + c := by
  intro x₁ x₂ h'
  exact (add_left_inj c).mp h'

example {c : ℝ} (h : c ≠ 0) : Injective fun x ↦ c * x := by
  sorry

最后，证明两个单射函数的复合是单射：

variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}

example (injg : Injective g) (injf : Injective f) : Injective fun x ↦ g (f x) := by
  sorry

3.2. 存在量词

存在量词 ∃ （ \ex ）用于表示短语“存在” 。Lean 中的形式表达式 ∃ x : ℝ, 2 < x ∧ x < 3 是说存在一个介于2到3之间的实数。（我们将在 Section 3.4 探讨合取符号。）证明这种语句的典型方式是给出一个实数并说明它具有语句指出的性质。我们可以用 5 / 2 输入2.5这个数，或者，当 Lean 无法从上下文推断出我们想输入实数时，用 (5 : ℝ) / 2 输入，它具有所需的性质，而 norm_num 策略可以证明它符合描述。

我们有一些方式可以把信息聚合在一起。给定一个以存在量词开头的目标，则 use 策略可用于提供对象，留下证明其属性的目标。

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  use 5 / 2
  norm_num

你不仅可以给 use 策略提供数据，还可以提供证明：

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h1 : 2 < (5 : ℝ) / 2 := by norm_num
  have h2 : (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2, h1, h2

事实上， use 策略同样自动地尝试可用的假设。

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2

或者，我们可以使用 Lean 的 匿名构造子（anonymous constructor） 符号来构造涉及存在量词的证明。

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  ⟨5 / 2, h⟩

这里没有用 by ，因为这是证明项。左右尖括号，可以分别用 \< 和 \> 输入，告诉 Lean 使用任何对当前目标合适的构造方式把给定的数据组织起来。我们可以不在策略模式下使用这种符号：

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
  ⟨5 / 2, by norm_num⟩

所以我们现在知道如何证明一个存在语句。但我们要如何 使用 它？如果我们知道存在一个具有特定性质的对象，我们就可以为任意一个对象命名并对其进行推理。例如， 回顾上一节的谓词 FnUb f a 和 FnLb f a ，它们分别是指 a 是 f 的一个上界或下界。我们可以使用存在量词说明 “ f 是有界的”，而无需指定它的界：

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def FnHasUb (f : ℝ → ℝ) :=
  ∃ a, FnUb f a

def FnHasLb (f : ℝ → ℝ) :=
  ∃ a, FnLb f a

我们可以使用上一节的定理 FnUb_add 证明若 f 和 g 具有上界，则 fun x ↦ f x + g x 也有。

variable {f g : ℝ → ℝ}

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  rcases ubf with ⟨a, ubfa⟩
  rcases ubg with ⟨b, ubgb⟩
  use a + b
  apply fnUb_add ubfa ubgb

rcases 策略解包了存在量词中的信息。像 ⟨a, ubfa⟩ 这样长得像是一个匿名构造子的记号，称为 模式（pattern），它们描述了我们在解包主参数时期望找到的信息。给出假设 ubf, 即 f 存在上界，rcases ubf with ⟨a, ubfa⟩ 在上下文中添加一个新变量 a 作为上界，并添加假设 ubfa ，即该变量有给定的性质。这有点像 intro ，目标没有变化，但引入了新对象和新假设来证明目标。这是数学推理的一种常规方法：我们解包对象，其存在性被一些假设断言或蕴含，然后使用它论证其他一些东西的存在性。

试着使用这个方法构建下列命题。你可能用到上一节中的一些例子，所以可以给它们起些名字，就像我们对 fn_ub_add 做的那样，或者你也可以直接把那些论证插入到证明中。

example (lbf : FnHasLb f) (lbg : FnHasLb g) : FnHasLb fun x ↦ f x + g x := by
  sorry

example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
  sorry

rcases 中的 “r” 表示 “recursive（递归）”，因为它允许我们使用任意复杂的模式解包嵌套数据。rintro 策略是 intro 和 rcases 的组合：

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
  rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

事实上，Lean 也支持表达式和证明项中的模式匹配函数：

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x :=
  fun ⟨a, ubfa⟩ ⟨b, ubgb⟩ ↦ ⟨a + b, fnUb_add ubfa ubgb⟩

在假设中解包信息的任务非常重要，以至于 Lean 和 Mathlib 提供了多种方式实施。例如， obtain 策略提供提示性语法：

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  obtain ⟨a, ubfa⟩ := ubf
  obtain ⟨b, ubgb⟩ := ubg
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

将第一条 obtain 指令看作是将 ubf 的“内容”与给定的模式匹配，并将成分赋值给具名变量。rcases 和 obtain 可以说是在 destruct 它们的参数，但有一点不同，rcases 在完成后会清除上下文中的 ubf, 而在 obtain 后它仍然存在。

Lean 还支持与其他函数式编程语言类似的语法：

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  cases ubf
  case intro a ubfa =>
    cases ubg
    case intro b ubgb =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  cases ubf
  next a ubfa =>
    cases ubg
    next b ubgb =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  match ubf, ubg with
    | ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x :=
  match ubf, ubg with
    | ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
      ⟨a + b, fnUb_add ubfa ubgb⟩

在第一个例子中，如果把光标放在 cases ubf 后面，就会看到该策略产生了一个目标，Lean 将其标记为 intro （所选的特定名称来自建立存在性语句证明的公理基元的内部名称）。然后， case 策略会命名各个组件。第二个例子也是类似的，只是使用了 next 而非 case 意味着可以避免提及 intro 。最后两个例子中的 match 一词强调了我们在这里做的是计算机科学家所说的“模式匹配”。请注意，第三个证明以 by 开头，之后的策略版 match 希望在箭头右侧有一个策略证明。最后一个例子是一个证明项，没有策略。

在本书其余部分，我们将坚持使用 rcases, rintros 和 obtain ，作为使用存在量词的首选方式。但看看其他语法也没坏处，尤其是当你有机会与计算机科学家合作时。

为了展示 rcases 的一种使用方法，我们来证明一个经典的数学结果：若两个整数 x 和 y 可以分别写成两个平方数之和，那么它们的乘积 x * y 也可以。事实上，这个结论对任何交换环都是正确的，而不仅仅适用于整数环。在下一个例子中， rcases 同时解包了两个存在量词。然后，我们以列表形式向 use 语句提供将 x * y 表示为平方和所需的值，并使用 ring 来验证它们是否有效。

variable {α : Type*} [CommRing α]

def SumOfSquares (x : α) :=
  ∃ a b, x = a ^ 2 + b ^ 2

theorem sumOfSquares_mul {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
    SumOfSquares (x * y) := by
  rcases sosx with ⟨a, b, xeq⟩
  rcases sosy with ⟨c, d, yeq⟩
  rw [xeq, yeq]
  use a * c - b * d, a * d + b * c
  ring

这个证明并未给出太多直觉洞见，现在我们展示证明思路。高斯整数 是形如 \(a + bi\) 的数，其中 \(a\) 和 \(b\) 是整数，而 \(i = \sqrt{-1}\) 。根据定义，高斯整数 \(a + bi\) 的 范数 是 \(a^2 + b^2\) 。所以高斯整数的范数是平方和，且任意平方和都可以这样表示。上述定理反映了一个事实，即高斯整数的乘积的范数等于范数的乘积：若 \(x\) 是 \(a + bi\) 的范数，且 \(y\) 是 \(c + di\) 的范数，则 \(xy\) 是 \((a + bi) (c + di)\) 的范数。我们充满惊人注意力的证明说明了这样一个事实：最容易形式化的证明并不总是最透彻的。在 Section 6.3 中，我们将为你介绍定义高斯整数的方法，并利用它们提供另一种证明。

在存在量词中解包等式，然后用它来重写目标中的表达式的模式经常出现，以至于 rcases 策略提供了一个缩写：如果使用关键字 rfl 代替新的标识符，rcases 就会自动进行重写（这一技巧不适用于模式匹配的 lambda）。

theorem sumOfSquares_mul' {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
    SumOfSquares (x * y) := by
  rcases sosx with ⟨a, b, rfl⟩
  rcases sosy with ⟨c, d, rfl⟩
  use a * c - b * d, a * d + b * c
  ring

与全称量词一样，存在量词也满地都是。例如，可除性隐含了一个“存在”语句。

example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
  rcases divab with ⟨d, beq⟩
  rcases divbc with ⟨e, ceq⟩
  rw [ceq, beq]
  use d * e; ring

这再次为和 rfl 一起使用 rcases 提供了一个很好的配置。在上面的证明中试试看。感觉还不错！

接下来尝试证明下列定理：

example (divab : a ∣ b) (divac : a ∣ c) : a ∣ b + c := by
  sorry

另一个重要的例子是，若函数 \(f : \alpha \to \beta\) 满足对值域 \(\beta\) 中任意的 \(y\), 存在定义域 \(\alpha\) 中的 \(x\), 使得 \(f(x) = y\) ，那么我们称这个函数是 满射 。注意到这个语句既包含全称量词，也包含存在量词，这解释了为什么接下来的例子同时使用了 intro 和 use 。

example {c : ℝ} : Surjective fun x ↦ x + c := by
  intro x
  use x - c
  dsimp; ring

试试这个，使用定理 mul_div_cancel₀ ：

example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
  sorry

技巧： field_simp 策略通常可以有效地去分母。它可以与 ring 策略结合使用。

example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
  field_simp [h]
  ring

下一个示例使用了满射性假设，将它应用于一个合适的值。你可以在任何表达式中使用 rcases ，而不仅仅是在假设中。

example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
  rcases h 2 with ⟨x, hx⟩
  use x
  rw [hx]
  norm_num

看看你能否用这些方法证明满射函数的复合是满射。

variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}

example (surjg : Surjective g) (surjf : Surjective f) : Surjective fun x ↦ g (f x) := by
  sorry

3.3. 否定

符号 ¬ （ \n , \neg）表示否定，所以 ¬ x < y 是说 x 不小于 y ， ¬ x = y （或者，等价地， x ≠ y）是说 x 不等于 y ，而 ¬ ∃ z, x < z ∧ z < y 是说不存在 z 使其严格位于 x 和 y 之间。在 Lean 中，符号 ¬ A 是 A → False 的缩写，你可以认为它表示 A 导出矛盾。聪明的你会发现，你可以通过引入假设 h : A 并证明 False 来证明 ¬ A ，如果你有 h : ¬ A 和 h' : A ，那么把 h 应用于 h' 就产生 False.

为了演示，考虑严格序的反自反律 lt_irrefl ，它是说对每个 a 我们有 ¬ a < a 。反对称律 lt_asymm 是说我们有 a < b → ¬ b < a 。我们证明， lt_asymm 可从 lt_irrefl 推出。

example (h : a < b) : ¬b < a := by
  intro h'
  have : a < a := lt_trans h h'
  apply lt_irrefl a this

这个例子引入了两个新技巧。第一，当我们使用 have 而不提供名字时，Lean 使用名字 this 。因为这个证明太短，我们提供了精确证明项。但你真正需要注意的是这个证明中 intro 策略的结果，它留下目标 False ，还有，我们最终对 a < a 使用 lt_irrefl 证明了 False 。

这里是另一个例子，它使用上一节定义的谓词 FnHasUb ，也就是说一个函数有上界。

example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
  intro fnub
  rcases fnub with ⟨a, fnuba⟩
  rcases h a with ⟨x, hx⟩
  have : f x ≤ a := fnuba x
  linarith

当目标可由语境中的线性等式和不等式得出时，使用 linarith 通常很方便。

类似地证明下列定理：

example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f :=
  sorry

example : ¬FnHasUb fun x ↦ x :=
  sorry

Mathlib 提供了一些关于序和否定的定理：

#check (not_le_of_gt : a > b → ¬a ≤ b)
#check (not_lt_of_ge : a ≥ b → ¬a < b)
#check (lt_of_not_ge : ¬a ≥ b → a < b)
#check (le_of_not_gt : ¬a > b → a ≤ b)

回顾谓词 Monotone f ，它表示 f 是非递减的。用刚才列举的一些定理证明下面的内容：

example (h : Monotone f) (h' : f a < f b) : a < b := by
  sorry

example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
  sorry

我们可以说明，如果我们把 < 换成 ≤ ，则上一段的第一个例子无法被证明。我们可以通过给出反例证明一个全称量词语句的否定。接下来完成证明：

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f := fun x : ℝ ↦ (0 : ℝ)
  have monof : Monotone f := by sorry
  have h' : f 1 ≤ f 0 := le_refl _
  sorry

这个例子引入了 let 策略，它向语境添加了一个 局部定义。如果你把光标移动到目标窗口的 let 命令后面的地方，你会看到 f : ℝ → ℝ := fun x ↦ 0 已经被添加到语境中。当必须展开定义时， Lean会展开。特别地，当我们使用 le_refl 证明 f 1 ≤ f 0 时，Lean 把 f 1 和 f 0 约化为 0.

使用 le_of_not_gt 证明下列内容：

example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
  sorry

我们刚才所做的许多证明都隐含着这样一个事实：如果 P 是任何属性，说没有任何事物具有 P 属性就等于说一切事物都不具有 P 属性，而说并非所有东西都具有 P 属性等同于说某些东西不具备 P 属性。换句话说，以下四个推理都是有效的（但其中有一个无法使用我们目前已讲解的内容证明）：

variable {α : Type*} (P : α → Prop) (Q : Prop)

example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
  sorry

example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
  sorry

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  sorry

example (h : ∃ x, ¬P x) : ¬∀ x, P x := by
  sorry

第一、二、四个可以使用你已经学到的方法直接证明。鼓励你尝试。然而，第三个更为困难，因为它是从一个对象的不存在可以得出矛盾的这一事实中得出结论，认为该对象是存在的。这是 经典 数学推理的一个实例。我们可以像下面这样使用反证法证明第三个结果。

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  by_contra h'
  apply h
  intro x
  show P x
  by_contra h''
  exact h' ⟨x, h''⟩

确保你搞懂了示例。 by_contra 策略允许我们通过假定 ¬ Q 推出矛盾来证明目标 Q 。事实上，它等价于使用等价关系 not_not : ¬ ¬ Q ↔ Q 。确认一下你可以使用 by_contra 证明这个等价的正方向，而反方向可从常规的否定法则得出。

example (h : ¬¬Q) : Q := by
  sorry

example (h : Q) : ¬¬Q := by
  sorry

用反证法证明下面的内容，它是我们在上面证明的一个蕴涵的相反方向。（提示：先使用 intro ）

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  sorry

处理前面带有否定词的复合语句通常很无趣，通常我们希望会把否定词放进里面。好消息，Mathlib 提供了 push_neg 策略来找到否定词在里面的等价命题。命令 push_neg at h 重述假设 h 。

example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
  push_neg at h
  exact h

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  dsimp only [FnHasUb, FnUb] at h
  push_neg at h
  exact h

在第二个例子中，我们可以使用 dsimp 展开 FnHasUb 和 FnUb 的定义。（我们需要使用 dsimp 而不是 rw 来展开 FnUb, 因为它出现在量词的辖域中。）在上面的例子中，你可以验证对于 ¬∃ x, P x 和 ¬∀ x, P x ， push_neg 策略做了我们期望的事情。即使不知道如何处理合取符号，你也应该能使用 push_neg 证明如下定理：

example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
  sorry

Mathlib 还有一个策略 contrapose ，它把目标 A → B 转化为 ¬B → ¬A 。类似地，给定从假设 h : A 证明 B 的目标， contrapose h 会给你留下从假设 ¬B 证明 ¬A 的目标。使用 contrapose! 将在 contrapose 之外对当前目标（事后假设）应用 push_neg 。

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  contrapose! h
  exact h

example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by
  contrapose! h
  use x / 2
  constructor <;> linarith

下一节解释 constructor 命令及其后分号的使用。

我们以 爆炸原理 （ex falso）结束本节，它是说从自相矛盾可以得出任何命题。在 Lean 中，它用 False.elim 表示，它对于任何命题 P 确认了 False → P 。这似乎是一个奇怪的原理，但它经常出现。我们经常通过分情况来证明定理，有时我们可以证明其中一种情况是矛盾的。在这种情况下，我们需要断言矛盾确证了目标，这样我们就可以继续下一个目标了。（在 Section 3.5 中，我们将看到分情况讨论的实例。）

Lean 提供了多种在出现矛盾时关闭目标的方法。

example (h : 0 < 0) : a > 37 := by
  exfalso
  apply lt_irrefl 0 h

example (h : 0 < 0) : a > 37 :=
  absurd h (lt_irrefl 0)

example (h : 0 < 0) : a > 37 := by
  have h' : ¬0 < 0 := lt_irrefl 0
  contradiction

exfalso 策略把当前的目标替换为证明 False 的目标。给定 h : P 和 h' : ¬ P ，项 absurd h h' 可证明任何命题。最后， contradiction 策略尝试通过在假设中找到矛盾，例如一对形如 h : P 和 h' : ¬ P 的假设来关闭目标。另外本例也可以用 linarith 。

3.4. 合取和双向蕴含

合取符号 ∧ （ \and ）用于表示“且”。 constructor 策略允许你通过分别证明 A 和 B 来证明形如 A ∧ B 的定理。

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
  constructor
  · assumption
  intro h
  apply h₁
  rw [h]

在这个例子中， assumption 策略要求 Lean 寻找一个能解决目标的假设。最后的 rw 应用了 ≤ 的自反性。展示一些使用角括号匿名构造子的等价方法。

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
  ⟨h₀, fun h ↦ h₁ (by rw [h])⟩

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
  have h : x ≠ y := by
    contrapose! h₁
    rw [h₁]
  ⟨h₀, h⟩

使用 合取命题需要拆开两部分的证明。你可以用 rcases 策略做这个，也可以使用 rintro 或一个模式匹配函数 fun ，使用方式和存在量词的情况类似。

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  rcases h with ⟨h₀, h₁⟩
  contrapose! h₁
  exact le_antisymm h₀ h₁

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩ h'
  exact h₁ (le_antisymm h₀ h')

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x :=
  fun ⟨h₀, h₁⟩ h' ↦ h₁ (le_antisymm h₀ h')

像 obtain 策略一样，还有一个模式匹配版的 have ：

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  have ⟨h₀, h₁⟩ := h
  contrapose! h₁
  exact le_antisymm h₀ h₁

和 rcases 相反，这里 have 策略把 h 留在了上下文中。另外，我们展示一些专家喜爱的模式匹配语法，尽管我们不会使用它们：

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  cases h
  case intro h₀ h₁ =>
    contrapose! h₁
    exact le_antisymm h₀ h₁

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  cases h
  next h₀ h₁ =>
    contrapose! h₁
    exact le_antisymm h₀ h₁

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  match h with
    | ⟨h₀, h₁⟩ =>
        contrapose! h₁
        exact le_antisymm h₀ h₁

与使用存在量词不同，你可以通过输入 h.left 和 h.right ，或者等价地， h.1 和 h.2 ，提取假设 h : A ∧ B 两部分的证明。

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  intro h'
  apply h.right
  exact le_antisymm h.left h'

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x :=
  fun h' ↦ h.right (le_antisymm h.left h')

尝试使用这些技术，想出多种方式证明以下内容：

example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m :=
  sorry

你可以通过匿名构造器， rintro 和 rcases 嵌套地使用 ∃ 和 ∧ 命题。

example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
  ⟨5 / 2, by norm_num, by norm_num⟩

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
  rintro ⟨z, xltz, zlty⟩
  exact lt_trans xltz zlty

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y :=
  fun ⟨z, xltz, zlty⟩ ↦ lt_trans xltz zlty

也可以使用 use 策略：

example : ∃ x : ℝ, 2 < x ∧ x < 4 := by
  use 5 / 2
  constructor <;> norm_num

example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
  use 5
  use 7
  norm_num

example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩
  use h₀
  exact fun h' ↦ h₁ (le_antisymm h₀ h')

在第一个例子中， constructor 命令后的分号要求 Lean 对产生的全部两个目标使用 norm_num 策略。

在 Lean 中， A ↔ B 并不 定义为 (A → B) ∧ (B → A) ，但其实如果这样定义也无妨，而且它的行为几乎与此相同。你可以输入 h.mp 和 h.mpr ，或者 h.1 和 h.2 ，用于表示 h : A ↔ B 的两个方向。你也可以使用 cases 及类似策略。要证明一条当且仅当语句，你可以使用 constructor 或角括号，就像你要证明一个合取一样。

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
  constructor
  · contrapose!
    rintro rfl
    rfl
  contrapose!
  exact le_antisymm h

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y :=
  ⟨fun h₀ h₁ ↦ h₀ (by rw [h₁]), fun h₀ h₁ ↦ h₀ (le_antisymm h h₁)⟩

最后一个证明项令人困惑。在编写这样的表达式时，可以使用下划线来查看 Lean 的预期。

尝试你刚才学到的的各种技术和工具以证明下列命题：

example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y :=
  sorry

一个更有意思的练习：请证明，对于任意两个实数 x 和 y ，x^2 + y^2 = 0 当且仅当 x = 0 且 y = 0 。建议使用 linarith, pow_two_nonneg 和 pow_eq_zero 证明一条辅助性的引理。

theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
  have h' : x ^ 2 = 0 := by sorry
  pow_eq_zero h'

example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 :=
  sorry

在 Lean 中，双向蕴含具有双重含义。其一是视为合取，分别使用其两个部分。其二是命题之间的一个反射、对称且传递的关系，可以通过 calc 和 rw 使用它。我们经常把一个语句重写为等价语句。在下一个例子中，我们使用 abs_lt 将形如 |x| < y 的表达式替换为等价表达式 - y < x ∧ x < y ，在下下个例子中，我们使用 Nat.dvd_gcd_iff 将形如 m ∣ Nat.gcd n k 的表达式替换为等价表达式 m ∣ n ∧ m ∣ k 。

example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
  rw [abs_lt]
  intro h
  constructor <;> linarith

example : 3 ∣ Nat.gcd 6 15 := by
  rw [Nat.dvd_gcd_iff]
  constructor <;> norm_num

看看你能否将 rw 与下面的定理结合起来使用来简短地证明“相反数不是一个非递减函数”。(注意 push_neg 不会为你展开定义，所以需要在定理证明中使用 rw [Monotone]）。

theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
  rw [Monotone]
  push_neg
  rfl

example : ¬Monotone fun x : ℝ ↦ -x := by
  sorry

关于合取和双向蕴含的进一步练习。偏序 是一种具有传递性、反身性和反对称性的二元关系。更弱的概念 预序 只是一个反身、传递关系。对于任何预序 ≤ ，Lean 把相应的严格预序公理化定义为 a < b ↔ a ≤ b ∧ ¬ b ≤ a 。证明如果 ≤ 是偏序，那么 a < b 等价于 a ≤ b ∧ a ≠ b ：

variable {α : Type*} [PartialOrder α]
variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b := by
  rw [lt_iff_le_not_le]
  sorry

你只需要 le_refl 和 le_trans 和逻辑运算。证明即使在只假定 ≤ 是预序的情况下，我们也可以证明严格序是反自反的和传递的。在第二个例子中，为了方便，我们使用了化简器而非 rw 把 < 表示为关于 ≤ 和 ¬ 的表达式。我们稍后再讨论化简器，现在你只需要知道它会重复使用指定的引理，即使需要用不同的值将其实例化。

variable {α : Type*} [Preorder α]
variable (a b c : α)

example : ¬a < a := by
  rw [lt_iff_le_not_le]
  sorry

example : a < b → b < c → a < c := by
  simp only [lt_iff_le_not_le]
  sorry

3.5. 析取

证明析取 A ∨ B （ \or ）的典型方式是证明 A 或证明 B 。 left 策略选择 A ， right 策略选择 B 。

variable {x y : ℝ}

example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
  left
  linarith [pow_two_nonneg x]

example (h : -y > x ^ 2 + 1) : y > 0 ∨ y < -1 := by
  right
  linarith [pow_two_nonneg x]

我们不能使用匿名构造子来构造“或”的证明，因为 Lean 猜不出来我们在尝试证明哪个分支。作为替代方式，证明项中可以使用 Or.inl 和 Or.inr 来做出明确的选择。这里， inl 是“引入左项”的缩写，而 inr 是“引入右项”的缩写。

example (h : y > 0) : y > 0 ∨ y < -1 :=
  Or.inl h

example (h : y < -1) : y > 0 ∨ y < -1 :=
  Or.inr h

通过证明一边或另一边来证明析取似乎很奇怪。实际上，哪种情况成立通常取决于假设中隐含或明确的情况区分。

我们通过 rcases 策略来使用形如 A ∨ B 的假设。与在合取或存在量词中使用 rcases 不同，这里的 rcases 策略产生 两个 目标。它们都有相同的结论，但在第一种情况下，A 被假定为真，而在第二种情况下，B 被假定为真。换句话说，顾名思义， rcases 策略给出一个分情况证明。像往常一样，我们可以把假设中用到的名字报告给 Lean。下例中我们告诉 Lean 对每个分支都使用名字 h 。

example : x < |y| → x < y ∨ x < -y := by
  rcases le_or_gt 0 y with h | h
  · rw [abs_of_nonneg h]
    intro h; left; exact h
  · rw [abs_of_neg h]
    intro h; right; exact h

模式从合取情况下的 ⟨h₀, h₁⟩ 变成了析取情况下的 h₀ | h₁ 。可以认为，第一种模式匹配包含 h₀ 和 h₁ 的数据，而第二种模式，也就是带竖线的那种，匹配包含 h₀ 或 h₁ 的数据。在这种情况下，因为两个目标分离，我们对两种情况可以使用同样的名字 h 。

绝对值函数的定义使得我们可以立即证明 x ≥ 0 蕴含着 |x| = x (这就是定理 abs_of_nonneg) 而 x < 0 则蕴含着 |x| = -x``（这是 ``abs_of_neg ）。表达式 le_or_gt 0 x 推出 0 ≤ x ∨ x < 0 ，使我们可以将这两种情况分开。

析取也支持专家式模式匹配语法。此时最好用 cases 策略，因为它允许我们为每个 cases 命名，并在更接近使用的地方为引入的假设命名。

example : x < |y| → x < y ∨ x < -y := by
  cases le_or_gt 0 y
  case inl h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  case inr h =>
    rw [abs_of_neg h]
    intro h; right; exact h

名字 inl 和 inr 分别是 “intro left” 和 “intro right” 的缩写。使用 cases 的好处是你可以以任意顺序证明每种情况；Lean 使用标签找到相关的目标。如果你不在乎这个，你可以使用 next 或者 match ，甚至是模式匹配版的 have 。

example : x < |y| → x < y ∨ x < -y := by
  cases le_or_gt 0 y
  next h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  next h =>
    rw [abs_of_neg h]
    intro h; right; exact h

example : x < |y| → x < y ∨ x < -y := by
  match le_or_gt 0 y with
    | Or.inl h =>
      rw [abs_of_nonneg h]
      intro h; left; exact h
    | Or.inr h =>
      rw [abs_of_neg h]
      intro h; right; exact h

match 下需要用全称 Or.inl 和 Or.inr 来证明析取。本书通常会使用 rcases 来分割析取的情况。

试着用下面前两个定理证明三角不等式。Mathlib 中它也叫这个名字。

namespace MyAbs

theorem le_abs_self (x : ℝ) : x ≤ |x| := by
  sorry

theorem neg_le_abs_self (x : ℝ) : -x ≤ |x| := by
  sorry

theorem abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| := by
  sorry

如果你喜欢这些“分情况讨论”，可以试试这些。 try these.

theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
  sorry

theorem abs_lt : |x| < y ↔ -y < x ∧ x < y := by
  sorry

你也可以将 rcases 和 rintro 与嵌套析取一起使用。当这些功能导致一个真正包含多个目标的情况划分时，每个新目标的模式都会用竖线隔开。

example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
  rcases lt_trichotomy x 0 with xlt | xeq | xgt
  · left
    exact xlt
  · contradiction
  · right; exact xgt

你仍然可以进行模式嵌套，并使用 rfl 来替换等式：

example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
  rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
  · rw [mul_assoc]
    apply dvd_mul_right
  · rw [mul_comm, mul_assoc]
    apply dvd_mul_right

尝试用一行证明下面的内容。使用 rcases 解包假设并分情况讨论，并使用分号和 linarith 解决每个分支。

example {z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
  sorry

在实数中，等式 x * y = 0 告诉我们 x = 0 或 y = 0 。在 Mathlib 中， 这个事实被命名为 eq_zero_or_eq_zero_of_mul_eq_zero ，它是展示生产析取的另一个好例子。使用它证明下列命题（使用 ring 策略简化计算）：

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

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

在任意环 \(R\) 中，对于元素 \(x\), 若存在非零元素 \(y\) 使得 \(x y = 0\) ，则我们把 \(x\) 称为一个 左零因子，若存在非零元素 \(y\) 使得 \(y x = 0\), 则我们把 \(x\) 称为一个 右零因子，是左或右零因子的元素称为 零因子。定理 eq_zero_or_eq_zero_of_mul_eq_zero 是说实数中没有非平凡的零因子。具有这一性质的交换环称为 整环。你对上面两个定理的证明在任意整环中应同样成立：

variable {R : Type*} [CommRing R] [IsDomain R]
variable (x y : R)

example (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  sorry

example (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
  sorry

你证明第一个定理时可以不使用乘法交换律。在那种情况下，只需假定 R 是一个 Ring 而非 CommRing 。

有时在一个证明中我们想要根据一个语句是否为真来划分情况。对于任何命题 P ，我们可以使用 em P : P ∨ ¬ P 。名字 em 是 “excluded middle (排中律)” 的缩写。

example (P : Prop) : ¬¬P → P := by
  intro h
  cases em P
  · assumption
  · contradiction

或者，你也可以使用 by_cases 策略。

example (P : Prop) : ¬¬P → P := by
  intro h
  by_cases h' : P
  · assumption
  contradiction

注意到 by_cases 策略要求你为假设提供一个标签，该标签被用于各个分支，在这个例子中，一个分支是 h' : P 而另一个是 h' : ¬ P 。如果你留空， Lean 默认使用标签 h 。尝试证明如下等价性，使用 by_cases 解决其中一个方向。

example (P Q : Prop) : P → Q ↔ ¬P ∨ Q := by
  sorry

3.6. 序列和收敛

来做一些真正的数学！在 Lean 中，我们可以把实数序列 \(s_0, s_1, s_2, \ldots\) 写成函数 s : ℕ → ℝ 。我们称这个序列 收敛 到数 \(a\) ，如果对任意 \(\varepsilon > 0\) ，存在一个位置，在该位置之后，序列留在距离 \(a\) 不超过 \(\varepsilon\) 的范围内，也就是说，存在数 \(N\), 使得对于任意 \(n \ge N\) ， \(| s_n - a | < \varepsilon\) 。

在 Lean 中，我们可以将其表述如下：

def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

符号 ∀ ε > 0, ... 是 ∀ ε, ε > 0 → ... 的方便缩写，类似地， ∀ n ≥ N, ... 是 ∀ n, n ≥ N →  ... 的缩写。记住 ε > 0 的定义是 0 < ε ，而 n ≥ N 的定义是 N ≤ n 。

本节将证明收敛的一些性质。但首先我们将介绍三个用于处理等式的策略。第一个是 ext 策略，它给我们提供了一种证明两个函数相等的途径。令 \(f(x) = x + 1\) 和 \(g(x) = 1 + x\) 是从实数到实数的函数。当然有 \(f = g\) ，因为对任意 \(x\), 它们返回相同的值。ext 策略允许我们通过证明函数在所有参数下的值都相同来证明函数等式。

example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
  ext
  ring

稍后将看到，可以指定 ext 中出现的变量名。例如，你可以尝试在上面的证明中把 ext 替换为 ext u v 。第二个策略是 congr 策略，它允许我们通过调和有差异的部分来证明两个表达式之间的等式：

example (a b : ℝ) : |a| = |a - b + b| := by
  congr
  ring

在这里 congr 策略剥离两边的 abs ，只留下 a = a - b + b 。

最后， convert 策略用于在定理和结论不完全一致时将定理应用于目标。例如，假定我们想从 1 < a 证明 a < a * a 。库定理 mul_lt_mul_right 让我们证明 1 * a < a * a 。一种可能的方法是逆向工作，重写目标使其具有这种形式。相反， convert 策略原封不动地应用定理，留下证明匹配目标所需等式的任务。

example {a : ℝ} (h : 1 < a) : a < a * a := by
  convert (mul_lt_mul_right _).2 h
  · rw [one_mul]
  exact lt_trans zero_lt_one h

这个示例还说明了另一个有用的技巧：Lean 无法自动填写带下划线的表达式时，它就会把下划线作为另一个目标留给我们。

下面证明任意常数序列 \(a, a, a, \ldots\) 收敛。

theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ ↦ a) a := by
  intro ε εpos
  use 0
  intro n nge
  rw [sub_self, abs_zero]
  apply εpos

策略 simp 经常可以为你省下手写 rw [sub_self, abs_zero] 这种步骤的麻烦。稍后详细介绍。

让我们证明一个更有趣的定理，如果 s 收敛到 a ， t 收敛到 b ，那么 fun n ↦ s n + t n 收敛到 a + b 。在开始写形式证明之前，先建立清晰的纸笔证明是很有帮助的。给定 ε 大于 0 ，思路是利用假设得到 Ns ，使得超出这一位置时， s 在 a 附近 ε / 2 内，以及 Nt ，使得超出这一位置时， s 在 b 附近 ε / 2 内。而后，当 n 大于或等于 Ns 和 Nt 的最大值时，序列 fun n ↦ s n + t n 应在 a + b 附近 ε 内。完成下面的证明。

（提示，你可以使用 le_of_max_le_left 和 le_of_max_le_right ； norm_num 可以证明 ε / 2 + ε / 2 = ε 。还有，使用 congr 策略有助于证明 |s n + t n - (a + b)| 等于 |(s n - a) + (t n - b)| ，因为在那之后你就可以使用三角不等式。把全部变量 s, t, a, b 标记为隐变量，因为它们可以从假设中推断出来。）

theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n + t n) (a + b) := by
  intro ε εpos
  dsimp -- this line is not needed but cleans up the goal a bit.
  have ε2pos : 0 < ε / 2 := by linarith
  rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
  rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
  use max Ns Nt
  sorry

证明把加法换成乘法的同样定理需要技巧。我们会先证明一些辅助性的结论。看看你能否同样完成下列证明，它表明若 s 收敛于 a ，则 fun n ↦ c * s n 收敛于 c * a 。根据 c 是否等于零来区分不同情况有助于证明。我们已经处理了零的情况，现在让你在另一种假设，即 c 非零时证明结论。

theorem convergesTo_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : ConvergesTo s a) :
    ConvergesTo (fun n ↦ c * s n) (c * a) := by
  by_cases h : c = 0
  · convert convergesTo_const 0
    · rw [h]
      ring
    rw [h]
    ring
  have acpos : 0 < |c| := abs_pos.mpr h
  sorry

下一个定理也很有趣：收敛序列在绝对值意义下最终是有界的。完成它。

theorem exists_abs_le_of_convergesTo {s : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) :
    ∃ N b, ∀ n, N ≤ n → |s n| < b := by
  rcases cs 1 zero_lt_one with ⟨N, h⟩
  use N, |a| + 1
  sorry

事实上，该定理还可以加强，断言存在一个对所有 n 值都成立的界 b 。但这个版本对我们的目的来说已经足够强了，我们将在本节结尾看到它在更一般的条件下成立。

接下来的引理是辅助性的：我们证明若 s 收敛到 a 且 t 收敛到 0 ，则 fun n ↦ s n * t n 收敛到 0 。为了证明它，我们使用上一个定理来找到 B ，作为 s 在超出 N₀ 时的界。看看你能否理解我们简述的思路并完成证明。

theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t 0) :
    ConvergesTo (fun n ↦ s n * t n) 0 := by
  intro ε εpos
  dsimp
  rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
  have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
  have pos₀ : ε / B > 0 := div_pos εpos Bpos
  rcases ct _ pos₀ with ⟨N₁, h₁⟩
  sorry

如果你已经走到这一步，那么恭喜你！我们现在已经离定理不远了。下面的证明将为我们画上圆满的句号。

theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n * t n) (a * b) := by
  have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
    apply aux cs
    convert convergesTo_add ct (convergesTo_const (-b))
    ring
  have := convergesTo_add h₁ (convergesTo_mul_const b cs)
  convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
  · ext; ring
  ring

另一个具有挑战性的练习，请试着填写下面的极限唯一性的证明概要。(如果你觉得自信，可以删除证明概要，然后尝试从头开始证明）。

theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ}
      (sa : ConvergesTo s a) (sb : ConvergesTo s b) :
    a = b := by
  by_contra abne
  have : |a - b| > 0 := by sorry
  let ε := |a - b| / 2
  have εpos : ε > 0 := by
    change |a - b| / 2 > 0
    linarith
  rcases sa ε εpos with ⟨Na, hNa⟩
  rcases sb ε εpos with ⟨Nb, hNb⟩
  let N := max Na Nb
  have absa : |s N - a| < ε := by sorry
  have absb : |s N - b| < ε := by sorry
  have : |a - b| < |a - b| := by sorry
  exact lt_irrefl _ this

在本节的最后，我们要指出，我们的证明是可以推广的。例如，我们使用的唯一一条自然数性质是它们的结构带有含 min 和 max 的偏序。如果把 ℕ 换成任意线性序 α, 你可以验证一切仍然正确：

variable {α : Type*} [LinearOrder α]

def ConvergesTo' (s : α → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

在 Section 10.1 中，我们将看到 Mathlib 有更一般的机制来处理收敛，它不仅抽象化了定义域和值域的特定特征，还在抽象意义下统一了不同类型的收敛。