12.1. 历史与哲学背景12.1. Historical and Philosophical Context🔗

在其历史的大部分时间里，数学本质上是计算的：几何学处理几何对象的构造，代数学关注方程组的算法求解，分析学提供了计算随时间演化的系统未来行为的方法。从“对每一个x，存在一个y使得……”这样的定理证明中，通常可以直接提取一个算法，用于在给定x时计算出这样的y。For most of its history, mathematics was essentially computational: geometry dealt with constructions of geometric objects, algebra was concerned with algorithmic solutions to systems of equations, and analysis provided means to compute the future behavior of systems evolving over time. From the proof of a theorem to the effect that “for every x, there is a y such that ...”, it was generally straightforward to extract an algorithm to compute such a y given x.

然而，在十九世纪，数学论证复杂性的增加促使数学家发展出新的推理风格，这些风格抑制了算法信息，并引用了对数学对象的描述，抽象掉了这些对象如何表示的细节。目标是获得强大的“概念性”理解而不陷入计算细节的泥潭，但这导致了在直接的计算解读下显然是错误的数学定理的产生。In the nineteenth century, however, increases in the complexity of mathematical arguments pushed mathematicians to develop new styles of reasoning that suppress algorithmic information and invoke descriptions of mathematical objects that abstract away the details of how those objects are represented. The goal was to obtain a powerful “conceptual” understanding without getting bogged down in computational details, but this had the effect of admitting mathematical theorems that are simply false on a direct computational reading.

今天仍然存在相当一致的共识，即计算对数学很重要。但对于如何最好地处理计算问题，存在不同的观点。从构造性（constructive）的观点来看，将数学与其计算根源分离开来是错误的；每一个有意义的数学定理都应该具有直接的计算解释。从经典（classical）的观点来看，更有效的方法是保持关注点分离（separation of concerns）：我们可以使用一种语言和一套方法来编写计算机程序，同时保持使用非构造性（nonconstructive）理论和方法来推理它们的自由。Lean 被设计为支持这两种方法。核心库的部分是以构造性方式开发的，但系统也提供了进行经典数学推理的支持。There is still fairly uniform agreement today that computation is important to mathematics. But there are different views as to how best to address computational concerns. From a constructive point of view, it is a mistake to separate mathematics from its computational roots; every meaningful mathematical theorem should have a direct computational interpretation. From a classical point of view, it is more fruitful to maintain a separation of concerns: we can use one language and body of methods to write computer programs, while maintaining the freedom to use nonconstructive theories and methods to reason about them. Lean is designed to support both of these approaches. Core parts of the library are developed constructively, but the system also provides support for carrying out classical mathematical reasoning.

从计算的角度来看，依值类型理论中最纯粹的部分完全避免使用Prop。归纳类型和依值函数类型可以被视为数据类型，这些类型的项（terms）可以通过应用归约规则直到无法再应用任何规则来“求值”。原则上，任何类型为Nat的封闭项（即没有自由变量的项）应该求值为一个数字，如succ (… (succ zero)…)。Computationally, the purest part of dependent type theory avoids the use of Prop entirely. Inductive types and dependent function types can be viewed as data types, and terms of these types can be “evaluated” by applying reduction rules until no more rules can be applied. In principle, any closed term (that is, term with no free variables) of type Nat should evaluate to a numeral, succ (… (succ zero)…).

引入证明无关的Prop并将定理标记为不可归约是迈向关注点分离的第一步。其意图是类型p : Prop的元素在计算中不应起作用，因此项prf : p的特定构造在这个意义上是“无关的”。仍然可以定义包含Prop类型元素的计算对象；关键是这些元素可以帮助我们推理计算的效果，但在从项中提取“代码”时可以忽略。然而，Prop类型的元素并非完全无害。它们包括任意类型α上的等式s = t : α，这样的等式可以用作强制类型转换（cast）来对项进行类型检查。下面我们将看到这样的强制转换如何阻塞系统中的计算。然而，在擦除命题内容、忽略中间类型约束并将项归约直至其达到范式（normal form）的求值方案下，计算仍然是可能的。这正是 Lean 的虚拟机（virtual machine）所做的。Introducing a proof-irrelevant Prop and marking theorems irreducible represents a first step towards separation of concerns. The intention is that elements of a type p : Prop should play no role in computation, and so the particular construction of a term prf : p is “irrelevant” in that sense. One can still define computational objects that incorporate elements of type Prop; the point is that these elements can help us reason about the effects of the computation, but can be ignored when we extract “code” from the term. Elements of type Prop are not entirely innocuous, however. They include equations s = t : α for any type α, and such equations can be used as casts, to type check terms. Below, we will see examples of how such casts can block computation in the system. However, computation is still possible under an evaluation scheme that erases propositional content, ignores intermediate typing constraints, and reduces terms until they reach a normal form. This is precisely what Lean's virtual machine does.

采用证明无关的Prop之后，人们可能会认为使用排中律p ∨ ¬p（其中p是任意命题）是合理的。当然，这也会阻塞 CIC 规则下的计算，但不会阻止如上所述的可执行代码的生成。只有在关于选择（choice）的章节中讨论的选择原理才完全抹消了理论中证明无关部分与数据相关部分之间的区别。Having adopted a proof-irrelevant Prop, one might consider it legitimate to use, for example, the law of the excluded middle, p ∨ ¬p, where p is any proposition. Of course, this, too, can block computation according to the rules of CIC, but it does not prevent the generation of executable code, as described above. It is only the choice principles discussed in the section on choice that completely erase the distinction between the proof-irrelevant and data-relevant parts of the theory.

12.2. 命题外延性（Propositional Extensionality）12.2. Propositional Extensionality🔗

命题外延性即以下公理：Propositional extensionality is the following axiom:

它断言当两个命题相互蕴涵时，它们实际上是相等的。这与集合论解释一致，其中a : Prop的任意元素要么是空集，要么是单点集{*}（对于某个特定的元素*）。该公理的效果是等价的命题可以在任何上下文中相互替换：It asserts that when two propositions imply one another, they are actually equal. This is consistent with set-theoretic interpretations in which any element a : Prop is either empty or the singleton set \{\ast\}, for some distinguished element \ast. The axiom has the effect that equivalent propositions can be substituted for one another in any context:

12.3. 函数外延性（Function Extensionality）12.3. Function Extensionality🔗

与命题外延性类似，函数外延性断言类型(x : α) → β x的任意两个函数，如果在所有输入上一致，则它们是相等的：Similar to propositional extensionality, function extensionality asserts that any two functions of type (x : α) → β x that agree on all their inputs are equal:

从经典的集合论视角来看，这正是两个函数相等的含义。这被称为函数的“外延（extensional）”观点。然而，从构造性视角来看，有时更自然的是将函数视为以某种显式方式呈现的算法或计算机程序。当然，两个计算机程序可以为每个输入计算出相同的答案，尽管它们在语法上相当不同。类似地，你可能会希望保持一种不强迫你将输入/输出行为相同的两个函数视为同一的函数观点。这被称为函数的“内涵（intensional）”观点。From a classical, set-theoretic perspective, this is exactly what it means for two functions to be equal. This is known as an “extensional” view of functions. From a constructive perspective, however, it is sometimes more natural to think of functions as algorithms, or computer programs, that are presented in some explicit way. It is certainly the case that two computer programs can compute the same answer for every input despite the fact that they are syntactically quite different. In much the same way, you might want to maintain a view of functions that does not force you to identify two functions that have the same input / output behavior. This is known as an “intensional” view of functions.

实际上，函数外延性可以从商（quotients）的存在性推导出来，我们将在下一节中描述。因此，在 Lean 标准库中，funext是从商构造中证明的。In fact, function extensionality follows from the existence of quotients, which we describe in the next section. In the Lean standard library, therefore, funext is thus proved from the quotient construction.

假设对于α : Type u，我们定义Set α:= α → Prop来表示α的子集类型，本质上是将子集与谓词（predicates）等同起来。通过组合funext和propext，我们获得了这些集合的外延理论：Suppose that for α : Type u we define the Set α:= α → Prop to denote the type of subsets of α, essentially identifying subsets with predicates. By combining funext and propext, we obtain an extensional theory of such sets:

然后我们可以继续定义空集和集合交集等，并证明集合恒等式：We can then proceed to define the empty set and set intersection, for example, and prove set identities:

以下是一个示例，说明函数外延性如何阻塞 Lean 内核内的计算：The following is an example of how function extensionality blocks computation inside the Lean kernel:

f_eq_g ▸ 0

0

首先，我们使用函数外延性证明两个函数f和g相等，然后通过将类型中的f替换为g来强制转换0（类型为Nat）的类型。当然，这个强制转换是空洞的，因为Nat不依赖于f。但这足以造成损害：在系统的计算规则下，我们现在有一个类型为Nat的封闭项，它不会归约为一个数字。在这种情况下，我们可能想将表达式归约为0。但在非平凡的例子中，消除强制转换会改变项的类型，可能使周围的表达式类型不正确。然而，虚拟机可以毫无问题地将表达式求值为0。以下是一个类似的人为示例，展示了propext如何造成阻碍：First, we show that the two functions f and g are equal using function extensionality, and then we cast 0 of type Nat by replacing f by g in the type. Of course, the cast is vacuous, because Nat does not depend on f. But that is enough to do the damage: under the computational rules of the system, we now have a closed term of Nat that does not reduce to a numeral. In this case, we may be tempted to reduce the expression to 0. But in nontrivial examples, eliminating cast changes the type of the term, which might make an ambient expression type incorrect. The virtual machine, however, has no trouble evaluating the expression to 0. Here is a similarly contrived example that shows how propext can get in the way:

tteq ▸ 0

0

当前的研究计划，包括观察类型论（observational type theory）和立方类型论（cubical type theory）的工作，旨在以允许对涉及函数外延性、商等的强制转换进行归约的方式来扩展类型论。但这些解决方案并不那么明确，Lean 底层演算的规则也不认可这样的归约。Current research programs, including work on observational type theory and cubical type theory, aim to extend type theory in ways that permit reductions for casts involving function extensionality, quotients, and more. But the solutions are not so clear-cut, and the rules of Lean's underlying calculus do not sanction such reductions.

然而从某种意义上说，强制转换并不改变表达式的含义。相反，它是推理表达式类型的一种机制。在适当的语义下，以保持其含义的方式归约项是合理的，忽略为使归约类型正确所需的中间簿记。在这种情况下，在Prop中添加新公理并不重要；通过证明无关性（proof irrelevance），Prop中的表达式不携带任何信息，可以被归约过程安全地忽略。In a sense, however, a cast does not change the meaning of an expression. Rather, it is a mechanism to reason about the expression's type. Given an appropriate semantics, it then makes sense to reduce terms in ways that preserve their meaning, ignoring the intermediate bookkeeping needed to make the reductions type-correct. In that case, adding new axioms in Prop does not matter; by proof irrelevance, an expression in Prop carries no information, and can be safely ignored by the reduction procedures.

12.4. 商（Quotients）12.4. Quotients🔗

设α为任意类型，r为α上的一个等价关系。数学上通常形成“商”α / r，即α“模”r的元素的类型。在集合论中，可以将α / r视为α模r的等价类集合。如果f : α → β是任何尊重该等价关系的函数，即对于任意x y : α，r x y蕴涵f x = f y，那么f可以“提升”为一个函数f’ : α / r → β，定义为f’ ⟦x⟧ = f x，其中⟦x⟧是包含x的等价类。Lean 的标准库使用额外的常量扩展了构造演算，这些常量精确地执行这些构造，并将最后一个等式作为定义性归约规则（definitional reduction rule）安装。Let α be any type, and let r be an equivalence relation on α. It is mathematically common to form the “quotient” α / r, that is, the type of elements of α “modulo” r. Set theoretically, one can view α / r as the set of equivalence classes of α modulo r. If f : α → β is any function that respects the equivalence relation in the sense that for every x y : α, r x y implies f x = f y, then f “lifts” to a function f' : α / r → β defined on each equivalence class ⟦x⟧ by f' ⟦x⟧ = f x. Lean's standard library extends the Calculus of Constructions with additional constants that perform exactly these constructions, and installs this last equation as a definitional reduction rule.

在其最基本的形式中，商构造甚至不需要r是等价关系。以下常量内置于 Lean 中：In its most basic form, the quotient construction does not even require r to be an equivalence relation. The following constants are built into Lean:

第一个常量根据任意二元关系r在类型α上形成一个类型Quot r。第二个将α映射到Quot α，因此如果r : α → α → Prop且a : α，则Quot.mk r a是Quot r的一个元素。第三个原理Quot.ind说明Quot.mk r a的每个元素都是这种形式。至于Quot.lift，给定一个函数f : α → β，如果h是f尊重关系r的证明，那么Quot.lift f h就是Quot r上对应的函数。其思想是，对于α中的每个元素a，函数Quot.lift f h将Quot.mk r a（包含a的r-类）映射到f a，其中h表明这个函数是良定义的。实际上，计算原理被声明为一条归约规则，如下面的证明所示。The first one forms a type Quot r given a type α by any binary relation r on α. The second maps α to Quot α, so that if r : α → α → Prop and a : α, then Quot.mk r a is an element of Quot r. The third principle, Quot.ind, says that every element of Quot.mk r a is of this form. As for Quot.lift, given a function f : α → β, if h is a proof that f respects the relation r, then Quot.lift f h is the corresponding function on Quot r. The idea is that for each element a in α, the function Quot.lift f h maps Quot.mk r a (the r-class containing a) to f a, wherein h shows that this function is well defined. In fact, the computation principle is declared as a reduction rule, as the proof below makes clear.

Quot mod7Rel : Type

Quot.mk mod7Rel 4 : Quot mod7Rel

Quot.lift f f_respects : Quot mod7Rel → Bool

这四个常量Quot、Quot.mk、Quot.ind和Quot.lift本身并不非常强大。你可以验证，如果我们简单地将Quot r取为α，并将Quot.lift取为恒等函数（忽略h），Quot.ind就被满足。因此，这四个常量不被视为额外的公理。The four constants, Quot, Quot.mk, Quot.ind, and Quot.lift in and of themselves are not very strong. You can check that the Quot.ind is satisfied if we take Quot r to be simply α, and take Quot.lift to be the identity function (ignoring h). For that reason, these four constants are not viewed as additional axioms.

它们就像归纳定义的类型及其相关的构造子和递归子（recursors）一样，被视为逻辑框架的一部分。They are, like inductively defined types and the associated constructors and recursors, viewed as part of the logical framework.

使Quot构造成为真正的商的是以下额外的公理：What makes the Quot construction into a bona fide quotient is the following additional axiom:

这个公理断言α中通过r相关联的任意两个元素在商中被等同起来。如果某个定理或定义使用了Quot.sound，它将会出现在#print axioms命令的输出中。This is the axiom that asserts that any two elements of α that are related by r become identified in the quotient. If a theorem or definition makes use of Quot.sound, it will show up in the #print axioms command.

当然，商构造最常用于r是等价关系的情况。给定如上的r，如果我们根据规则r’ a b当且仅当Quot.mk r a = Quot.mk r b来定义r’，那么显然r’是一个等价关系。实际上，r’是函数fun a => Quot.mk r a的核（kernel）。公理Quot.sound说明r a b蕴涵r’ a b。使用Quot.lift和Quot.ind，我们可以证明r’是包含r的最小等价关系，即如果r’’是任何包含r的等价关系，那么r’ a b蕴涵r’’ a b。特别地，如果r一开始就是等价关系，那么对所有a和b，r a b当且仅当r’ a b。Of course, the quotient construction is most commonly used in situations when r is an equivalence relation. Given r as above, if we define r' according to the rule r' a b iff Quot.mk r a = Quot.mk r b, then it's clear that r' is an equivalence relation. Indeed, r' is the kernel of the function fun a => Quot.mk r a. The axiom Quot.sound says that r a b implies r' a b. Using Quot.lift and Quot.ind, we can show that r' is the smallest equivalence relation containing r, in the sense that if r'' is any equivalence relation containing r, then r' a b implies r'' a b. In particular, if r was an equivalence relation to start with, then for all a and b we have r a b iff r' a b.

为了支持这种常见用例，标准库定义了集合论（setoid）的概念，它就是一个带有相关等价关系的类型：To support this common use case, the standard library defines the notion of a setoid, which is simply a type with an associated equivalence relation:

给定一个类型α、α上的一个关系r以及r是等价关系的证明iseqv，我们可以定义Setoid类的一个实例。Given a type α, a relation r on α, and a proof iseqv that r is an equivalence relation, we can define an instance of the Setoid class.

常量Quotient.mk、Quotient.ind、Quotient.lift和Quotient.sound不过是Quot对应元素的特化。类型类（type class）推理可以为类型α找到相关的 setoid，这一事实带来了许多好处。首先，我们可以使用记号a ≈ b（通过pprox输入）表示Setoid.r a b，其中Setoid实例在记号Setoid.r中是隐式的。我们可以使用泛型定理Setoid.refl、Setoid.symm、Setoid.trans来推理该关系。特别是在商中，我们可以使用定理Quotient.exact：The constants Quotient.mk, Quotient.ind, Quotient.lift, and Quotient.sound are nothing more than the specializations of the corresponding elements of Quot. The fact that type class inference can find the setoid associated to a type α brings a number of benefits. First, we can use the notation a ≈ b (entered with \approx) for Setoid.r a b, where the instance of Setoid is implicit in the notation Setoid.r. We can use the generic theorems Setoid.refl, Setoid.symm, Setoid.trans to reason about the relation. Specifically with quotients we can use the theorem Quotient.exact:

与Quotient.sound一起，这意味着商中的元素恰好对应于α中元素的等价类。Together with Quotient.sound, this implies that the elements of the quotient correspond exactly to the equivalence classes of elements in α.

回顾一下，在标准库中，α × β表示类型α和β的笛卡尔积。为了说明商的使用，让我们将类型α的无序对定义为类型α × α的商。首先，定义相关的等价关系：Recall that in the standard library, α × β represents the Cartesian product of the types α and β. To illustrate the use of quotients, let us define the type of unordered pairs of elements of a type α as a quotient of the type α × α. First, we define the relevant equivalence relation:

下一步是证明eqv实际上是一个等价关系，即它是自反的、对称的和传递的。我们可以通过使用依值模式匹配（dependent pattern matching）进行情况分析，将假设分解成若干部分，然后再重新组合以产生结论，以一种方便且可读的方式来证明这三个事实。The next step is to prove that eqv is in fact an equivalence relation, which is to say, it is reflexive, symmetric and transitive. We can prove these three facts in a convenient and readable way by using dependent pattern matching to perform case-analysis and break the hypotheses into pieces that are then reassembled to produce the conclusion.

既然我们已经证明了eqv是一个等价关系，我们可以构造一个Setoid (α × α)，并使用它来定义无序对的类型UProd α。Now that we have proved that eqv is an equivalence relation, we can construct a Setoid (α × α), and use it to define the type UProd α of unordered pairs.