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 写一个表达式时不写它们， 但它们仍然是我们要证明的语句的重要组成部分。 在 intro 命令之后， 如果我们在冒号 之前 列出所有变量和假设，目标就会和开始时一样， 就像我们在上一节中做的那样。 稍后，我们将看到为什么有时候有必要在证明开始之后引入变量和假设。

为了帮你证明这个引理，我们会给你开个头：

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

使用定理 abs_mul, mul_le_mul, abs_nonneg, mul_lt_mul_right 和 one_mul 完成证明。 记住你可以使用Ctrl-space补全（或者，在Mac中，Cmd-space补全）找到像这样的定理。 也记住你可以使用 .mp 和 .mpr 或者 .1 和 .2 来提取一个当且仅当语句的两个方向。

全称量词通常隐藏在定义中， 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抽象。

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 的结果应该是 f x + g x, 而 dsimp 命令执行了这个简化。 （其中 “d” 是指 “定义性的”） 你可以删除这个命令，证明仍然有效； Lean将不得不执行那个化简，才能使下一个 apply 有意义。 dsimp 命令只是让目标更可读，并帮我们弄清楚下一步要做什么。 另一种选择是通过输入 change f x + g x ≤ a + b 来使用 change 策略。 这有助于提高证明的可读性， 并让你对目标的转换方式有更多的控制。

证明的其余部分都是例行公事。 最后两条 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 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. 要使用单调性假设，可以将其应用于合适的参数和假设，然后将得到的表达式应用于目标。 或者，你也可以将它应用到目标上，然后让 Lean 通过将剩余的假设显示为新的子目标来帮助你向后工作。

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₂ 是隐含的。 下一个例子表明，在实数上，任何由自变量加上非零常数得到的函数都是单射。 然后，我们要求您利用示例中的引理名称作为灵感来源， 证明非零常数乘法也是单射的。 请记住，在猜出一个引理名称的开头后，应使用 Ctrl-space 补全。

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. 存在量词

存在量词，在VS Code中可以用 \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 的 匿名构造器 符号来构造涉及存在量词的证明。

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⟩ 这样，和匿名构造器使用同样的尖括号书写的记号， 称为 样式，它们描述了我们在解包主参数时期望找到的信息。 给出假设 ubf, 即 f 存在上界， rcases ubf with ⟨a, ubfa⟩ 在上下文中添加一个新变量 a 作为上界， 并添加假设 ubfa, 即该变量有给定的性质。 目标没有变化； 已 变化的是我们现在可以使用新对象和新假设来证明目标。 这是数学推理的一种常规方法： 我们解包对象，其存在性被一些假设断言或蕴含， 然后使用它论证其他一些东西的存在性。

试着使用这个方法构建下列事实。 你可能会发现，把上一节中的一些例子转换为具名定理是很有用的， 就像我们对 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 它们的参数。

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. 否定

符号 ¬ 表示否定， 所以 ¬ 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 命令或其后分号的使用， 但我们将在下一节进行讲解。

我们以 爆炸 原理结束本节， 它是说从自相矛盾可以得出任何命题。 在 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. 合取和等价

你已经看到，合取符号 ∧ 用于表示 “且”。 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 应用了 ≤ 的自反性以完成目标。 下面是解决前面的例子的其他一些方法，使用匿名构造器角括号。 第一个是前述证明熟练的证明项版本，在关键字 by 处落入策略模式。

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 中，双向蕴含具有双重身份。 你可以将其视为合取，分别使用其两个部分。 但 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 的典型方式是证明 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, 使我们可以将这两种情况分开。

Lean 也支持计算机科学家用于析取的模式匹配语法。 此时， 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” 的缩写。 使用 case 的好处是你可以以任意顺序证明每种情况； 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

如果你喜欢这些（分情况讨论），并想进一步练习析取，可以试试这些。

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, 它是另一个好例子，展示了析取是如何产生的。 看看你能否使用它证明下列命题：

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

记住你可以使用 ring 策略以帮助计算。

在任意环 \(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

Lean 有一个策略 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 附近 ε 内。 下列例子开始实现这一策略。 看看你能不能完成它。

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

提示，你可以使用 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 标记为隐含变量， 因为它们可以从假设中推断出来。

证明把加法换成乘法的同样定理需要技巧。 为了达到目标，我们会先证明一些辅助性的结论。 看看你能否同样完成下列证明，它表明若 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 有更一般的机制来处理收敛， 它不仅抽象化了定义域和值域的特定特征，还在抽象意义下统一了不同类型的收敛。