Axioms and Computation

我们已经看到，已经在Lean中实现的构造演算的版本包括依赖函数类型、归纳类型和一个宇宙层次结构，这个层次结构从底部的非直谓的、与证明无关的Prop开始。在这一章中，我们考虑用额外的公理和规则来扩展CIC的方法。以这种方式扩展基础系统通常是很方便的；它可以证明更多的定理，也可以使原本的证明变得更容易。但是增加额外的公理可能会有负面的后果，这些后果可能超出了对其正确性的关注。特别是，公理的使用对定义和定理的计算内容有影响，我们将在此探讨。

Lean的设计既支持计算推理也支持经典推理。有此倾向的用户可以坚持使用“计算上纯粹”的片段，这保证了系统中的封闭表达式可以评估为典型的正常形式。例如，任何类型为Nat的封闭计算上纯粹的表达式，将还原为一个数字。

Lean的标准库定义了一个额外的公理，即命题扩展性，以及一个商结构，可导致函数扩展性。例如，这些扩展性被用来发展集合和有限集合的理论。我们将在下面看到，使用这些定理可以在Lean的内核中阻止求值，因此类型Nat的封闭项不再计算为数字。但是Lean在为其虚拟机求值器编译定义到字节码时，会抹去类型和命题信息，而且由于这些公理只是增加了新的命题，它们与这种计算解释是兼容的。即使是有计算倾向的用户也可能希望使用经典的排中律来推理计算。这也会阻止内核中的求值，但它与编译为字节码兼容。

标准库还定义了一个与计算解释完全对立的选择原则，因为它神奇地从一个断言其存在的命题中产生了“数据”。它的使用对于一些经典的构造来说是必不可少的，用户可以在需要时导入它。但是使用这种结构来产生数据的表达式并没有计算内容，在Lean中，我们需要把这种定义标记为noncomputable，以表明这一事实。

使用一个巧妙的技巧(被称为Diaconescu定理)，我们可以使用命题扩展性、函数扩展性和选择原则来推导排中律。然而，如上所述，使用排中律仍然与字节码编译和代码提取兼容，就像其他经典原则一样，只要它们不被用来制造数据。

总而言之，在宇宙、依赖函数类型和归纳类型的基础框架之上，标准库增加了三个额外的组成部分。

• 命题扩展性公理
• 一个商结构，它意味着函数的扩展性
• 选择原则，从一个存在性命题中产生数据。

其中前两个是在Lean内部的标准化，但与字节码求值兼容，而第三个则不适合于计算解释。我们将在下文中更精确地阐述这些细节。

历史和哲学背景

数学在历史中大部分时间都表现为计算性的：几何学处理几何对象的构造，代数关注方程组的算法解，而分析提供了计算随时间演变的系统的未来行为的手段。从一个定理的证明来看，“对于每一个x，都有一个y，以便......”，一般来说，开发一个算法，从给定的x来计算y是很直接的思路。

然而在19世纪，数学论证复杂性的增加促使数学家开发新的推理方式，轻视算法信息，重视对数学对象的描述，抽象出这些对象如何被表示的细节。这样做的目的是为了获得强大的“概念性”理解，而不被计算细节所困扰，但这样做的结果是承认了那些在直接的计算性解释中根本就是假的数学定理。

今天，人们仍然相当一致地认为计算对数学是重要的。但是，对于如何最好地解决计算问题，人们有不同的看法。从结构主义的观点来看，把数学从其计算的根源中分离出来是一个错误；每个有意义的数学定理都应该有一个直接的计算解释。从经典的角度来看，分别看待会更有成效：我们可以使用一种语言和方法体系来编写计算机程序，同时保持使用非结构性理论和方法来自由推理。Lean的设计是为了支持这两种方法。库的核心部分是结构性地开发的，但该系统也为进行经典的数学推理提供支持。

在计算上，依赖类型论的最纯粹部分完全避免了使用Prop。归纳类型和依赖函数类型可以被看作是数据类型，这些类型的项可以通过应用规约规则进行“求值”，直到没有规则可以应用为止。原则上，任何类型为Nat的封闭项（即没有自由变量的项）都应该算为一个数字，succ (...(succ zero）...)。

引入一个与证明无关的Prop，并将定理标记为不可还原的，代表了向分离两种倾向迈出的第一步。我们的意图是，一个元素p : Prop不应该在计算中扮演任何角色，所以项t : p的具体构造在这个意义上是“不相关的”。我们仍然可以定义包含Prop类型元素的计算对象；问题是这些元素可以帮助我们推理计算的效果，但是当我们从项中提取“代码”时，可以忽略不计。然而，Prop类型的元素并不完全是无害的。它们包括方程s = t : α，适用于任何类型的α，这样的方程可以被用作转换，对项进行类型检查。下面，我们将看到这样的转换如何阻止系统的计算的例子。然而，在一个抹去命题内容、忽略中间类型约束、减少项直到它们达到正常形式的评估方案下，计算仍然是可能的。这正是Lean的虚拟机所做的。

在采用了与证明无关的Prop之后，人们可能认为使用排中律是合法的，例如，p ∨ ¬p，其中p是任何命题。当然，根据CIC的规则，这也可以阻止计算，但它不会阻止字节码的求值，如上所述。只有在(选择)[#选择]一节中讨论的选择原则才完全消除了理论中与证明无关的部分和与数据有关的部分之间的区别。

Propositional Extensionality

Propositional extensionality is the following axiom:

# namespace Hidden
axiom propext {a b : Prop} : (a ↔ b) → a = b
# end Hidden

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 {*}, for some distinguished element *. The axiom has the effect that equivalent propositions can be substituted for one another in any context:

theorem thm₁ (a b c d e : Prop) (h : a ↔ b) : (c ∧ a ∧ d → e) ↔ (c ∧ b ∧ d → e) :=
  propext h ▸ Iff.refl _

theorem thm₂ (a b : Prop) (p : Prop → Prop) (h : a ↔ b) (h₁ : p a) : p b :=
  propext h ▸ h₁

Function Extensionality

Similar to propositional extensionality, function extensionality asserts that any two functions of type (x : α) → β x that agree on all their inputs are equal.

universe u v
#check (@funext :
           {α : Type u}
         → {β : α → Type u}
         → {f g : (x : α) → β x}
         → (∀ (x : α), f x = g x)
         → f = g)

#print funext

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.

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.

Suppose that for α : Type 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:

def Set (α : Type u) := α → Prop

namespace Set

def mem (x : α) (a : Set α) := a x

infix:50 "∈" => mem

theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
  funext (fun x => propext (h x))

end Set

We can then proceed to define the empty set and set intersection, for example, and prove set identities:

# def Set (α : Type u) := α → Prop
# namespace Set
# def mem (x : α) (a : Set α) := a x
# infix:50 "∈" => mem
# theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
#  funext (fun x => propext (h x))
def empty : Set α := fun x => False

notation (priority := high) "∅" => empty

def inter (a b : Set α) : Set α :=
  fun x => x ∈ a ∧ x ∈ b

infix:70 " ∩ " => inter

theorem inter_self (a : Set α) : a ∩ a = a :=
  setext fun x => Iff.intro
    (fun ⟨h, _⟩ => h)
    (fun h => ⟨h, h⟩)

theorem inter_empty (a : Set α) : a ∩ ∅ = ∅ :=
  setext fun x => Iff.intro
    (fun ⟨_, h⟩ => h)
    (fun h => False.elim h)

theorem empty_inter (a : Set α) : ∅ ∩ a = ∅ :=
  setext fun x => Iff.intro
    (fun ⟨h, _⟩ => h)
    (fun h => False.elim h)

theorem inter.comm (a b : Set α) : a ∩ b = b ∩ a :=
  setext fun x => Iff.intro
    (fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
    (fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
# end Set

The following is an example of how function extensionality blocks computation inside the Lean kernel.

def f (x : Nat) := x
def g (x : Nat) := 0 + x

theorem f_eq_g : f = g :=
  funext fun x => (Nat.zero_add x).symm

def val : Nat :=
  Eq.recOn (motive := fun _ _ => Nat) f_eq_g 0

-- does not reduce to 0
#reduce val

-- evaluates to 0
#eval val

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.

theorem tteq : (True ∧ True) = True :=
  propext (Iff.intro (fun ⟨h, _⟩ => h) (fun h => ⟨h, h⟩))

def val : Nat :=
  Eq.recOn (motive := fun _ _ => Nat) tteq 0

-- does not reduce to 0
#reduce val

-- evaluates to 0
#eval val

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.

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.

Quotients

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.

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:

# namespace Hidden
universe u v

axiom Quot : {α : Sort u} → (α → α → Prop) → Sort u

axiom Quot.mk : {α : Sort u} → (r : α → α → Prop) → α → Quot r

axiom Quot.ind :
    ∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop},
      (∀ a, β (Quot.mk r a)) → (q : Quot r) → β q

axiom Quot.lift :
    {α : Sort u} → {r : α → α → Prop} → {β : Sort u} → (f : α → β)
    → (∀ a b, r a b → f a = f b) → Quot r → β
# end Hidden

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.

def mod7Rel (x y : Nat) : Prop :=
  x % 7 = y % 7

-- the quotient type
#check (Quot mod7Rel : Type)

-- the class of a
#check (Quot.mk mod7Rel 4 : Quot mod7Rel)

def f (x : Nat) : Bool :=
   x % 7 = 0

theorem f_respects (a b : Nat) (h : mod7Rel a b) : f a = f b := by
  simp [mod7Rel, f] at *
  rw [h]

#check (Quot.lift f f_respects : Quot mod7Rel → Bool)

-- the computation principle
example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
  rfl

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:

They are, like inductively defined types and the associated constructors and recursors, viewed as part of the logical framework.

What makes the Quot construction into a bona fide quotient is the following additional axiom:

# namespace Hidden
# universe u v
axiom Quot.sound :
      ∀ {α : Type u} {r : α → α → Prop} {a b : α},
        r a b → Quot.mk r a = Quot.mk r b
# end Hidden

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.

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 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.

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:

# namespace Hidden
class Setoid (α : Sort u) where
  r : α → α → Prop
  iseqv {} : Equivalence r

instance {α : Sort u} [Setoid α] : HasEquiv α :=
  ⟨Setoid.r⟩

namespace Setoid

variable {α : Sort u} [Setoid α]

theorem refl (a : α) : a ≈ a :=
  (Setoid.iseqv α).refl a

theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
  (Setoid.iseqv α).symm hab

theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
  (Setoid.iseqv α).trans hab hbc

end Setoid
# end Hidden

Given a type α, a relation r on α, and a proof p that r is an equivalence relation, we can define Setoid.mk p as an instance of the setoid class.

# namespace Hidden
def Quotient {α : Sort u} (s : Setoid α) :=
  @Quot α Setoid.r
# end Hidden

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 generic notation ⟦a⟧ for Quot.mk Setoid.r where the instance of Setoid is implicit in the notation Setoid.r, as well as the theorem Quotient.exact:

# universe u
#check (@Quotient.exact :
         ∀ {α : Sort u} [s : Setoid α] {a b : α},
           Quotient.mk a = Quotient.mk b → a ≈ b)

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:

private def eqv (p₁ p₂ : α × α) : Prop :=
  (p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)

infix:50 " ~ " => eqv

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.

# private def eqv (p₁ p₂ : α × α) : Prop :=
#  (p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
# infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
  Or.inl ⟨rfl, rfl⟩

private theorem eqv.symm  : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
  | (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
    Or.inl (by simp_all)
  | (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
    Or.inr (by simp_all)

private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
  | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
    Or.inl (by simp_all)
  | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
    Or.inr (by simp_all)
  | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
    Or.inr (by simp_all)
  | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
    Or.inl (by simp_all)

private theorem is_equivalence : Equivalence (@eqv α) :=
   { refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }

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.

# private def eqv (p₁ p₂ : α × α) : Prop :=
#  (p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
# infix:50 " ~ " => eqv
# private theorem eqv.refl (p : α × α) : p ~ p :=
#  Or.inl ⟨rfl, rfl⟩
# private theorem eqv.symm  : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
#   | (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
#     Or.inl (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
#     Or.inr (by simp_all)
# private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
#     Or.inl (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
#     Or.inr (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
#     Or.inr (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
#     Or.inl (by simp_all)
# private theorem is_equivalence : Equivalence (@eqv α) :=
#   { refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
   r     := eqv
   iseqv := is_equivalence

def UProd (α : Type u) : Type u :=
  Quotient (uprodSetoid α)

namespace UProd

def mk {α : Type} (a₁ a₂ : α) : UProd α :=
  Quotient.mk (a₁, a₂)

notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂

end UProd

Notice that we locally define the notation {a₁, a₂} for ordered pairs as Quotient.mk (a₁, a₂). This is useful for illustrative purposes, but it is not a good idea in general, since the notation will shadow other uses of curly brackets, such as for records and sets.

We can easily prove that {a₁, a₂} = {a₂, a₁} using quot.sound, since we have (a₁, a₂) ~ (a₂, a₁).

# private def eqv (p₁ p₂ : α × α) : Prop :=
#  (p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
# infix:50 " ~ " => eqv
# private theorem eqv.refl (p : α × α) : p ~ p :=
#  Or.inl ⟨rfl, rfl⟩
# private theorem eqv.symm  : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
#   | (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
#     Or.inl (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
#     Or.inr (by simp_all)
# private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
#     Or.inl (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
#     Or.inr (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
#     Or.inr (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
#     Or.inl (by simp_all)
# private theorem is_equivalence : Equivalence (@eqv α) :=
#   { refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
# instance uprodSetoid (α : Type u) : Setoid (α × α) where
#    r     := eqv
#    iseqv := is_equivalence
# def UProd (α : Type u) : Type u :=
#   Quotient (uprodSetoid α)
# namespace UProd
# def mk {α : Type} (a₁ a₂ : α) : UProd α :=
#   Quotient.mk (a₁, a₂)
# notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
  Quot.sound (Or.inr ⟨rfl, rfl⟩)
# end UProd

To complete the example, given a : α and u : uprod α, we define the proposition a ∈ u which should hold if a is one of the elements of the unordered pair u. First, we define a similar proposition mem_fn a u on (ordered) pairs; then we show that mem_fn respects the equivalence relation eqv with the lemma mem_respects. This is an idiom that is used extensively in the Lean standard library.

# private def eqv (p₁ p₂ : α × α) : Prop :=
#  (p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
# infix:50 " ~ " => eqv
# private theorem eqv.refl (p : α × α) : p ~ p :=
#  Or.inl ⟨rfl, rfl⟩
# private theorem eqv.symm  : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
#   | (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
#     Or.inl (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
#     Or.inr (by simp_all)
# private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
#     Or.inl (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
#     Or.inr (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
#     Or.inr (by simp_all)
#   | (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
#     Or.inl (by simp_all)
# private theorem is_equivalence : Equivalence (@eqv α) :=
#   { refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
# instance uprodSetoid (α : Type u) : Setoid (α × α) where
#    r     := eqv
#    iseqv := is_equivalence
# def UProd (α : Type u) : Type u :=
#   Quotient (uprodSetoid α)
# namespace UProd
# def mk {α : Type} (a₁ a₂ : α) : UProd α :=
#   Quotient.mk (a₁, a₂)
# notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
# theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
#   Quot.sound (Or.inr ⟨rfl, rfl⟩)

private def mem_fn (a : α) : α × α → Prop
  | (a₁, a₂) => a = a₁ ∨ a = a₂

-- auxiliary lemma for proving mem_respects
private theorem mem_swap {a : α} :
      ∀ {p : α × α}, mem_fn a p = mem_fn a (⟨p.2, p.1⟩)
  | (a₁, a₂) => by
    apply propext
    apply Iff.intro
    . intro
      | Or.inl h => exact Or.inr h
      | Or.inr h => exact Or.inl h
    . intro
      | Or.inl h => exact Or.inr h
      | Or.inr h => exact Or.inl h


private theorem mem_respects
      : {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
  | (a₁, a₂), (b₁, b₂), a, Or.inl ⟨a₁b₁, a₂b₂⟩ => by simp_all
  | (a₁, a₂), (b₁, b₂), a, Or.inr ⟨a₁b₂, a₂b₁⟩ => by simp_all; apply mem_swap

def mem (a : α) (u : UProd α) : Prop :=
  Quot.liftOn u (fun p => mem_fn a p) (fun p₁ p₂ e => mem_respects a e)

infix:50 " ∈ " => mem

theorem mem_mk_left (a b : α) : a ∈ {a, b} :=
  Or.inl rfl

theorem mem_mk_right (a b : α) : b ∈ {a, b} :=
  Or.inr rfl

theorem mem_or_mem_of_mem_mk {a b c : α} : c ∈ {a, b} → c = a ∨ c = b :=
  fun h => h
# end UProd

For convenience, the standard library also defines Quotient.lift₂ for lifting binary functions, and Quotient.ind₂ for induction on two variables.

We close this section with some hints as to why the quotient construction implies function extenionality. It is not hard to show that extensional equality on the (x : α) → β x is an equivalence relation, and so we can consider the type extfun α β of functions "up to equivalence." Of course, application respects that equivalence in the sense that if f₁ is equivalent to f₂, then f₁ a is equal to f₂ a. Thus application gives rise to a function extfun_app : extfun α β → (x : α) → β x. But for every f, extfun_app ⟦f⟧ is definitionally equal to fun x => f x, which is in turn definitionally equal to f. So, when f₁ and f₂ are extensionally equal, we have the following chain of equalities:

    f₁ = extfun_app ⟦f₁⟧ = extfun_app ⟦f₂⟧ = f₂

As a result, f₁ is equal to f₂.

选择

To state the final axiom defined in the standard library, we need the Nonempty type, which is defined as follows:

# namespace Hidden
class inductive Nonempty (α : Sort u) : Prop where
  | intro (val : α) : Nonempty α
# end Hidden

Because Nonempty α has type Prop and its constructor contains data, it can only eliminate to Prop. In fact, Nonempty α is equivalent to ∃ x : α, True:

example (α : Type u) : Nonempty α ↔ ∃ x : α, True :=
  Iff.intro (fun ⟨a⟩ => ⟨a, trivial⟩) (fun ⟨a, h⟩ => ⟨a⟩)

Our axiom of choice is now expressed simply as follows:

# namespace Hidden
# universe u
axiom choice {α : Sort u} : Nonempty α → α
# end Hidden

Given only the assertion h that α is nonempty, choice h magically produces an element of α. Of course, this blocks any meaningful computation: by the interpretation of Prop, h contains no information at all as to how to find such an element.

This is found in the Classical namespace, so the full name of the theorem is Classical.choice. The choice principle is equivalent to the principle of indefinite description, which can be expressed with subtypes as follows:

# namespace Hidden
# universe u
# axiom choice {α : Sort u} : Nonempty α → α
noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
                                        (h : ∃ x, p x) : {x // p x} :=
  choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
# end Hidden

Because it depends on choice, Lean cannot generate bytecode for indefiniteDescription, and so requires us to mark the definition as noncomputable. Also in the Classical namespace, the function choose and the property choose_spec decompose the two parts of the output of indefinite_description:

# open Classical
# namespace Hidden
noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
  (indefiniteDescription p h).val

theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
  (indefiniteDescription p h).property
# end Hidden

The choice principle also erases the distinction between the property of being Nonempty and the more constructive property of being Inhabited:

# open Classical
theorem inhabited_of_nonempty :Nonempty α → Inhabited α :=
  fun h => choice (let ⟨a⟩ := h; ⟨⟨a⟩⟩)

In the next section, we will see that propext, funext, and choice, taken together, imply the law of the excluded middle and the decidability of all propositions. Using those, one can strengthen the principle of indefinite description as follows:

# open Classical
# universe u
#check (@strongIndefiniteDescription :
         {α : Sort u} → (p : α → Prop)
         → Nonempty α → {x // (∃ (y : α), p y) → p x})

Assuming the ambient type α is nonempty, strongIndefiniteDescription p produces an element of α satisfying p if there is one. The data component of this definition is conventionally known as Hilbert's epsilon function:

# open Classical
# universe u
#check (@epsilon :
         {α : Sort u} → [Nonempty α]
         → (α → Prop) → α)

#check (@epsilon_spec :
          ∀ {a : Sort u} {p : a → Prop}(hex : ∃ (y : a), p y),
            p (@epsilon _ (nonempty_of_exists hex) p))

The Law of the Excluded Middle

The law of the excluded middle is the following

open Classical

#check (@em : ∀ (p : Prop), p ∨ ¬p)

Diaconescu's theorem states that the axiom of choice is sufficient to derive the law of excluded middle. More precisely, it shows that the law of the excluded middle follows from Classical.choice, propext, and funext. We sketch the proof that is found in the standard library.

First, we import the necessary axioms, and define two predicates U and V:

# namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
  let U (x : Prop) : Prop := x = True ∨ p
  let V (x : Prop) : Prop := x = False ∨ p

  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
#   sorry
# end Hidden

If p is true, then every element of Prop is in both U and V. If p is false, then U is the singleton true, and V is the singleton false.

Next, we use some to choose an element from each of U and V:

# namespace Hidden
# open Classical
# theorem em (p : Prop) : p ∨ ¬p :=
#   let U (x : Prop) : Prop := x = True ∨ p
#   let V (x : Prop) : Prop := x = False ∨ p
#   have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
#   have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
  let u : Prop := choose exU
  let v : Prop := choose exV

  have u_def : U u := choose_spec exU
  have v_def : V v := choose_spec exV
#   sorry
# end Hidden

Each of U and V is a disjunction, so u_def and v_def represent four cases. In one of these cases, u = True and v = False, and in all the other cases, p is true. Thus we have:

# namespace Hidden
# open Classical
# theorem em (p : Prop) : p ∨ ¬p :=
#   let U (x : Prop) : Prop := x = True ∨ p
#   let V (x : Prop) : Prop := x = False ∨ p
#   have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
#   have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
#   let u : Prop := choose exU
#   let v : Prop := choose exV
#   have u_def : U u := choose_spec exU
#   have v_def : V v := choose_spec exV
  have not_uv_or_p : u ≠ v ∨ p :=
    match u_def, v_def with
    | Or.inr h, _ => Or.inr h
    | _, Or.inr h => Or.inr h
    | Or.inl hut, Or.inl hvf =>
      have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
      Or.inl hne
#   sorry
# end Hidden

On the other hand, if p is true, then, by function extensionality and propositional extensionality, U and V are equal. By the definition of u and v, this implies that they are equal as well.

# namespace Hidden
# open Classical
# theorem em (p : Prop) : p ∨ ¬p :=
#   let U (x : Prop) : Prop := x = True ∨ p
#   let V (x : Prop) : Prop := x = False ∨ p
#   have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
#   have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
#   let u : Prop := choose exU
#   let v : Prop := choose exV
#   have u_def : U u := choose_spec exU
#   have v_def : V v := choose_spec exV
#   have not_uv_or_p : u ≠ v ∨ p :=
#     match u_def, v_def with
#     | Or.inr h, _ => Or.inr h
#     | _, Or.inr h => Or.inr h
#     | Or.inl hut, Or.inl hvf =>
#       have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
#       Or.inl hne
  have p_implies_uv : p → u = v :=
    fun hp =>
    have hpred : U = V :=
      funext fun x =>
        have hl : (x = True ∨ p) → (x = False ∨ p) :=
          fun _ => Or.inr hp
        have hr : (x = False ∨ p) → (x = True ∨ p) :=
          fun _ => Or.inr hp
        show (x = True ∨ p) = (x = False ∨ p) from
          propext (Iff.intro hl hr)
    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
      rw [hpred]; intros; rfl
    show u = v from h₀ _ _
#   sorry
# end Hidden

Putting these last two facts together yields the desired conclusion:

# namespace Hidden
# open Classical
# theorem em (p : Prop) : p ∨ ¬p :=
#   let U (x : Prop) : Prop := x = True ∨ p
#   let V (x : Prop) : Prop := x = False ∨ p
#   have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
#   have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
#   let u : Prop := choose exU
#   let v : Prop := choose exV
#   have u_def : U u := choose_spec exU
#   have v_def : V v := choose_spec exV
#   have not_uv_or_p : u ≠ v ∨ p :=
#     match u_def, v_def with
#     | Or.inr h, _ => Or.inr h
#     | _, Or.inr h => Or.inr h
#     | Or.inl hut, Or.inl hvf =>
#       have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
#       Or.inl hne
#  have p_implies_uv : p → u = v :=
#     fun hp =>
#     have hpred : U = V :=
#       funext fun x =>
#         have hl : (x = True ∨ p) → (x = False ∨ p) :=
#           fun _ => Or.inr hp
#         have hr : (x = False ∨ p) → (x = True ∨ p) :=
#           fun _ => Or.inr hp
#         show (x = True ∨ p) = (x = False ∨ p) from
#           propext (Iff.intro hl hr)
#     have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
#       rw [hpred]; intros; rfl
#     show u = v from h₀ _ _
  match not_uv_or_p with
  | Or.inl hne => Or.inr (mt p_implies_uv hne)
  | Or.inr h   => Or.inl h
# end Hidden

Consequences of excluded middle include double-negation elimination, proof by cases, and proof by contradiction, all of which are described in the Section Classical Logic. The law of the excluded middle and propositional extensionality imply propositional completeness:

# namespace Hidden
open Classical
theorem propComplete (a : Prop) : a = True ∨ a = False :=
  match em a with
  | Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
  | Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
# end Hidden

Together with choice, we also get the stronger principle that every proposition is decidable. Recall that the class of Decidable propositions is defined as follows:

# namespace Hidden
class inductive Decidable (p : Prop) where
  | isFalse (h : ¬p) : Decidable p
  | isTrue  (h : p)  : Decidable p
# end Hidden

In contrast to p ∨ ¬ p, which can only eliminate to Prop, the type decidable p is equivalent to the sum type Sum p (¬ p), which can eliminate to any type. It is this data that is needed to write an if-then-else expression.

As an example of classical reasoning, we use choose to show that if f : α → β is injective and α is inhabited, then f has a left inverse. To define the left inverse linv, we use a dependent if-then-else expression. Recall that if h : c then t else e is notation for dite c (fun h : c => t) (fun h : ¬ c => e). In the definition of linv, choice is used twice: first, to show that (∃ a : A, f a = b) is "decidable," and then to choose an a such that f a = b. Notice that propDecidable is a scoped instance and is activated by the open Classical command. We use this instance to justify the if-then-else expression. (See also the discussion in Section Decidable Propositions).

open Classical

noncomputable def linv [Inhabited α] (f : α → β) : β → α :=
  fun b : β => if ex : (∃ a : α, f a = b) then choose ex else arbitrary

theorem linv_comp_self {f : α → β} [Inhabited α]
                       (inj : ∀ {a b}, f a = f b → a = b)
                       : linv f ∘ f = id :=
  funext fun a =>
    have ex  : ∃ a₁ : α, f a₁ = f a := ⟨a, rfl⟩
    have feq : f (choose ex) = f a  := choose_spec ex
    calc linv f (f a) = choose ex := dif_pos ex
               _      = a         := inj feq

From a classical point of view, linv is a function. From a constructive point of view, it is unacceptable; because there is no way to implement such a function in general, the construction is not informative.