4.5. 商数🔗

商类型允许通过减小现有类型的命题等价的粒度来形成新类型。特别是，给定类型 A 和等价关系 \sim，商 A / \sim 包含与 A 相同的元素，但与 \sim 相关的每对元素都被视为相等。平等受到普遍尊重； Lean 的逻辑中没有任何内容可以观察到两个相等项之间的任何差异。因此，商类型提供了一种构建难以逾越的抽象障碍的方法。特别是，商类型的所有函数都必须证明它们遵循等价关系。

def

Quotient.{u} {α : Sort u} (s : Setoid α) : Sort u
Quotient.{u} {α : Sort u} (s : Setoid α) :
  Sort u

Quotient types coarsen the propositional equality for a type so that terms related by some equivalence relation are considered equal. The equivalence relation is given by an instance of Setoid.

Set-theoretically, Quotient s can seen as the set of equivalence classes of α modulo the Setoid instance's relation s.r. Functions from Quotient s must prove that they respect s.r: to define a function f : Quotient s → β, it is necessary to provide f' : α → β and prove that for all x : α and y : α, s.r x y → f' x = f' y. Quotient.lift implements this operation.

The key quotient operators are:

Quotient.mk places elements of the underlying type α into the quotient.
Quotient.lift allows the definition of functions from the quotient to some other type.
Quotient.sound asserts the equality of elements related by r
Quotient.ind is used to write proofs about quotients by assuming that all elements are constructed with Quotient.mk.

Quotient is built on top of the primitive quotient type Quot, which does not require a proof that the relation is an equivalence relation. Quotient should be used instead of Quot for relations that actually are equivalence relations.

证明基础类型的两个元素通过等价关系相关就足以证明它们在 Quotient 中相等。但是，定义等价不受使用 Quotient 的影响：商中的两个元素定义等价当且仅当它们在基础类型中定义等价时。

商类型在编程中并未广泛使用。然而，它们在数学中经常出现：

整数: 这些整数传统上定义为一对自然数(n, k)，对整数 n - k 进行编码。在此编码中，如果 n_1 + k_2 = n_2 + k_1，则两个整数 (n_1, k_1) 和 (n_2, k_2) 相等。
有理数: 编号 \frac{n}{d} can be encoded as the pair (n, d)，其中 d \neq 0。两个有理数 \frac{n_1}{d_1} and \frac{n_2}{d_2} are equal if n_1 d_2 = n_2 d_1。
实数: 实数可以表示为柯西序列，但这种编码不是唯一的。使用商类型，当两个柯西序列的差值收敛到零时，可以使它们相等。
有限集: 有限集可以表示为元素列表。对于商类型，如果两个有限集包含相同的元素，则它们可以相等；该定义不对元素的类型强加任何要求（例如可判定的相等性或排序关系）。

商类型的一种替代方法是直接推理关系引入的等价类。这种方法的缺点是它不允许进行计算：除了知道存在一个整数是 5 与 8 的和之外，知道 5 + 8 = 13 并不是一个需要证明的定理也很有用。从等价类集合中定义函数依赖于非计算经典推理原理，而商类型的函数是额外遵循等价关系的普通计算函数。

4.5.1. 商类型的替代方案🔗

虽然 Quotient 是形成具有合理计算属性的商的便捷方法，但通常也可以通过其他方式定义商。

一般来说，如果类型 Q 遵循商的通用属性，则通过等价关系 \sim 可以将类型 Q 称为 A 的商：存在一个函数 q:A\to Q，其属性为 q(a)=q(b) 当且仅当 a\sim b 对于所有a 和 b 位于 A 中。

由 Quotient 形成的商在命题等价范围内具有此属性：与 \sim 相关的 A 的元素相等，因此无法区分它们。但是，同一等价类的成员的商不一定是定义等价。

商还可以通过在 A 本身中指定每个等价类的单个代表，然后将 Q 定义为 A 中的元素对并证明它们是这样的规范代表来实现。与将 A 中的每个 a 映射到其规范代表的函数一起，Q 是 A 的商。由于证明无关，同一等价类的Q中的代表是定义等价。

这种手动实现的商 Q 比 Quotient 更容易使用。特别是，因为每个等价类都由其单个规范代表表示，所以无需证明商的函数遵循等价关系。由于计算给出归一化值，它还可以具有更好的计算属性（相反，Quotient 的元素可以用多种方式表示）。最后，由于手动实现的商是归纳类型，因此它可以在其他类型不能使用的上下文中使用，例如定义嵌套归纳类型时。然而，并非所有商都可以手动实现。

Manually Quotiented Integers

当作为一对 Nat 实现时，根据所需的整数相等性，每个等价类都具有一个规范表示，其中 Nat 中至少有一个为零。这可以表示为 Lean 结构：

structure Z where
  a : Nat
  b : Nat
  canonical : a = 0 ∨ b = 0

由于证明无关性，表示相同整数的该结构类型的每个值已经相等。使用包装器可以更方便地构建 Z，该包装器利用自然数的减法在零处截断的事实来自动构建证明：

def Z.mk' (n k : Nat) : Z where
  a := n - k
  b := k - n
  canonical := byn:Natk:Nat⊢ n - k = 0 ∨ k - n = 0 omegaAll goals completed! 🐙

这种构造尊重整数的相等要求：

theorem Z_mk'_respects_eq :
    (Z.mk' n k = Z.mk' n' k') ↔ (n + k' = n' + k) := byn:Natk:Natn':Natk':Nat⊢ Z.mk' n k = Z.mk' n' k' ↔ n + k' = n' + k
  simp [Z.mk']n:Natk:Natn':Natk':Nat⊢ n - k = n' - k' ∧ k - n = k' - n' ↔ n + k' = n' + k
  omegaAll goals completed! 🐙

要在示例中使用此类型，拥有 Neg、OfNat 和 ToString 实例会很方便。这些实例使阅读或编写示例变得更加容易。

instance : Neg Z where
  neg n := Z.mk' n.b n.a

instance : OfNat Z n where
  ofNat := Z.mk' n 0

instance : ToString Z where
  toString n :=
    if n.a = 0 then
      if n.b = 0 then "0"
      else s!"-{n.b}"
    else toString n.a

5#eval (5 : Z)

-5#eval (-5 : Z)

-5

加法是基础 Nat 的加法：

instance : Add Z where
  add n k := Z.mk' (n.a + k.a) (n.b + k.b)

17#eval (-5 + 22: Z)

由于每个等价类都是唯一表示的，因此无需编写 Z 中的这些函数遵循等价关系的证明。然而，在实践中，API 对于商应该针对手动构造的商实现，并证明尊重通用属性。

Live ↪

Built-In Integers as Quotients

Lean 的内置整数类型 Int 满足商的通用性质，因此可以将其视为 Nat 对的商。每个等价类的规范代表可以通过比较和减法来计算：这个toInt函数在标准库中称为Int.subNatNat。

def toInt (n k : Nat) : Int :=
  if n < k then - (k - n : Nat)
  else if n = k then 0
  else (n - k : Nat)

它满足普遍性质。当且仅当 toInt 为两对 Int 计算相同的 Int 时，两对 Nat 表示相同的整数：

theorem toInt_sound :
    n + k' = k + n' ↔
    toInt n k = toInt n' k' := byn:Natk':Natk:Natn':Nat⊢ n + k' = k + n' ↔ toInt n k = toInt n' k'
  simp only [toInt]n:Natk':Natk:Natn':Nat⊢ n + k' = k + n' ↔
  (if n < k then -↑(k - n) else if n = k then 0 else ↑(n - k)) =
    if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')
  splitisTruen:Natk':Natk:Natn':Nath✝:n < k⊢ n + k' = k + n' ↔ -↑(k - n) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalsen:Natk':Natk:Natn':Nath✝:¬n < k⊢ n + k' = k + n' ↔ (if n = k then 0 else ↑(n - k)) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') <;>isTruen:Natk':Natk:Natn':Nath✝:n < k⊢ n + k' = k + n' ↔ -↑(k - n) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalsen:Natk':Natk:Natn':Nath✝:¬n < k⊢ n + k' = k + n' ↔ (if n = k then 0 else ↑(n - k)) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') splitisFalse.isTruen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:n = k⊢ n + k' = k + n' ↔ 0 = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalse.isFalsen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:¬n = k⊢ n + k' = k + n' ↔ ↑(n - k) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') <;>isTrue.isTruen:Natk':Natk:Natn':Nath✝¹:n < kh✝:n' < k'⊢ n + k' = k + n' ↔ -↑(k - n) = -↑(k' - n')isTrue.isFalsen:Natk':Natk:Natn':Nath✝¹:n < kh✝:¬n' < k'⊢ n + k' = k + n' ↔ -↑(k - n) = if n' = k' then 0 else ↑(n' - k')isFalse.isTruen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:n = k⊢ n + k' = k + n' ↔ 0 = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k')isFalse.isFalsen:Natk':Natk:Natn':Nath✝¹:¬n < kh✝:¬n = k⊢ n + k' = k + n' ↔ ↑(n - k) = if n' < k' then -↑(k' - n') else if n' = k' then 0 else ↑(n' - k') omegaAll goals completed! 🐙

Live ↪

4.5.2. 类固醇🔗

商类型是建立在 setoid 之上的。 setoid 是与区分的等价关系配对的类型。与商类型不同，不强制执行抽象障碍，并且围绕相等性设计的证明自动化不能与 setoid 的等价关系一起使用。 Setoid 除了作为商类型的构建块之外，本身也很有用。

type class

Setoid.{u} (α : Sort u) : Sort (max 1 u)
Setoid.{u} (α : Sort u) : Sort (max 1 u)

A setoid is a type with a distinguished equivalence relation, denoted ≈.

The Quotient type constructor requires a Setoid instance.

Instance Constructor

Setoid.mk.{u}

Methods

r : α → α → Prop

x ≈ y is the distinguished equivalence relation of a setoid.

iseqv : Equivalence Setoid.r

The relation x ≈ y is an equivalence relation.

theorem

Setoid.refl.{u} {α : Sort u} [Setoid α] (a : α) : a ≈ a
Setoid.refl.{u} {α : Sort u} [Setoid α]
  (a : α) : a ≈ a

A setoid's equivalence relation is reflexive.

theorem

Setoid.symm.{u} {α : Sort u} [Setoid α] {a b : α} (hab : a ≈ b) : b ≈ a
Setoid.symm.{u} {α : Sort u} [Setoid α]
  {a b : α} (hab : a ≈ b) : b ≈ a

A setoid's equivalence relation is symmetric.

theorem

Setoid.trans.{u} {α : Sort u} [Setoid α] {a b c : α} (hab : a ≈ b)
  (hbc : b ≈ c) : a ≈ c
Setoid.trans.{u} {α : Sort u} [Setoid α]
  {a b c : α} (hab : a ≈ b)
  (hbc : b ≈ c) : a ≈ c

A setoid's equivalence relation is transitive.

4.5.3. 等价关系🔗

等价关系是自反、对称和传递的关系。

syntaxEquivalence Relations

根据类型的某些规范等价关系的等价性是使用 ≈ 编写的，它是使用类型类 HasEquiv 重载的。

term ::= ...
    | `x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`.term ≈ term

type class

HasEquiv.{u, v} (α : Sort u) : Sort (max u (v + 1))
HasEquiv.{u, v} (α : Sort u) :
  Sort (max u (v + 1))

HasEquiv α is the typeclass which supports the notation x ≈ y where x y : α.

Instance Constructor

HasEquiv.mk.{u, v}

Methods

Equiv : α → α → Sort v

x ≈ y says that x and y are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent.

Conventions for notations in identifiers:

The recommended spelling of ≈ in identifiers is equiv.

关系 r 实际上是等价关系，这一事实被声明为 Equivalence r。

structure

Equivalence.{u} {α : Sort u} (r : α → α → Prop) : Prop
Equivalence.{u} {α : Sort u}
  (r : α → α → Prop) : Prop

An equivalence relation r : α → α → Prop is a relation that is

reflexive: r x x,
symmetric: r x y implies r y x, and
transitive: r x y and r y z implies r x z.

Equality is an equivalence relation, and equivalence relations share many of the properties of equality.

Constructor

Equivalence.mk.{u}

Fields

refl : ∀ (x : α), r x x

An equivalence relation is reflexive: r x x

symm : ∀ {x y : α}, r x y → r y x

An equivalence relation is symmetric: r x y implies r y x

trans : ∀ {x y z : α}, r x y → r y z → r x z

An equivalence relation is transitive: r x y and r y z implies r x z

每个 Setoid 实例都会导致一个对应的 HasEquiv 实例。

4.5.4. 商 API🔗

商 API 依赖于预先存在的 Setoid 实例。

4.5.4.1. 商数介绍🔗

类型 Quotient 需要 Setoid 的实例作为普通参数，而不是作为实例隐式参数。这有助于确保商使用预期的等价关系。可以通过命名实例或使用 inferInstance 来提供实例。

商中的值是来自 setoid 基础类型的值，包装在 Quotient.mk 中。

def

Quotient.mk.{u} {α : Sort u} (s : Setoid α) (a : α) : Quotient s
Quotient.mk.{u} {α : Sort u}
  (s : Setoid α) (a : α) : Quotient s

Places an element of a type into the quotient that equates terms according to an equivalence relation.

The setoid instance is provided explicitly. Quotient.mk' uses instance synthesis instead.

Given v : α, Quotient.mk s v : Quotient s is like v, except all observations of v's value must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long as the mapping respects s.r.

def

Quotient.mk'.{u} {α : Sort u} [s : Setoid α] (a : α) : Quotient s
Quotient.mk'.{u} {α : Sort u}
  [s : Setoid α] (a : α) : Quotient s

Places an element of a type into the quotient that equates terms according to an equivalence relation.

The equivalence relation is found by synthesizing a Setoid instance. Quotient.mk instead expects the instance to be provided explicitly.

Given v : α, Quotient.mk' v : Quotient s is like v, except all observations of v's value must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long as the mapping respects s.r.

The Integers as a Quotient Type

整数定义为自然数对，其中表示的整数是两个数字的差，可以通过商类型表示。这种表示形式并不唯一：(4, 7) 和 (1, 4) 均表示 -3。

当两个编码整数通过 Z.eq 相关时，应将其视为相等：

def Z' : Type := Nat × Nat

def Z.eq (n k : Z') : Prop :=
  n.1 + k.2 = n.2 + k.1

这个关系是一个等价关系：

def Z.eq.eqv : Equivalence Z.eq where
  refl := by⊢ ∀ (x : Z'), eq x x
    intro (x, y)x:Naty:Nat⊢ eq (x, y) (x, y)
    simp +arith [eq]All goals completed! 🐙
  symm := by⊢ ∀ {x y : Z'}, eq x y → eq y x
    intro (x, y) (x', y') heqx:Naty:Natx':Naty':Natheq:eq (x, y) (x', y')⊢ eq (x', y') (x, y)
    simp_all only [eq]x:Naty:Natx':Naty':Natheq:x + y' = y + x'⊢ x' + y = y' + x
    omegaAll goals completed! 🐙
  trans := by⊢ ∀ {x y z : Z'}, eq x y → eq y z → eq x z
    intro (x, y) (x', y') (x'', y'')x:Naty:Natx':Naty':Natx'':Naty'':Nat⊢ eq (x, y) (x', y') → eq (x', y') (x'', y'') → eq (x, y) (x'', y'')
    intro heq1 heq2x:Naty:Natx':Naty':Natx'':Naty'':Natheq1:eq (x, y) (x', y')heq2:eq (x', y') (x'', y'')⊢ eq (x, y) (x'', y'')
    simp_all only [eq]x:Naty:Natx':Naty':Natx'':Naty'':Natheq1:x + y' = y + x'heq2:x' + y'' = y' + x''⊢ x + y'' = y + x''
    omegaAll goals completed! 🐙

因此，它可以用作 Setoid：

instance Z.instSetoid : Setoid Z' where
  r := Z.eq
  iseqv := Z.eq.eqv

整数类型 Z 就是 Z' 除以 Setoid 实例的商：

def Z : Type := Quotient Z.instSetoid

帮助程序 Z.mk 使创建整数变得更简单，而无需担心 Setoid 实例的选择：

def Z.mk (n : Z') : Z := Quotient.mk _ n

然而，数字文字更方便。 OfNat 实例允许将数字文字用于整数：

instance : OfNat Z n where
  ofNat := Z.mk (n, 0)

Live ↪

4.5.4.2. 消除商数🔗

商的函数可以通过证明基础类型的函数遵循商的等价关系来定义。这是使用 Quotient.lift 或其二进制对应物 Quotient.lift₂ 来完成的。变体 Quotient.liftOn 和 Quotient.liftOn₂ 将商参数放在参数列表中的第一个而不是最后一个。

def

Quotient.lift.{u, v} {α : Sort u} {β : Sort v} {s : Setoid α}
  (f : α → β) : (∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β
Quotient.lift.{u, v} {α : Sort u}
  {β : Sort v} {s : Setoid α}
  (f : α → β) :
  (∀ (a b : α), a ≈ b → f a = f b) →
    Quotient s → β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's equivalence relation.

Given s : Setoid α and a quotient Quotient s, applying a function f : α → β requires a proof h that f respects the equivalence relation s.r. In this case, the function Quotient.lift f h : Quotient s → β computes the same values as f.

Quotient.liftOn is a version of this operation that takes the quotient value as its first explicit parameter.

def

Quotient.liftOn.{u, v} {α : Sort u} {β : Sort v} {s : Setoid α}
  (q : Quotient s) (f : α → β) (c : ∀ (a b : α), a ≈ b → f a = f b) : β
Quotient.liftOn.{u, v} {α : Sort u}
  {β : Sort v} {s : Setoid α}
  (q : Quotient s) (f : α → β)
  (c : ∀ (a b : α), a ≈ b → f a = f b) : β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's equivalence relation.

Given s : Setoid α and a quotient value q : Quotient s, applying a function f : α → β requires a proof c that f respects the equivalence relation s.r. In this case, the term Quotient.liftOn q f h : β reduces to the result of applying f to the underlying α value.

Quotient.lift is a version of this operation that takes the quotient value last, rather than first.

def

Quotient.lift₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB} {φ : Sort uC}
  {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ
Quotient.lift₂.{uA, uB, uC} {α : Sort uA}
  {β : Sort uB} {φ : Sort uC}
  {s₁ : Setoid α} {s₂ : Setoid β}
  (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ →
        b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) :
  φ

Lifts a binary function from the underlying types to a binary function on quotients. The function must respect both quotients' equivalence relations.

Quotient.lift is a version of this operation for unary functions. Quotient.liftOn₂ is a version that take the quotient parameters first.

def

Quotient.liftOn₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB} {φ : Sort uC}
  {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) :
  φ
Quotient.liftOn₂.{uA, uB, uC}
  {α : Sort uA} {β : Sort uB}
  {φ : Sort uC} {s₁ : Setoid α}
  {s₂ : Setoid β} (q₁ : Quotient s₁)
  (q₂ : Quotient s₂) (f : α → β → φ)
  (c :
    ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β),
      a₁ ≈ a₂ →
        b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) :
  φ

Lifts a binary function from the underlying types to a binary function on quotients. The function must respect both quotients' equivalence relations.

Quotient.liftOn is a version of this operation for unary functions. Quotient.lift₂ is a version that take the quotient parameters last.

Integer Negation and Addition

给定整数的编码 Z 作为自然数对的商，可以通过交换第一个和第二个投影来实现求反：

def neg' : Z' → Z
  | (x, y) => .mk (y, x)

通过证明否定遵循等价关系，可以将其转换为从 Z 到 Z 的函数：

instance : Neg Z where
  neg :=
    Quotient.lift neg' <| by⊢ ∀ (a b : Z'), a ≈ b → neg' a = neg' b
      intro n k equivn:Z'k:Z'equiv:n ≈ k⊢ neg' n = neg' k
      cases nmkk:Z'fst✝:Natsnd✝:Natequiv:(fst✝, snd✝) ≈ k⊢ neg' (fst✝, snd✝) = neg' k; cases kmk.mkfst✝¹:Natsnd✝¹:Natfst✝:Natsnd✝:Natequiv:(fst✝¹, snd✝¹) ≈ (fst✝, snd✝)⊢ neg' (fst✝¹, snd✝¹) = neg' (fst✝, snd✝)
      apply Quotient.soundmk.mkfst✝¹:Natsnd✝¹:Natfst✝:Natsnd✝:Natequiv:(fst✝¹, snd✝¹) ≈ (fst✝, snd✝)⊢ (snd✝¹, fst✝¹) ≈ (snd✝, fst✝)
      simp [· ≈ ·, instHasEquivOfSetoid, Setoid.r, Z.eq] at *mk.mkfst✝¹:Natsnd✝¹:Natfst✝:Natsnd✝:Natequiv:fst✝¹ + snd✝ = snd✝¹ + fst✝⊢ snd✝¹ + fst✝ = fst✝¹ + snd✝
      grindAll goals completed! 🐙

同样，Quotient.lift₂ 对于从商类型定义二元函数很有用。加法是逐点定义的：

def add' (n k : Nat × Nat) : Z :=
  .mk (n.1 + k.1, n.2 + k.2)

将其提升为商需要证明加法遵循等价关系：

instance : Add Z where
  add (n : Z) :=
    n.lift₂ add' <| byn:Z⊢ ∀ (a₁ : Nat × Nat) (b₁ : Z') (a₂ : Nat × Nat) (b₂ : Z'), a₁ ≈ a₂ → b₁ ≈ b₂ → add' a₁ b₁ = add' a₂ b₂
      intro n k n' k'n✝:Zn:Nat × Natk:Z'n':Nat × Natk':Z'⊢ n ≈ n' → k ≈ k' → add' n k = add' n' k'
      intro heq heq'n✝:Zn:Nat × Natk:Z'n':Nat × Natk':Z'heq:n ≈ n'heq':k ≈ k'⊢ add' n k = add' n' k'
      apply Quotient.soundn✝:Zn:Nat × Natk:Z'n':Nat × Natk':Z'heq:n ≈ n'heq':k ≈ k'⊢ (n.fst + k.fst, n.snd + k.snd) ≈ (n'.fst + k'.fst, n'.snd + k'.snd)
      cases nmkn:Zk:Z'n':Nat × Natk':Z'heq':k ≈ k'fst✝:Natsnd✝:Natheq:(fst✝, snd✝) ≈ n'⊢ ((fst✝, snd✝).fst + k.fst, (fst✝, snd✝).snd + k.snd) ≈ (n'.fst + k'.fst, n'.snd + k'.snd); cases kmk.mkn:Zn':Nat × Natk':Z'fst✝¹:Natsnd✝¹:Natheq:(fst✝, snd✝) ≈ n'fst✝:Natsnd✝:Natheq':(fst✝, snd✝) ≈ k'⊢ ((fst✝¹, snd✝¹).fst + (fst✝, snd✝).fst, (fst✝¹, snd✝¹).snd + (fst✝, snd✝).snd) ≈ (n'.fst + k'.fst, n'.snd + k'.snd); cases n'mk.mk.mkn:Zk':Z'fst✝²:Natsnd✝²:Natfst✝¹:Natsnd✝¹:Natheq':(fst✝, snd✝) ≈ k'fst✝:Natsnd✝:Natheq:(fst✝², snd✝²) ≈ (fst✝, snd✝)⊢ ((fst✝², snd✝²).fst + (fst✝¹, snd✝¹).fst, (fst✝², snd✝²).snd + (fst✝¹, snd✝¹).snd) ≈
  ((fst✝, snd✝).fst + k'.fst, (fst✝, snd✝).snd + k'.snd); cases k'mk.mk.mk.mkn:Zfst✝³:Natsnd✝³:Natfst✝²:Natsnd✝²:Natfst✝¹:Natsnd✝¹:Natheq:(fst✝², snd✝²) ≈ (fst✝, snd✝)fst✝:Natsnd✝:Natheq':(fst✝², snd✝²) ≈ (fst✝, snd✝)⊢ ((fst✝³, snd✝³).fst + (fst✝², snd✝²).fst, (fst✝³, snd✝³).snd + (fst✝², snd✝²).snd) ≈
  ((fst✝¹, snd✝¹).fst + (fst✝, snd✝).fst, (fst✝¹, snd✝¹).snd + (fst✝, snd✝).snd)
      simp_all only [· ≈ ·, instHasEquivOfSetoid, Setoid.r, Z.eq]mk.mk.mk.mkn:Zfst✝³:Natsnd✝³:Natfst✝²:Natsnd✝²:Natfst✝¹:Natsnd✝¹:Natfst✝:Natsnd✝:Natheq:fst✝³ + snd✝¹ = snd✝³ + fst✝¹heq':fst✝² + snd✝ = snd✝² + fst✝⊢ fst✝³ + fst✝² + (snd✝¹ + snd✝) = snd✝³ + snd✝² + (fst✝¹ + fst✝)
      grindAll goals completed! 🐙

Live ↪

当函数的结果类型为 subsingleton 时，可使用 Quotient.recOnSubsingleton 或 Quotient.recOnSubsingleton₂ 来定义函数。因为子单例的所有元素都是相等的，所以这样的函数自动遵守等价关系，因此没有证明义务。

def

Quotient.recOnSubsingleton.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v}
  [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))]
  (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) : motive q
Quotient.recOnSubsingleton.{u, v}
  {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v}
  [h :
    ∀ (a : α),
      Subsingleton
        (motive (Quotient.mk s a))]
  (q : Quotient s)
  (f :
    (a : α) → motive (Quotient.mk s a)) :
  motive q

An alternative recursion or induction principle for quotients that can be used when the target type is a subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial, so any function can be lifted.

Quotient.rec does not assume that the target type is a subsingleton.

def

Quotient.recOnSubsingleton₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB}
  {s₁ : Setoid α} {s₂ : Setoid β}
  {motive : Quotient s₁ → Quotient s₂ → Sort uC}
  [s :
    ∀ (a : α) (b : β),
      Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))]
  (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g :
    (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) :
  motive q₁ q₂
Quotient.recOnSubsingleton₂.{uA, uB, uC}
  {α : Sort uA} {β : Sort uB}
  {s₁ : Setoid α} {s₂ : Setoid β}
  {motive :
    Quotient s₁ → Quotient s₂ → Sort uC}
  [s :
    ∀ (a : α) (b : β),
      Subsingleton
        (motive (Quotient.mk s₁ a)
          (Quotient.mk s₂ b))]
  (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g :
    (a : α) →
      (b : β) →
        motive (Quotient.mk s₁ a)
          (Quotient.mk s₂ b)) :
  motive q₁ q₂

An alternative induction or recursion operator for defining binary operations on quotients that can be used when the target type is a subsingleton.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial, so any function can be lifted.

4.5.4.3. 关于商的证明🔗

证明商类型元素属性的基本工具是健全性公理和归纳原理。健全性公理指出，如果基础类型的两个元素通过商的等价关系相关，则它们在商类型中相等。归纳原理遵循归纳类型的递归结构：为了证明谓词包含商类型的所有元素，只需证明它适用于将 Quotient.mk 应用于基础类型的每个元素即可。由于 Quotient 不是归纳类型，因此策略（例如 cases 和 induction）要求使用 using 修饰符显式指定 Quotient.ind。

theorem

Quotient.sound.{u} {α : Sort u} {s : Setoid α} {a b : α} :
  a ≈ b → Quotient.mk s a = Quotient.mk s b
Quotient.sound.{u} {α : Sort u}
  {s : Setoid α} {a b : α} :
  a ≈ b →
    Quotient.mk s a = Quotient.mk s b

The quotient axiom, which asserts the equality of elements related in the setoid.

Because Quotient is built on a lower-level type Quot, Quotient.sound is implemented as a theorem. It is derived from Quot.sound, the soundness axiom for the lower-level quotient type Quot.

theorem

Quotient.ind.{u} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Prop} :
  (∀ (a : α), motive (Quotient.mk s a)) → ∀ (q : Quotient s), motive q
Quotient.ind.{u} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Prop} :
  (∀ (a : α), motive (Quotient.mk s a)) →
    ∀ (q : Quotient s), motive q

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quotient.mk.

Proofs About Quotients

考虑到前面示例中将整数定义为商类型，Quotient.ind 和 Quotient.sound 可用于证明负数是加法逆元。首先，Quotient.ind 用于将 n 的实例替换为 Quotient.mk 的应用程序。完成此操作后，通过 Quotient.lift 的展开定义和计算规则，等式的左侧在定义上变得等于 Quotient.mk 的单个应用程序。这使得 Quotient.sound 变得适用，从而产生了一个新的目标：表明双方通过等价关系相关。这可以使用 simp_arith 来证明。

theorem Z.add_neg_inverse (n : Z) : n  + (-n) = 0 := byn:Z⊢ n + -n = 0
  cases n using Quotient.indaa✝:Z'⊢ Quotient.mk instSetoid a✝ + -Quotient.mk instSetoid a✝ = 0
  apply Quotient.soundaa✝:Z'⊢ (a✝.fst + (a✝.snd, a✝.fst).fst, a✝.snd + (a✝.snd, a✝.fst).snd) ≈ (0, 0)
  simp +arith [· ≈ ·, instHasEquivOfSetoid, Setoid.r, eq]All goals completed! 🐙

Live ↪

对于更专业的用例，Quotient.rec、Quotient.recOn 和 Quotient.hrecOn 可用于定义从商类型到任何其他 Universe 中的类型的依赖函数。声明依赖函数遵循商的等价关系需要一种方法来处理依赖结果类型是用等式两边的商的不同值实例化这一事实的。 Quotient.rec 和 Quotient.recOn 使用 Quotient.sound 使相关元素相等，将适当的转换插入到相等语句中，而 Quotient.hrecOn 使用异构相等。

def

Quotient.rec.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v}
  (f : (a : α) → motive (Quotient.mk s a))
  (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) (q : Quotient s) :
  motive q
Quotient.rec.{u, v} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Sort v}
  (f : (a : α) → motive (Quotient.mk s a))
  (h :
    ∀ (a b : α) (p : a ≈ b),
      ⋯ ▸ f a = f b)
  (q : Quotient s) : motive q

A dependent recursion principle for Quotient. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

Quotient.lift is useful for defining non-dependent functions.
Quotient.ind is useful for proving theorems about quotients.
Quotient.recOnSubsingleton can be used whenever the target type is a Subsingleton.
Quotient.hrecOn uses heterogeneous equality instead of rewriting with Quotient.sound.

Quotient.recOn is a version of this recursor that takes the quotient parameter first.

def

Quotient.recOn.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v} (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) : motive q
Quotient.recOn.{u, v} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Sort v}
  (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (h :
    ∀ (a b : α) (p : a ≈ b),
      ⋯ ▸ f a = f b) :
  motive q

A dependent recursion principle for Quotient. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

Quotient.lift is useful for defining non-dependent functions.
Quotient.ind is useful for proving theorems about quotients.
Quotient.recOnSubsingleton can be used whenever the target type is a Subsingleton.
Quotient.hrecOn uses heterogeneous equality instead of rewriting with Quotient.sound.

Quotient.rec is a version of this recursor that takes the quotient parameter last.

def

Quotient.hrecOn.{u, v} {α : Sort u} {s : Setoid α}
  {motive : Quotient s → Sort v} (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (c : ∀ (a b : α), a ≈ b → f a ≍ f b) : motive q
Quotient.hrecOn.{u, v} {α : Sort u}
  {s : Setoid α}
  {motive : Quotient s → Sort v}
  (q : Quotient s)
  (f : (a : α) → motive (Quotient.mk s a))
  (c : ∀ (a b : α), a ≈ b → f a ≍ f b) :
  motive q

A dependent recursion principle for Quotient that uses heterogeneous equality, analogous to a recursor for a structure.

Quotient.recOn is a version of this recursor that uses Eq instead of HEq.

如果某个类型的两个元素的商相等，则它们通过 setoid 的等价关系相关。该属性称为 Quotient.exact。

theorem

Quotient.exact.{u} {α : Sort u} {s : Setoid α} {a b : α} :
  Quotient.mk s a = Quotient.mk s b → a ≈ b
Quotient.exact.{u} {α : Sort u}
  {s : Setoid α} {a b : α} :
  Quotient.mk s a = Quotient.mk s b →
    a ≈ b

If two values are equal in a quotient, then they are related by its equivalence relation.

4.5.5. 逻辑模型🔗

与函数和宇宙一样，商类型是 Lean 类型系统的内置功能。但是，底层原语基于稍微简单的 Quot 类型，而不是 Quotient，并且 Quotient 是根据 Quot 定义的。主要区别在于 Quot 基于任意关系，而不是 Setoid 实例。所提供的关系不必是等价关系；管理 Quot 和 Eq 的规则自动将所提供的关系扩展为其自反、传递、对称闭包。当关系已经是等价关系时，应使用 Quotient 代替 Quot，以便 Lean 可以利用该关系是等价关系的事实。

基本商类型 API 由 Quot、Quot.mk、Quot.lift、Quot.ind 和 Quot.sound 组成。它们的使用方式与基于 Quotient 的对应产品相同。

primitive

Quot.{u} {α : Sort u} (r : α → α → Prop) : Sort u
Quot.{u} {α : Sort u} (r : α → α → Prop) :
  Sort u

Low-level quotient types. Quotient types coarsen the propositional equality for a type α, so that terms related by some relation r are considered equal in Quot r.

Set-theoretically, Quot r can seen as the set of equivalence classes of α modulo r. Functions from Quot r must prove that they respect r: to define a function f : Quot r → β, it is necessary to provide f' : α → β and prove that for all x : α and y : α, r x y → f' x = f' y.

Quot is a built-in primitive:

Quot.mk places elements of the underlying type α into the quotient.
Quot.lift allows the definition of functions from the quotient to some other type.
Quot.sound asserts the equality of elements related by r.
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed with Quot.mk.

The relation r is not required to be an equivalence relation; the resulting quotient type's equality extends r to an equivalence as a consequence of the rules for equality and quotients. When r is an equivalence relation, it can be more convenient to use the higher-level type Quotient.

primitive

Quot.mk.{u} {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
Quot.mk.{u} {α : Sort u}
  (r : α → α → Prop) (a : α) : Quot r

Places an element of a type into the quotient that equates terms according to the provided relation.

Given v : α and relation r : α → α → Prop, Quot.mk r v : Quot r is like v, except all observations of v's value must respect r.

Quot.mk is a built-in primitive:

Quot is the built-in quotient type.
Quot.lift allows the definition of functions from the quotient to some other type.
Quot.sound asserts the equality of elements related by r.
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed with Quot.mk.

primitive

Quot.lift.{u, v} {α : Sort u} {r : α → α → Prop} {β : Sort v}
  (f : α → β) (a : ∀ (a b : α), r a b → f a = f b) : Quot r → β
Quot.lift.{u, v} {α : Sort u}
  {r : α → α → Prop} {β : Sort v}
  (f : α → β)
  (a : ∀ (a b : α), r a b → f a = f b) :
  Quot r → β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's relation.

Given a relation r : α → α → Prop and a quotient Quot r, applying a function f : α → β requires a proof a that f respects r. In this case, Quot.lift f a : Quot r → β computes the same values as f.

Lean's type theory includes a definitional reduction from Quot.lift f h (Quot.mk r v) to f v.

Quot.lift is a built-in primitive:

Quot is the built-in quotient type.
Quot.mk places elements of the underlying type α into the quotient.
Quot.sound asserts the equality of elements related by r
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed with Quot.mk; it is analogous to the recursor for a structure.

primitive

Quot.ind.{u} {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}
  (mk : ∀ (a : α), β (Quot.mk r a)) (q : Quot r) : β q
Quot.ind.{u} {α : Sort u}
  {r : α → α → Prop} {β : Quot r → Prop}
  (mk : ∀ (a : α), β (Quot.mk r a))
  (q : Quot r) : β q

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quot.mk.

Quot.rec is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

Quot.ind is a built-in primitive:

Quot is the built-in quotient type.
Quot.mk places elements of the underlying type α into the quotient.
Quot.lift allows the definition of functions from the quotient to some other type.
Quot.sound asserts the equality of elements related by r.

axiom

Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} :
  r a b → Quot.mk r a = Quot.mk r b
Quot.sound.{u} {α : Sort u}
  {r : α → α → Prop} {a b : α} :
  r a b → Quot.mk r a = Quot.mk r b

The quotient axiom, which asserts the equality of elements related by the quotient's relation.

The relation r does not need to be an equivalence relation to use this axiom. When r is not an equivalence relation, the quotient is with respect to the equivalence relation generated by r.

Quot.sound is part of the built-in primitive quotient type:

Quot is the built-in quotient type.
Quot.mk places elements of the underlying type α into the quotient.
Quot.lift allows the definition of functions from the quotient to some other type.
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed with Quot.mk; it is analogous to the recursor for a structure.

Quotient types are described in more detail in the Lean Language Reference.

4.5.5.1. 商约减🔗

除了上述常量之外，Lean 的内核还包含 Quot.lift 的缩减规则，该规则导致其与 Quot.mk 一起使用时缩减，类似于归纳类型的 ι-缩减。给定 r 与 α 的关系，从 α 到 β 的函数 f，以及 resp 证明 f 尊重 r，术语Quot.lift f resp (Quot.mk r x) 是定义等于 f x。

variable
  (r : α → α → Prop)
  (f : α → β)
  (ok : ∀ x y, r x y → f x = f y)
  (x : α)

example : Quot.lift f ok (Quot.mk r x) = f x := rfl

4.5.5.2. 商和归纳类型🔗

由于 Quot 不是归纳类型，因此作为商实现的类型可能不会出现在归纳类型声明中的嵌套出现次数周围。必须重写这些类型声明以删除嵌套商，这通常可以通过定义无商版本，然后单独定义实现所需相等关系的等价关系来完成。

Nested Inductive Types and Quotients

玫瑰树的嵌套归纳类型将 RoseTree 的递归出现嵌套在 List 下：

inductive RoseTree (α : Type u) where
  | leaf : α → RoseTree α
  | branch : List (RoseTree α) → RoseTree α

但是，对标识 squash types 样式的所有元素的 List 进行商会导致 Lean 拒绝该声明：

(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declaredinductive SetTree (α : Type u) where
  | leaf : α → SetTree α
  | branch :
    Quot (fun (xs ys : List (SetTree α)) => True) →
    SetTree α

(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declared

Live ↪

4.5.5.3. 低级商 API🔗

Quot.liftOn 是 Quot.lift 的一个版本，它首先取商类型的值，类似于 Quotient.liftOn。

def

Quot.liftOn.{u, v} {α : Sort u} {β : Sort v} {r : α → α → Prop}
  (q : Quot r) (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) : β
Quot.liftOn.{u, v} {α : Sort u}
  {β : Sort v} {r : α → α → Prop}
  (q : Quot r) (f : α → β)
  (c : ∀ (a b : α), r a b → f a = f b) : β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's relation.

Given a relation r : α → α → Prop and a quotient's value q : Quot r, applying a f : α → β requires a proof c that f respects r. In this case, Quot.liftOn q f h : β evaluates to the result of applying f to the underlying value in α from q.

Quot.liftOn is a version of the built-in primitive Quot.lift with its parameters re-ordered.

Quotient types are described in more detail in the Lean Language Reference.

Lean 还提供从 Quot 到任何子单例的便捷消除，无需进一步的证明义务，以及与 Quotient 所使用的相关消除原则相对应的相关消除原则。

def

Quot.recOnSubsingleton.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v}
  [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a)) : motive q
Quot.recOnSubsingleton.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v}
  [h :
    ∀ (a : α),
      Subsingleton (motive (Quot.mk r a))]
  (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a)) :
  motive q

An alternative induction principle for quotients that can be used when the target type is a subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's relation is trivial, so any function can be lifted.

Quot.rec does not assume that the type is a subsingleton.

def

Quot.rec.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a))
  (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) (q : Quot r) : motive q
Quot.rec.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v}
  (f : (a : α) → motive (Quot.mk r a))
  (h :
    ∀ (a b : α) (p : r a b),
      ⋯ ▸ f a = f b)
  (q : Quot r) : motive q

A dependent recursion principle for Quot. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

Quot.lift is useful for defining non-dependent functions.
Quot.ind is useful for proving theorems about quotients.
Quot.recOnSubsingleton can be used whenever the target type is a Subsingleton.
Quot.hrecOn uses heterogeneous equality instead of rewriting with Quot.sound.

Quot.recOn is a version of this recursor that takes the quotient parameter first.

def

Quot.recOn.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) : motive q
Quot.recOn.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (h :
    ∀ (a b : α) (p : r a b),
      ⋯ ▸ f a = f b) :
  motive q

A dependent recursion principle for Quot that takes the quotient first. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

Quot.lift is useful for defining non-dependent functions.
Quot.ind is useful for proving theorems about quotients.
Quot.recOnSubsingleton can be used whenever the target type is a Subsingleton.
Quot.hrecOn uses heterogeneous equality instead of rewriting with Quot.sound.

Quot.rec is a version of this recursor that takes the quotient parameter last.

def

Quot.hrecOn.{u, v} {α : Sort u} {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (c : ∀ (a b : α), r a b → f a ≍ f b) : motive q
Quot.hrecOn.{u, v} {α : Sort u}
  {r : α → α → Prop}
  {motive : Quot r → Sort v} (q : Quot r)
  (f : (a : α) → motive (Quot.mk r a))
  (c : ∀ (a b : α), r a b → f a ≍ f b) :
  motive q

A dependent recursion principle for Quot that uses heterogeneous equality, analogous to a recursor for a structure.

Quot.recOn is a version of this recursor that uses Eq instead of HEq.

4.5.6. 商和函数外延🔗

由于 Lean 的定义等价包含 Quot.lift 的计算归约规则，因此标准库中使用商类型来证明函数外延性，否则需要为 axiom。这是通过首先定义一种由外延相等引用的函数类型来完成的，对于该函数，外延相等根据定义成立。

variable {α : Sort u} {β : α → Sort v}

def extEq (f g : (x : α) → β x) : Prop :=
  ∀ x, f x = g x

def ExtFun (α : Sort u) (β : α → Sort v) :=
  Quot (@extEq α β)

扩展函数可以像普通函数一样应用。根据定义，应用程序尊重外延平等：如果应用于函数会产生相同的结果，那么应用它们会产生相同的结果。

def extApp
    (f : ExtFun α β)
    (x : α) :
    β x :=
  f.lift (· x) fun g g' h => byα:Sort uβ:α → Sort vf:ExtFun α βx:αg:(x : α) → β xg':(x : α) → β xh:extEq g g'⊢ g x = g' x
    exact h xAll goals completed! 🐙

为了证明两个外延相等的函数实际上相等，只需证明外延应用相应的外延函数所得到的函数是相等的即可。这是因为

extApp (Quot.mk _ f)

定义上等于

fun x => (Quot.mk extEq f).lift (· x) (fun _ _ h => h x)

它定义上等于 fun x => f x，它定义上等于（通过 η-等价）f。 Quot.lift 的计算规则的命题版本是不够的，因为可约表达式出现在函数体中，并且通过函数中的等式重写已经需要函数外延性。

从这里，足以表明两个函数的扩展版本是相等的。由于 Quot.sound，这是正确的：它们处于商的等价关系中这一事实是一个假设。该证明是标准库中的证明的更明确的版本：

theorem funext'
    {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) :
    f = g := byα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g x⊢ f = g
  suffices extApp (Quot.mk _ f) = extApp (Quot.mk _ g) byα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:extApp (Quot.mk extEq f) = extApp (Quot.mk extEq g)⊢ f = g
    unfold extApp at thisα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:(fun x => Quot.lift (fun x_1 => x_1 x) ⋯ (Quot.mk extEq f)) = fun x => Quot.lift (fun x_1 => x_1 x) ⋯ (Quot.mk extEq g)⊢ f = g
    dsimp at thisα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:(fun x => f x) = fun x => g x⊢ f = g
    exact thisα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g x⊢ extApp (Quot.mk extEq f) = extApp (Quot.mk extEq g)
  suffices Quot.mk extEq f = Quot.mk extEq g byα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:Quot.mk extEq f = Quot.mk extEq g⊢ extApp (Quot.mk extEq f) = extApp (Quot.mk extEq g)
    apply congrArgα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g xthis:Quot.mk extEq f = Quot.mk extEq g⊢ Quot.mk extEq f = Quot.mk extEq g
    exact thisα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g x⊢ Quot.mk extEq f = Quot.mk extEq g
  apply Quot.soundα:Sort uβ:α → Sort vf:(x : α) → β xg:(x : α) → β xh:∀ (x : α), f x = g x⊢ extEq f g
  exact hAll goals completed! 🐙

4.5.7. 壁球类型🔗

Squash 类型是通过关联所有元素的关系得出的商，将其转换为 subsingleton。换句话说，如果 α 是有人居住的，那么 Squash α 就有一个元素，如果 α 无人居住，那么 Squash α 也是无人居住的。 Nonempty α 是一个命题，声明 α 已被占用，因此在运行时由虚拟值表示，而 Squash α 与 Squash α 不同，Squash α 是与 α 表示相同的类型。由于Squash α与α在同一个宇宙中，因此它不受命题计算数据的限制。

def

Squash.{u} (α : Sort u) : Sort u
Squash.{u} (α : Sort u) : Sort u

The quotient of α by the universal relation. The elements of Squash α are those of α, but all of them are equal and cannot be distinguished.

Squash α is a Subsingleton: it is empty if α is empty, otherwise it has just one element. It is the “universal Subsingleton” mapped from α.

Nonempty α also has these properties. It is a proposition, which means that its elements (i.e. proofs) are erased from compiled code and represented by a dummy value. Squash α is a Type u, and its representation in compiled code is identical to that of α.

Consequently, Squash.lift may extract an α value into any subsingleton type β, while Nonempty.rec can only do the same when β is a proposition.

Squash is defined in terms of Quotient, so Squash can be used when a Quotient argument is expected.

def

Squash.mk.{u} {α : Sort u} (x : α) : Squash α
Squash.mk.{u} {α : Sort u} (x : α) :
  Squash α

Places a value into its squash type, in which it cannot be distinguished from any other.

def

Squash.lift.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} [Subsingleton β]
  (s : Squash α) (f : α → β) : β
Squash.lift.{u_1, u_2} {α : Sort u_1}
  {β : Sort u_2} [Subsingleton β]
  (s : Squash α) (f : α → β) : β

Extracts a squashed value into any subsingleton type.

If β is a subsingleton, a function α → β cannot distinguish between elements of α and thus automatically respects the universal relation that Squash quotients with.

theorem

Squash.ind.{u} {α : Sort u} {motive : Squash α → Prop}
  (h : ∀ (a : α), motive (Squash.mk a)) (q : Squash α) : motive q
Squash.ind.{u} {α : Sort u}
  {motive : Squash α → Prop}
  (h : ∀ (a : α), motive (Squash.mk a))
  (q : Squash α) : motive q

A reasoning principle that allows proofs about squashed types to assume that all values are constructed with Squash.mk.

4.1.	功能
4.2.	提案
4.3.	宇宙
4.4.	归纳类型
4.5.	商数