import FormalLab.Recursion.FixedPoints

/-!
# 第29章：最大不動点・余帰納的述語・双模倣

帰納的述語は有限な導出で正当化される最小の閉包を選びます。一方、無限に動き続ける系では
「どの有限段階でも安全である」ことを扱います。二状態が観察を保ちながら対応し続けることもあります。
これらを述べるには、生成を有限で打ち切らない最大の解が必要です。

本章では最大不動点を余帰納的述語として使います。決定的遷移系の「常に安全」を定義し、後不動点を
見つければ最大不動点への包含が得られる余帰納原理を証明します。さらに双模倣作用素を構成し、同じ
観察を永久に保つ状態対を最大不動点として表します。

## 一段先も候補に属する状態を集める

状態型 `A`、遷移 `next:A→A`、安全述語 `good:A→Prop` を固定します。候補 `X` に対し

$$
F(X)=\{x\mid \mathsf{good}(x)\land X(\mathsf{next}(x))\}.
$$

と定めます。`νF` に属する状態は現在安全であり、次状態も同じ最大不動点に属します。この方程式を
無限個の連言へ展開する代わりに、不動点の一段観察として使います。
-/

namespace FormalLab.Recursion.CoinductivePredicates

universe u v

open FormalLab.Recursion.Lattices
open FormalLab.Recursion.FixedPoints

def alwaysOperator {A : Type u} (good : PredSet A) (next : A → A)
    (candidate : PredSet A) : PredSet A :=
  fun state => good state ∧ candidate (next state)

theorem alwaysOperatorMonotone {A : Type u} (good : PredSet A) (next : A → A) :
    Monotone (alwaysOperator good next) := by
  intro left right inclusion state hypothesis
  exact ⟨hypothesis.1, inclusion hypothesis.2⟩

def Always {A : Type u} (good : PredSet A) (next : A → A) : PredSet A :=
  greatestFixedPoint (alwaysOperator good next)

theorem Always_now {A : Type u} {good : PredSet A} {next : A → A} {state : A}
    (always : Always good next state) : good state := by
  have unfolded := (greatestIsFixedPoint (alwaysOperatorMonotone good next)).2 always
  exact unfolded.1

theorem Always_next {A : Type u} {good : PredSet A} {next : A → A} {state : A}
    (always : Always good next state) : Always good next (next state) := by
  have unfolded := (greatestIsFixedPoint (alwaysOperatorMonotone good next)).2 always
  exact unfolded.2

/-!
`Always_now` と `Always_next` は最大不動点を一層展開する除去則です。有限回繰り返せば任意の時刻の
安全性を得られますが、各時刻について別々の有限証明を列挙する必要はありません。

## 余帰納法は後不動点を不変量として使う

集合 `S` が `S⊆F(S)` を満たすなら後不動点です。最大不動点は全後不動点の和なので `S⊆νF` が
従います。これが本章の余帰納原理です。

$$
\frac{S\subseteq F(S)}{S\subseteq\nu F}.
$$
-/

theorem coinduction {A : Type u} {operator : PredSet A → PredSet A}
    {invariant : PredSet A} (postFixed : Postfixpoint operator invariant) :
    Subset invariant (greatestFixedPoint operator) :=
  everyPostfixpointBelowGreatest operator postFixed

def toggle : Bool → Bool := Bool.not

def anyBool : PredSet Bool := fun _ => True

theorem toggleAlwaysSafe (state : Bool) : Always anyBool toggle state := by
  have postFixed : Postfixpoint (alwaysOperator anyBool toggle) anyBool := by
    intro current _
    exact ⟨True.intro, True.intro⟩
  exact coinduction postFixed True.intro

/-!
証明に選んだ不変量は `anyBool` です。各状態が安全で、次状態も同じ不変量に属することを一段だけ示します。
結論が無限の実行全体に及ぶ根拠は、有限回の帰納ではなく最大不動点の最大性です。

根拠なく目標そのものを余帰納仮定に置けば循環になります。許されるのは、候補集合 `S` の各要素から
`F(S)` の証拠を一段構成し、`S` が後不動点だと示すことです。この一段の生産性条件が循環を制御します。

## 双模倣は状態対の後不動点である

二つの決定的遷移系が同じ観察型 `O` を持つとします。関係 `R⊆A×B` が双模倣であるとは、関連する状態の
観察が等しく、次状態も再び `R` で関連することです。

$$
\mathcal B(R)=
\{(a,b)\mid
  \mathsf{obs}_A(a)=\mathsf{obs}_B(b)
  \land R(\mathsf{next}_A(a),\mathsf{next}_B(b))\},
\qquad
\mathord\sim\;=\nu\mathcal B.
$$
-/

def bisimulationOperator {A : Type u} {B : Type v} {O : Type}
    (observeLeft : A → O) (observeRight : B → O)
    (nextLeft : A → A) (nextRight : B → B)
    (relation : PredSet (A × B)) : PredSet (A × B) :=
  fun pair =>
    observeLeft pair.1 = observeRight pair.2 ∧
      relation (nextLeft pair.1, nextRight pair.2)

theorem bisimulationOperatorMonotone {A : Type u} {B : Type v} {O : Type}
    (observeLeft : A → O) (observeRight : B → O)
    (nextLeft : A → A) (nextRight : B → B) :
    Monotone (bisimulationOperator observeLeft observeRight nextLeft nextRight) := by
  intro left right inclusion pair hypothesis
  exact ⟨hypothesis.1, inclusion hypothesis.2⟩

def Bisimilar {A : Type u} {B : Type v} {O : Type}
    (observeLeft : A → O) (observeRight : B → O)
    (nextLeft : A → A) (nextRight : B → B) : PredSet (A × B) :=
  greatestFixedPoint
    (bisimulationOperator observeLeft observeRight nextLeft nextRight)

theorem deterministicBisimilarityReflexive {A : Type u} {O : Type}
    (observe : A → O) (next : A → A) (state : A) :
    Bisimilar observe observe next next (state, state) := by
  let diagonal : PredSet (A × A) := fun pair => pair.1 = pair.2
  have postFixed : Postfixpoint
      (bisimulationOperator observe observe next next) diagonal := by
    intro pair equal
    rcases pair with ⟨left, right⟩
    dsimp [diagonal] at equal ⊢
    subst right
    exact ⟨rfl, rfl⟩
  exact coinduction postFixed rfl

/-!
対角関係は、一段観察と次状態で保存される後不動点です。したがって任意状態は自分自身と双模倣的です。
非決定的遷移では相手の各遷移へ対応する遷移の存在を両方向に量化する必要があり、本章の決定的な
一関数モデルより作用素が複雑になります。

## 要点

* 余帰納的述語は単調作用素の最大不動点として解釈できる。
* 最大不動点の一段展開から現在の観察と次状態の所属を得る。
* 余帰納法では候補不変量が後不動点 `S⊆F(S)` であることを一段で示す。
* 双模倣は観察の一致と次状態関係の保存を要求する状態対の後不動点である。
* 生産性を示さない循環仮定と、後不動点によって正当化された余帰納を区別する。

## 研究史と文献案内

最大不動点による余帰納は順序論的不動点理論 [TAR55] と並行計算・遷移系の研究が交差して発展しました。
双模倣と余帰納的証明法の標準的な展開は [PFPL16] を参照してください。本章の決定的遷移関数による作用素は
教育用の限定された体系であり、非決定的・確率的・ラベル付き遷移系を一括して形式化したものではありません。

## 問題

### 常時安全性を有限観察へ展開する

`Always_now` と `Always_next` を組み合わせ、`Always good next x` から最初の五状態が全て `good` を
満たすことを証明してください。自然数時刻 `n` へ一般化し、どこで時刻について帰納し、どこで最大不動点を
一段展開するかを分離します。有限観察だけから逆に `Always` を得られる条件も述べれば完了です。

### 余帰納不変量を小さく選ぶ

三状態の周期遷移と、一状態だけを除く安全述語を定義してください。`anyBool` のような全体集合では
後不動点にならない例を作り、安全に閉じた最大の候補を選び直します。各状態の現在条件と次状態条件を
表にし、`coinduction` へ渡す一段証明を構成すれば完了です。
選んだ候補から状態を一つ除いた場合にも後不動点かを調べ、不変量が最大である必要の有無を述べてください。

### 双模倣と単なる観察一致を分ける

最初の観察だけは等しいが次状態で異なる二系を作り、観察一致関係が後不動点でないことを示してください。
次に周期の位相をずらした二系の双模倣関係を構成します。関係の各対について観察と次状態を検査し、
最大不動点への包含から無限の観察列が一致する理由を説明すれば完了です。
関係へ不要な対を加えたとき一段条件が壊れる例も示し、関係の大きさと証明の容易さを比較してください。
-/

end FormalLab.Recursion.CoinductivePredicates