Learning Quotients in Lean 4

Identifying elements that a binary relation treats as "the same" is called taking a quotient. A familiar example is clock time: two times that are 24 hours apart are treated as the same time. This can be thought of as identifying values under the relation "have the same remainder when divided by 24".

The set of terms that an equivalence relation treats as equal to a given term is called the equivalence class of that term. In this article, based on "ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発", we look at how Lean handles quotients.

Creating equivalence classes (Quotient.mk)

In Lean, given a type α and an equivalence relation sr : Setoid α on it, Quotient.mk sr lets us obtain the equivalence class of a term.

variable {α : Type} (sr : Setoid α)
#check (Quotient.mk sr : α → Quotient sr)

Every term of the original type α belongs to exactly one equivalence class; no term can belong to more than one. In other words, the set of α is partitioned into a disjoint union of equivalence classes. The set of all these equivalence classes is the quotient of α by the equivalence relation sr : Setoid α, and is represented as Quotient sr.

Example: remainder mod 3

Let's take the remainder mod 3 as an example.

• α is the integer type Int
• The Setoid is the relation "have the same remainder when divided by 3", i.e. \( a \equiv b \pmod 3 \)
• The quotient type is ZMod 3

With this, the infinite set of integers Int is neatly partitioned into the following three equivalence classes (a disjoint union).

\[ [0] = \{ \dots, -3, 0, 3, 6, \dots \} \] \[ [1] = \{ \dots, -2, 1, 4, 7, \dots \} \] \[ [2] = \{ \dots, -1, 2, 5, 8, \dots \} \]

Taking a representative (Quotient.inductionOn)

Picking out a single element from an equivalence class is called "taking a representative". This can be done with Quotient.inductionOn. In the example below, notice how we obtain an element x of α from the equivalence class a : Quotient sr.

example (a : Quotient sr) : True := by
  induction a using Quotient.inductionOn with
  | h x =>
      guard_hyp x : α
      trivial

Lifting a function to the quotient (Quotient.lift)

Quotient.lift lifts a function defined on the base type to a function on the quotient type. This requires the function to be compatible with the equivalence relation.

In the example below, the function f maps α to β. The hypothesis h guarantees that whenever two terms x, y of α are equivalent, f gives the same result for both. Under this condition, Quotient.lift f h lets us lift the domain of f to the quotient type Quotient sr.

section
  variable {α β : Type} (sr : Setoid α)
  variable (f : α → β) (h : ∀ x y, x ≈ y → f x = f y)

  #check (Quotient.lift f h : Quotient sr → β)

  example : ∀ x, (Quotient.lift f h) (Quotient.mk sr x) = f x := by
    intro x
    rfl
end

Applying this to the earlier remainder-mod-3 example gives the following.

• α is the integer type Int
• The Setoid is the relation "have the same remainder when divided by 3"
• The quotient type is \( \mathbb{Z}/3\mathbb{Z} = \{[0], [1], [2]\} \)
• f is Int → Bool, returning true when the argument is a multiple of 3 (\( f(x) = (x \bmod 3 = 0) \))
• h guarantees that if x and y are equivalent they have the same remainder mod 3, so the "is a multiple of 3" check always gives the same result

Quotient.lift f h changes the domain of f to the quotient type \( \mathbb{Z}/3\mathbb{Z} = \{[0], [1], [2]\} \). Since h guarantees the result doesn't change, this lift is valid.

Equivalent implies equal (Quotient.sound)

Quotient.sound is the theorem stating that if an equivalence relation holds between two terms, they are equal as elements of the quotient type. "sound" is short for soundness.

section
  variable {α : Type} (sr : Setoid α)
  variable (x y : α) (h : x ≈ y)

  example : Quotient.mk sr x = Quotient.mk sr y := by
    -- h : x ≈ y ⊢ Quotient.mk sr x = Quotient.mk sr y
    apply Quotient.sound -- h : x ≈ y ⊢ x ≈ y
    exact h
end

Equal implies equivalent (Quotient.exact)

Quotient.exact is the converse of Quotient.sound. It states that if two terms are equal after converting to the quotient type, the original terms are equivalent.

section
  variable {α : Type} (sr : Setoid α)
  variable (x y : α)

  example (h : Quotient.mk sr x = Quotient.mk sr y) : x ≈ y := by
    exact Quotient.exact h
end

The code for this article is available in the following repository.

https://github.com/ringring-creator/LearnLean