------------------------------------------------------------------------
-- An alternative (non-standard) coinductive definition of weak
-- bisimilarity
------------------------------------------------------------------------

-- This definition is based on the function "wb" in Section 6.5.1 of
-- Pous and Sangiorgi's "Enhancements of the bisimulation proof
-- method".

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Bisimilarity.Weak.Alternative {ℓ} (lts : LTS ℓ) where

open import Prelude

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning

open LTS lts

-- We get weak bisimilarity by instantiating strong bisimilarity with
-- a different LTS.

private
  module WB = Bisimilarity (weak lts)

open WB public
  using ( ⟨_,_⟩
        ; [_]_≡_
        ; [_]_≡′_
        ; Extensionality
        ; force
        ; left-to-right
        ; right-to-left
        )
  renaming ( _∼_         to _≈_
           ; _∼′_        to _≈′_
           ; [_]_∼_      to [_]_≈_
           ; [_]_∼′_     to [_]_≈′_
           ; _⟶⟨_⟩ʳˡ_    to _⇒⟨_⟩ʳˡ_
           ; _[_]⟶⟨_⟩ʳˡ_ to _[_]⇒⟨_⟩ʳˡ_
           )

infix -3 lr-result-with-action lr-result-without-action

lr-result-without-action = WB.lr-result-without-action
lr-result-with-action    = WB.lr-result-with-action

syntax lr-result-without-action p′≈q′   q q⟶q′ = p′≈q′      ⇐⟨ q⟶q′ ⟩ q
syntax lr-result-with-action    p′≈q′ μ q q⟶q′ = p′≈q′ [ μ ]⇐⟨ q⟶q′ ⟩ q

-- Strongly bisimilar processes are weakly bisimilar.

private
  module SB = Bisimilarity lts

open SB using (_∼_; _∼′_; [_]_∼_; [_]_∼′_; force)

mutual

  ∼⇒≈ : ∀ {i p q} → p ∼ q → [ i ] p ≈ q
  ∼⇒≈ {i} = λ p∼q →
    ⟨ lr p∼q
    , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p∼q)
    ⟩
    where
    lr : ∀ {p p′ q μ} →
         p ∼ q → p [ μ ]⇒̂ p′ →
         ∃ λ q′ → q [ μ ]⇒̂ q′ × [ i ] p′ ≈′ q′
    lr p∼q p⇒̂p′ =
      Σ-map id (Σ-map id ∼⇒≈′) (SB.strong-is-weak⇒̂ p∼q p⇒̂p′)

  ∼⇒≈′ : ∀ {i p q} → p ∼ q → [ i ] p ≈′ q
  force (∼⇒≈′ p∼q) = ∼⇒≈ p∼q

∼⇒≈″ : ∀ {p q} → p ∼′ q → p ≈′ q
force (∼⇒≈″ p∼′q) = ∼⇒≈ (force p∼′q)

-- TODO: I suspect that the size isn't necessarily preserved: A weak
-- proof of a given size might require a strong proof which is much
-- larger, because a single weak transition might correspond to a
-- large number of strong transitions. I guess this has to be proved
-- for a particular LTS, or with certain assumptions about the LTS.