import FormalLab.Mathematics.Relations

/-!
# 第39章：商型とwell-definedness

整数を偶数と奇数の二種類だけに分けるとき、同じ偶奇を持つ異なる数を一つの値として扱います。
しかし商の値はどの代表元を選んだかを隠すため、商から関数を定義するには、代表元を変えても
結果が変わらないことを証明しなければなりません。これがwell-definednessの内容です。

本章では同値関係を `Setoid` に束ね、標準射影と `Quotient.lift` を使って偶奇の商から関数を
定義します。代表元に依存する定義が拒否される理由を型から読み、集合論的な同値類、
命題的等式、商の普遍性を区別します。

## 代表元の違いを忘れて同値類を作る

集合または型 `A` と同値関係 `∼` から商を `A/∼` と書き、標準射影を
`q : A → A/∼`, `a ↦ [a]` と書きます。商からの関数 `\bar f : A/∼ → B` を定めるには、
元の関数 `f : A → B` が

$$
\forall a,a':A.\;a\sim a'\to f(a)=f(a')
$$

を満たす必要があります。この代表元不変性がwell-definednessです。

商は代表元を一つ選んで保存するだけのデータ構造ではありません。標準射影
`Quotient.mk` は各代表元を同値類へ送り、`Quotient.sound` は関係する代表元の像が等しい
ことを保証します。利用側が代表元の偶然へ依存できないよう、商から関数を定義する際に
不変性の証明を要求します。


-/

namespace FormalLab.TypeTheory.Quotients

universe u v

/-! ## 商の一般的な除去原理 -/

/-- 関係する代表元で値が一致する関数を、商からの関数へ降ろします。 -/
def descend {α : Type u} {β : Type v} (setoid : Setoid α) (f : α → β)
    (respects : ∀ a b, setoid.r a b → f a = f b) : Quotient setoid → β :=
  Quotient.lift f respects

/-- 下降写像を標準射影へ適用すると、代表元上の元の関数へ計算されます。 -/
theorem descend_mk {α : Type u} {β : Type v} (setoid : Setoid α) (f : α → β)
    (respects : ∀ a b, setoid.r a b → f a = f b) (a : α) :
    descend setoid f respects (Quotient.mk setoid a) = f a :=
  rfl

/-!
数式では、標準射影を $q:A\to A/{\sim}$、下降写像を
$\bar f:A/{\sim}\to B$ として、次の可換条件で特徴づけます。

$$
\bar f\circ q=f.
$$

可換性だけでなく、`respects` が下降写像を構成できるための条件です。`descend_mk` は、この三角形の
可換性が代表元上で計算規則として成立することを表します。
-/

/-! ## 偶奇を同一視する関係を定義する -/

/-- 二自然数を、2で割った余りが等しいとき関係づけます。 -/
def SameParity (m n : Nat) : Prop :=
  m % 2 = n % 2

/-- 偶奇関係と同値関係の三法則を束ねます。 -/
def paritySetoid : Setoid Nat where
  r := SameParity
  iseqv := {
    refl := fun _ => rfl
    symm := fun h => h.symm
    trans := fun hmn hnk => hmn.trans hnk
  }

/-- 自然数を偶奇で割った商型です。 -/
def ParityClass :=
  Quotient paritySetoid

/-- 代表元をその同値類へ送る標準射影です。 -/
def parityClass (n : Nat) : ParityClass :=
  Quotient.mk paritySetoid n

/-- `0` と `2` は異なる代表元ですが、同じ商の値です。 -/
theorem zeroAndTwoAgree : parityClass 0 = parityClass 2 := by
  apply Quotient.sound
  rfl

/-- `1` と `3` も同じ奇数類を表します。 -/
theorem oneAndThreeAgree : parityClass 1 = parityClass 3 := by
  apply Quotient.sound
  rfl

/-!
`Quotient.sound` の入力は元の型の等式ではなく、setoidの関係です。実際 `0 ≠ 2` ですが、
`SameParity 0 2` なので商の中では等しくなります。商は元の等式を証明するのではなく、
新しい型の等式がどの関係によって生成されるかを定めます。
-/

/-! ## 商から出る関数は代表元の変更で値が変わってはならない -/

/-- 各偶奇類を余り `0` または `1` へ送る、代表元によらない関数です。 -/
def parityValue : ParityClass → Nat :=
  descend paritySetoid (fun n => n % 2) (fun _ _ sameParity => sameParity)

#eval parityValue (parityClass 5)

theorem parityValueOfRepresentative (n : Nat) :
    parityValue (parityClass n) = n % 2 :=
  rfl

/-!
`Quotient.lift` の第二引数は、同値な代表元で元の関数の値が等しいという証明です。
この条件がwell-definednessです。代表元そのものを返す関数はこの条件を満たしません。

定義の形を一般化すると、元の関数 `f : α → β` が `r a b → f a = f b` を満たすとき、
一意な意味で商から `β` への関数へ降ります。これは商の普遍性の計算的な姿です。後の
普遍性の章では、「構成から出る写像は、必要な整合条件を満たすデータと対応する」という
共通パターンとして読み直します。

well-definednessに失敗する例は `fun n : Nat => n` です。`0` と `2` は同じ偶奇類なのに
出力は等しくないため、この関数を `ParityClass → Nat` へ降ろすことはできません。

## 商が許す定義

部分型は条件を満たす値だけを**選び**、元の値を区別したまま保持します。商型は関係する
値を**同一視**します。制約を加える操作と区別を減らす操作であり、方向が異なります。

Leanの商は、各同値類から標準的な代表元を計算して返す操作を一般には提供しません。そのような
選択は追加構造や選択原理を必要とし、しかも代表元不変な観察とは別物です。

## 要点

* setoidは関係と、その関係が同値関係である証明を束ねる。
* 標準射影は代表元を商へ送り、関係する代表元を商の等式として同一視する。
* 商から関数を定義するには、元の関数が代表元の変更で値を変えない証明が必要である。
* 部分型は許す値を減らし、商型は値同士の区別を減らす。

## 研究史と文献案内

剰余類、整数・有理数の構成、同値類による対象形成は近代数学の多くの領域で現れます。
型理論では商をprimitiveに持つか、setoidを使うか、higher inductive typeを使うかで
理論が異なります。Leanは商をkernelで支持し、命題的等式を粗くします [LEAN-REF]。
Martin-Löf型理論のsetoid的扱い [ML84] とLeanの `Quotient` を同一視しません。

## 問題

### 関係を新しい等式へ送る

`paritySetoid` の関係成分と反射・対称・推移の証明成分を特定せよ。そのうえで
`parityClass 1 = parityClass 3` を `Quotient.sound` から再構成し、元の自然数の等式ではなく、
商型上の等式が得られたことを説明する。

`0` と `2`、`1` と `3` についても同じ確認を行い、同値類により保持される情報と失われる情報を
列挙せよ。代表元と同値類を同一視しないことが到達条件である。

### 代表元に依存しない関数を設計する

偶奇類を `Bool` へ送る関数を、代表元上の関数と関係を保存する証明から構成せよ。
`parityValue (parityClass 8)` の簡約を追い、商からの除去がどの計算規則を与えるかを確認する。

対照として代表元そのものを返す関数を定義しようとし、`0` と `2` が同じ類に属するため
well-definedにならないことを示せ。関数が同値な入力へ同じ出力を返すという条件を、数式と
Leanが要求する証明引数の双方で書くこと。

### 部分型と商型が捨てるものを対照する

正の自然数の部分型と、偶奇による自然数の商を比較せよ。前者は条件を満たす元だけを残すが元同士の
区別は保ち、後者は全ての元を受け入れる代わりに一部の区別を消す。この差を包含と射影の向きから
説明する。

同じ基礎型について部分型と商型を一つずつ独自に設計し、許される構成子と除去原理を比較せよ。
「条件を付ける」と「同一視する」を型の表現から判別できれば完了である。
-/

end FormalLab.TypeTheory.Quotients