------------------------------------------------------------------------
-- A comparison of the classical definition of weak bisimilarity and
-- one of the coinductive ones
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Bisimilarity.Weak.Comparison where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import H-level equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

import Bisimilarity.Classical
import Bisimilarity.Coinductive
import Bisimilarity.Comparison as Comp
import Bisimilarity.Weak.Classical
import Bisimilarity.Weak.Coinductive
open import Labelled-transition-system

module _ {lts : LTS} where

  open LTS lts

  private
    module Cl = Bisimilarity.Weak.Classical   lts
    module Co = Bisimilarity.Weak.Coinductive lts

  -- Classically weakly bisimilar processes are coinductively weakly
  -- bisimilar.

  cl⇒co :  { i p q}  Cl.[  ] p  q  Co.[ i ] p  q
  cl⇒co = Comp.cl⇒co

  -- Coinductively weakly bisimilar processes are classically weakly
  -- bisimilar.

  co⇒cl :  { p q}  p Co.≈ q  Cl.[  ] p  q
  co⇒cl = Comp.co⇒cl

  -- The function cl⇒co is a left inverse of co⇒cl (up to pointwise
  -- bisimilarity).

  cl⇒co∘co⇒cl :  { i p q}
                (p≈q : p Co.≈ q) 
                Co.[ i ] cl⇒co (co⇒cl { = } p≈q)  p≈q
  cl⇒co∘co⇒cl = Comp.cl⇒co∘co⇒cl

  -- If there are two processes that are not equal, but weakly
  -- bisimilar, then co⇒cl is not a left inverse of cl⇒co.

  co⇒cl∘cl⇒co :  {p q } 
                p  q  p Co.≈ q 
                 λ (p≈p : Cl.[  ] p  p)  co⇒cl (cl⇒co p≈p)  p≈p
  co⇒cl∘cl⇒co = Comp.co⇒cl∘cl⇒co

  -- The two definitions of weak bisimilarity are logically
  -- equivalent.

  classical⇔coinductive :
     { p q}  Cl.[  ] p  q  p Co.≈ q
  classical⇔coinductive = Comp.classical⇔coinductive

  -- The larger classical versions of weak bisimilarity are logically
  -- equivalent to the smallest one.

  larger⇔smallest :  { p q}  Cl.[  ] p  q  p Cl.≈ q
  larger⇔smallest = Comp.larger⇔smallest

  -- There is a split surjection from the classical definition of
  -- bisimilarity to the coinductive one (assuming extensionality).

  classical↠coinductive :
    Co.Extensionality 
     { p q}  Cl.[  ] p  q  p Co.≈ q
  classical↠coinductive = Comp.classical↠coinductive

-- There is at least one LTS for which there is a split surjection
-- from the coinductive definition of weak bisimilarity to the
-- classical one.

coinductive↠classical :
   { p q} 
  Bisimilarity.Weak.Coinductive._≈_  empty   p q 
  Bisimilarity.Weak.Classical.[_]_≈_ empty  p q
coinductive↠classical {p = ()}

-- There is an LTS for which coinductive weak bisimilarity is
-- pointwise propositional (assuming extensionality and univalence).

coinductive-weak-bisimilarity-is-sometimes-propositional :
  Univalence lzero 
  let module Co = Bisimilarity.Weak.Coinductive one-loop in
  Co.Extensionality  Is-proposition (tt Co.≈ tt)
coinductive-weak-bisimilarity-is-sometimes-propositional univ =
  subst  lts  let module Co = Bisimilarity.Coinductive lts in
                   p  Co.Extensionality  Is-proposition (p Co.∼ p))
        (sym $ weak≡id univ one-loop  _ ()))
         _  Comp.coinductive-bisimilarity-is-sometimes-propositional)
        _

-- However, classical weak bisimilarity is, for the same LTS, not
-- pointwise propositional (assuming univalence).

classical-weak-bisimilarity-is-not-propositional :
  Univalence lzero 
  let module Cl = Bisimilarity.Weak.Classical one-loop in
   {}  ¬ Is-proposition (Cl.[  ] tt  tt)
classical-weak-bisimilarity-is-not-propositional univ {} =
  subst  lts  let module Cl = Bisimilarity.Classical lts in
                  p  ¬ Is-proposition (Cl.[  ] p  p))
        (sym $ weak≡id univ one-loop  _ ()))
         _  Comp.classical-bisimilarity-is-not-propositional)
        _

-- Thus there is, in general, no split surjection from the coinductive
-- definition of weak bisimilarity to the classical one (assuming
-- extensionality and univalence).

¬coinductive↠classical :
  Univalence lzero 
   {} 
  Bisimilarity.Weak.Coinductive.Extensionality one-loop 
  ¬ (∀ {p q}  Bisimilarity.Weak.Coinductive._≈_  one-loop   p q 
               Bisimilarity.Weak.Classical.[_]_≈_ one-loop  p q)
¬coinductive↠classical univ {} =
  subst  lts  Bisimilarity.Coinductive.Extensionality lts 
                 ¬ (∀ {p q}  Bisimilarity.Coinductive._∼_  lts   p q 
                              Bisimilarity.Classical.[_]_∼_ lts  p q))
        (sym $ weak≡id univ one-loop  _ ()))
        Comp.¬coinductive↠classical

-- Note also that coinductive weak bisimilarity is not always
-- propositional (assuming univalence).

coinductive-weak-bisimilarity-is-not-propositional :
  Univalence lzero 
  let open Bisimilarity.Weak.Coinductive two-bisimilar-processes in
  ¬ (∀ {p q}  Is-proposition (p  q))
coinductive-weak-bisimilarity-is-not-propositional univ =
  subst  lts  let open Bisimilarity.Coinductive lts in
                 ¬ (∀ {p q}  Is-proposition (p  q)))
        (sym $ weak≡id univ two-bisimilar-processes  _ ()))
        Comp.coinductive-bisimilarity-is-not-propositional

-- In fact, for every type A there is a pointwise split surjection
-- from a certain instance of weak bisimilarity to equality on A
-- (assuming univalence).

weak-bisimilarity↠equality :
  Univalence lzero 
  {A : Set} 
  let open Bisimilarity.Weak.Coinductive (bisimilarity⇔equality A) in
  {p q : A}  p  q  p  q
weak-bisimilarity↠equality univ {A} =
  subst  lts  let open Bisimilarity.Coinductive lts in
                  {p q}  p  q  p  q)
        (sym $ weak≡id univ (bisimilarity⇔equality A)  _ ()))
        Comp.bisimilarity↠equality