2. 基础

介绍 Lean 中数学推理的基本要素：计算、应用引理和定理，以及对通用结构进行推理。

2.1. 计算

通常我们学习数学计算时并不将其视为证明。但是，当我们像 Lean 要求的那样验证计算中的每一步时，最终的结果就是一个证明，我们在证明了算式的左侧等于右侧。

在 Lean 中，陈述一个定理等同于设立证明该定理的目标。Lean 提供了重写（rewrite）策略 rw，它会使用一个等式，rw 在目标中找到符合等式左侧的部分，然后将这部分替换为等式右侧。例如：如果 a、 b 和 c 是实数，那么 mul_assoc a b c 是等式 a * b * c = a * (b * c), 而 mul_comm a b 是等式 a * b = b * a。你想运用这些等式时可以只引用它们的名字。在 Lean 中，乘法左结合，因此 mul_assoc 的左侧也可以写成 (a * b) * c，但是没必要写括号就最好不写。

让我们尝试一下 rw。

example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

教材源码里的 import 行从 Mathlib 中导入了实数理论，以及有用的自动化功能。为简洁计正文中省略，如果你想自己试着运行例子，你可以查询源码来了解。

ℝ 字符通过 \R 或 \real 输入，然后按下空格或 Tab 键。当阅读 Lean 文件时，如果你将光标悬停在一个符号上，VS Code 将显示用于输入该符号的语法。如果你想查看所有可用的缩写，可以按下 Ctrl-Shift-P，然后输入 abbreviations 来访问 Lean 4: Show all abbreviations 命令。如果您的键盘上没有方便使用的反斜杠，可以通过更改 lean4.input.leader 设置来改变前导字符。

当光标位于策略证明的中间时，Lean 会在 Lean Infoview 窗口中报告当前的 证明状态 。当你将光标移到证明的每一步时，你可以看到状态的变化。Lean 中的典型证明状态可能如下所示： .. code-block:

1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4

⊢ 前面的部分是当前位置处我们所拥有的对象和假设，称为 语境（context） 。在这个例子中，语境包括两个对象，自然数 x 和 y；包括三个假设，分别具有标识符 h₁ 、 h₂ 和 h₃ （下标用 \1、\2 …… 键入）。 Lean 的语法要求在语境中每个假设都拥有一个名字，叫什么都可以，比如不下标的 h1 也可以（实际上这是类型论的要求，例如本例中 h₁ 这个”名字”其实标记着类型为命题 Prime x 的项。），或者 foo、 bar 和 baz。最后一行用 ⊢ 标记的代表 目标（goal） ，即要证明的事实。对于目标这个词，一些人有时人们使用 目的（target） 表示要证明的事实，使用 目标（goal） 表示语境和目的（target）的组合，不过在特定上下文中不致混淆。

接下来做一些练习！用 rw 策略替换掉下面的 sorry 。为此再告诉你一个新技巧：你可以用左箭头 ← （ \l ）来调转一个等式的方向，从而让 rw 从另一边做替换操作。例如，rw ← mul_assoc a b c 会把目标里的 a * (b * c) 替换成 a * b * c 。注意这里指的是 mul_assoc 等式的从右到左，它与目标的左边或右边无关。

example (a b c : ℝ) : c * b * a = b * (a * c) := by
  sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

你也可以不带参数使用诸如 mul_assoc 或者 mul_comm 这些等式。这些情况下重写策略会识别它在目标中匹配到的第一个模式。

example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]

你还可以只提供一部分参数，例如 mul_comm a 识别所有形如 a * ? 或者 ? * a 的模式。下面的练习中你可以试试在第一个里面不给参数，第二个里面只给一个参数。

example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
  sorry

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  sorry

你也可以 rw 局部语境里的条件：

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h']
  rw [← mul_assoc]
  rw [h]
  rw [mul_assoc]

试试看：（第二个练习里面你可以使用定理 sub_self，sub_self a 代表等式 a - a = 0。）

example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by
  sorry

example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := by
  sorry

现在我们介绍 Lean 的一些有用的特性. 首先，通过在方括号内列出相关等式，可以用一行重写执行多个命令。

example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

将光标放在 rewrite 列表中的任意逗号后，仍然可以看到进度。

另一个技巧是我们可以在例子或定理之外一次性地声明变量. 当 Lean 在定理的陈述中看到它们时，它会自动将它们包含进来。

variable (a b c d e f : ℝ)

example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]

检查上述证明开头的策略状态，可以发现 Lean 确实包含了相关变量，而忽略了声明中没有出现的 g。我们可以把声明的范围放在一个 section ... end 块中做成类似其他编程语言中局部变量的效果. 最后，回顾一下第一章，Lean为我们提供了一个命令来确定表达式的类型：

section
variable (a b c : ℝ)

#check a
#check a + b
#check (a : ℝ)
#check mul_comm a b
#check (mul_comm a b : a * b = b * a)
#check mul_assoc c a b
#check mul_comm a
#check mul_comm

end

#check 命令对对象和命题都有效。在响应命令 #check a 时，Lean 报告 a 的类型为 ℝ。作为对命令 #check mul_comm a b 的响应，Lean报告 mul_comm a b 是事实 a * b = b * a 的证明。命令 #check (a : ℝ) 表明我们期望 a 的类型是 ℝ，如果不是这样，Lean 将引发一个错误。稍后我们将解释最后三个 #check 命令的输出，你可以尝试自己写一些 #check 命令。

我们再举几个例子。定理 two_mul a 表示 2 * a = a + a。定理 add_mul 和 mul_add 表示乘法对加法的分配律，定理 add_assoc 表示加法的结合律。使用 #check 命令查看精确的语句。

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  rw [mul_add, add_mul, add_mul]
  rw [← add_assoc, add_assoc (a * a)]
  rw [mul_comm b a, ← two_mul]

虽然可以通过在编辑器中逐步检查来弄清楚这个证明中发生了什么，但很难单独阅读。Lean 使用 calc 关键字提供了一种更结构化的方法来编写类似这样的证明。

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    _ = a * a + (b * a + a * b) + b * b := by
      rw [← add_assoc, add_assoc (a * a)]
    _ = a * a + 2 * (a * b) + b * b := by
      rw [mul_comm b a, ← two_mul]

请注意，证明不以 by 开头：以 calc 开头的表达式是一个证明项。 calc 表达式也可以在策略证明块中使用，Lean将其解释为使用证明项的结果来解决当前目标的指令。calc 语法必须严格仿照上例格式使用下划线和对齐。Lean 使用缩进来确定策略块或 calc 块开始和结束的地方。试着改变上面证明中的缩进，看看会发生什么。

编写 calc 证明的一种方法是首先使用 sorry 策略填空，确保 Lean 认可中间步骤表达式，然后使用策略对各个步骤进行论证。

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      sorry
    _ = a * a + (b * a + a * b) + b * b := by
      sorry
    _ = a * a + 2 * (a * b) + b * b := by
      sorry

试试用两种方法证明以下等式：只用 rw 和用更结构化的 calc 。

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  sorry

接下来的练习有点挑战性。你可以用下列的定理。

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

#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a

我们还可以在语句集中的假设中执行重写。例如，rw [mul_comm a b] at hyp 将假设 hyp 中的 a * b 替换为 b * a 。

example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp'] at hyp
  rw [mul_comm d a] at hyp
  rw [← two_mul (a * d)] at hyp
  rw [← mul_assoc 2 a d] at hyp
  exact hyp

最后一步中 exact 策略使用 hyp 来解决目标的原理是，到此 hyp 不就是目标本身了吗！（Exactly!）

最后我们介绍一个 Mathlib 提供的强力自动化工具 ring 策略，它专门用来解决交换环中的等式，只要这些等式是完全由环公理导出的而不涉及别的假设。

example : c * b * a = b * (a * c) := by
  ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
  ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

ring 策略通过 import Mathlib.Data.Real.Basic 导入，但下一节会看到它不止可以用在实数的计算上。它还可以通过 import Mathlib.Tactic 导入。对于其他常见的代数结构也有类似的策略。

rw 有一种叫做 nth_rewrite 的变体，如果目标中存在多处匹配，nth_rw 允许你指出想要实施替换的位置。匹配项从 1 开始计数，在下面的例子中 nth_rewrite 2 [h] 用 c 替换了第二个 a + b。

example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]
  rw [add_mul]

2.2. 证明代数结构中的等式

数学中，环由一个对象集合 \(R\)、运算 \(+\) \(\times\)、常数 \(0\) 和 \(1\)、求逆运算 \(x \mapsto -x\) 构成，并满足：

\(R\) 与 \(+\) 构成阿贝尔群，\(0\) 是加法单位元，负数是逆。
\(1\) 是乘法单位元，乘法满足结合律和对加法的分配律。

在 Lean 中，一组对象被表示为类型 R。环公理如下：

variable (R : Type*) [Ring R]

#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)

一会儿再讲第一行的方括号是什么意思，现在你只需要知道我们声明了一个类型 R 和 R 上的环结构。这样我们就可以表示一般的环中的元素并使用环的定理库。

前一节用过上面的一些定理，所以你应该感觉很熟悉。Lean 不止能在例如自然数和整数这样具体的数学结构上证明东西，也可以在环这样抽象的公理化的结构上证明东西。Lean 支持抽象和具体结构的通用推理，并且有能力识别符合公理的实例。任何关于环的定理都可以应用于具体的环，如整数 ℤ、有理数 ℚ、复数 ℂ，和抽象的环，如任何有序环或任何域。

然而，并不是所有实数的重要性质在任意环中都成立。例如，实数乘法是可交换的，但一般情况下并不成立。例如实数矩阵构成的环的乘法通常不能交换。如果我们声明 R 是一个交换环 CommRing，那么上一节中的所有关于 ℝ 的定理在 R 中仍然成立。

variable (R : Type*) [CommRing R]
variable (a b c d : R)

example : c * b * a = b * (a * c) := by ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring

example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']
  ring

别的证明也都不需要变，你可以自己试试看。当证明很短时，比如你只用了一个 ring 或者 linarith 或者 sorry，你可以把它们写进 by 的同一行里。好的证明写手需要平衡简洁性和可读性。

本节里面我们会证明更多环定理，它们基本上都在 Mathlib 里面，看完这一节你会对 Mathlib 里面的东西更熟悉。同时这也是训练你的证明能力。

Lean 提供了类似于别的编程语言中的 “局域变量” 的变量名组织机制。通过命令 namespace bar 创建一个命名空间 bar 并引入定义或者定理 foo，你在命名空间外面引用它时全名为 bar.foo。命令 open bar 可以打开这个命名空间，此时你可以用短名字 foo。下面我们为了不与 Mathlib 中的定理名冲突，我们打开一个名为 MyRing 的命名空间。

下面的例子证明了 add_zero 和 add_right_neg，所以它们不需要作为环公理。

namespace MyRing
variable {R : Type*} [Ring R]

theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]

theorem add_right_neg (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]

#check MyRing.add_zero
#check add_zero

end MyRing

我们重新证明了库中的定理，但是我们可以继续使用库中的版本。但是下面的练习中请不要作弊，我们只能用我们之前证明过的定理。

（如果你仔细注意的话，你可能已经注意到我们把 (R: Type*) 中的圆括号改成了 {R: Type*} 中的花括号。这里声明 R 是一个 隐式参数（implicit argument） 。稍后会解释这意味着什么。）

下面这个定理很有用：

theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
  rw [← add_assoc, neg_add_cancel, zero_add]

证明它的配套版本：

theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
  sorry

然后用它们证明下面几个（最佳方案仅需三次重写）：

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
  sorry

theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
  sorry

现在解释一下花括号的意思。假设你现在语句集里面拥有变量 a、b、c 和一个假设 h : a + b = a + c，然后你想得到结论 b = c。在Lean中，定理可以应用于假设和事实，就像将它们应用于对象一样，因此你可能会认为 add_left_cancel a b c h 是事实 b = c 的证明。但其实明确地写出 a b c 是多余的，因为假设 h 的形式就限定了它们正是我们想使用的对象。现下输入几个额外的字符并不麻烦，但是更复杂的表达式中就会很繁琐。Lean 支持把参数标记为隐式，这意味着它们可以且应该被省略，能通过后面的的命题和假设中推断出来。{a b c: R} 中的花括号正是这种隐式参数标记。因此根据定理的表述，正确的表达式是 add_left_cancel h。

下面演示个新玩意儿，让我们从环公理中证明 a * 0 = 0。

theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]

你通过 have 策略引入了一个辅助性新目标，a * 0 + a * 0 = a * 0 + 0，与原始目标具有相同的语境。这个目标下的“子证明”块需要缩进。证出这个子目标之后我们就多了一个新的命题 h ，可以用于证明原目标。这里我们看到 add_left_cancel h 的结果恰好就是原目标。

我们同样可以使用 apply add_left_cancel h 或 exact add_left_cancel h 来结束证明。exact 策略将能够完整证明当前目标的证明项作为参数，而不创建任何新目标。apply 策略是一种变体，它的论证不一定是一个完整的证明。缺失的部分要么由 Lean 自动推断，要么成为需要证明的新目标。虽然 exact 策略在技术上是多余的，因为它严格来说不如 apply 强大，但它增加了可读性。(下一节详细讲解 apply 策略的用法。)

乘法不一定可交换，所以下面的定理也需要证。

theorem zero_mul (a : R) : 0 * a = 0 := by
  sorry

更多练习：

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  sorry

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  sorry

theorem neg_zero : (-0 : R) = 0 := by
  apply neg_eq_of_add_eq_zero
  rw [add_zero]

theorem neg_neg (a : R) : - -a = a := by
  sorry

我们必须在第三个定理中指定 (-0 : R), 因为 Lean 不知道我们想到的是哪个 0，默认情况下它是自然数。

在 Lean 中，环中减去一个元素等于加上它的加法逆元。

example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b

实数的减法就是被如此定义的，因此：

example (a b : ℝ) : a - b = a + -b :=
  rfl

example (a b : ℝ) : a - b = a + -b := by
  rfl

rfl 是自反性（reflexivity）的缩写。第一个例子中当它作为 a - b = a + -b 的证明项，Lean 展开定义并验证两边是相同的。第二个例子中 rfl 策略也是如此。这是在 Lean 的基础逻辑中所谓的定义相等的一个例子。这意味着不仅可以用 sub_eq_add_neg 重写来替换 a - b = a + -b，而且在某些情况下，当处理实数时，您可以互换使用方程的两边。例如，您现在有足够的信息来证明上一节中的 self_sub 定理:

theorem self_sub (a : R) : a - a = 0 := by
  sorry

你可以使用 rw 来证，不过如果不是任意环 R 而是实数的话，你也可以用 apply 或者 exact。

Lean 知道 1 + 1 = 2 对任何环都成立。你可以用它来证明上一节中的定理 two_mul：

theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
  norm_num

theorem two_mul (a : R) : 2 * a = a + a := by
  sorry

上面的一些定理并不需要环结构甚至加法交换律，有群结构就够了，群公理是下面这些：

variable (A : Type*) [AddGroup A]

#check (add_assoc : ∀ a b c : A, a + b + c = a + (b + c))
#check (zero_add : ∀ a : A, 0 + a = a)
#check (neg_add_cancel : ∀ a : A, -a + a = 0)

群运算可交换的话习惯上用加号（但是这只是习惯而已，AddGroup 并不真的可交换），否则用乘号。Lean 提供乘法版本 Group 和加法版本 AddGroup ，以及它们的可交换版本 CommGroup 和 AddCommGroup。

variable {G : Type*} [Group G]

#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1)

试试用这些群公理证明以下命题。你可以引入一些引理。

theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by
  sorry

theorem mul_one (a : G) : a * 1 = a := by
  sorry

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  sorry

一步一步用这些定理做证明非常麻烦，所以在这些代数结构上 Mathlib 提供了类似 ring 的策略：group 用于非交换的乘法群，abel 用于可交换加法群，noncomm_ring 用于非交换环。代数结构 Ring 和 CommRing 分别对应的自动化策略被称做 noncomm_ring 和 ring，这似乎很奇怪。这在一定程度上是由于历史原因，但也因为使用更短的名称来处理交换环的策略更方便，因为它使用得更频繁。

2.3. 使用定理和引理

重写对于证明等式很有用，但是对于其他类型的定理呢？例如，我们如何证明一个不等式，比如在 \(b \le c\) 时 \(a + e^b \le a + e^c\) ？本节我们会着重使用 apply 和 exact 。

考虑库定理 le_refl 和 le_trans：

#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)

→ 是右结合的，因此 le_trans 应该被解释为 a ≤ b → (b ≤ c → a ≤ c) 。详细规则在 Section 3.1 一节中解释。标准库设计者已经将 le_trans 中的 a , b 和 c 设置为隐式参数，也就是在使用时从语境中推断。(强制显式参数将在后面讨论)。例如，当假设 h : a ≤ b 和 h' : b ≤ c 在语境中时，以下所有语句都有效：

variable (h : a ≤ b) (h' : b ≤ c)

#check (le_refl : ∀ a : Real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)

apply 策略的作用规则是：它把被 apply 的表达式的结论与当前的目标相匹配，并将前提（如果有的话）作为新目标。如果给定的证明与目标完全匹配（定义等价），则可以使用 exact 策略代替 apply 。你可以考察下面的例子：

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  -- le_trans : a ≤ b → b ≤ c → a ≤ c, `a ≤ c` 匹配到了目标 `x ≤ z`
  -- 于是 `a` 被重命名（正式地：“实例化”）为 `x`，`c`被重命名为 `z`，
  -- `b` 尚未得到它的新名字，因此处在“元变量”（metavariable）状态，表示为 `?b`
  -- 接下来两个前提 `x ≤ ?b`，`?b ≤ z` 成为了新目标
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x

在第一个示例中， apply le_trans 创建两个目标，我们使用点 · （用 \. 或 \centerdot 键入，或者直接用英文句号 . 也可以）来指示对每个目标分别进行证明。这些点并不是语法上必要的，但它们聚焦了目标增加了可读性：在点引入的代码块中，只有一个目标可见，并且必须在代码块结束之前完成证明。另外，点和策略之间其实也可以不用空格。在第三个和最后一个示例中，我们直接构造了证明项 le_transle_trans h₀ h₁ 和 le_refl x 。

另一些库定理：

#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

利用这些定理和 apply 和 exact 策略来证明下面的问题：

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  sorry

实际上 Lean 有一个自动化策略来证明这类问题：

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  linarith

linarith 策略用于处理 线性算术 ，也就是仅涉及加法和数乘的等式和不等式。

example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
  linarith

除了语境中的等式和不等式之外，你还能把其他式子作为参数传给 linarith 。在下一个示例中， exp_le_exp.mpr h' 对应表达式 exp b ≤ exp c ，稍后解释原因。在 Lean 中，我们用 f x 来表示将函数 f 应用于参数 x ，类似地我们用 h x 来表示将事实或定理 h 应用到参数 x 。括号仅用于复合参数，如 f (x + y) 。如果没有括号，f x + y 将被解析为 (f x) + y 。

example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
  linarith [exp_le_exp.mpr h']

这里列出更多库定理，可以用于实数上的不等式：

#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
#check (add_le_add_right : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
#check (add_lt_add_left : a < b → ∀ c, c + a < c + b)
#check (add_lt_add_right : a < b → ∀ c, a + c < b + c)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check add_le_add_left

exp_le_exp 、 exp_lt_exp 和 log_le_log 等定理使用双向蕴含，表示“当且仅当”。(用 \lr 或者 \iff 输入)。我们将在下一章更详细地讨论这个连接词。 rw 也可以处理双向蕴含，就像等号一样，将目标中匹配到的表达式右侧重写成左侧。

example (h : a ≤ b) : exp a ≤ exp b := by
  rw [exp_le_exp]
  exact h

实际上，表达式 h : A ↔ B 是 A → B 和 B → A 的合取，我们可以用 h.mp “肯定前件式”（modus ponens）指代 A → B ，而 h.mpr “肯定前件式的反向”（modus ponens reverse）指代 B → A 。另外还可以用 h.1 表示 h.mp 和用``h.2`` 表示 h.mpr ，虽然这样或许会影响可读性。你可以考察下例；

example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := by
  apply add_lt_add_of_lt_of_le
  · apply add_lt_add_of_le_of_lt h₀
    apply exp_lt_exp.mpr h₁
  apply le_refl

第一行，apply add_lt_add_of_lt_of_le 创建了两个目标，我们再次使用点将两个证明分开。

试试下面的例子。中间的例子展示了 norm_num 策略可用于解决具体数字的问题。

example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry

example : (0 : ℝ) < 1 := by norm_num

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
  have h₀ : 0 < 1 + exp a := by sorry
  apply log_le_log h₀
  sorry

你也许体会到了，寻找你想要的库定理是形式化的重要环节。有以下方式：

在 GitHub 存储库中浏览 Mathlib。
在 Mathlib 网页上查询 API 文档。
根据 Mathlib 命名惯例和编辑器智能代码提示功能来猜测定理名称（有时需要手动用 Ctrl-空格 或 Mac 键盘上的 Cmd-空格 来开启自动补全）。 Mathlib 的一种命名惯例是，定理 A_of_B_of_C 是以前提 B 和 C 推出 A，其中 A 、B 和 C 差不多是把表达式用人类语言朗读出来的样子（但经常会去掉变量名）。因此，形如 x + y ≤ ... 的定理可能会以 add_le 开头。键入 add_le 然后看看编辑器有没有好建议。请注意，按两次 Ctrl-空格 将显示更多可用的信息。（译注：快捷键可能无效，和 VS Code 设置有关，在弹出的提示菜单中可以看到右箭头，点击可展开完整信息。）
VS Code 中，右键单击定理名称将显示一个菜单，其中包含“转到定义”，你可以在附近找到类似的定理。
你可以使用 apply? 策略，这是一个 Mathlib 自带的定理搜索工具，它会自己尝试在库中找到相关的定理。

example : 0 ≤ a ^ 2 := by
  -- apply?
  exact sq_nonneg a

-- 是注释行，你可以取消注释来试着用用 apply? ，然后你可以尝试用这个工具证明下面的例子：

example (h : a ≤ b) : c - exp b ≤ c - exp a := by
  sorry

你可以再试试用 linarith 而不是 apply? 来实现它。其他例子：

example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
  calc
    a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg

  calc
    2 * a * b = 2 * a * b + 0 := by ring
    _ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) := add_le_add (le_refl _) h
    _ = a ^ 2 + b ^ 2 := by ring

Mathlib 习惯于在二元运算符如 * 和 ^ 旁边加空格，不过我不会干扰你的审美喜好。

有几个值得注意的地方。首先，表达式 s ≥ t 和 t ≤ s 定义等价，对人类来说可以互换，但是 Lean 的某些功能不理解这种等价（so sad），因此在 Mathlib 中习惯于使用 ≤ 而不是 ≥。其次，ring 策略真好用！最后，注意到在第二个 calc 证明的第二行中使用了证明项 add_le_add (le_refl _) h，没必要写成 by exact add_le_add (le_refl _) h。

事实上，上例中的唯一需要人类智慧的地方就是找出假设 h ，后面其实只涉及线性算术，都交给 linarith ：

example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
  calc
    a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg
  linarith

好极了！下面是对你的挑战。你可以使用定理 abs_le'.mpr 。你大概还会用到 constructor 策略将一个合取分解为两个目标；参见 Section 3.4 。

example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
  sorry

#check abs_le'.mpr

如果你连这都解决了，说明你马上要成为形式化大师了！

2.4. apply 和 rw 的更多例子

实数上的 min 函数是由以下三个事实定义的：

#check (min_le_left a b : min a b ≤ a)
#check (min_le_right a b : min a b ≤ b)
#check (le_min : c ≤ a → c ≤ b → c ≤ min a b)

你可以想象 max 也使用了类似的定义方式。

注意到我们使用 min a b 而不是 min (a, b) 来将 min 应用于一对参数 a 和 b 。从形式上讲，min 是有两个参数的函数，类型为 ℝ → ℝ → ℝ ，箭头是右结合的，也就是 ℝ → (ℝ → ℝ)。其实际效果是，如果 a 和 b 的类型是 ℝ ，那么 min a 的类型是 ℝ → ℝ，而 min a b 的类型是 ℝ。以这种方式处理多个参数被称为 柯里化（currying），以逻辑学家 Haskell Curry 的名字命名。

在 Lean 中，运算的顺序也可能需要一些时间来适应。函数应用比中缀运算的优先级更高，因此表达式 min a b + c 被解释为 (min a b) + c。你会习惯的。

使用定理 le_antisymm ，我们可以证明两个实数如果彼此小于或等于对方，则它们相等。利用这一点和上述的事实，我们可以证明 min 是可交换的：

example : min a b = min b a := by
  apply le_antisymm
  · show min a b ≤ min b a
    apply le_min
    · apply min_le_right
    apply min_le_left
  · show min b a ≤ min a b
    apply le_min
    · apply min_le_right
    apply min_le_left

这里我们使用点号来分隔不同目标的证明。我们的用法是不一致的：外层对两个目标都使用点和缩进，而内层只对第一个目标使用点。这两种约定都是合理且有用的。我们还使用了 show 策略，它只是展示目标，没它也一样，但这样更易于阅读和维护。

你可能觉得这个证明有两段是重复的。避免重复的一种方法是陈述一个局部引理，然后使用它：

example : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    apply min_le_right
    apply min_le_left
  apply le_antisymm
  apply h
  apply h

我们将在 Section 3.1 中更多地讨论全称量词，但在这里只需说一下，假设 h 表示对于任意的 x 和 y，所需的不等式成立，intro 策略引入了任意的 x 和 y 来证明结论。在 le_antisymm 后的第一个 apply 隐式使用了 h a b，而第二个使用了 h b a 。

另一个避免重复的方法是使用 repeat 策略，它将一个策略（或一个块）尽可能多次地应用。

example : min a b = min b a := by
  apply le_antisymm
  repeat
    apply le_min
    apply min_le_right
    apply min_le_left

练习。你可以使用刚刚描述的任一技巧来缩短第一个证明。

example : max a b = max b a := by
  sorry
example : min (min a b) c = min a (min b c) := by
  sorry

你还可以尝试证明 max 的结合律。

有趣的是， min 在 max 上的分配律就像乘法对加法的分配律一样，反之亦然。换句话说，在实数上，我们有等式 min a (max b c) ≤ max (min a b) (min a c)，以及将 max 和 min 交换后的对应版本。但在下一节中，我们将看到这并不是从 ≤ 的传递性和自反性以及上面列举的 min 和 max 的特性推导出来的。我们需要使用实数上的 ≤ 是全序的事实，也就是说，它满足 ∀ x y，x ≤ y ∨ y ≤ x 。这里的析取符号， ∨ ，代表“或”。在第一种情况下，我们有 min x y = x，而在第二种情况下，我们有 min x y = y。我们将在 Section 3.5 中学习如何根据情况来推理，但现在我们只会使用不需要拆分情况的例子。

例子：

theorem aux : min a b + c ≤ min (a + c) (b + c) := by
  sorry
example : min a b + c = min (a + c) (b + c) := by
  sorry

显然，aux 提供了证明等式所需的两个不等式中的一个，但巧妙地使用它也能证明另一个方向。提示，你可以使用定理 add_neg_cancel_right 和 linarith 策略。

Mathlib 库中的三角不等式体现了 Lean 的命名规则：

#check (abs_add : ∀ a b : ℝ, |a + b| ≤ |a| + |b|)

使用它和 add_sub_cancel_right 和 ``sub_add_cancel``来证明以下变形。最好用三行或更少的代码完成。

example : |a| - |b| ≤ |a - b| :=
  sorry
end

接下来，我们将考察可整除性 x ∣ y 。可整除符号不是你键盘上的普通的竖线，而是通过输入 \| 获得的 Unicode 字符。Mathlib 在定理名称中使用 dvd 来指代它。

example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z :=
  dvd_trans h₀ h₁

example : x ∣ y * x * z := by
  apply dvd_mul_of_dvd_left
  apply dvd_mul_left

example : x ∣ x ^ 2 := by
  apply dvd_mul_left

在最后一个例子中，对于自然数次幂，应用 dvd_mul_left 会强制 Lean 将 x^2 的定义展开为 x^1 * x。

看看你能否找出证明以下内容所需的定理：

example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
  sorry
end

就可整除性而言， 最大公约数 （ gcd ）和最小公倍数（ lcm ）类似于 min 和 max 。由于每个数都可以整除 0，因此 0 在可整除性的意义下表现得像是最大的元素：

variable (m n : ℕ)

#check (Nat.gcd_zero_right n : Nat.gcd n 0 = n)
#check (Nat.gcd_zero_left n : Nat.gcd 0 n = n)
#check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0)
#check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0)

试证明：

example : Nat.gcd m n = Nat.gcd n m := by
  sorry

提示：你可以使用 dvd_antisymm，但它有通用定理和专门针对自然数的两个版本，Lean 有可能会抱怨这里的歧义。此时你可以使用 _root_.dvd_antisymm 来明确指定使用通用版本，或者 Nat.dvd_antisymm 来指定使用自然数版本，任何一个都有效。

2.5. 证明关于代数结构的命题

在 Section 2.2 中，我们看到许多关于实数的常见恒等式适用于更一般的代数结构类，比如交换环。我们还有其他代数结构，例如，偏序是一个具有二元关系的集合，该关系是自反的、传递的和反对称的，就像实数上的 ≤ 。

variable {α : Type*} [PartialOrder α]
variable (x y z : α)

#check x ≤ y
#check (le_refl x : x ≤ x)
#check (le_trans : x ≤ y → y ≤ z → x ≤ z)
#check (le_antisymm : x ≤ y → y ≤ x → x = y)

Mathlib 中习惯用希腊字母 α、 β 和 γ （用 \a、\b 和 \g 输入）等等表示一般类型，使用 R 和 G 等来表示如环和群等特殊的代数结构。

对于任何偏序 ≤，还有一个 严格偏序 <，类似实数上的 < ，是去掉等于的小于等于。

#check x < y
#check (lt_irrefl x : ¬ (x < x))
#check (lt_trans : x < y → y < z → x < z)
#check (lt_of_le_of_lt : x ≤ y → y < z → x < z)
#check (lt_of_lt_of_le : x < y → y ≤ z → x < z)

example : x < y ↔ x ≤ y ∧ x ≠ y :=
  lt_iff_le_and_ne

在这个例子中，符号 ∧ 表示 “且”，符号 ¬ 表示 “非”，而 x ≠ y 是 ¬ (x = y) 的缩写。第 3 章会讲到如何使用这些逻辑连接词来证明 < 具有所示的性质。

一个格是给偏序添加运算符 ⊓ 和 ⊔ 的结构，这些运算符类似于实数上的 min 和 max，称为 最大下界 和 最小上界 （greatest lower bound, least upper bound），用 \glb 和 \lub 输入：

variable {α : Type*} [Lattice α]
variable (x y z : α)

#check x ⊓ y
#check (inf_le_left : x ⊓ y ≤ x)
#check (inf_le_right : x ⊓ y ≤ y)
#check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)
#check x ⊔ y
#check (le_sup_left : x ≤ x ⊔ y)
#check (le_sup_right : y ≤ x ⊔ y)
#check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z)

这些符号通常也称为 下确界 和 上确界 ，在 Mathlib 的定理名称中被记为 inf 和 sup。与此同时它们也经常被称为 meet 和 join。因此，如果你使用格，需要记住以下术语：

⊓ 是最大下界、下确界或 meet 。
⊔ 是最小上界、上确界或 join 。

一些格的实例包括：

任何全序上的 min 和 max，例如带有 ≤ 的整数或实数
某个域的子集合的 ∩ ( \cap ) 和 ∪ ( \cup )，其中的序是 ⊆ ( \subseteq )
布尔真值的 ∧ 和 ∨，其中的序是如果 x 是假或 y 是真，则 x ≤ y
自然数（或正自然数）上的 gcd 和 lcm，其中的序是 ∣
向量空间的线性子空间的集合，其中最大下界由交集给出，最小上界由两个空间的和给出，序是包含关系
一个集合（或在 Lean 中，一个类型）上的拓扑的集合，其中两个拓扑的最大下界由它们的并集生成的拓扑给出，最小上界是它们的交集，并且排序是逆包含关系

你可以验证，与 min / max 和 gcd / lcm 一样，你可以仅使用刻画它们的公理以及 le_refl 和 le_trans 来证明下确界和上确界的交换律和结合律。

example : x ⊓ y = y ⊓ x := by
  sorry

example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := by
  sorry

example : x ⊔ y = y ⊔ x := by
  sorry

example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := by
  sorry

在 Mathlib 中它们分别叫 inf_comm 、 inf_assoc 、 sup_comm 和 sup_assoc 。

另一个很好的练习是仅使用这些公理证明 吸收律：

theorem absorb1 : x ⊓ (x ⊔ y) = x := by
  sorry

theorem absorb2 : x ⊔ x ⊓ y = x := by
  sorry

在 Mathlib 中它们分别叫 inf_sup_self 和 sup_inf_self.

格上附加条件 x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z) 和 x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) 称为 分配格 （distributive lattice）。

variable {α : Type*} [DistribLattice α]
variable (x y z : α)

#check (inf_sup_left x y z : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z)
#check (inf_sup_right x y z : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
#check (sup_inf_left x y z : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
#check (sup_inf_right x y z : x ⊓ y ⊔ z = (x ⊔ z) ⊓ (y ⊔ z))

使用 ⊓ 和 ⊔ 的交换律易证左右两个版本等价。有兴趣的话你可以构造一个不分配的格。现在的目标是尝试证明在任何格中，一个分配律可以推导出另一个分配律。

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

example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) := by
  sorry

example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  sorry

可以将结构公理组合成更大的结构。例如，严格有序环 是一个环上附加偏序，且满足环运算与序是兼容的：

variable {R : Type*} [StrictOrderedRing R]
variable (a b c : R)

#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
#check (mul_pos : 0 < a → 0 < b → 0 < a * b)

第 3 章将从 mul_pos 和 < 的定义中得出以下定理：

#check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b)

下面是一个拓展练习，展示了任何有序环上的算术和序的常见引理。希望你仅使用环、偏序以及上面两个示例中列举的事实来证明它们（环可能并非交换，因此不能用 ring 策略）：

example (h : a ≤ b) : 0 ≤ b - a := by
  sorry

example (h: 0 ≤ b - a) : a ≤ b := by
  sorry

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
  sorry

最后，度量空间 是配备了距离 dist x y 的集合，距离将任何一对元素映射到一个实数，满足以下公理：

variable {X : Type*} [MetricSpace X]
variable (x y z : X)

#check (dist_self x : dist x x = 0)
#check (dist_comm x y : dist x y = dist y x)
#check (dist_triangle x y z : dist x z ≤ dist x y + dist y z)

证明距离始终是非负的。你可能会用到 nonneg_of_mul_nonneg_left 。在 Mathlib 中这个定理被称为 dist_nonneg 。

example (x y : X) : 0 ≤ dist x y := by
  sorry