------------------------------------------------------------------------
-- The two coinductive definitions of weak bisimilarity are pointwise
-- logically equivalent
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Weak.Equivalent {} {lts : LTS } where

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

import Bisimilarity.Weak lts as Std
import Bisimilarity.Weak.Alternative lts as Alt
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning

open LTS lts

mutual

  -- The alternative definition of weak bisimilarity can be converted
  -- to the standard one, in a size-preserving way.

  alternative⇒ :  {i p q}  Alt.[ i ] p  q  Std.[ i ] p  q
  alternative⇒ {i} p≈q =
    Std.⟨ lr p≈q
        , Σ-map id (Σ-map id symmetric)  lr (symmetric p≈q)
        
    where
    lr :  {p p′ q μ} 
         Alt.[ i ] p  q  p [ μ ]⟶ p′ 
          λ q′  q [ μ ]⇒̂ q′ × Std.[ i ] p′ ≈′ q′
    lr p≈q p⟶p′ =
      Σ-map id (Σ-map id alternative⇒′)
        (Alt.left-to-right p≈q (⟶→⇒̂ p⟶p′))

  alternative⇒′ :  {i p q}  Alt.[ i ] p ≈′ q  Std.[ i ] p ≈′ q
  Std.force (alternative⇒′ p≈′q) = alternative⇒ (Alt.force p≈′q)

mutual

  -- One can also convert in the other direction. Note that this
  -- conversion is not guaranteed to be size-preserving. For at least
  -- one LTS it cannot (in general) be size-preserving, see
  -- Bisimilarity.Weak.Delay-monad.size-preserving-⇒alternative⇔uninhabited.

  ⇒alternative :  {i p q}  p Std.≈ q  Alt.[ i ] p  q
  ⇒alternative {i} p≈q =
    Alt.⟨ lr p≈q
        , Σ-map id (Σ-map id symmetric)  lr (symmetric p≈q)
        
    where
    lr :  {p p′ q μ} 
         p Std.≈ q  p [ μ ]⇒̂ p′ 
          λ q′  q [ μ ]⇒̂ q′ × Alt.[ i ] p′ ≈′ q′
    lr p≈q p⇒̂p′ =
      Σ-map id (Σ-map id ⇒alternative′) (Std.weak-is-weak⇒̂ p≈q p⇒̂p′)

  ⇒alternative′ :  {i p q}  p Std.≈ q  Alt.[ i ] p ≈′ q
  Alt.force (⇒alternative′ p≈q) = ⇒alternative p≈q

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

alternative⇔ :  {p q}  p Alt.≈ q  p Std.≈ q
alternative⇔ = record
  { to   = alternative⇒
  ; from = ⇒alternative
  }

-- TODO: I don't know if the two definitions of weak bisimilarity are
-- isomorphic.