4.1. 全称量词🔗

如果 α 是任何类型，我们可以将 α 上的一元谓词 p 作为 α → Prop 类型的对象。在这种情况下，给定 x : α， p x 表示断言 p 在 x 上成立。类似地，一个对象 r : α → α → Prop 表示 α 上的二元关系：给定 x y : α，r x y 表示断言 x 与 y 相关。

全称量词 ∀ x : α, p x 表示，对于每一个 x : α，p x 成立。与命题连接词一样，在自然演绎系统中，「forall」有引入和消去规则。非正式地，引入规则是：

在 x : α 是任意的情况下，给定 p x 的证明，就可以得到 ∀ x : α, p x 的证明。

消去规则是：

给定 ∀ x : α, p x 的证明和任何项 t : α，就可以得到 p t 的证明。

与蕴含的情况一样，命题即类型。回想依值箭头类型的引入规则：

在 x : α 是任意的情况下，给定类型为 β x 的项 t，就可以得到 (fun x : α => t) : (x : α) → β x。

消去规则：

给定项 s : (x : α) → β x 和任何项 t : α，就可以得到 s t : β t。

在 p x 具有 Prop 类型的情况下，如果我们用 ∀ x : α, p x 替换 (x : α) → β x，就得到构建涉及全称量词的证明的规则。

因此，构造演算用全称表达式来识别依值箭头类型。如果 p 是任何表达式，∀ x : α, p 不过是 (x : α) → p 的替代符号，在 p 是命题的情况下，前者比后者更自然。通常，表达式 p 取决于 x : α。回想一下，在普通函数空间中，我们可以将 α → β 解释为 (x : α) → β 的特殊情况，其中 β 不依赖于 x。类似地，我们可以把命题之间的蕴涵 p → q 看作是 ∀ x : p, q 的特殊情况，其中 q 不依赖于 x。

下面是一个例子，说明了如何运用 命题即类型 对应规则。

作为记法约定，我们给全称量词尽可能大的作用域，因此在上面的例子中需要括号来将 x 的量词限制在假设中。证明 ∀ y : α, p y 的规范方法是取一个任意的 y 并证明 p y。这就是引入规则。现在，给定 h 的类型为 ∀ x : α, p x ∧ q x，表达式 h y 的类型为 p y ∧ q y。这就是消去规则。取左结合项得到了所需的结论 p y。

记住，在重命名绑定变量后相同的表达式被认为是等价的。例如，我们可以在假设和结论中使用相同的变量 x，并在证明中用不同的变量 z 来实例化它：

作为另一个例子，下面是我们如何表达一个关系 r 是传递的：

trans_r : ∀ (x y z : α), r x y → r y z → r x z

trans_r a b c : r a b → r b c → r a c

trans_r a b c hab : r b c → r a c

trans_r a b c hab hbc : r a c

思考一下这里发生了什么。当我们用值 a b c 实例化 trans_r 时，我们最终得到了 r a b → r b c → r a c 的证明。将其应用于「假设」hab : r a b，我们得到了蕴涵式 r b c → r a c 的证明。最后，将其应用于假设 hbc 得到了结论 r a c 的证明。

在这种情况下，当可以从 hab hbc 推断出参数 a b c 时，提供这些参数可能会很繁琐。因此，通常将这些参数设为隐式：

trans_r : r ?m.4 ?m.5 → r ?m.5 ?m.6 → r ?m.4 ?m.6

trans_r hab : r b ?m.6 → r a ?m.6

trans_r hab hbc : r a c

这样做的好处是我们可以简单地将 trans_r hab hbc 写成 r a c 的证明。缺点是 Lean 没有足够的信息来推断表达式 trans_r 和 trans_r hab 中参数的类型。第一个 #check 命令的输出是 r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3，表示在这种情况下隐式参数是未指定的。

下面是一个我们如何使用等价关系进行基本推理的例子：

为了习惯使用全称量词，你应该尝试本节末尾的一些练习。

正是依值箭头类型的类型规则，特别是全称量词，将 Prop 与其他类型区分开来。假设我们有 α : Sort i 和 β : Sort j，其中表达式 β 可能取决于变量 x : α。那么 (x : α) → β 是 Sort (imax i j) 的一个元素，其中 imax i j 是 i 和 j 的最大值（如果 j 不是 0），否则为 0。

其思想如下。如果 j 不是 0，那么 (x : α) → β 是 Sort (max i j) 的一个元素。换句话说，从 α 到 β 的依值函数类型「生活」在索引为 i 和 j 的最大值的宇宙中。然而，假设 β 是 Sort 0 的，即 Prop 的一个元素。在这种情况下，无论 α 生活在哪个类型宇宙中，(x : α) → β 也是 Sort 0 的一个元素。换句话说，如果 β 是取决于 α 的命题，那么 ∀ x : α, β 仍然是一个命题。这反映了将 Prop 解释为命题类型而非数据类型，这也是使 Prop 具有 非直谓性（impredicative） 的原因。

术语「谓词性（predicative）」源于 20 世纪初的基础发展，当时庞加莱（Poincaré）和罗素（Russell）等逻辑学家将集合论悖论归咎于「恶性循环」，即当我们通过对包含正在定义的属性本身的集合进行量化来定义该属性时，就会产生这种循环。请注意，如果 α 是任何类型，我们可以形成 α 上所有谓词的类型 α → Prop（α 的「幂类型」）。Prop 的非直谓性意味着我们可以形成对 α → Prop 进行量化的命题。特别是，

我们可以通过对 α 上的所有谓词进行量化来定义 α 上的谓词，这正是曾经被认为有问题的那种循环。

4.2. 相等🔗

现在让我们转向 Lean 库中定义的最基本的关系之一，即相等关系。在关于 归纳类型 的章节中，我们将解释如何从 Lean 逻辑框架的原语中定义相等。与此同时，在这里我们解释如何使用它。

当然，相等的一个基本性质是它是一个等价关系：

Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

我们可以通过告诉 Lean 不要插入隐式参数（在这里显示为元变量）来使输出更容易阅读。

@Eq.refl : ∀ {α : Sort u} (a : α), a = a

@Eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a

@Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c

标记 .{u} 告诉 Lean 在宇宙 u 实例化常量。

因此，例如，我们可以将上一节中的示例专门用于相等关系：

我们也可以使用投影记法：

自反性比看起来更强大。回想一下，构造演算中的项具有计算解释，并且逻辑框架将具有共同归约结果的项视为相同。因此，一些非平凡的恒等式可以通过自反性来证明：

框架的这一特性非常重要，以至于库为 Eq.refl _ 定义了一个记法 rfl：

然而，相等不仅仅是一个等价关系。它具有一个重要的性质，即每个断言都遵循这种等价性，也就是说，我们可以替换相等的表达式而不改变真值。也就是说，给定 h1 : a = b 和 h2 : p a，我们可以使用替换构造 p b 的证明：Eq.subst h1 h2。

第二个演示中的三角形是建立在 Eq.subst 和 Eq.symm 之上的宏，你可以通过输入 \t 来输入它。

规则 Eq.subst 用于定义以下辅助规则，这些规则执行更显式的替换。它们旨在处理应用项，即形式为 s t 的项。具体来说，congrArg 可用于替换参数，congrFun 可用于替换正在应用的项，而 congr 可用于同时替换两者。

Lean 库包含大量的常用恒等式，例如：

请注意，Nat.mul_add 和 Nat.add_mul 分别是 Nat.left_distrib 和 Nat.right_distrib 的替代名称。上述性质是针对自然数（类型 Nat）陈述的。

下面是一个自然数计算的例子，它使用了替换结合结合律和分配律。

注意，Eq.subst 的第二个隐式参数（提供进行替换的上下文）的类型为 α → Prop。因此，推断此谓词需要 高阶合一（higher-order unification） 的实例。在一般情况下，确定是否存在高阶合一器的问题是不可判定的，Lean 最多只能提供该问题的不完美且近似的解决方案。因此，Eq.subst 并不总是能达到你想要的效果。宏 h ▸ e 使用更有效的启发式方法来计算此隐式参数，并且通常在应用 Eq.subst 失败的情况下成功。

由于等式推理非常普遍且重要，Lean 提供了许多机制来更有效地执行它。下一节提供的语法允许你以更自然、更清晰的方式编写计算证明。但更重要的是，等式推理得到了项重写器、简化器和其他自动化工具的支持。项重写器和简化器将在下一节中简要介绍，然后在下一章中进行更详细的介绍。

4.3. 计算证明🔗

计算证明只是一系列中间结果，这些结果旨在通过基本原理（如相等的传递性）组合而成。在 Lean 中，计算证明以关键字 calc 开始，并具有以下语法：

calc
  <expr>_0  'op_1'  <expr>_1  ':='  <proof>_1
  '_'       'op_2'  <expr>_2  ':='  <proof>_2
  ...
  '_'       'op_n'  <expr>_n  ':='  <proof>_n

注意，calc 关系都具有相同的缩进。每个 <proof>_i 都是 <expr>_{i-1} op_i <expr>_i 的证明。

我们也可以在第一个关系中（紧跟在 <expr>_0 之后）使用 _，这对于对齐关系/证明对序列很有用：

calc <expr>_0
    '_' 'op_1' <expr>_1 ':=' <proof>_1
    '_' 'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_' 'op_n' <expr>_n ':=' <proof>_n

这里有一个例子：

这种编写证明的风格在与 simp 和 rw 策略结合使用时最有效，这些策略将在下一章中更详细地讨论。例如，使用 rw（表示重写），上面的证明可以写成如下形式：

本质上，rw 策略使用给定的等式（可以是假设、定理名称或复杂项）来「重写」目标。如果这样做将目标归约为恒等式 t = t，则该策略应用自反性来证明它。

重写可以按顺序应用，因此上面的证明可以缩短为：

甚至可以这样：

相反，simp 策略通过重复应用给定的恒等式来重写目标，可以以任何顺序应用在项中任何适用的地方。它还使用先前向系统声明的其他规则，并明智地应用交换律以避免循环。因此，我们也可以按如下方式证明该定理：

我们将在下一章讨论 rw 和 simp 的变体。

calc 命令可以为任何支持某种形式传递性的关系进行配置。它甚至可以组合不同的关系。

你可以通过添加 Trans 类型类的新实例来「教」calc 新的传递性定理。类型类将在后面介绍，但下面的小例子演示了如何使用新的 Trans 实例扩展 calc 记法。

上面的例子也清楚地表明，即使你没有关系的中缀记法，你也可以使用 calc。Lean 已经包含了可整除性的标准 Unicode 记法（使用 ∣，可以输入为 \dvd 或 \mid），因此上面的例子使用普通的竖线来避免冲突。在实践中，这不是一个好主意，因为它可能与 match ... with 表达式中使用的 ASCII | 混淆。

使用 calc，我们可以以一种更自然、更清晰的方式编写上一节中的证明。

另一种 calc 记法在这里值得考虑。当第一个表达式占用这么多空间时，在第一个关系中使用 _ 可以自然地对齐所有关系：