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

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

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

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⟩

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

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⟩