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

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

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

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