4.1. 全称量词4.1. The Universal Quantifier🔗

注意，如果α是任意类型，我们可以将p上的一个一元谓词（predicate）表示为类型α → Prop的对象。在这种情况下，给定x : α，p x表示断言p对x成立。类似地，对象r : α → α → Prop表示α上的二元关系（binary relation）：给定x y : α，r x y表示断言x与y相关。Notice that if α is any type, we can represent a unary predicate p on α as an object of type α → Prop. In that case, given x : α, p x denotes the assertion that p holds of x. Similarly, an object r : α → α → Prop denotes a binary relation on α: given x y : α, r x y denotes the assertion that x is related to y.

全称量词（universal quantifier），∀ x : α, p x旨在表示断言“对于每一个x : α，p x”成立。与命题连接词一样，在自然演绎（natural deduction）系统中，“forall”由引入规则（introduction rule）和消去规则（elimination rule）支配。非正式地说，引入规则指出：The universal quantifier, ∀ x : α, p x is supposed to denote the assertion that “for every x : α, p x” holds. As with the propositional connectives, in systems of natural deduction, “forall” is governed by an introduction and elimination rule. Informally, the introduction rule states:

给定p x的一个证明，在x : α是任意的上下文中，我们得到证明∀ x : α, p x。Given a proof of p x, in a context where x : α is arbitrary, we obtain a proof ∀ x : α, p x.

消去规则如下：The elimination rule states:

给定一个证明∀ x : α, p x和任意项t : α，我们得到p t的一个证明。Given a proof ∀ x : α, p x and any term t : α, we obtain a proof of p t.

与蕴含（implication）的情况一样，命题即类型（propositions-as-types）的解释现在发挥了作用。回忆依值箭头类型（dependent arrow type）的引入和消去规则：As was the case for implication, the propositions-as-types interpretation now comes into play. Remember the introduction and elimination rules for dependent arrow types:

给定一个项t，其类型为β x，在x : α是任意的上下文中，我们有(fun x : α => t) : (x : α) → tGiven a term t of type β x, in a context where x : α is arbitrary, we have (fun x : α => t) : (x : α) → β x.

消去规则如下：The elimination rule states:

给定一个项s : (x : α) → β x和任意项t : α，我们有s t : β t。Given a term s : (x : α) → β x and any term t : α, we have s t : β t.

当p x的类型为Prop时，如果我们用∀ x : α, p x替换(x : α) → β x，我们可以将这些解读为构建涉及全称量词的证明的正确规则。In the case where p x has type Prop, if we replace (x : α) → β x with ∀ x : α, p x, we can read these as the correct rules for building proofs involving the universal quantifier.

构造演算（Calculus of Constructions）因此以这种方式将依值箭头类型与全称量词表达式等同起来。如果p是任意表达式，∀ x : α, p不过是(x : α) → p的另一种符号表示，在p是命题的情况下，前者比后者更自然。通常，表达式p将依赖于x : α。回想一下，在普通函数空间的情况下，我们可以将α → β解释为(x : α) → β的特例，其中β不依赖于x。类似地，我们可以将命题之间的蕴含p → q视为∀ x : p, q的特例，其中表达式q不依赖于x。The Calculus of Constructions therefore identifies dependent arrow types with forall-expressions in this way. If p is any expression, ∀ x : α, p is nothing more than alternative notation for (x : α) → p, with the idea that the former is more natural than the latter in cases where p is a proposition. Typically, the expression p will depend on x : α. Recall that, in the case of ordinary function spaces, we could interpret α → β as the special case of (x : α) → β in which β does not depend on x. Similarly, we can think of an implication p → q between propositions as the special case of ∀ x : p, q in which the expression q does not depend on x.

以下是一个示例，展示了命题即类型（propositions-as-types）对应关系如何付诸实践。Here is an example of how the propositions-as-types correspondence gets put into practice.

作为记法约定，我们给予全称量词最宽的作用域，因此需要括号来将上例中的量词限制在假设范围内。证明∀ y : α, p y的标准方式是取一个任意的y，然后证明p y。这就是引入规则。现在，给定h的类型为∀ x : α, p x ∧ q x，表达式h y的类型为p y ∧ q y。这就是消去规则。取左合取（left conjunct）给出所需的结论，p y。As a notational convention, we give the universal quantifier the widest scope possible, so parentheses are needed to limit the quantifier over x to the hypothesis in the example above. The canonical way to prove ∀ y : α, p y is to take an arbitrary y, and prove p y. This is the introduction rule. Now, given that h has type ∀ x : α, p x ∧ q x, the expression h y has type p y ∧ q y. This is the elimination rule. Taking the left conjunct gives the desired conclusion, p y.

记住，仅在约束变量重命名上不同的表达式被视为等价的。因此，例如，我们可以在假设和结论中使用相同的变量x，并在证明中通过不同的变量z来实例化它：Remember that expressions which differ up to renaming of bound variables are considered to be equivalent. So, for example, we could have used the same variable, x, in both the hypothesis and conclusion, and instantiated it by a different variable, z, in the proof:

作为另一个例子，以下是我们如何表达一个关系r是传递的（transitive）：As another example, here is how we can express the fact that a relation, r, is transitive:

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的一个证明。Think about what is going on here. When we instantiate trans_r at the values a b c, we end up with a proof of r a b → r b c → r a c. Applying this to the “hypothesis” hab : r a b, we get a proof of the implication r b c → r a c. Finally, applying it to the hypothesis hbc yields a proof of the conclusion r a c.

在这种情况下，提供参数a b c可能会很繁琐，而它们可以从hab hbc中推断出来。因此，通常将这些参数设为隐式（implicit）：In situations like this, it can be tedious to supply the arguments a b c, when they can be inferred from hab hbc. For that reason, it is common to make these arguments implicit:

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的证明。缺点是在表达式trans_r和trans_r hab中，Lean没有足够的信息来推断参数的类型。第一个#check命令的输出是r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3，表明在这种情况下隐式参数是未指定的。The advantage is that we can simply write trans_r hab hbc as a proof of r a c. A disadvantage is that Lean does not have enough information to infer the types of the arguments in the expressions trans_r and trans_r hab. The output of the first #check command is r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3, indicating that the implicit arguments are unspecified in this case.

以下是一个示例，展示了我们如何使用等价关系（equivalence relation）进行基本推理：Here is an example of how we can carry out elementary reasoning with an equivalence relation:

为了熟悉使用全称量词，你应该尝试本节末尾的一些练习。To get used to using universal quantifiers, you should try some of the exercises at the end of this section.

正是依值箭头类型（以及其中的全称量词）的 typing 规则将Prop与其他类型区分开来。假设我们有α : Sort i和β : Sort j，其中表达式β可能依赖于变量x : α。那么(x : α) → β是Sort (imax i j)的一个元素，其中imax i j是i和j的最大值（如果j不为0），否则为0。It is the typing rule for dependent arrow types, and the universal quantifier in particular, that distinguishes Prop from other types. Suppose we have α : Sort i and β : Sort j, where the expression β may depend on a variable x : α. Then (x : α) → β is an element of Sort (imax i j), where imax i j is the maximum of i and j if j is not 0, and 0 otherwise.

其思想如下。如果j不为0，那么(x : α) → β是Sort (max i j)的一个元素。换句话说，从α到β的依值函数类型“存在于”索引为i和j的最大值的宇宙中。然而，假设β是Sort 0，即Prop的一个元素。在这种情况下，(x : α) → β也是Sort 0的一个元素，无论α存在于哪个类型宇宙中。换句话说，如果β是一个依赖于α的命题，那么∀ x : α, β也是一个命题。这反映了将Prop解释为命题（而非数据）的类型，也是使Prop成为非直谓的（impredicative）的原因。The idea is as follows. If j is not 0, then (x : α) → β is an element of Sort (max i j). In other words, the type of dependent functions from α to β “lives” in the universe whose index is the maximum of i and j. Suppose, however, that β is of Sort 0, that is, an element of Prop. In that case, (x : α) → β is an element of Sort 0 as well, no matter which type universe α lives in. In other words, if β is a proposition depending on α, then ∀ x : α, β is again a proposition. This reflects the interpretation of Prop as the type of propositions rather than data, and it is what makes Prop impredicative.

术语“直谓的（predicative）”源于二十世纪之交的基础性发展，当时像庞加莱（Poincaré）和罗素（Russell）这样的逻辑学家将集合论悖论归咎于“恶性循环”——当我们通过对包含正在被定义的属性本身的集合进行量化来定义一个属性时，这种循环就会出现。注意，如果α是任意类型，我们可以构造所有α上谓词的类型α → Prop（即“α的幂类型”）。Prop的非直谓性意味着我们可以形成对α → Prop进行量化的命题。特别地，我们可以通过对α上所有谓词进行量化来定义α上的谓词，这正是曾被认为有问题的循环类型。The term “predicative” stems from foundational developments around the turn of the twentieth century, when logicians such as Poincaré and Russell blamed set-theoretic paradoxes on the “vicious circles” that arise when we define a property by quantifying over a collection that includes the very property being defined. Notice that if α is any type, we can form the type α → Prop of all predicates on α (the “power type of α”). The impredicativity of Prop means that we can form propositions that quantify over α → Prop. In particular, we can define predicates on α by quantifying over all predicates on α, which is exactly the type of circularity that was once considered problematic.

4.2. 等式4.2. Equality🔗

现在让我们转向 Lean 库中定义的最基本关系之一，即等式关系（equality relation）。在关于归纳类型（inductive types）的章节中，我们将解释等式是如何从 Lean 逻辑框架的原语出发定义的。在此之前，我们在此解释如何使用它。Let us now turn to one of the most fundamental relations defined in Lean's library, namely, the equality relation. In the chapter on inductive types, we will explain how equality is defined from the primitives of Lean's logical framework. In the meanwhile, here we explain how to use it.

当然，等式的一个基本性质是它是一个等价关系（equivalence relation）：Of course, a fundamental property of equality is that it is an equivalence relation:

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 不要插入隐式参数（此处显示为元变量（metavariable））来使输出更易读。We can make the output easier to read by telling Lean not to insert the implicit arguments (which are displayed here as metavariables).

@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处实例化常量。The inscription .{u} tells Lean to instantiate the constants at the universe u.

因此，例如，我们可以将上一节的示例特化到等式关系：Thus, for example, we can specialize the example from the previous section to the equality relation:

我们也可以使用投影记号（projection notation）：We can also use the projection notation:

自反性（Reflexivity）比它看起来更强大。回想一下，构造演算（Calculus of Constructions）中的项具有计算解释，逻辑框架将具有共同归约（reduct）的项视为相同。因此，一些非平凡等式可以通过自反性来证明：Reflexivity is more powerful than it looks. Recall that terms in the Calculus of Constructions have a computational interpretation, and that the logical framework treats terms with a common reduct as the same. As a result, some nontrivial identities can be proved by reflexivity:

框架的这个特性如此重要，以至于库为rfl定义了一个表示法用于Eq.refl _：This feature of the framework is so important that the library defines a notation rfl for Eq.refl _:

然而，等式远不止是一个等价关系。它有一个重要性质：每个断言都尊重等价关系，即我们可以替换相等的表达式而不改变真值。也就是说，给定h1 : a = b和h2 : p a，我们可以使用替换（substitution）构造出p b的证明：Eq.subst h1 h2。Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given h1 : a = b and h2 : p a, we can construct a proof for p b using substitution: Eq.subst h1 h2.

第二种表示法中的三角形是一个宏，构建在Eq.subst和Eq.symm之上，你可以通过输入\t来输入它。The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t.

规则Eq.subst用于定义以下辅助规则，它们执行更明确的替换。它们旨在处理 applicative 项，即形式为s t的项。具体来说，congrArg可用于替换参数，congrFun可用于替换被应用的项，而congr可同时替换两者。The rule Eq.subst is used to define the following auxiliary rules, which carry out more explicit substitutions. They are designed to deal with applicative terms, that is, terms of form s t. Specifically, congrArg can be used to replace the argument, congrFun can be used to replace the term that is being applied, and congr can be used to replace both at once.

Lean 的库包含大量常见的恒等式，例如：Lean's library contains a large number of common identities, such as these:

注意，Nat.mul_add和Nat.add_mul分别是Nat.left_distrib和Nat.right_distrib的别名。以上性质是针对自然数（类型Nat）陈述的。Note that Nat.mul_add and Nat.add_mul are alternative names for Nat.left_distrib and Nat.right_distrib, respectively. The properties above are stated for the natural numbers (type Nat).

以下是一个自然数中结合了替换与结合律和分配律的计算示例。Here is an example of a calculation in the natural numbers that uses substitution combined with associativity and distributivity.

注意，Eq.subst的第二个隐式参数（提供替换发生的上下文）的类型为α → Prop。因此推断这个谓词需要高阶统一（higher-order unification）的实例。一般而言，确定高阶统一子是否存在的问题是不可判定的，Lean最多只能提供不完善和近似的解决方案。因此，Eq.subst并不总能如你所愿。宏h ▸ e使用更有效的启发式方法来计算这个隐式参数，并且通常能在应用Eq.subst失败的情况下成功。Notice that the second implicit parameter to Eq.subst, which provides the context in which the substitution is to occur, has type α → Prop. Inferring this predicate therefore requires an instance of higher-order unification. In full generality, the problem of determining whether a higher-order unifier exists is undecidable, and Lean can at best provide imperfect and approximate solutions to the problem. As a result, Eq.subst doesn't always do what you want it to. The macro h ▸ e uses more effective heuristics for computing this implicit parameter, and often succeeds in situations where applying Eq.subst fails.

由于等式推理非常常见且重要，Lean 提供了多种机制来更有效地执行它。下一节提供了让你以更自然和清晰的方式编写计算证明的语法。但更重要的是，等式推理得到了项重写器（term rewriter）、化简器（simplifier）和其他形式自动化的支持。项重写器和化简器将在下一节中简要描述，然后在下一章中更详细地介绍。Because equational reasoning is so common and important, Lean provides a number of mechanisms to carry it out more effectively. The next section offers syntax that allow you to write calculational proofs in a more natural and perspicuous way. But, more importantly, equational reasoning is supported by a term rewriter, a simplifier, and other kinds of automation. The term rewriter and simplifier are described briefly in the next section, and then in greater detail in the next chapter.

4.3. 计算证明4.3. Calculational Proofs🔗

计算证明（calculational proof）只是一系列中间结果的链条，旨在通过诸如等式的传递性等基本原理组合起来。在 Lean 中，计算证明以关键字calc开始，语法如下：A calculational proof is just a chain of intermediate results that are meant to be composed by basic principles such as the transitivity of equality. In Lean, a calculational proof starts with the keyword calc, and has the following syntax:

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的一个证明。Note that the calc relations all have the same indentation. Each <proof>_i is a proof for <expr>_{i-1} op_i <expr>_i.

我们也可以在第一个关系（紧接在<expr>_0之后）中使用_，这对于对齐关系/证明对的序列很有用：We can also use _ in the first relation (right after <expr>_0) which is useful to align the sequence of relation/proof pairs:

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

示例如下：Here is an example:

这种编写证明的风格在与simp和rw策略（tactic）结合使用时最为有效，这些策略将在下一章中更详细地讨论。例如，使用rw进行重写（rewrite），上述证明可以写成如下形式：This style of writing proofs is most effective when it is used in conjunction with the simp and rw tactics, which are discussed in greater detail in the next chapter. For example, using rw for rewrite, the proof above could be written as follows:

本质上，rw策略使用一个给定的等式（可以是假设、定理名称或复杂项）来“重写”目标。如果这样做将目标简化为恒等式t = t，该策略应用自反性来证明它。Essentially, the rw tactic uses a given equality (which can be a hypothesis, a theorem name, or a complex term) to “rewrite” the goal. If doing so reduces the goal to an identity t = t, the tactic applies reflexivity to prove it.

重写可以顺序应用，因此上述证明可以缩短为：Rewrites can be applied sequentially, so that the proof above can be shortened to this:

甚至更简洁：Or even this:

而simp策略通过反复应用给定的恒等式，以任意顺序，在项中任何适用之处进行重写。它还使用先前已声明给系统的其他规则，并明智地应用交换律以避免循环。因此，我们也可以如下证明该定理：The simp tactic, instead, rewrites the goal by applying the given identities repeatedly, in any order, anywhere they are applicable in a term. It also uses other rules that have been previously declared to the system, and applies commutativity wisely to avoid looping. As a result, we can also prove the theorem as follows:

我们将在下一章讨论rw和simp的变体。We will discuss variations of rw and simp in the next chapter.

calc命令可以为任何支持某种形式传递性的关系配置。它甚至可以组合不同的关系。The calc command can be configured for any relation that supports some form of transitivity. It can even combine different relations.

你可以通过添加Trans类型类的新实例来“教会”calc新的传递性定理。类型类将在后面介绍，但以下小示例演示了如何使用新的Trans实例来扩展calc表示法。You can “teach” calc new transitivity theorems by adding new instances of the Trans type class. Type classes are introduced later, but the following small example demonstrates how to extend the calc notation using new Trans instances.

上面的例子也清楚地表明，即使你的关系没有中缀表示法，你也可以使用calc。Lean 已经包含了整除性的标准 Unicode 表示法（使用∣，可以通过输入\dvd或\mid来输入），所以上面的例子使用了普通的竖线以避免冲突。在实践中，这不是一个好主意，因为它有可能与match ... with表达式中使用的 ASCII |混淆。The example above also makes it clear that you can use calc even if you do not have an infix notation for your relation. Lean already includes the standard Unicode notation for divisibility (using ∣, which can be entered as \dvd or \mid), so the example above uses the ordinary vertical bar to avoid a conflict. In practice, this is not a good idea, as it risks confusion with the ASCII | used in the match ... with expression.

使用calc，我们可以用更自然和清晰的方式编写上一节的证明。With calc, we can write the proof in the last section in a more natural and perspicuous way.