本文介绍 Lean 的商类型 Quot。
商与代表元
设 \alpha 是集合，r 是 \alpha 上的二元关系。 数学上，一个二元关系如果满足自反性、对称性和传递性，就称为 等价关系（equivalence relation）。
记 r^{\mathrm{eq}} 为包含 r 的最小等价关系，称为 r 的等价闭包（equivalence closure）。
具体地，r^{\mathrm{eq}} 可以这样给出：对于任意 a,b\in \alpha，r^{\mathrm{eq}}(a,b) 成立当且仅当存在自然数 n 和 \alpha 中的元素 \tag{1} \begin{gathered} a=x_0,x_1,\ldots,x_n=b, \\ \text{满足 }\quad r(x_i,x_{i+1})\lor r(x_{i+1},x_i)\qquad(0\leq i\lt n). \end{gathered} 不难看出，r^{\mathrm{eq}} 满足自反性、对称性和传递性，且包含 r。
若 r 本来就是等价关系，则 r^{\mathrm{eq}}=r。
定义 a 的等价类（equivalence class）、 商集合（quotient set）及商映射： \begin{aligned} \relax [a]_{r^{\mathrm{eq}}}&:=\{b\in \alpha\mid r^{\mathrm{eq}}(a,b)\},\\ \alpha/r^{\mathrm{eq}}&:=\{[a]_{r^{\mathrm{eq}}}\mid a\in \alpha\},\\ \pi(a)&:=[a]_{r^{\mathrm{eq}}}. \end{aligned} 商集的元素是等价类。一个等价类中的任意元素都可以用来表示这个类，称为它的代表元（representative）。 两个代表元给出相同的等价类当且仅当它们由 r^{\mathrm{eq}} 联系起来。
Lean 中的商类型
商类型是在 Lean 的内核中实现的，因此并没有实现商类型的 Lean 代码。
但是在 Init/Prelude.lean 中以占位声明的方式列出了商类型的接口：
opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β qopaque 意为“不透明”，表示内核判断定义相等时不会展开常量的定义体。 这里的四个常量由内核直接提供，称为内核原语（kernel primitive），没有 Lean 定义体。 r : α → α → Prop 给每一对 a b : α 一个命题 r a b，命题成立表示 a、b 在关系 r 下相关。 Quot r 是关系 r 相对应的商类型（quotient type）。
Quot.mk r 是对应的商映射 \alpha \rightarrow \operatorname{Quot}\,r，这样 Quot.mk r a 就表示了 a 代表的等价类。
商上的函数、命题与相等
商类型的泛性质是：给定 \alpha 上的函数 f:\alpha\to \beta，若它满足 r\,a\,b 可以推出 f\,a = f\,b，则 f 可以提升为商上的函数 F:\operatorname{Quot}\,r\to \beta，使得 F(\pi(a))=f(a)。
商类型上的函数由以下接口定义：
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β给定函数 f:\alpha\to \beta 和证明 h : \forall a\,b : \alpha,\; r\,a\,b \to f\,a = f\,b，Quot.lift f h 就是商上的函数 F。
而等式 F(\pi(a))=f(a) 由下面的定理给出（位于 Quot 命名空间）：
protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v}
(f : α → β)
(c : (a b : α) → r a b → f a = f b)
(a : α)
: lift f c (Quot.mk r a) = f a :=
rfl简单地说，内核保证等式两边定义相等。
类似地，商类型上的命题成立当且仅当它对每个代表元都成立，这由如下内核接口给出：
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β qQuot.sound 与商中的相等
axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α},
r a b → Eq (Quot.mk r a) (Quot.mk r b)给定 h : r a b，Quot.sound h 保证对应的两个商元素相等：
Quot.sound h : Quot.mk r a = Quot.mk r b在商的泛性质中，sound 保证商映射自身尊重关系，lift 负责相容函数的分解。
沿用 \pi(a):=\operatorname{Quot.mk}\;r\;a 的记号。 Quot.sound 这个公理给出了商映射的基本性质： \operatorname{Quot.mk}\;r\;a=\operatorname{Quot.mk}\;r\;b \quad\Longleftrightarrow\quad r^{\mathrm{eq}}(a,b). 事实上，把 Quot.sound 应用到式 (1) 给出的有限链，可以看出 r^{\mathrm{eq}}(a,b) 蕴含 \pi(a)=\pi(b)。 反向可以用 lift。把 \alpha 中元素送到其等价类的映射 f : a \mapsto [a]_{r^{\mathrm{eq}}}，显然满足：如果 r\,a\,b 成立，就有 f\,a = f\,b。所以它可以提升为商上的函数 F，满足 F(\pi(a))=[a]_{r^{\mathrm{eq}}}。 若 \pi(a)=\pi(b)，就有 [a]_{r^{\mathrm{eq}}}=[b]_{r^{\mathrm{eq}}}。
用商类型证明函数外延性
函数外延性（function extensionality） 说的是：两个函数在每个输入处都有相等的值，它们就相等。 这是 Lean 内核中的一个基本的定理，陈述和它的证明1如下：
theorem funext' {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
(h : ∀ x, Eq (f x) (g x)) : Eq f g :=
let eqv (f g : (x : α) → β x) := ∀ x, Eq (f x) (g x)
let extfunApp (q : Quot eqv) (x : α) : β x :=
Quot.lift
(fun (f : ∀ (x : α), β x) => f x)
(fun _ _ h => h x) q
congrArg extfunApp (Quot.sound h)下面我们来分析这个证明。首先在（依赖）函数类型 (x:\alpha) \to \beta\,x 上定义一个等价关系 eqv：两个函数满足 eqv 当且仅当它们逐点相等。
另一方面，要利用 Quot.lift 这个接口，构造一个从商类型到函数类型的映射 \operatorname{extfunApp}: \operatorname{Quot}\,\mathit{eqv} \to ((x : \alpha) \to \beta\,x). 给定 x : \alpha，通过 Quot.lift 把 f \mapsto f\,x 提升为 \operatorname{Quot}\,\mathit{eqv} \to \beta\,x 的映射。这里显然，如果有 h : \mathit{eqv}\,f\,g，那么根据定义 f\,x = g\,x。
注意这个构造满足 \operatorname{extfunApp}\,(\operatorname{Quot.mk}\,\mathit{eqv}\,f) = (\lambda x.\,f\,x) = f. 这里第一个等号是因为前面的 Quot.liftBeta，而第二个等号是因为 lambda calculus 的 eta reduction。总之这个等式两边其实是定义相等的，可以直接用 rfl 处理（自己试一下）。
最后 Quot.sound h 给出 \operatorname{Quot.mk}\,\mathit{eqv}\,f = \operatorname{Quot.mk}\,\mathit{eqv}\,g，把这个等式传给 congrArg extfunApp 就得到 \begin{aligned} f &= \operatorname{extfunApp}\,(\operatorname{Quot.mk}\,\mathit{eqv}\,f) \\ &= \operatorname{extfunApp}\,(\operatorname{Quot.mk}\,\mathit{eqv}\,g) = g, \end{aligned} 从而证明了函数的外延性。
读者也许会不禁疑惑，为什么函数的外延性的证明这么复杂？一个原因是我们在这边只假设 f\,x 和 g\,x 命题相等，而不是定义相等。
-
和标准库比略有改动↩︎