12. 公理与计算
我们已经看到 Lean 中实现的构造演算的版本包括有：依值函数类型、
归纳类型以及一个满足 非直谓性 和 证明无关性 的 Prop 为底层的宇宙层级。
在本章中，我们要探讨使用附加公理和规则扩展 CIC 的方法。
用这种方式扩展一个基础系统通常很方便；它可以使得证明更多的定理成为可能，
并使得证明原本可以被证明的定理变得更容易。但是，添加附加公理可能会产生负面后果，
这些后果可能超出了人们对它们的正确性的担忧。
特别是，公理的使用会以我们将在本文中探究的方式，对定义和定理的计算内容产生影响。
Lean 被设计为支持计算推理和经典推理。有此需求的用户可坚持使用“计算上纯粹”的片段，
它可以确保系统中的封闭表达式会求值为标准范式。具体说来，任何类型为 Nat
的封闭计算上纯粹表达式最终都将归约为一个数值。
Lean 的标准库定义了一个公理：命题外延性（Propositional Extensionality）。
以及一个商（Quotient）结构，它蕴含了函数外延性的公理。
这些扩展被用来发展如集合与有限集这些理论。我们在后面会看到，
这些定理的使用会阻碍 Lean 内核中的求值，因此 Nat 类型的封闭项不再求值为数值。
但是 Lean 在将定义编译为可执行代码时会擦除类型和命题信息，
并且由于这些公理只增加了新的命题，它们与这种计算解释是相容的。
即使是倾向于可计算性的用户也可能希望使用排中律来推理计算。
这也会阻碍内核中的求值，但它与编译后的代码是兼容的。
标准函数库还定义了一个选择公理（Choice Principle），该公理与计算诠释完全相反，
因为它神奇地根据断言自身存在的命题产生“数据”。
它对于一些经典结构来说是必不可少的，用户可以在需要时导入它。
但使用此构造来产生数据的表达式将不存在计算内容，
在 Lean 中我们需要将此类定义标记为 noncomputable（不可计算的）以表明该事实。
使用一个巧妙的技巧（称为狄阿科涅斯库定理），人们可以使用命题外延性、 函数外延性和选择公理来导出排中律。然而，如上所述，使用排中律仍然兼容编译， 就像其他经典公理一样，只要它们不被用来制造数据。
总而言之，在我们的宇宙类型，依值函数类型和归纳类型的底层框架之上， 标准库增加了三个附加元素：
-
命题外延性公理
-
蕴含了函数外延性的的商构造
-
选择公理，它从存在命题中产生数据。
前两项在 Lean 中对这些块标准化，但与代码生成兼容， 而第三项不适合可计算性解释。我们将在下面更精确地说明这些细节。
12.1. 历史与哲学背景
历史上大部分时候，数学主要是计算性的：几何处理涉及几何对象的构造，
代数涉及方程组的算法解，分析提供了计算系统随时间演变的未来行为的方法。
从定理的证明到“对于每个 x，都有一个 y 使得 ...”这一效果，
通常可以提取一种算法来根据给定的 x 计算这样的的 y。
然而在 19 世纪，数学论证复杂性的提升推动了数学家发展新的推理风格， 抑制算法信息并调用数学对象，从而抽象掉了对象被表征的细节。 目标是在不陷入繁重的计算细节的情况下获得强大的“概念”理解， 但这可能导致数学定理在直接计算的解读上干脆就是 错误 的。
今天数学界仍在相当普遍地同意计算对于数学很重要。 但对于如何以最佳方式解决计算问题有不同的看法。 从 构造性 的角度来看，将数学与其计算根源分开是一个错误； 每条有意义的数学定理都应具有直接的计算解释。 从 经典的 角度来看，保持关注点的分离更有成效： 我们可以使用一种语言和方法体系编写计算机程序， 同时保持使用非构造性理论和方法对其进行推理的自由。 Lean 旨在支持这两种方法。库的核心部分以构造性方式开发， 但该系统还提供了支持进行经典数学推理的支持。
从计算的角度来看，依值类型论中最纯粹的部分完全避免使用 Prop。
归纳类型和依值函数类型可以看作是数据类型，这些类型的项可以通过应用归约规则进行“求值”，
直到不能再应用任何规则为止。原则上，类型为 Nat 的任何封闭项（即没有自由变量的项）
都应求值为一个数值：succ (… (succ zero)…)。
引入一个与证明无关的 Prop 并标记定理不可约表示了分离关注点的第一步。
目的是类型为 p : Prop 的元素在计算中不应发挥任何作用，因此从这个意义上说，
项 prf : p 的特定构造是“无关的”。人们仍然可以定义包含类型为 Prop
的元素的计算对象；关键是这些元素可以帮助我们推理计算的影响，
但在我们从项中提取“代码”时可以忽略。但是，Prop 类型的元素并非完全无害。
它们包括任何类型 α 的方程 s = t : α，并且此类方程可以作为强制转换使用，
以对项进行类型检查。在后面，我们将看到此类强制转换是如何阻碍系统中的计算的示例。
但是，在擦除命题内容、忽略中间定型约束并归约项，直到它们达到正规形式的求值方案下，
它们仍然可以进行计算。这正是 Lean 的虚拟机所做的。
在通过了证明无关的 Prop 之后，可以认为使用排中律 p ∨ ¬p 是合法的，
其中 p 是任何命题。当然，这也可能根据 CIC 的规则阻止计算，
但它不会阻止可执行代码的生成，如上所述。仅在关于选择的章节
中讨论过的选择原则才能完全消除理论中与证明无关的部分和与数据相关部分之间的区别。
12.2. 命题外延性
命题外延性公理如下：
axiom propext {a b : Prop} : (a ↔ b) → a = b
它断言当两个命题互相蕴含时，二者实质相等。这与集合论的解释一致，
即对于某个特定的元素 \ast，其中任何元素 a : Prop 要么为空集，
要么是单元素集 \{\ast\}。此公理具有这样的效果，即等价的命题可以在任何语境中彼此替换：
12.3. 函数外延性
Similar to propositional extensionality, function extensionality
asserts that any two functions of type (x : α) → β x that agree on
all their inputs are equal:
funext.{u, v}
{α : Sort u} {β : α → Sort v}
{f g : (x : α) → β x}
(h : ∀ (x : α), f x = g x) :
f = g
与命题外延性类似，函数外延性断言任何两个类型为 (x : α) → β x
的函数，如果它们在所有输入上都一致，那么它们就是相等的：
从经典的集合论角度来看，这正是两个函数相等的确切含义。 它被称作函数的“外延性（Extensional）”视角。然而，从构造主义的角度来看， 有时把函数看作算法，或者以某种明确的方式给出的计算机程序要更加自然。 肯定存在这样的情况：两个计算机程序对每个输入都计算出相同的答案， 尽管它们在语法上非常不同。与此类似，你可能想要维护一种函数的视角， 它不会强迫你将具有相同输入/输出行为的两个函数认定为同样的。 这被称为函数的“内涵（Intensional）”视角。
实际上，函数外延性来自于商的存在，我们将在下一节中进行描述。
因此，在 Lean 标准库中，funext 通过商的构造来证明。
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:
def Set (α : Type u) := α → Prop
namespace Set
def mem (x : α) (a : Set α) := a x
infix:50 (priority := high) "∈" => mem
theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x => propext (h x))
end Set
假设对于 α : Type u，我们定义 Set α:= α → Prop 来表达 α 子集的类型，
本质上是用谓词来表示子集。通过组合 funext 和 propext，
我们得到了一个这样的集合的外延性理论：
然后我们可以继续定义空集和集合交集，例如，并证明集合恒等式：
def Set (α : Type u) := α → Prop
namespace Set
def mem (x : α) (a : Set α) := a x
infix:50 (priority := high) "∈" => mem
theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x => propext (h x))
def empty : Set α := fun _ => 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 _ => Iff.intro
(fun ⟨_, h⟩ => h)
(fun h => False.elim h)
theorem empty_inter (a : Set α) : ∅ ∩ a = ∅ :=
setext fun _ => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => False.elim h)
theorem inter.comm (a b : Set α) : a ∩ b = b ∩ a :=
setext fun _ => Iff.intro
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
end Set
以下是函数外延性如何阻碍 Lean 内核中计算的示例：
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
首先，我们使用函数外延性证明两个函数 f 和 g 相等，
然后我们通过在类型中将 f 替换为 g 来转换类型为 Nat 的 0。
当然，这种转换是空洞的，因为 Nat 不依赖于 f。但这足以造成破坏：
在系统的计算规则下，我们现在有一个 Nat 的封闭项，它不会归约为一个数值。
在这种情况下，我们可能会试图将表达式归约为 0。但在非平凡的例子中，
消除转换会改变项的类型，这可能会使周围的表达式类型不正确。
然而，虚拟机在将表达式求值为 0 方面没有任何问题。
这是一个类似的人为示例，展示了 propext 如何造成阻碍：
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当前的研究项目，包括观察类型论（Observational Type Theory）和立方类型论（Cubical Type Theory）的工作， 旨在以允许涉及函数外延性、商等的转换进行归约的方式扩展类型论。 但解决方案并不那么明确，Lean 的底层演算规则也不支持这种归约。
然而，从某种意义上说，转换并不会改变表达式的含义。相反，它是一种推理表达式类型的机制。
给定适当的语义，以保留其含义的方式归约项是有意义的，忽略使归约类型正确所需的中间簿记。
在这种情况下，在 Prop 中添加新公理并不重要；通过证明无关性，
Prop 中的表达式不携带任何信息，并且可以被归约过程安全地忽略。
12.4. 商
设 α 为任意类型，且 r 为 α 上的等价关系。在数学中，
常见的做法是形成 商（Quotient） α / r，即 α 中元素的类型 模（modulo） r。
从集合论的角度，可以将 α / r 视为 α 模 r 的等价类的集合。
若 f : α → β 是任意满足等价关系的函数，即对于任意 x y : α，r x y
蕴含 f x = f y，则 f 提升（lift） 到函数 f' : α / r → β，
其在每个等价类 ⟦x⟧ 上由 f' ⟦x⟧ = f x 定义。
Lean 的标准库通过执行这些构造的附加常量来扩展构造演算，并将该最后的方程作为定义归约规则。
在最基本的表述形式中，商构造甚至不需要 r 成为一个等价关系。
下列常量被内置在 Lean 中：
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 → β
第一条公理根据任何二元关系 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 表明此函数是良定义的。事实上，计算公理被声明为一个归约规则，
如下方的证明所示。
def mod7Rel (x y : Nat) : Prop :=
x % 7 = y % 7
-- the quotient type
#check (Quot mod7Rel : Type)
-- the class of numbers equivalent to 4
#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 := a:Natb:Nath:mod7Rel a b⊢ f a = f b
a:Natb:Nath:a % 7 = b % 7⊢ a % 7 = 0 ↔ b % 7 = 0
All goals completed! 🐙
#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
四个常量 Quot、Quot.mk、Quot.ind 和 Quot.lift 在它们本身上并不强。
你可以检查如果我们把 Quot r 简单地取为 α，并取 Quot.lift 为恒等函数
（忽略 h），那么 Quot.ind 将得到满足。
由于这个原因，这四个常量并没有被看作附加公理。
这条公理断言 α 的任何两个元素，只要满足关系 r，就能在商中被识别。
如果定理或定义使用了 Quot.sound，它将会在 #print axioms 命令中显示。
当然，当 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。
为支持这种通用使用案例，标准库定义了 广集（Setoid） 的概念， 它只是一个带有与之关联的等价关系的类型：
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 :=
iseqv.refl a
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
iseqv.symm hab
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
iseqv.trans hab hbc
end Setoid
给定一个类型 α，其上的关系 r，
以及一个证明 iseqv 证明 r 是一个等价关系，
我们可以定义 Setoid 类的一个实例。
常量 Quotient.mk、Quotient.ind、Quotient.lift
以及 Quotient.sound 仅为 Quot 对应元素的特化形式。
类型类推断能找到与类型 α 关联的广集，这带来了大量好处。
首先，我们可以对 Setoid.r a b 使用符号 a ≈ b（用 \approx 输入），
其中 Setoid 的实例在符号 Setoid.r 中是内隐的。
我们可以使用通用定理 Setoid.refl、Setoid.symm、Setoid.trans
来推断关系。具体来说，在商中，我们可以使用定理 Quotient.exact：
Quotient.exact {α : Sort u} {s : Setoid α} {a b : α} :
Quotient.mk s a = Quotient.mk s b →
a ≈ b
结合 Quotient.sound，这意味着商的各个元素精确对应于 α 中各元素的等价类。
回顾一下标准库中的 α × β 代表类型 α 和 β 的笛卡尔积。
为了说明商的用法，让我们将类型为 α 的元素构成的 无序对（Unordered Pair） 的类型定义为
α × α 类型的商。首先，我们定义相关的等价关系：
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
下一步是证明 eqv 实际上是一个等价关系，即满足自反性、对称性和传递性。
我们可以使用依值模式匹配进行情况分析，将假设分解然后重新组合以得出结论，
从而以一种简便易读的方式证明这三个事实。
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
现在我们已经证明了 eqv 是一个等价关系，我们可以构造一个 Setoid (α × α)，
并使用它来定义无序对的类型 UProd α。
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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
注意，我们局部地将无序对的符号 {a₁, a₂} 定义为 Quotient.mk' (a₁, a₂)。
这对于演示目的很有用，但通常不是一个好主意，因为该符号会遮蔽花括号的其他用途，
例如用于记录和集合。
我们可以使用 Quot.sound 轻松证明 {a₁, a₂} = {a₂, a₁}，
因为我们有 (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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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
为了完成这个例子，给定 a : α 和 u : UProd α，
我们定义命题 a ∈ u，如果 a 是无序对 u
的元素之一，则该命题成立。首先，我们在（有序）对上定义一个类似的命题
mem_fnau；然后我们用引理 mem_respects
证明 mem_fn 遵循等价关系 eqv。
这是 Lean 标准库中广泛使用的一种惯用语。
set_option linter.unusedVariables false
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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⟩)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) = mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) = mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) ↔ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) → mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) → mem_fn a (a₁, a₂)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) → mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) intro
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a (a₁, a₂)h:a = a₁⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a (a₁, a₂)h:a = a₂⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) → mem_fn a (a₁, a₂) intro
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)h:a = (a₁, a₂).snd⊢ mem_fn a (a₁, a₂) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)h:a = (a₁, a₂).fst⊢ mem_fn a (a₁, a₂) All goals completed! 🐙
private theorem mem_respects : {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂) α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂)
All goals completed! 🐙
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂) α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂)
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:a₁ = b₂a₂b₁:a₂ = b₁⊢ mem_fn a (b₂, b₁) = mem_fn a (b₁, b₂)
All goals completed! 🐙
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 (priority := high) " ∈ " => 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
为了方便起见，标准库还定义了用于提升二元函数的 Quotient.lift₂，
以及用于两个变量归纳的 Quotient.ind₂。
我们在本节的最后给出一些提示，说明为什么商构造蕴含函数外延性。
不难证明 (x : α) → β x 上的外延相等是一个等价关系，
因此我们可以考虑“在等价意义下”的函数类型 extfun α β。
当然，应用（Application）遵循该等价关系，即如果 f₁ 等价于 f₂，
则 f₁ a 等于 f₂ a。因此，应用产生了一个函数
extfun_app : extfun α β → (x : α) → β x。但是对于每个 f，
extfun_app (.mk _ f) 在定义上等于 fun x => f x，
而后者在定义上又等于 f。因此，当 f₁ 和 f₂ 外延相等时，
我们有以下等式链：
variable {α : Sort u} {β : α → Sort v}
def extfun (α : Sort u) (β : α → Sort v) := Quot (fun (f g : (x : α) → β x) => ∀ x, f x = g x)
def extfun_app {α β} (f : extfun α β) (x : α) : β x :=
Quot.lift (· x) (α✝:Sort uβ✝:α✝ → Sort vα:Sort ?u.75β:α → Sort ?u.74f:extfun α βx:α⊢ ∀ (a b : (x : α) → β x), (∀ (x : α), a x = b x) → (fun x_1 => x_1 x) a = (fun x_1 => x_1 x) b α✝:Sort uβ✝:α✝ → Sort vα:Sort ?u.75β:α → Sort ?u.74f:extfun α βx:αa✝¹:(x : α) → β xb✝:(x : α) → β xa✝:∀ (x : α), a✝¹ x = b✝ x⊢ (fun x_1 => x_1 x) a✝¹ = (fun x_1 => x_1 x) b✝; All goals completed! 🐙) f
example (f₁ f₂ : (x : α) → β x) (h : ∀ x, f₁ x = f₂ x) :=
calc f₁
_ = extfun_app (.mk _ f₁) := rfl
_ = extfun_app (.mk _ f₂) := α:Sort uβ:α → Sort vf₁:(x : α) → β xf₂:(x : α) → β xh:∀ (x : α), f₁ x = f₂ x⊢ extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₁) = extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₂) α:Sort uβ:α → Sort vf₁:(x : α) → β xf₂:(x : α) → β xh:∀ (x : α), f₁ x = f₂ x⊢ ∀ (x : α), f₁ x = f₂ x; All goals completed! 🐙
_ = f₂ := rfl
结果是，f₁ 等于 f₂。
12.5. 选择公理
为了陈述标准库中定义的最后一个公理，我们需要 Nonempty 类型，它的定义如下：
class inductive Nonempty (α : Sort u) : Prop where
| intro (val : α) : Nonempty α
由于 Nonempty α 的类型为 Prop，其构造子包含数据，所以只能消去到 Prop。
事实上，Nonempty α 等价于 ∃ x : α, True：
example (α : Type u) : Nonempty α ↔ ∃ x : α, True :=
Iff.intro (fun ⟨a⟩ => ⟨a, trivial⟩) (fun ⟨a, h⟩ => ⟨a⟩)
我们的选择公理现在可以简单地表示如下：
给定唯一断言 h，即 α 非空，choice h 神奇地产生了一个 α 的元素。
当然，这阻碍了任何有意义的计算：根据 Prop 的解释，h 根本不包含任何信息，
因而无法找到这样的元素。
这可以在 Classical 命名空间中找到，所以定理的全名是 Classical.choice。
选择公理等价于非限定摹状词（Indefinite Description）原理，可通过子类型表示如下：
noncomputable def indefiniteDescription {α : Sort u}
(p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
因为依赖于 choice，Lean 不能为 indefiniteDescription 生成可执行代码，
所以要求我们将定义标记为 noncomputable。同样在 Classical 命名空间中，
函数 choose 和属性 choose_spec 分离了 indefiniteDescription 输出的两个部分：
variable {α : Sort u} {p : α → Prop}
noncomputable def choose (h : ∃ x, p x) : α :=
(indefiniteDescription p h).val
theorem choose_spec (h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property
choice 选择公理也消除了 Nonempty 特性与更加具有构造性的
Inhabited 特性之间的区别。
open Classical
noncomputable def inhabited_of_nonempty (h : Nonempty α) : Inhabited α :=
choice (let ⟨a⟩ := h; ⟨⟨a⟩⟩)
在下一节中，我们将会看到 propext、funext 和 choice，
合起来就构成了排中律以及所有命题的可判定性。使用它们，我们可以加强如下非限定摹状词原理：
strongIndefiniteDescription {α : Sort u} (p : α → Prop)
(h : Nonempty α) :
{x // (∃ (y : α), p y) → p x}
假设环境类型 α 非空，strongIndefiniteDescription p 产生一个满足 p
的元素 α（如果存在的话）。该定义的数据部分通常被称为 希尔伯特 ε 函数：
epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
epsilon_spec {α : Sort u} {p : α → Prop}
(hex : ∃ (y : α), p y) :
p (@epsilon _ (nonempty_of_exists hex) p)
12.6. 排中律
排中律如下所示：
Classical.em : ∀ (p : Prop), p ∨ ¬p
迪亚科内斯库定理 表明
选择公理足以导出排中律。更确切地说，它表明排中律源自于 Classical.choice，
propext 和 funext。我们概述了标准库中的证明。
首先，我们导入必要的公理，并定义两个谓词 U 和 V：
open Classical
theorem em (p : Prop) : p ∨ ¬p := p:Prop⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ p⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ p⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)⊢ p ∨ ¬p
当 p 为真时，Prop 的所有元素既在 U 中又在 V 中。
当 p 为假时，U 是单元素的 True，V 是单元素的 False。
接下来，我们使用 choose 从 U 和 V 中各选取一个元素：
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exU⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exV⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exU⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exV⊢ p ∨ ¬p
U 和 V 都是析取，所以 u_def 和 v_def 表示四种情况。
在其中一种情况下，u = True 且 v = False，在所有其他情况下，
p 为真。因此我们有：
have not_uv_or_p : u ≠ v ∨ p := p:Prop⊢ p ∨ ¬p
match u_def, v_def with
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVh:px✝:V v⊢ u ≠ v ∨ p All goals completed! 🐙
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVx✝:U uh:p⊢ u ≠ v ∨ p All goals completed! 🐙
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVhut:u = Truehvf:v = False⊢ u ≠ v ∨ p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVhut:u = Truehvf:v = False⊢ u ≠ v
All goals completed! 🐙
另一方面，若 p 为真，则由函数的外延性和命题的外延性，可得 U 和 V 相等。
根据 u 和 v 的定义，这蕴含了它们也相等。
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 := p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, x => Or.inr h
| x, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
Or.inl
(of_eq_true
(Eq.trans (congr (congrArg Ne hut) hvf)
(Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false)))
not_false_eq_true)))hp:phpred:U = V :=
funext fun x =>
have hl := fun x_1 => Or.inr hp;
have hr := fun x_1 => Or.inr hp;
have this := propext { mp := hl, mpr := hr };
this⊢ ∀ (exU : ∃ x, U x) (exV : ∃ x, V x), choose exU = choose exV
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, x => Or.inr h
| x, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
Or.inl
(of_eq_true
(Eq.trans (congr (congrArg Ne hut) hvf)
(Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false)))
not_false_eq_true)))hp:phpred:U = V :=
funext fun x =>
have hl := fun x_1 => Or.inr hp;
have hr := fun x_1 => Or.inr hp;
have this := propext { mp := hl, mpr := hr };
this⊢ ∀ (exU exV : ∃ x, V x), choose exU = choose exV; p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, x => Or.inr h
| x, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
Or.inl
(of_eq_true
(Eq.trans (congr (congrArg Ne hut) hvf)
(Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false)))
not_false_eq_true)))hp:phpred:U = V :=
funext fun x =>
have hl := fun x_1 => Or.inr hp;
have hr := fun x_1 => Or.inr hp;
have this := propext { mp := hl, mpr := hr };
thisexU✝:∃ x, V xexV✝:∃ x, V x⊢ choose exU✝ = choose exV✝; All goals completed! 🐙
show u = v from h₀ _ _
将最后两个事实放在一起可以得出期望的结论：
match not_uv_or_p with
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, x => Or.inr h
| x, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
Or.inl
(of_eq_true
(Eq.trans (congr (congrArg Ne hut) hvf)
(Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false)))
not_false_eq_true)))p_implies_uv:p → u = v :=
fun hp =>
have hpred :=
funext fun x =>
have hl := fun x_1 => Or.inr hp;
have hr := fun x_1 => Or.inr hp;
have this := propext { mp := hl, mpr := hr };
this;
have h₀ :=
Eq.mpr (id (congrArg (fun _a => ∀ (exU : ∃ x, _a x) (exV : ∃ x, V x), choose exU = choose exV) hpred))
fun exU exV => Eq.refl (choose exU);
have this := h₀ exU exV;
thishne:u ≠ v⊢ p ∨ ¬p
All goals completed! 🐙
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x := Exists.intro True (Or.inl rfl)exV:∃ x, V x := Exists.intro False (Or.inl rfl)u:Prop := choose exUv:Prop := choose exVu_def:U u := choose_spec exUv_def:V v := choose_spec exVnot_uv_or_p:u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, x => Or.inr h
| x, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
Or.inl
(of_eq_true
(Eq.trans (congr (congrArg Ne hut) hvf)
(Eq.trans (congrArg Not (Eq.trans eq_iff_iff._simp_1 (Eq.trans (iff_false True) not_true_eq_false)))
not_false_eq_true)))p_implies_uv:p → u = v :=
fun hp =>
have hpred :=
funext fun x =>
have hl := fun x_1 => Or.inr hp;
have hr := fun x_1 => Or.inr hp;
have this := propext { mp := hl, mpr := hr };
this;
have h₀ :=
Eq.mpr (id (congrArg (fun _a => ∀ (exU : ∃ x, _a x) (exV : ∃ x, V x), choose exU = choose exV) hpred))
fun exU exV => Eq.refl (choose exU);
have this := h₀ exU exV;
thish:p⊢ p ∨ ¬p
All goals completed! 🐙
排除中律的推论包括双重否定消除、分情况证明和反证法， 所有这些都在经典逻辑一节中描述。 排除中律和命题外延性律蕴含了命题完备性：
open Classical
theorem propComplete (a : Prop) : a = True ∨ a = False :=
match em a with
| Or.inl ha =>
Or.inl (propext (Iff.intro (fun _ => True.intro) (fun _ => ha)))
| Or.inr hn =>
Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
有了选择公理，我们也能得到一个更强的原则，即每个命题都是可判定的。
回想一下 Decidable 可判定性命题集定义如下：
namespace Hidden
class inductive Decidable (p : Prop) where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p
end Hidden
与 p ∨ ¬ p 不同，它只能消去到 Prop，类型 Decidable p 等效于和类型
Sum p (¬ p)，它可以消除至任何类型。
这就是编写“if-then-else（若-则-否则）”表达式所需的数据。
作为经典推理的一个示例，我们使用 choose 来证明，若 f : α → β 是单射的，
且 α 是可居的，则 f 是左逆的。为了定义左逆 linv，我们使用一个依值的
if-then-else 表达式。回忆一下，if h : c then t else e 是
dite c (fun h : c => t) (fun h : ¬ c => e) 的记法。在 linv 的定义中，
选择公理使用了两次：首先，为了证明 (∃ a : α, f a = b) 是“可判定的”，
需要选择一个 a，使得 f a = b。请注意，propDecidable 是一个作用域实例，
它通过 open Classical 命令激活。我们使用此实例来证明 if-then-else 表达式。
（还可以参阅 可判命题一节 中的讨论）。
open Classical
noncomputable def linv [Inhabited α] (f : α → β) : β → α :=
fun b : β => if ex : (∃ a : α, f a = b) then choose ex else default
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 := rfl
_ = a := inj feq
从经典逻辑的视角来看，linv 是一个函数。而从构造性视角来看，
它是不可接受的；由于没有实现这样一种函数的通用方法，因此该构造不具备信息量。