本文介绍 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 中的元素 a=x_0,x_1,\ldots,x_n=b, 使每一步都满足 r(x_i,x_{i+1})\lor r(x_{i+1},x_i)\qquad(0\leq i\lt n). 不难看出，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, β q

opaque 意为“不透明”，表示内核判断定义相等时不会展开常量的定义体。 这里的四个常量由内核直接提供，称为内核原语（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, β q

Quot.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 的记号。 sound 给出每一步关系对应的商等式，等式的自反性、对称性和传递性又把这些等式延伸到整个有限链，因此 r^{\mathrm{eq}}(a,b) 蕴含 \pi(a)=\pi(b)。 反向可以用 lift 说明。记 E=r^{\mathrm{eq}}，把代表元 a 送到其等价类 [a]_E，这个映射尊重 r，所以能提升为商上的函数 C，满足 C(\pi(a))=[a]_E。 若 \pi(a)=\pi(b)，就有 [a]_E=[b]_E，从而 E(a,b)。两边合起来便得到 ² \operatorname{Quot.mk}\;r\;a=\operatorname{Quot.mk}\;r\;b \quad\Longleftrightarrow\quad r^{\mathrm{eq}}(a,b).

用商类型证明函数外延性

函数外延性（function extensionality） 说的是：两个函数在每个输入处都有相等的值，它们就相等。 这是 Lean 内核中的一个基本的定理，陈述和它的证明³如下：

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 命题相等，而不是定义相等。

---

1. 商公理的原声明见 Quot.sound。↩︎

2. 这里用集合论的等价类说明数学构造；参见 Theorem Proving in Lean 4：Quotients。↩︎

3. 和标准库比略有改动↩︎