Lean 4で学ぶ商（Quotient）

ある二項関係によって同じとみなされるものを同一視することを、「商を取る」と呼びます。身近な例で言うと、時刻は24時間経つと同じ時刻として扱われます。これは「24で割った余りが等しい」という関係で同一視していると考えることができます。

同値関係によって同じとみなされる項からなる集合のことを、その項の同値類と呼びます。今回は「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」を参考に、Leanにおける商の扱い方を学びます。

同値類を作る（Quotient.mk）

Leanでは、型αとα上の同値関係 sr : Setoid α が与えられたとき、Quotient.mk sr によって項の同値類を取得できます。

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

元の型αに属する全ての項は、必ずどれか1つの同値類に属します。複数の同値類に同時に属する項は存在しません。つまり型αの集合は、同値類によって直和に分割されることになります。この同値類全体の集合が、α上の同値関係 sr : Setoid α による商であり、Quotient sr として表されます。

3で割った余りの例

3で割った余りを例に考えます。

• αは整数型のIntです
• Setoidは「3で割った余りが等しい」という関係、つまり \( a \equiv b \pmod 3 \) です
• 商型QuotientはZMod 3になります

この時、無限に存在する整数Int全体は、以下の3つの同値類（直和）にきれいに分割されます。

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

代表元を取る（Quotient.inductionOn）

同値類から1つの要素を選び出すことを「代表元を取る」と呼びます。この操作は Quotient.inductionOn で実現できます。以下の例では、同値類 a : Quotient sr からαの要素 x を取得できていることに着目してください。

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

関数を商型へ持ち上げる（Quotient.lift）

Quotient.liftは、基底型上で定義された関数を商型上の関数へ持ち上げます。ただし、持ち上げる関数が同値関係と整合的であることが条件になります。

以下の例では、関数fがαからβへの変換を行います。そして、任意のαの項x, yが同値であれば、fの結果も等しいことが仮定hによって保証されています。この条件のもとで Quotient.lift f h により、fの定義域を商型 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

先ほどの3で割った余りの例に当てはめると、以下のようになります。

• αは整数型のInt
• Setoidは「3で割った余りが等しい」という関係
• 商型は \( \mathbb{Z}/3\mathbb{Z} = \{[0], [1], [2]\} \)
• fはInt → Boolで、3の倍数ならばtrueを返す関数（\( f(x) = (x \bmod 3 = 0) \)）
• hはx, yが同値であれば3で割った余りが等しいため、3の倍数かどうかの判定が必ず同じ結果になることを保証しています

Quotient.lift f hにより、fの定義域は商型 \( \mathbb{Z}/3\mathbb{Z} = \{[0], [1], [2]\} \) に変更されます。hによって結果が変わらないことが保証されているため、この持ち上げは問題なく行えます。

同値ならば等しい（Quotient.sound）

Quotient.soundは、同値関係が成り立つならば、商型として等しいとみなせることを示す定理です。soundは健全性（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

等しいならば同値（Quotient.exact）

Quotient.exactはQuotient.soundの逆方向にあたる定理です。商型に変換した結果が等しいならば、元の項が同値であることを示します。

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

本記事のコードは以下のリポジトリにあります。

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