import FormalLab.CategoryTheory.EndofunctorCoalgebras

/-!
# 第57章：終余代数・anamorphism・振舞意味論

余代数は一段観察を与えますが、観察を何段も続けた全振舞いをどこに置くかは決めません。全ての余代数から
一意な観察保存写像を受ける余代数を選ぶと、各状態をその完全な振舞いへ写せます。この普遍対象が終余代数です。

本章では `F(X)=A×X` に対するストリーム `ℕ→A` を終余代数として構成します。任意の状態機械からストリームを
生成するanamorphismを定義し、一意性を有限段階の観察に関する帰納法で証明します。終余代数の構造射が同型に
なる双対Lambek補題と、双模倣による振舞いの等しさへの入口も扱います。

## `A×X` は出力と次状態を表す

出力型 `A` を固定し、自己関手

$$
F(X)=A\times X.
$$

を考えます。`F`-余代数 `c:S→A×S` は各状態から現在の出力と次状態を一つずつ返す決定的機械です。
-/

namespace FormalLab.CategoryFoundations.FinalCoalgebras

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open _root_.CategoryTheory.Limits

universe u

def streamFunctor (α : Type u) : Type u ⥤ Type u where
  obj X := α × X
  map f := ↾fun pair => (pair.1, f pair.2)
  map_id X := by
    ext pair <;> simp
  map_comp f g := by
    ext pair <;> simp

def streamStructure (α : Type u) : (Nat → α) → α × (Nat → α) :=
  fun stream => (stream 0, fun n => stream (n + 1))

def streamCoalgebra (α : Type u) : Coalgebra (streamFunctor α) where
  V := Nat → α
  str := ↾streamStructure α

theorem streamStructure_head_tail (stream : Nat → α) : (streamCoalgebra α).str stream =
    (stream 0, fun n => stream (n + 1)) := rfl

/-!
ストリームは先頭と尾に分解でき、尾も再びストリームです。Leanの関数 `Nat→α` を使うことで、任意の有限位置を
観察できます。これはLeanに一般の余帰納型定義機構があると主張するものではなく、この関手の終余代数候補を
既存の関数型で表現しています。

## anamorphismは状態から振舞いを生成する

任意の余代数 `c:S→A×S` から、初期状態 `s` を繰り返し観察してストリームを作ります。

$$
\begin{aligned}
\mathsf{unfold}_c(s)(0)&=\mathsf{head}(c(s)),\\
\mathsf{unfold}_c(s)(n+1)&=
  \mathsf{unfold}_c(\mathsf{next}(c(s)))(n).
\end{aligned}
$$

この生成写像をanamorphism、unfold、またはcoiterationと呼びます。
-/

variable {α : Type u}

def unfold (S : Coalgebra (streamFunctor α)) (state : S.V) : Nat → α
  | 0 => (S.str state).1
  | n + 1 => unfold S (S.str state).2 n

def unfoldHom (S : Coalgebra (streamFunctor α)) : S ⟶ streamCoalgebra α where
  f := ↾unfold S
  h := by
    ext state
    rfl

/-!
可換正方形は、状態を一段観察して残りをunfoldする経路と、先に全ストリームを生成して先頭・尾へ分解する経路が
一致することを述べます。

偶数を順に出力する機械を具体化します。
-/

def evenMachine : Coalgebra (streamFunctor Nat) where
  V := Nat
  str := ↾fun n => (2 * n, n + 1)

def evenMachineUnfold (start : Nat) : Nat → Nat := unfold evenMachine start

def evens : Nat → Nat := evenMachineUnfold 0

theorem evens_zero : evens 0 = 0 := rfl

theorem evens_three : evens 3 = 6 := rfl

#eval [evens 0, evens 1, evens 2, evens 3]

/-!
## 観察保存写像はunfoldに限る

余代数準同型 `f:S→streamCoalgebra A` の条件を状態 `s` で評価すると、`f(s)` の先頭は `c(s)` の出力に等しく、
`f(s)` の尾は次状態の像 `f(next(s))` に等しくなります。位置 `n` に関する帰納法で全成分が `unfold` と一致します。
-/

theorem unfold_unique (S : Coalgebra (streamFunctor α))
    (f : S ⟶ streamCoalgebra α) : f = unfoldHom S := by
  apply Coalgebra.ext
  apply ConcreteCategory.hom_ext
  intro state
  funext n
  change f.f state n = unfold S state n
  induction n generalizing state with
  | zero =>
      have h := types_congr_hom f.h state
      exact (congrArg Prod.fst h).symm
  | succ n ih =>
      have h := types_congr_hom f.h state
      have tail := congrArg (fun pair => pair.2 n) h
      calc
        f.f state (n + 1) = f.f (S.str state).2 n := tail.symm
        _ = unfold S (S.str state).2 n := ih (S.str state).2
        _ = unfold S state (n + 1) := rfl

def streamIsTerminal (α : Type u) : IsTerminal (streamCoalgebra α) :=
  IsTerminal.ofUniqueHom (fun S => unfoldHom S) (fun S f => unfold_unique S f)

/-!
終性は全ての状態機械からストリーム余代数への準同型がただ一つであることを示します。各状態は、内部表現ではなく
無限に続けられる観察列によって意味づけられます。

## 双対Lambek補題

終 `F`-余代数 `(νF,out)` の構造射 `out:νF→F(νF)` は同型です。終性から逆向きの射を構成し、余代数準同型の
一意性で逆法則を示します。
-/

example : IsIso (streamCoalgebra α).str :=
  Coalgebra.Terminal.str_isIso (streamIsTerminal α)

/-!
ストリームでは、先頭と尾への分解と、先頭を尾へ付ける構成が互いに逆です。ここでも不動点同型
`νF≅F(νF)` は終性から従う結論であり、任意の不動点が終余代数であるわけではありません。

## 振舞いの等しさと双模倣

終余代数への一意な準同型 `beh:S→νF` は状態の振舞意味論です。二状態 `s,t` が同じ像を持てば、全有限段階の
観察が一致します。逆に双模倣関係が存在すれば、適切な関手の関係持ち上げの下で両状態は同じ終振舞いへ写ります。

ストリームの場合、二ストリームの先頭が等しく、尾も再び関係することを繰り返せば関数外延性による等式へ至ります。
無制約な循環仮定ではなく、一段観察を保存する関係が必要です。

## 始代数との違い

始代数のfoldは有限に構成された値を解釈し、一意性を構造帰納法で示します。終余代数のunfoldは状態から任意の有限段階を
観察できる振舞いを生成し、一意性を観察位置の帰納法で示します。両者は反対圏で双対ですが、有限生成と潜在的無限観察を
同じデータ構造として扱いません。

## 要点

* 終 `F`-余代数は全ての `F`-余代数から一意な準同型を受ける。
* `F(X)=A×X` ではストリームが終余代数となり、唯一の準同型がanamorphismである。
* anamorphismは状態を繰り返し一段観察して完全な振舞いを生成する。
* 双対Lambek補題により終余代数の構造射は同型になるが、不動点同型だけでは終性を含まない。
* 終余代数への像が振舞意味論を与え、双模倣は同じ像を証明する関係的手法になる。

## 研究史と文献案内

終余代数によるシステムの振舞意味論と双模倣の統一については Rutten [RUT00] が基準的な研究論文です。
始代数・終余代数と関手不動点の存在・構成を対称的に扱う研究書として [AMM25] を参照してください。
mathlibの `Coalgebra.Terminal.str_isIso` は [MATHLIB] の双対Lambek補題の実装です。ストリーム表現にLeanの
関数型を用いたことと、一般の余帰納型機構の仕様を同一視しません。

## 問題

### 状態機械からストリームを生成する

状態 `S=Nat×Nat`、出力を第一成分、次状態を `(b,a+b)` とするFibonacci機械を構成してください。`unfold` で
最初の十項を計算し、余代数準同型の可換正方形が先頭方程式と尾方程式を同時に表すことを示します。計算例だけでなく、
生成関数が全状態について観察を保つ証明まで完成させてください。

### anamorphismの一意性を証明する

任意の準同型 `f:S→Stream A` について、位置 `n` に関する帰納法を組み立ててください。基底では可換正方形の第一成分、
後者では第二成分と帰納仮定を使います。全位置の一致から関数外延性、台射の一致、余代数準同型の一致へ順に進み、
終性がどの外延性原理を必要とするかを説明できれば完了です。

### 双模倣からストリーム等式を導く

二ストリーム間の関係 `R` が、関係する二ストリームの先頭を等しくし、尾も再び `R` で結ぶと仮定してください。
任意の位置 `n` の値が等しいことを帰納法で示し、関数外延性からストリーム等式を導きます。循環仮定だけの不正な証明と、
一段観察で保たれる双模倣証明の差を明示してください。関係として単なる全関係を選んだ場合に先頭一致条件が
どこで失敗するかを反例で示し、余帰納仮定の許される形を説明できれば完了です。
-/

end FormalLab.CategoryFoundations.FinalCoalgebras