import FormalLab.Foundation.Functions

/-!
# 第9章：等式・代入・外延性・一意存在

`(fun x => x) 2` と `2` は計算すれば同じ式になります。一方、変数 `x` と `y` が等しいことは、
通常は仮定または証明を必要とします。さらに関数の等しさは、全ての入力で結果が等しいという
観察から導く外延性を要します。「同じ」という語は、ここで少なくとも三つの仕事をしています。

本章では定義的等しさと命題的等式を分け、反射性から対称性・推移性・代入・合同性を導きます。
続いて関数外延性と命題外延性が追加する原理を明示し、存在量化へ等式条件を加えて一意存在を
定義します。これは商、普遍性、圏論で一意性を読む準備になります。

## 等しい対象をあらゆる性質の中で置き換える

型理論の論文では少なくとも二種類の等しさを区別します。

$$
\Gamma\vdash t\equiv u:A
\qquad\text{と}\qquad
\Gamma\vdash p:t={}_A u
$$

は、それぞれ定義展開・簡約による判断的等しさと、型 $A$ の内部にある等式命題の証明を表します。

**定義的等しさ**は、定義展開と計算で同じ式になることです。型検査器自身が判定に使い、
新しい仮定を要求しません。これに対し `x = y : Prop` は**命題的等しさ**で、その型の
証明項を要求します。`rfl` は `x = x` の基本構成子です。両辺が定義的に同じ式へ計算
される場合にも `rfl` を使えます。

この区別は「明らかな等式」と「難しい等式」の差ではありません。前者は型検査の一部で、
後者は型の内部に現れるデータです。命題的等式を仮定として受け取れば、述語や関数の中へ
運べます。この**代入可能性**が、等式を単なる二項関係以上のものにしています。

命題的等式の形成、反射性、代入、計算は次の規則でまとめられます。$P:A\to\mathsf{Prop}$ は
等しい項を入れ替える文脈です。

$$
\frac{\Gamma\vdash x:A\qquad\Gamma\vdash y:A}
     {\Gamma\vdash x={}_A y:\mathsf{Prop}}
\qquad
\frac{\Gamma\vdash x:A}{\Gamma\vdash \mathsf{refl}_x:x={}_A x}
$$

$$
\frac{\Gamma\vdash h:x={}_A y\qquad\Gamma\vdash p:P(x)}
     {\Gamma\vdash \mathsf{transport}_P(h,p):P(y)},
\qquad
\mathsf{transport}_P(\mathsf{refl}_x,p)\equiv p.
$$

最後の式は反射性に沿った移送が何もしないという計算規則です。対称性・推移性・合同性は、
この除去と計算から導出する性質であり、等式へ別々に追加する原始規則ではありません。


-/

namespace FormalLab.Logic.Equality

universe u v

/-!
## 等式を作る・反転する・つなぐ

Leanの `Eq` は、概略的には次のように反射性だけから生成される帰納族です。

```lean
inductive Eq {α : Sort u} (a : α) : α → Prop where
  | refl : Eq a a
```

右辺が変化する型族になっているため、`h : x = y` を除去するときは `y` を `x` に
置き換えてよいことが導かれます。対称性や推移性は追加の構成子ではなく、この除去原理
から証明できる性質です。
-/

/-- 任意の項は自分自身と等しいという反射性です。 -/
theorem reflexive {α : Type u} (x : α) : x = x :=
  rfl

/-- 等式の向きを反転します。 -/
theorem symmetric {α : Type u} {x y : α} (h : x = y) : y = x :=
  h.symm

/-- 二つの等式を中間項でつなぎます。 -/
theorem transitive {α : Type u} {x y z : α} (hxy : x = y) (hyz : y = z) : x = z :=
  hxy.trans hyz

/-!
## 計算で閉じる等式と、仮定を使う等式

次の左辺は関数適用と自然数の計算を進めると右辺になるので、証明は `rfl` です。これは
「`rfl` が算術定理を知っている」のではなく、両辺が同じ正規形へ計算されるからです。
-/

example : (fun n : Nat => n + 1) 2 = 3 :=
  rfl

/-!
変数 `x` と `y` は計算だけでは一致しません。`hxy : x = y` が与えられて初めて、
`x + 1` の中の `x` を `y` へ置換できます。`rw [hxy]` はこの等式除去を使うための
タクティク記法です。
-/

example {x y : Nat} (hxy : x = y) : x + 1 = y + 1 := by
  rw [hxy]

/-!
## 代入と合同性

`p : α → Prop` を、穴に値を入れると命題になる**文脈**だと考えます。`hxy : x = y` が
あれば、穴へ `x` を入れて得た証明 `p x` を、`y` を入れた側の `p y` へ運べます。
記法 `hxy ▸ proof` の三角形は、等式に沿った置換を表します。向きが逆なら `hxy.symm`
を使います。
-/

/-- `x = y` を使い、`x` に依存する命題の証明を `y` 側へ運びます。 -/
theorem substitute {α : Type u} (p : α → Prop) {x y : α}
    (hxy : x = y) (proof : p x) : p y :=
  hxy ▸ proof

/-- 関数は等しい入力を等しい出力へ送ります。 -/
theorem congruence {α : Type u} {β : Type v} (f : α → β)
    {x y : α} (hxy : x = y) : f x = f y :=
  congrArg f hxy

/-- 同じ関数同士が等しければ、同じ引数へ適用した結果も等しくなります。 -/
theorem congruenceOfFunctions {α : Type u} {β : Type v} {f g : α → β}
    (hfg : f = g) (x : α) : f x = g x :=
  congrFun hfg x

/-- 関数と引数をそれぞれ等しいものへ替えても、適用結果は等しい。 -/
theorem congruenceOfApplication {α : Type u} {β : Type v} {f g : α → β}
    {x y : α} (hfg : f = g) (hxy : x = y) : f x = g y :=
  (congrFun hfg x).trans (congrArg g hxy)

/-!
`congrArg` は「等しい入力を同じ関数へ」、`congrFun` は「等しい関数を同じ入力へ」運びます。
両方を組み合わせれば、関数と引数がそれぞれ等しい場合も扱えます。ただし合同性は一方向
です。`f x = f y` から `x = y` が戻るには、後に導入する単射性が必要です。

## 外延性：観察結果から対象の等しさへ

合同性は関数の等しさから各点の等しさを得ます。**関数外延性**は逆向きに、すべての入力
で観察結果が等しければ関数自体も等しいと述べます。この結論は一般に計算だけでは得られ
ないため、`rfl` ではなく `funext` を使います。
-/


/-- 全入力で値が等しい関数は等しい、という関数外延性です。 -/
theorem functionExtensionality {α : Type u} {β : Type v} {f g : α → β}
    (pointwise : ∀ x, f x = g x) : f = g := by
  funext x
  exact pointwise x

/-- 論理的に同値な二命題は命題として等しい、という命題外延性です。 -/
theorem propositionExtensionality {P Q : Prop} (bothWays : P ↔ Q) : P = Q :=
  propext bothWays

/-!
`P ↔ Q` と `P = Q` も同じ構文ではありません。前者は二方向の含意、後者は命題を項と
して見た等式です。`propext` は論理的同値から命題の等しさへ進む外延性原理です。
-/

open FormalLab.Foundation.Functions

/-- 合成の結合則は、各入力で両辺を計算して関数外延性を使います。 -/
theorem composeAssociative {α β γ δ : Type}
    (h : γ → δ) (g : β → γ) (f : α → β) :
    compose h (compose g f) = compose (compose h g) f := by
  funext x
  rfl

/-!
この証明は二つの推論から成ります。

1. `funext x` で、関数の等式を任意の入力 `x` における値の等式へ変える。
2. 両側の合成を展開すると同じ式になるので、`rfl` で閉じる。

つまり結合則全体は定義的等しさではありませんが、外延性で観察点へ移った後の等式は
計算で成立します。外延性を使う箇所と定義展開だけで閉じる箇所が、証明項にも順に現れます。

## 存在に等式を加えて一意性を述べる

単なる `∃ x, p x` は、条件を満たす項を一つ提供しますが、別の項が同じ条件を満たす
可能性を排除しません。一意存在は、存在証人に加えて、任意の別候補がその証人と等しい
ことを要求します。

$$
\exists!x:A.\,P(x)
\quad\Longleftrightarrow\quad
\exists x:A.\,P(x)\land\forall y:A.\,P(y)\to y=x.
$$
-/


/-- 述語 `p` を満たす項が存在し、満たす項が全てその証人と等しいという定義です。 -/
def ExistsExactlyOne {α : Type u} (p : α → Prop) : Prop :=
  ∃ x, p x ∧ ∀ y, p y → y = x

/-- `0` は `n = 0` を満たす唯一の自然数です。 -/
theorem existsUniqueZero : ExistsExactlyOne (fun n : Nat => n = 0) :=
  ⟨0, rfl, fun _ proof => proof⟩

/-!
`existsUniqueZero` の三成分を順に読むと、証人は `0`、存在条件 `0 = 0` は `rfl`、別候補
`y` の条件 `proof : y = 0` はそのまま必要な一意性 `y = 0` になります。一意性の等式を
`y = x` と置くか `x = y` と置くかは慣習の差で、必要なら対称性で変換できます。

## 三種類の「同じ」を混同しない

`funext` と `propext` の結論は定義的等しさではありません。Leanの論理が提供する
外延性原理を明示的に使っています。また `f x = f y` から `x = y` は一般には戻せず、
戻せる関数を「数学的関数とその性質」で単射と定義します。

この章の `Eq` を、型の同値や同型と混同してはいけません。二つの型の間に往復する関数が
あっても、それだけで型が命題的に等しいとは限りません。型同士をいつ同一視できるかは、
より強い原理や後の構造の議論に関わります。

Leanの等式証拠は `Prop` に属するため、同じ等式を示す二証拠は証明無関連性により等しいと扱われます。
一般の同一性型理論ではこの一意性は自動的ではありません。端点の置換に使えることから、経路間の
高次情報まで同じだとは結論しません。

## 要点

* 定義的等しさはkernelが計算と展開で判定し、証明項を追加しない。
* 命題的等式 `x = y` は型内部の命題で、`rfl` と等式除去から扱う。
* 代入は、`x` に依存する性質を等式に沿って `y` 側へ運ぶ。
* 合同性は対象の等しさから観察結果の等しさへ、外延性は十分な観察結果から対象の等しさへ進む。
* 一意存在は、証人・存在条件・他の候補との等式の三成分を持つ。

## 研究史と文献案内

Fregeの論理にも同一性は含まれますが [FRE79]、型に依存する同一性型とは役割が異なります。
Martin-Löf型理論は判断的等しさと同一性型を区別して意味説明を与えます [ML84]。Leanの
`Eq` は反射性を唯一の構成子に持つ帰納族ですが、Leanのkernel規則をMartin-Löf型理論の
特定版と同一視しません。現行の `Eq`、`propext`、商による等式生成は [LEAN-REF] を参照します。

## 問題

### 等式除去を置き換えの原理として展開する

`h : x = y` から `y = x` を `cases h` と `rfl` だけで証明し、`cases h` の前後で文脈と目標がどう変わったかを書いてください。
この変化を「等式を場合分けした」という表面的な説明で済ませず、任意の述語 `p : A → Prop` に対して `p x` から `p y` へ移送できる原理の特殊例として述べます。

`x = y` と `f = g` から `f x = g y` を二通り証明します。一方は項の等式を先に消去し、他方は関数の等式を先に消去します。
中間目標を全て記録し、除去順が変わっても最終的な証拠の型が一致することを検証してください。

### 定義的等しさと外延性の役割分担を証明の各段で指す

`composeAssociative` の証明を、関数等式を点ごとの等式へ移す段階と、各点で両辺が計算によって同じ項になる段階に分けてください。
`funext` と `rfl` のどちらかを取り除いた場合に、どの形の目標が未解決で残るかを具体的に示します。

さらに定数関数 `fun _ : Bool => 0` を使い、`f false = f true` が成り立っても `false = true` は導けないことを反例として完成させます。
関数合同性と関数外延性を逆向きの原理と誤読せず、逆を得るには単射性という追加仮定が必要だと説明してください。

### 存在と一意存在が持つ証拠の成分を分解する

`∃ x, p x` の証明と `ExistsExactlyOne p` の証明を、証人、性質の証明、任意の他の候補との等式という成分に分けてください。
存在証明だけでは二つの候補が異なることを排除できない例と、一意性だけでは候補が一つも存在しない場合を排除できない例をそれぞれ作ります。

最後に、`Nat` 上で「`x + 1 = 3`」の一意解を述べる命題を書き、存在、性質、一意性の各部を個別に証明します。
解答は `∃!` の記法だけで終えず、Leanの構成子へ展開したときにどの証明がどのフィールドを満たすかまで示します。
-/

end FormalLab.Logic.Equality