本文介绍 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, β 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 的记号。 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 内核中的一个基本的定理，陈述和它的证明¹如下：

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

本文要讲清楚 Lean 中的定义相等和命题相等这两个概念。 在这个过程中，我们也会解释其他相关概念。

相等命题的定义

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

Eq a b 记作 a = b，表示同一类型 α 中两个项相等的命题，称为命题相等（propositional equality）。 唯一的构造子 Eq.refl 给出自反性的证明：对每个 a : α，都有 Eq.refl a : a = a。 ¹

rfl 的定义

def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a

花括号中的参数称为隐式参数，Lean 可以根据上下文推断它们，调用时通常不必填写。 rfl 的定义体就是 Eq.refl a，只是把 a 也设成了隐式参数。 在 := rfl 中，Lean 根据目标推断 a。

内核检查证明项的类型时，按定义展开、计算等转换规则识别相同的表达式。 这种关系叫定义相等（definitional equality）。 如果目标 Eq t s 与某个 Eq a a 定义相等， Eq.refl a 就能作为该目标的证明。 例如，1 + 2 和 2 + 1 都归约为 3， 目标 1 + 2 = 2 + 1 因而与 3 = 3 定义相等：

import Init

example : 1 + 2 = 2 + 1 := rfl

这里的 example 让 Lean 检查冒号后的命题与 := 后的证明是否匹配。 rfl 在这里构造的是一个 Eq 证明；定义相等使它的类型与目标匹配。 ²

归纳类型与递归器

归纳类型 A 的定义列出了构造子，也就列出了定义函数时要处理的各种情形。 Lean 同时生成递归器（recursor）A.rec，让我们按这些情形定义函数。

先考虑单独定义的归纳类型 A : Type u，其构造子都返回 A。我们要定义的函数可以具有下面的类型：

F : (a : A) → motive a

这里 motive: A → Sort v 是函数的目标类型族，motive a 是函数在 a 处的返回类型。 我们要为每个 a 给出一个值 F a : motive a。 这样的函数称为依赖函数，因为返回类型可以随输入变化。 若结果总属于同一个类型 β，取 motive := fun _ ↦ β，就得到普通函数 A → β。 若 motive a 是命题，F a 就是这个命题的证明。

使用 A.rec 定义 F，需要提供两部分内容：

1. motive：说明每个输入 a 所需的结果类型 motive a。

2. 每个构造子对应的分支：说明输入由这个构造子构成时，F 的值怎样给出。 若构造子含有递归子项，分支还可以使用 F 处理那些子项所得的结果。

递归器把这些分支组成所需的函数，并规定它在各个构造子上的计算方式。 它规定怎样使用归纳类型中的项得到结果，因此也称为消去原则。 当函数的结果是证明时，这也给出了归纳证明的方法。 ³

下面的递归器把 motive 写在花括号里，同样作为隐式参数。 这是因为 Lean 通常可以从后面参数的类型推断出 motive，不必每次都写出来。

PUnit：只有一个元素的类型

只有一个元素的类型称为单元素类型（singleton type）。 Core 中的 PUnit 就是这样的归纳类型： ⁴

inductive PUnit : Sort u where
  | unit : PUnit

PUnit 只有一个元素 PUnit.unit。 给定目标类型族 motive : PUnit.u → Sort v，我们要定义函数：

F : (x : PUnit.{u}) → motive x

PUnit.rec 的完整类型是：

PUnit.rec :
  ∀ {motive : PUnit.{u} → Sort v}
    (unitCase : motive PUnit.unit.{u})
    (x : PUnit.{u}),
    motive x

由于 PUnit 只有一个元素，我们只需给出 motive PUnit.unit 中的一个元素 unitCase。 PUnit.rec 就用这个值作为 F PUnit.unit，给出所求的函数。

等式消去：Eq.rec

Eq.rec 的完整类型是：

Eq.rec :
  ∀ {α : Sort u} {a : α}
    {motive : (b : α) → (h : a = b) → Sort v}
    (reflCase : motive a (Eq.refl a))
    {b : α} (h : a = b),
    motive b h

先固定类型 α : Sort u 和左端 a : α，再让右端 b 变化。 等式证明 h : a = b 是递归器要处理的输入， motive b h 则是所求函数在这一输入处的返回类型，或此时要证明的命题。

Eq 只有 refl 这一个构造子。 因此，我们只须给出：

reflCase : motive a (Eq.refl a)

再给定任意 b 和证明 h : a = b，Eq.rec 就返回一个 motive b h 中的结果。

用 Eq.rec 证明 congrArg

congrArg 说的是：对相等的两个项应用同一个函数，结果仍然相等。 f a 这样的表达式称为函数应用（function application，简称 app）。 定理的完整陈述是：

congrArg : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β),
  a₁ = a₂ → f a₁ = f a₂

这里 f : α → β 的结果类型是固定的 β，所以两个应用项具有同一个类型。

example {α : Sort u} {β : Sort v} {a₁ a₂ : α}
    (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
  Eq.rec (motive := fun x _ ↦ f a₁ = f x) (Eq.refl (f a₁)) h

这里的 motive 表示：右端为 x 时，要证明 f a₁ = f x；下划线表示不使用等式证明本身。 在自反情形下，目标变成 f a₁ = f a₁，由 Eq.refl (f a₁) 证明。 最后将 h : a₁ = a₂ 交给 Eq.rec，便得到 f a₁ = f a₂ 的证明。

对类型进行等式替换

如果你打开 Lean 的标准库会发现congrArg并不是用上面的方法证明的，而是用 ▸ 记号：

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β)
    (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
  h ▸ rfl

h ▸ e 是 Lean 的等式替换记号，替换发生在类型中的参数位置。 在安装了 Lean 4 扩展的 VS Code 中，输入 \t，再按 Tab，就得到 ▸。 ⁵ 把程序确定的类型族记作 P。沿 h : a = b 正向替换时，程序从 e : P a 构造 h ▸ e : P b。 这里 e 可以是证明，也可以是数据。

负责 h ▸ e 的精化程序是 Lean.Elab.Term.elabSubst。 给定 h : a = b，它从类型中确定替换位置，构造通过类型检查的目标类型族，再按 Eq.rec 的等式消去规则构造结果，交给内核检查。 ⁶

例如，Lean 核心库的 Vector α n 表示由 n 个 α 类型的元素组成的向量，长度 n 是类型的一部分。 ⁷ 某个函数要求输入 Vector α m，而我们手中有 v : Vector α n 和长度相等的证明 h : n = m，就可以这样转换类型：

example {α : Type} {n m : Nat} (h : n = m) (v : Vector α n) : Vector α m :=
  h ▸ v

这里替换的是类型 Vector α n 中的长度参数 n，结果的类型是 Vector α m；向量中的元素及其顺序保持不变。

Nat.zero_add 的证明

自然数的两种构造形式是零和后继 Nat.succ n，后者就是 n + 1。 自然数递归器 Nat.rec 的完整类型是：

Nat.rec :
  ∀ {motive : Nat → Sort u}
    (zeroCase : motive 0)
    (succCase : (n : Nat) → motive n → motive (Nat.succ n))
    (n : Nat),
    motive n

它让我们按零和后继两种情形定义函数：先给出零处的值， 再说明怎样利用 n 及 n 处的结果，得到 Nat.succ n 处的结果。 如果 motive 是命题族，后继分支收到的 motive n 就是归纳假设。

我们要证明命题相等 0 + n = n，其中 n : Nat 是任意自然数。

Nat.add 按第二个参数递归，定义如下： ⁸

def Nat.add : Nat → Nat → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

由第二个分支，0 + Nat.succ n 定义相等于 Nat.succ (0 + n)。

当 n 是任意变量时，0 + n 与 n 并不定义相等。直接用 rfl 证明会失败：

example (n : Nat) : 0 + n = n := by rfl

Lean 报错：

Tactic `rfl` failed: The left-hand side
  0 + n
is not definitionally equal to the right-hand side
  n

此时第二个参数 n 尚未确定是零还是后继，无法按上述分支继续计算。

对 n 使用 Nat.rec，可以把库中证明的两个分支写成下面的显式递归器形式： ⁹

theorem Nat.zero_add : ∀ (n : Nat), 0 + n = n :=
  Nat.rec (motive := fun n ↦ 0 + n = n)
    rfl
    (fun n ih ↦ congrArg Nat.succ ih)

这里的 motive 是 fun n ↦ 0 + n = n，所以零处要证明 0 + 0 = 0，由 rfl 完成。 后继分支中的 ih 是归纳假设 0 + n = n。 congrArg Nat.succ ih 在等式两边应用后继函数，得到 Nat.succ (0 + n) = Nat.succ n 的证明。 由上面的加法定义，这个证明的类型与后继目标 0 + Nat.succ n = Nat.succ n 定义相等，因而完成证明。

2026 年 10 月 9 日，Thomas Hales 在《What’s new》发表了 一篇关于 Lean 可靠性的客座文章。 他指出，Lean 类型论中的一些基本性质仍缺少完整证明。这颇令人意外。

本文在 GPT 和 Codex 的辅助下完成资料查证、讨论和改稿。 我试图弄清楚 Lean 的理论基础是什么，现有的验证结果覆盖到了哪里，以及还有哪些问题尚未解决。

我目前的理解是，这些问题中最“严重”的是定义相等的不可判定性。 但不可判定性本身不妨碍可靠的证明检查。 有些类型转换在理论上成立，算法却无法确认。相应的证明项便无法通过检查。 检查算法的可靠性（soundness） 要求的是：凡是检查器接受的证明，都符合规定的规则。¹

Hales 提到的类型唯一性、\Pi 单射性等，是另外一些仍需研究的元理论性质。 但这些未证明的性质，并不妨碍通过其他路线建立可靠性保证。²

Upshot（我的理解）：就理论基础而言，Lean 的可靠性（soundness）并没有实质性的问题。

Continue reading →