import FormalLab.Mathematics.FunctionProperties

/-!
# 第22章：関係・同値・順序

大小、割り切り、同じ剰余を持つことは、二つの値の間に成り立つ主張です。関数と違い、
一つの入力に相手が一つだけ決まる必要はありません。この自由さのため、関係そのものと、
反射性・対称性・推移性など関係が満たす法則を分けなければなりません。

本章では二項関係を二引数述語として表し、同値関係と半順序を法則の異なる組として構成します。
特に対称性と反対称性を具体例で分け、関数の核が同値関係になることを証明します。関係は
帰納法の整礎性、商、書換え、順序による不動点へ続く基盤です。

## 二つの対象の間に成り立つ命題を束ねる

集合 `A` 上の二項関係は通常 `R ⊆ A × A` と書き、`(x,y) ∈ R` を `x R y` または
`R(x,y)` と略記します。型理論では関係を二引数の述語として表せます。

`r : α → α → Prop` は、二値 `x y : α` から命題 `r x y` を作ります。関数が各入力に
出力を一つ与えるのに対し、関係は二値の間で命題が成り立つかを述べます。一つの `x` が
多数の `y` と関係しても、どの `y` とも関係しなくても構いません。したがって関係は一般に
値を計算する関数ではありません。

* 対称性：`r x y → r y x`
* 反対称性：`r x y → r y x → x = y`

標準記法では、主な法則を次の閉じた命題として定義します。

$$
\begin{aligned}
\mathsf{Refl}(R)&\;\Longleftrightarrow\;\forall x.\,R(x,x),\\
\mathsf{Sym}(R)&\;\Longleftrightarrow\;\forall x,y.\,R(x,y)\to R(y,x),\\
\mathsf{Trans}(R)&\;\Longleftrightarrow\;\forall x,y,z.\,R(x,y)\to R(y,z)\to R(x,z),\\
\mathsf{AntiSym}(R)&\;\Longleftrightarrow\;\forall x,y.\,R(x,y)\to R(y,x)\to x=y.
\end{aligned}
$$

名前は似ていますが、前者は向きを反転し、後者は両方向が成り立つ場合を等式へ潰します。
たとえば等式は対称かつ反対称ですが、整数上の「差が偶数」は対称でも反対称ではありません。
自然数の `≤` は反対称ですが対称ではありません。


-/

namespace FormalLab.Mathematics.Relations

universe u v

open FormalLab.Mathematics.FunctionProperties

/-! ## 関係と四つの基本性質を定義する -/

/-- 型 `α` 上の二項関係です。 -/
def Rel (α : Type u) :=
  α → α → Prop

def IsReflexive {α : Type u} (r : Rel α) : Prop :=
  ∀ x, r x x

def IsSymmetric {α : Type u} (r : Rel α) : Prop :=
  ∀ ⦃x y⦄, r x y → r y x

def IsTransitive {α : Type u} (r : Rel α) : Prop :=
  ∀ ⦃x y z⦄, r x y → r y z → r x z

def IsAntisymmetric {α : Type u} (r : Rel α) : Prop :=
  ∀ ⦃x y⦄, r x y → r y x → x = y

/-- 任意の二要素が少なくとも一方向に比較できるという全域性です。 -/
def IsTotal {α : Type u} (r : Rel α) : Prop :=
  ∀ x y, r x y ∨ r y x

/-!
四性質は独立した問いです。反射性は一点、対称性と反対称性は二点、推移性は三点について
量化します。性質名から雰囲気で証明せず、量化子と含意の結論を毎回展開して読みます。
-/

/-! ## 性質を束ねる -/

/-- 反射・対称・推移を満たす関係です。 -/
structure IsEquivalence {α : Type u} (r : Rel α) : Prop where
  reflexive : IsReflexive r
  symmetric : IsSymmetric r
  transitive : IsTransitive r

/-- 反射・反対称・推移を満たす関係です。 -/
structure IsPartialOrder {α : Type u} (r : Rel α) : Prop where
  reflexive : IsReflexive r
  antisymmetric : IsAntisymmetric r
  transitive : IsTransitive r

/-- 半順序に全域性を加えた全順序です。 -/
structure IsLinearOrder {α : Type u} (r : Rel α) extends IsPartialOrder r where
  total : IsTotal r

/-- 自然数の `≤` は半順序です。実際には全域性も持ちます。 -/
theorem natLeIsPartialOrder : IsPartialOrder (fun x y : Nat => x ≤ y) where
  reflexive := fun x => Nat.le_refl x
  antisymmetric := by
    intro x y hxy hyx
    exact Nat.le_antisymm hxy hyx
  transitive := by
    intro x y z hxy hyz
    exact Nat.le_trans hxy hyz

theorem natLeIsTotal : IsTotal (fun x y : Nat => x ≤ y) :=
  fun x y => Nat.le_total x y

/-- 自然数の `≤` は全順序です。 -/
theorem natLeIsLinearOrder : IsLinearOrder (fun x y : Nat => x ≤ y) where
  toIsPartialOrder := natLeIsPartialOrder
  total := natLeIsTotal

/-!
半順序は「すべての二要素を比較できる」とは要求しません。全域性を加えたものが全順序です。
たとえば集合包含は半順序ですが、互いに包含しない二集合があるため一般には全順序では
ありません。必要な法則を構造体のフィールドとして列挙することで、名称の違いを定義へ
還元できます。
-/

/-! ## 等式と関数の核は同値関係になる -/

def EqualityRelation (α : Type u) : Rel α :=
  fun x y => x = y

theorem equalityIsEquivalence (α : Type u) : IsEquivalence (EqualityRelation α) where
  reflexive := fun _ => rfl
  symmetric := fun {_ _} h => h.symm
  transitive := fun {_ _ _} hxy hyz => hxy.trans hyz

/-- `f` で同じ値へ写る二入力を関係づけます。 -/
def Kernel {α : Type u} {β : Type v} (f : α → β) : Rel α :=
  fun x y => f x = f y

theorem kernelIsEquivalence {α : Type u} {β : Type v} (f : α → β) :
    IsEquivalence (Kernel f) where
  reflexive := fun _ => rfl
  symmetric := fun {_ _} h => h.symm
  transitive := fun {_ _ _} hxy hyz => hxy.trans hyz

/-!
核 `Kernel f` は、`f` が見分けられない入力を同じ類へまとめます。たとえば
`fun n : Nat => n % 2` の核は、同じ偶奇を持つ自然数を関係づけます。`1` と `3` は
等しくありませんが、どちらも剰余 `1` へ写るので核では関係します。
-/

example : Kernel (fun n : Nat => n % 2) 1 3 := by
  change 1 % 2 = 3 % 2
  decide
example : (1 : Nat) ≠ 3 := by decide

/-- 単射なら、核で関係する二入力は命題的にも等しくなります。 -/
theorem kernelOfInjectiveImpliesEquality {α : Type u} {β : Type v}
    {f : α → β} (injective : IsInjective f) {x y : α} : Kernel f x y → x = y :=
  by
    intro sameImage
    apply injective
    exact sameImage

/-- 単射の核関係は、元の型の等式とちょうど一致します。 -/
theorem kernel_iff_eq_of_injective {α : Type u} {β : Type v}
    {f : α → β} (injective : IsInjective f) {x y : α} : Kernel f x y ↔ x = y := by
  constructor
  · exact kernelOfInjectiveImpliesEquality injective
  · intro equality
    cases equality
    rfl

/-!
## 関係の法則を取り違えない

同値関係は等式そのものではありません。商型を作る前は、`r x y` の証明があっても
`x = y` とは限りません。また単射 `f` の核は等式と同じ関係になりますが、一般の関数の
核は異なる入力を結び得ます。

同値関係から実際に同値類を一つの値として扱うには、代表元の選択に依存しない商構成が
必要です。「商型とwell-definedness」で明示的に商を構成するまでは、`r x y` と `x = y` を置き換えません。

## 要点

* 二項関係は二値から命題を作り、一意の出力を選ぶ必要はない。
* 対称性は向きを反転し、反対称性は両方向の成立から等式を得る。
* 同値関係は反射・対称・推移、半順序は反射・反対称・推移を束ねる。
* 全域性は半順序とは別の性質であり、加えると全順序になる。
* 関数の核は、その関数が同じ出力へ潰す入力を同値とみなす。

## 研究史と文献案内

Fregeの1879年の論理体系は多項関係を形式的推論の対象に含めました [FRE79]。その記法と
現代の `R(x,y)` は同じではありません。同値関係は商、順序関係は比較構造の基礎となり、
圏論ではさらに対象間の射へ視点が移ります。本章では関係の集合論的・述語的表現を扱い、
関係代数や順序理論の一般理論までは仮定しません。

## 問題

### 対称性と反対称性を反例で分ける

二つの性質を量化記号を省かずに展開し、仮定と結論を比較せよ。自然数の `≤`、等式、空関係、
常に真な関係を行とする表を作る。各関係について反射性・対称性・反対称性・推移性の真偽を記し、
偽の場合には最小限の具体的反例を添える。

とくに「対称でない」ことと「反対称である」ことが両立する例を説明せよ。名称の類似ではなく、
含意の向きと等式が現れる位置から両者を再構成できれば完了である。

### 関数の核関係を証明する

`Kernel f x y :↔ f x = f y` から反射性・対称性・推移性を証明し、それぞれが等式のどの法則に
由来するか注記せよ。さらに `f` が単射なら `Kernel f x y ↔ x = y` をLeanで示し、逆向きには
単射を必要としない理由を述べる。

定数関数の核関係も計算し、単射性を失うと異なる入力の区別がどのように消えるか確認する。
これにより核が関数によって観測できない差を表すことを、自分の例で説明せよ。

### 同値関係から商へ進む理由を説明する

偶奇が等しいという自然数上の関係を定義し、同値関係であることを確認せよ。しかし、関係が
成り立つ二数をLeanの等式で置換してはならない。`1` と `3` を使い、その誤った置換が何を
壊すか示すこと。

同値関係は「等しいと扱いたい」という規約を与え、商はその規約を新しい等式へ反映する構成で
ある。この二段階を、関係、同値類、代表元不変な関数という三語を用いて説明できれば完了である。
-/

end FormalLab.Mathematics.Relations