2. 基础知识

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

2.1. 计算

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

在Lean中，陈述一个定理等同于陈述一个目标，即证明该定理的目标。Lean 提供了重写策略 rw，用于在目标中将等式的左侧替换为右侧。 如果 a、 b 和 c 是实数，那么 mul_assoc a b c 是等式 a * b * c = a * (b * c), 而 mul_comm a b 是等式 a * b = b * a. Lean 提供了自动化工具，通常可以消除精确引用这类事实的必要性，但它们对于说明的目的很有用。 在Lean中，乘法左结合，因此 mul_assoc 的左侧也可以写成 (a * b) * c. 然而，通常要注意Lean的记号约定，好的风格是在Lean省略括号时也这样做。

让我们尝试一下 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 中导入了实数理论，以及有用的自动化功能。出于简洁起见，我们通常在教科书中删除此类信息。

欢迎你进行更改以观察发生了什么。你可以在 VS Code 中将 ℝ 字符输入为 \R 或 \real. 该符号直到你按下空格键或制表符键才会出现。当阅读 Lean 文件时，如果你将光标悬停在一个符号上，VS Code 将显示用于输入该符号的语法。 如果你想查看所有可用的缩写，可以按下 Ctrl-Shift-P，然后输入abbreviations来访问 Lean 4: Show Unicode Input Abbreviations 命令。 如果您的键盘上没有方便使用的反斜杠，可以通过更改 lean4.input.leader 设置来改变前导字符。

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

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

在以 ⊢ 开头的行之前的行表示 上下文：它们是当前正在使用的对象和假设。 在这个例子中，它们包括两个对象， x 和 y，每个都是自然数。 它们还包括三个假设，标记为 h₁、 h₂ 和 h₃. 在Lean中，上下文中的所有内容都用标识符标记。你可以将这些带下标的标签键入为 h\1、h\2 和 h\3, 但任何合法的标识符都可以：你可以使用 h1、 h2、 h3，或者 foo、 bar 和 baz. 最后一行代表 目标(goal)，即要证明的事实。有时人们使用 目的(target) 表示要证明的事实，使用 目标(goal) 表示上下文和目的(target)的组合。在实践中，意图通常是明确的。

尝试证明这些等式，在每种情况下都将 sorry 替换为策略证明。 使用 rw 策略时，你可以使用左箭头（\l）来反转一个等式。 例如，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 完成第二个：

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

通过在方括号内用逗号分隔列出相关的等式，可以一次性执行多个重写命令。

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]

你仍然可以通过将光标放置在任何重写列表中逗号的后面，看到增量进展。

另一个技巧是，我们可以在示例或定理之外一次性声明变量。然后，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 确实包含了所有变量。我们可以通过将其放置在一个 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 精确地匹配了目标。

在本节最后，我们将看到，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 策略是在我们导入 Mathlib.Data.Real.Basic 的时候间接导入的，但我们将在下一节中看到它可以用于除了实数之外的其他结构的计算。 可以使用命令 import Mathlib.Tactic 明确导入它。我们将会看到，有一些类似的策略适用于其他常见类型的代数结构。

还有一个名为 nth_rw 的 rw 的变体，它允许你仅替换目标中特定的表达式实例。 可能的匹配项从 1 开始枚举，所以在下面的例子中， nth_rw 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 允许我们使用一般的环定义以及 R 中的元素，并引用一个关于环的定理库。

一些定理的名称可能会令人感到熟悉：它们正是我们在上一节中用来进行实数计算的定理。 Lean 不仅适用于证明关于具体数学结构（如自然数和整数）的事实，还适用于证明关于抽象结构（例如环）的事实，这些抽象结构可以通过公理来刻画。 此外，Lean 支持对抽象和具体结构进行 通用推理，并且可以被训练用于识别适当的实例。 因此，关于环的任何定理都可以应用于具体的环，如整数 ℤ、有理数 ℚ 和复数 ℂ，也可以应用于扩展环的抽象结构的任何实例，例如任何有序环或任何域。

然而，这并不是说实数的所有重要性质在任意环中都成立。 例如，实数上的乘法是交换的，但这对一般的环并不成立。 如果你曾学过线性代数课程，你会意识到，对于每个 \(n\)，由实数组成的 \(n\) 乘 \(n\) 的矩阵形成一个环，在这个环中通常不满足交换性质。 事实上，如果我们声明 R 是一个 交换 环，则在用 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

我们把检查其余证明的过程都不变的任务留给你。 注意，当一个证明很简短时，比如 by ring 或 by linarith 或 by sorry，将其放在与 by 同一行上是常见的（也是允许的）。 良好的证明写作风格应该在简洁性和可读性之间取得平衡。

本节的目标是加强你在上一节中所发展的技能，并将它们应用于对环进行公理推理。 我们将从上面列出的公理开始，利用它们推导出其他事实。 我们证明的大部分事实已经在 Mathlib 中了。 我们将对这些事实在我们证明的版本中赋予相同的名称，以帮助你学习库的内容以及命名惯例。

Lean 提供了与编程语言类似的组织机制：当一个定义或定理 foo 被引入到 命名空间 bar 中时，它的完整名称是 bar.foo. 稍后的命令 open bar 会 打开 这个命名空间，这样我们就可以使用更短的名称 foo. 为了避免由于名称冲突而产生的错误，在下一个示例中，我们将我们的库定理版本放在一个名为 MyRing 的新命名空间中。

下一个示例显示，我们不需要环公理 add_zero 或 add_neg_cancel，因为它们可以由其他公理推导出来。

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

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

theorem add_neg_cancel (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 是一个 隐式参数。我们将在稍后解释这意味着什么，但在现阶段不用担心它。）

下面是一个有用的定理：

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 明确指出了我们所关注的对象。 在这种情况下，输入一些额外的字符并不困难，但如果我们想将 add_left_cancel 应用于更复杂的表达式，写起来将会很繁琐。 在这种情况下，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，它与原始目标具有相同的上下文。 下一行被缩进的事实表明，Lean 正在期待一个策略块来证明这个新目标。 因此，缩进鼓励一种模块化的证明风格：缩进的子证明构建了由 have 引入的目标。 在此之后，我们回到了证明原始目标的过程中，只是添加了一个新的假设 h：一旦证明了它，我们现在就可以自由地使用它。 在这个位置，最终目标正是 add_left_cancel h 的结果。

我们同样可以用 apply add_left_cancel h 或 exact add_left_cancel h 来结束证明。 exact 策略接受一个完全证明当前目标的证明项作为参数，而不会创建任何新的目标。 apply 策略是一个变种，其参数不一定是一个完整的证明。 缺失的部分要么由 Lean 自动推断，要么成为要证明的新目标。 虽然 exact 策略在技术上是多余的，因为它比 apply 更弱，但它略微使证明脚本对人类读者更清晰，并且在库升级时更易于维护。

请记住，乘法并不被假设为可交换的，因此下面的定理也需要一些工作。

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

到现在，你应该也能够在下一个练习中用证明替换每个 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) 而不是 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 是“自反性”的简写。将它作为 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)

当群运算是可交换的时，惯例上使用加法符号，否则使用乘法符号。因此，Lean 定义了一个乘法版本以及一个加法版本（还有它们的阿贝尔变体，AddCommGroup 和 CommGroup）。

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)

正如我们将在 Section 3.1 中更详细地解释的那样， 在 le_trans 的陈述中，隐含的括号向右关联，因此它应被解释为 a ≤ b → (b ≤ c → a ≤ c). 库设计者将参数 a、 b 和 c 设置为 le_trans 的隐含参数，因此 Lean 不会 允许你显式地提供它们（除非你非常坚持，我们稍后将讨论）。 相反，它期望从它们被使用的上下文中推断出它们。 例如，当假设 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 策略接受一个一般陈述或蕴含的证明，尝试将结论与当前目标匹配，并将假设（如果有的话）留作新的目标。 如果给定的证明与目标完全匹配（除了 定义等价性），你可以使用 exact 策略代替 apply. 因此，以下所有操作都是有效的：

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  · 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

在第一个示例中，应用 le_trans 会创建两个目标，并且我们使用点号来表示每个目标的证明开始的位置。 点号是可选的，但它们用于 聚焦 目标：在由点引入的块内，只有一个目标是可见的，并且它必须在块结束之前完成。 在这里，我们通过用另一个点开始一个新块来结束第一个块。我们也可以通过减少缩进来结束。 在第三个示例和最后一个示例中，我们完全避免了进入策略模式： le_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，使用了 双向蕴含，表示“当且仅当”这一短语。 （你可以在 VS Code 中使用 \lr 或 \iff 来输入它。）我们将在下一章更详细地讨论这个连接词。 这样的定理可以与 rw 结合使用，将目标重写为一个等价的目标：

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

然而，在本节中，我们将使用这样一个事实，即如果 h : A ↔ B 是这样一个等价关系， 那么 h.mp 确立了正向方向， A → B，而 h.mpr 确立了逆向方向， B → A. 这里， mp 代表“肯定前件（modus ponens）”， 而 mpr 代表“肯定前件逆向（modus ponens reverse）”。如果你愿意，你还可以分别使用 h.1 和 h.2 来代替 h.mp 和 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

从这些示例中应该清楚，能够找到所需的库定理构成了形式化的重要部分。你可以使用以下几种策略：

• 你可以在 Mathlib 的 GitHub 仓库 中浏览。

• 你可以使用 Mathlib 的 API 文档，位于 Mathlib 的 网页 上。

• 你可以依靠 Mathlib 命名约定和编辑器中的 Ctrl-space 自动完成来猜测定理名称（在 Mac 键盘上是 Cmd-space）。 在 Lean 中，一个名为 A_of_B_of_C 的定理构建了形式为 A 的东西，其假设的形式为 B 和 C ， 其中 A、 B 和 C 近似于我们可能口头读出目标的方式。 因此，一个建立类似于 x + y ≤ ... 的东西的定理可能以 add_le 开头。键入 add_le 并按下 Ctrl-space 将为你提供一些有用的选择。 请注意，按两次 Ctrl-space 会显示有关可用补全的更多信息。

• 如果你在 VS Code 中右键单击现有的定理名称，编辑器将显示一个菜单，其中包含跳转到定义该定理的文件的选项，并且你可以在附近找到类似的定理。

• 你可以使用 apply? 策略，它尝试在库中找到相关的定理。

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

要在此示例中尝试 apply?，请删除 exact 命令并取消注释前一行。利用这些技巧，看看你是否可以找到完成下一个示例所需的内容：

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 的一些自动化功能并不识别这种等价性，因此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 的类型是 ℝ，因此 min 的作用就像我们期望的那样是一个有两个参数的函数。 以这种方式处理多个参数被称为 柯里化，以逻辑学家 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 策略来组织证明，并指示每个块中正在证明的内容。 没有 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 策略。

Lean 的命名规则体现在库中三角不等式的名称里：

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

使用它来证明以下变体，也使用 add_sub_cancel_right ：

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

看看你是否能用三行或更少的代码完成。你可以使用定理 sub_add_cancel.

在接下来的章节中，我们将要使用的另一个重要关系是自然数上的可除性关系，即 x ∣ y. 注意：可除性符号 不 是你键盘上的普通的竖线。相反，它是通过在 VS Code 中键入 \| 获得的 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 将抱怨表达式在通用定理和专门针对自然数的版本 Nat.dvd_antisymm 之间存在歧义。 你可以使用 _root_.dvd_antisymm 来指定通用的版本；任何一个都有效。

2.5. 证明关于代数结构的事实

在 Section 2.2 中，我们看到许多关于实数的常见恒等式适用于更一般的代数结构类，比如交换环。 我们可以使用任何我们想要的公理描述代数结构，而不是仅仅用方程式。 例如，偏序 包括一个具有二元关系的集合，该关系是自反的、传递的和反对称的，就像实数上的 ≤。Lean 知道偏序：

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 这样的字母来表示代数结构（如环和群）的载体，但是一般希腊字母用于类型，特别是当它们与很少或没有结构与之关联时。

对于任何偏序 ≤，还有一个 严格偏序 <，它的行为有点像实数上的 <. 说 x 在此顺序中小于 y 等价于说它小于或等于 y，但不等于 y.

#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

在这个例子中，符号 ∧ 表示 “and”，符号 ¬ 表示 “not”，而 x ≠ y 是 ¬ (x = y) 的缩写。 在 Chapter 3 中，你将学习如何使用这些逻辑连接词来 证明 < 具有所示的属性。

一个 格 是将偏序扩展为具有运算符 ⊓ 和 ⊔ 的结构，这些运算符类似于实数上的 min 和 max：

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)

⊓ 和 ⊔ 的特征使得我们可以合理地称它们为 最大下界 和 最小上界。 在 VS Code 中，你可以使用 glb 和 lub 输入它们。这些符号通常也称为 下确界 和 上确界，在 Mathlib 中，它们在定理名称中被记为 inf 和 sup。 更复杂的是，它们也经常被称为 meet 和 join。因此，如果你使用格，需要记住以下字典：

• ⊓ 是 最大下界、下确界 或 meet.

• ⊔ 是 最小上界、上确界 或 join.

一些格的实例包括：

• 任何全序上的 min 和 max，例如带有 ≤ 的整数或实数

• 某个域的子集合的 ∩ 和 ∪，其中的序是 ⊆

• 布尔真值的 ∧ 和 ∨，其中的序是如果 x 是假或 y 是真，则 x ≤ y

• 自然数（或正自然数）上的 gcd 和 lcm，其中的排序是 ∣

• 向量空间的线性子空间的集合，其中最大下界由交集给出，最小上界由两个空间的和给出，并且序是包含关系

• 一个集合（或在 Lean 中，一个类型）上的拓扑的集合，其中两个拓扑的最大下界由它们的并集生成的拓扑给出，最小上界是它们的交集，并且排序是逆包含关系

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

当看到目标 x ≤ z 时使用 apply le_trans 不是个好主意。 事实上 Lean 无法猜测我们想使用哪个中间元素 y. 因此 apply le_trans 产生形如 x ≤ ?a, ?a ≤ z 以及 α 的三个目标，其中 ?a （也可能有一个更复杂的、自动生成的名字）表示神秘的 y. 最后的目标具有类型 α, 用于提供 y 的值。 它之所以出现在最后，是因为 Lean 希望从第一个目标 x ≤ ?a 的证明中自动推断它。 为了避免这种令人不快的情况， 你可以使用 calc 策略提供精确的 y. 或者，你也可以使用 trans 策略， 它将 y 作为参数，产生期望的目标 x ≤ y 和 y ≤ z. 当然，你也可以通过直接提供完整的证明来避免这个问题，例如 exact le_trans inf_le_left inf_le_right, 但这需要更多规划。

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) 的格，称为 分配格。Lean 也知道这些：

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)

Chapter 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)

掌握了本节内容后，你可以利用以上公理证明距离始终是非负的：

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

我们建议利用 nonneg_of_mul_nonneg_left 完成这个定理的证明。正如你可能已经猜到的那样，在Mathlib中这个定理被称为 dist_nonneg .