import FormalLab.CategoryTheory.FinalCoalgebras
import FormalLab.Recursion.CoinductivePredicates

/-!
# 第68章：余帰納法・双模倣・最大不動点・終余代数——関係と振舞いを接続する

二つの状態が同じ振舞いを持つことは、少なくとも二通りに表せます。一つは、現在の観察が等しく、次状態も
再び関係するような双模倣を見つける方法です。もう一つは、各状態を終余代数へ写し、その像が等しいと示す
方法です。前者は状態対の集合上の最大不動点、後者は余代数圏の終対象を使います。

両者は密接ですが、同じ定義ではありません。最大不動点は包含順序を持つ述語の束で構成され、終余代数は
全ての余代数から一意な準同型を受けます。対応を示すには、関手が関係をどう持ち上げるか、双模倣関係から
どの余代数を作れるかなどの条件が要ります。

本章では決定的ストリーム系 `S→A×S` に範囲を限定します。この場合は関係持ち上げを観察の等式と次状態の
関係として明示できるため、終余代数への像の等しさと最大双模倣が同値であることをLeanで直接証明できます。

## ストリームは有限位置から観察できる

ストリームを関数 `Nat→A` と表すと、先頭は位置 `0`、尾は位置を一つずらした関数です。二ストリームが等しい
ことを示すには、全ての有限位置で値が等しいことを示し、関数外延性を使います。
-/

namespace FormalLab.Bridges.CoinductionAndFinalCoalgebras

open FormalLab.Recursion.Lattices
open FormalLab.Recursion.FixedPoints
open FormalLab.Recursion.CoinductivePredicates
open FormalLab.CategoryFoundations.FinalCoalgebras

def streamHead {A : Type} (stream : Nat → A) : A := stream 0

def streamTail {A : Type} (stream : Nat → A) : Nat → A :=
  fun n => stream (n + 1)

example (stream : Nat → A) : streamStructure A stream =
    (streamHead stream, streamTail stream) := rfl

def StreamBisimilar {A : Type} : PredSet ((Nat → A) × (Nat → A)) :=
  Bisimilar streamHead streamHead streamTail streamTail

/-!
この宣言では `A : Type` としています。第29章の教育用 `Bisimilar` が観察型を宇宙0に固定しているためです。
双模倣の数学的定義が宇宙0を本質的に要求するわけではなく、現行の局所APIの宇宙境界です。

`StreamBisimilar(s,t)` は、先頭が等しく、尾の対も再び同じ関係に入るという作用素の最大不動点です。最大不動点の
固定点方程式から、現在の観察と次の関係を一段ずつ取り出せます。

$$
\Phi(R)=\{(s,t)\mid
\mathsf{head}(s)=\mathsf{head}(t)
\land R(\mathsf{tail}(s),\mathsf{tail}(t))\},
\qquad
\mathord\sim\;=\nu\Phi.
$$
-/

theorem StreamBisimilar.head {A : Type} {left right : Nat → A}
    (h : StreamBisimilar (left, right)) : streamHead left = streamHead right := by
  have unfolded := (greatestIsFixedPoint
    (bisimulationOperatorMonotone streamHead streamHead streamTail streamTail)).2 h
  exact unfolded.1

theorem StreamBisimilar.tail {A : Type} {left right : Nat → A}
    (h : StreamBisimilar (left, right)) :
    StreamBisimilar (streamTail left, streamTail right) := by
  have unfolded := (greatestIsFixedPoint
    (bisimulationOperatorMonotone streamHead streamHead streamTail streamTail)).2 h
  exact unfolded.2

/-!
## 双模倣からストリーム等式を得る

余帰納仮定をLeanの関数等式へ直接循環的に使うことはできません。代わりに位置 `n` について帰納します。
位置 `0` では先頭の一致を使い、位置 `n+1` では尾に対する双模倣と帰納仮定を使います。
-/

theorem stream_eq_of_bisimilar {A : Type} {left right : Nat → A}
    (h : StreamBisimilar (left, right)) : left = right := by
  funext n
  induction n generalizing left right with
  | zero => exact h.head
  | succ n ih =>
      change streamTail left n = streamTail right n
      exact ih h.tail

theorem stream_bisimilar_of_eq {A : Type} {left right : Nat → A}
    (h : left = right) : StreamBisimilar (left, right) := by
  subst right
  exact deterministicBisimilarityReflexive streamHead streamTail left

theorem streamBisimilar_iff_eq {A : Type} (left right : Nat → A) :
    StreamBisimilar (left, right) ↔ left = right :=
  ⟨stream_eq_of_bisimilar, stream_bisimilar_of_eq⟩

/-!
ここで自然数帰納法が現れるのは、ストリームを生成された有限データとみなすためではありません。任意の一つの
観察位置へ到達するために尾を有限回たどるからです。双模倣そのものの正当化は最大不動点の余帰納原理にあり、
有限位置の一致を関数等式へまとめる段階で外延性を使います。

## 状態機械の振舞いは終余代数への像である

`F(X)=A×X` の余代数 `C` を固定します。状態 `s` の振舞いは、終ストリーム余代数への一意な準同型
`unfoldHom C` の値です。
-/

def observe {A : Type} (C : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor A)) : C.V → A :=
  fun state => (C.str state).1

def next {A : Type} (C : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor A)) : C.V → C.V :=
  fun state => (C.str state).2

def behavior {A : Type} (C : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor A)) : C.V → (Nat → A) :=
  unfold C

def BehaviorallyEqual {A : Type}
    (C : _root_.CategoryTheory.Endofunctor.Coalgebra (streamFunctor A)) :
    PredSet (C.V × C.V) :=
  fun pair => behavior C pair.1 = behavior C pair.2

example {A : Type}
    (C : _root_.CategoryTheory.Endofunctor.Coalgebra (streamFunctor A)) :
    behavior C = (unfoldHom C).f := rfl

/-!
`BehaviorallyEqual C` は終余代数への準同型の核関係です。次に、この関係が双模倣作用素の後不動点であることを
示します。振舞いの位置 `0` の等式が現在の観察を、位置 `n+1` の等式が次状態の振舞いの等式を与えます。
-/

theorem behaviorallyEqual_postfixed {A : Type}
    (C : _root_.CategoryTheory.Endofunctor.Coalgebra (streamFunctor A)) :
    Postfixpoint (bisimulationOperator (observe C) (observe C) (next C) (next C))
      (BehaviorallyEqual C) := by
  intro pair h
  rcases pair with ⟨left, right⟩
  constructor
  · exact congrFun h 0
  · funext n
    exact congrFun h (n + 1)

theorem bisimilar_of_behaviorallyEqual {A : Type}
    (C : _root_.CategoryTheory.Endofunctor.Coalgebra (streamFunctor A))
    {left right : C.V} (h : BehaviorallyEqual C (left, right)) :
    Bisimilar (observe C) (observe C) (next C) (next C) (left, right) :=
  coinduction (behaviorallyEqual_postfixed C) h

/-!
この向きでは、終余代数への像が等しい状態対全体を余帰納不変量に選びました。その集合が一段観察で閉じるため、
最大不動点へ含まれます。候補関係が最大であることを別に示す必要はありません。

## 双模倣は終振舞いを等しくする

逆向きでは、双模倣から各有限位置の出力一致を導きます。状態対に対する最大不動点を一段展開し、次状態へ
移る操作を位置の帰納法と組み合わせます。
-/

theorem behavior_eq_of_bisimilar {A : Type}
    (C : _root_.CategoryTheory.Endofunctor.Coalgebra (streamFunctor A))
    {left right : C.V}
    (h : Bisimilar (observe C) (observe C) (next C) (next C) (left, right)) :
    behavior C left = behavior C right := by
  funext n
  induction n generalizing left right with
  | zero =>
      have unfolded := (greatestIsFixedPoint
        (bisimulationOperatorMonotone (observe C) (observe C) (next C) (next C))).2 h
      exact unfolded.1
  | succ n ih =>
      have unfolded := (greatestIsFixedPoint
        (bisimulationOperatorMonotone (observe C) (observe C) (next C) (next C))).2 h
      change behavior C (next C left) n = behavior C (next C right) n
      exact ih unfolded.2

theorem bisimilar_iff_same_terminal_image {A : Type}
    (C : _root_.CategoryTheory.Endofunctor.Coalgebra (streamFunctor A))
    (left right : C.V) :
    Bisimilar (observe C) (observe C) (next C) (next C) (left, right) ↔
      (unfoldHom C).f left = (unfoldHom C).f right :=
  ⟨behavior_eq_of_bisimilar C, bisimilar_of_behaviorallyEqual C⟩

/-!
この同値が本章の中心です。左辺は状態対の述語束における最大不動点、右辺は余代数圏の終対象への一意射の
核関係です。決定的ストリーム関手では両者が一致します。

$$
s\sim t
\quad\Longleftrightarrow\quad
\mathsf{beh}(s)=\mathsf{beh}(t),
$$

ここで `beh` は終ストリーム余代数への一意な準同型です。

一般の関手へ同じ議論を移すには、関係 `R⊆X×Y` から `F(X)` と `F(Y)` の間の関係を作る関係持ち上げが必要です。
非決定的遷移では「左の各遷移に右の対応遷移があり、逆も成り立つ」という量化が加わります。また、弱双模倣や
確率的双模倣では観察と遷移の比較方法そのものが変わります。本章の同値を無条件に全関手へ一般化しません。

## 最大不動点と終余代数が答える問いは異なる

最大不動点 `νΦ` は「どの状態対が一段条件を永久に保つか」を分類します。終余代数 `νF` は「各状態の完全な
振舞いをどの対象に写すか」を与えます。同じ記号 `ν` が使われることがありますが、前者の `Φ` は関係上の
単調作用素、後者の `F` は対象と射に作用する関手です。

終余代数の構造射が同型であるという双対Lambek補題も、双模倣原理そのものではありません。同型は一層の分解と
再構成を与えます。二状態を等しい振舞いへ送るには、終性による一意射と関係持ち上げを使う追加の議論が要ります。

## 要点

* 双模倣は観察の一致と次状態関係の保存を要求する関係作用素の最大不動点である。
* 終余代数への一意な準同型は各状態を完全な観察振舞いへ写す。
* 決定的ストリーム系では、終余代数への像が等しい状態対が双模倣作用素の後不動点になる。
* 逆に双模倣から全有限位置の観察一致を導き、関数外延性によって終振舞いの等式を得られる。
* 最大不動点は述語束の順序論、終余代数は余代数圏の普遍性に属し、両者の接続には関係持ち上げが要る。
* 不動点同型、終性、双模倣、終振舞いの等式は、それぞれ異なるデータと証明義務を持つ。

## 研究史と文献案内

Knaster–Tarski型の最大不動点による余帰納原理は [TAR55] を順序論的背景とします。終余代数、双模倣、
システムの振舞意味論を統一的に扱う基準文献は Rutten [RUT00] です。始代数と終余代数の構成・存在条件を
対称的に追うには [AMM25] を参照してください。本章の定理は決定的ストリーム関手に限定した直接証明です。
一般の弱pullback保存関手などに対する双模倣と振舞同値の対応を、仮定なしに [RUT00] へ帰属させません。
Leanの最大不動点は本書の述語集合上の実装、終余代数はmathlibの `Endofunctor.Coalgebra` を使用しています。

## 問題

### 双模倣からストリーム等式までの二種類の帰納を分ける

`stream_eq_of_bisimilar` を、最大不動点の一段展開、位置についての自然数帰納法、関数外延性の三段階に分解して
書き直してください。余帰納仮定が正当化するのはどの関係所属で、自然数帰納法が進めるのはどの有限観察かを
各ゴールの型で示します。一段条件を確認しない循環証明が作れない理由もLeanの型から説明できれば完了です。

### 異なる内部状態表現の機械を比較する

偶数列を、状態 `Nat` から `2n` を出す機械と、偶数だけからなる部分型を状態にして値を直接出す機械の二通りで
構成してください。二状態型の間に関係を定義し、観察一致と次状態保存を示します。両機械を一つの直和状態機械へ
まとめるか異種関係版の作用素を使い、対応する初期状態が同じ終ストリームへ写ることまで証明してください。

### 終余代数への核関係が後不動点になる理由を一般化する

`behaviorallyEqual_postfixed` の証明で、位置 `0` と `n+1` の等式がそれぞれ何を使っているかを可換正方形へ戻して
ください。一般の関手 `F` について同じ証明を書くために必要な関係持ち上げを定義し、終余代数の等式関係を
持ち上げた関係へ送る条件を列挙します。ストリーム積関手では条件が成分ごとの等式へ簡約されることを示せれば完了です。

### 最大不動点・不動点同型・終性の反例を整理する

恒等関手や定数関手を使い、構造射が同型であっても終余代数でない余代数を探してください。次に、状態対上の
双模倣最大不動点が存在することから終余代数の存在が直ちに従わない理由を、作用素の定義域と普遍量化の違いから
説明します。三概念について必要な圏・順序・射・関係を表にし、誤った含意ごとに最小の反例を対応させれば完了です。
-/

end FormalLab.Bridges.CoinductionAndFinalCoalgebras