本文介绍 Lean 的商类型 Quot。 商与代表元 设 是集合， 是 上的二元关系。 数学上，一个二元关系如果满足自反性、对称性和传递性，就称为 等价关系（equivalence relation）。 记 为包含 的最小等价关系，称为 的等价闭包（equivalence closure）。 具体地， 可以这样给出：对于任意 ， 成立当且仅当存在自然数 和 中的元素 不难看出， 满足自反性、对称性和传递性，且包含 。 若 本来就是等价关系，则 。 定义 的等价类（equivalence class）、 商集合（quotient set）及商映射： 商集的元素是等价类。一个等价类中的任意元素都可以用来表示这个类，称为它的代表元（representative）。 两个代表元给出相同的等价类当且仅当它们由 联系起来。 Lean 中的商类型 商类型是在 Lean 的内核中实现的，因此并没有实现商类型的 Lean 代码。 但是在 Init/Prelude.lean 中以占位声明的方式列出了商类型的接口： opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u opaque Quot.mk {α : Sort u} (r…

本文要讲清楚 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。 1 rfl 的定义 def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a 花括号中的参数称为隐式参数，Lean 可以根据上下文推断它们，调用时通常不必填写。 rfl 的定义体就是 Eq.refl a，只是把…

接着 Hales 对 Lean 可靠性的追问，解释 Lean 的基础规则、已经证明与尚未证明的元理论，以及现有研究和不同检查器各自提供的保证。