strong bisimulation is equivalence

Bisim.agda

module Bisim where

open import Data.Nat
open import Data.List
open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)

open import Relation.Binary using (IsEquivalence)

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Coinduction

-- http://www.iis.sinica.edu.tw/~scm/2008/aopa/a
open import Relations
open import Sets

Action = ℕ

data Proc : Set where
  branch : List (Action × (∞ Proc)) → Proc

data Step : Proc → Action → Proc → Set where
  go    : ∀ {l} → {a : Action} {Q : Proc} → Step (branch ((a , ♯ Q) ∷ l)) a Q
  other : ∀ {l} → {a b : Action} {P Q : Proc} →
          Step (branch l) a Q → Step (branch ((b , ♯ P) ∷ l)) a Q

Rel = Proc ← Proc

StrongSimulation : Rel → Set
StrongSimulation S = ∀ {P P′ Q} {α} →
                     S P Q →
                     Step P α P′ →
                     (∃ λ (Q′ : Proc) → Step Q α Q′ × (S P′ Q′))

-- strongly simulates
_≼_ : Proc → Proc → Set₁
P ≼ Q = ∃ λ (S : Rel) → StrongSimulation S × S P Q

StrongBisimulation : Rel → Set
StrongBisimulation S = StrongSimulation S × StrongSimulation (S ˘)

_~_ : Proc → Proc → Set₁
P ~ Q = ∃ λ (S : Rel) → StrongBisimulation S × S P Q

~-refl : {P : Proc} → P ~ P
~-refl {P} = idR , (idisSS , idisSS˘) , refl
             where idisSS : StrongSimulation idR
                   idisSS {P} {P′} {.P} {α} refl P-α->P′ = P′ , P-α->P′ , refl
                   idisSS˘ : StrongSimulation (idR ˘)
                   idisSS˘ {P} {P′} {.P} {α} refl P-α->P′ = P′ , P-α->P′ , refl

~-sym : {P Q : Proc} → P ~ Q → Q ~ P
~-sym (R , (RisSS , R˘isSS) , PQ) = R ˘ , (R˘isSS , RisSS) , PQ

compose-ss : {R S : Rel} →
             StrongSimulation R → StrongSimulation S →
             StrongSimulation (S ○ R)
compose-ss RisSS SisSS =
    λ {P} {P′} {R} {α} PR P-α->P′ →
        let Q = proj₁ PR
            ev = RisSS {P} {P′} {Q} {α} (proj₁ (proj₂ PR)) P-α->P′
            Q′ = proj₁ ev
            Q-α->Q′ = proj₁ (proj₂ ev)
            P′Q′ = proj₂ (proj₂ ev)
            ev₂ = SisSS {Q} {Q′} {R} {α} (proj₂ (proj₂ PR)) Q-α->Q′
            R′ = proj₁ ev₂
            R-α->R′ = proj₁ (proj₂ ev₂)
            Q′R′ = proj₂ (proj₂ ev₂)
        in
          R′ , R-α->R′ , (Q′ , P′Q′ , Q′R′)

compose-ss˘ : {P-Q Q-R : Rel} →
              StrongSimulation (P-Q ˘) → StrongSimulation (Q-R ˘) →
              StrongSimulation ((Q-R ○ P-Q) ˘)
compose-ss˘ {P-Q} {Q-R} P-Q˘isSS Q-R˘isSS =
    λ {R} {R′} {P} {α} RP R-α->R′ →
        let Q = proj₁ RP
            ev = Q-R˘isSS {R} {R′} {Q} {α} (proj₂ (proj₂ RP)) R-α->R′
            Q′ = proj₁ ev
            Q-α->Q′ = proj₁ (proj₂ ev)
            R′Q′ = proj₂ (proj₂ ev)
            ev₂ = P-Q˘isSS {Q} {Q′} {P} {α} (proj₁ (proj₂ RP))  Q-α->Q′
            P′ = proj₁ ev₂
            P-α->P′ = proj₁ (proj₂ ev₂)
            Q′P′ = proj₂ (proj₂ ev₂)
        in
          P′ , P-α->P′ , (Q′ , Q′P′ , R′Q′)

~-trans : {P Q R : Proc} → P ~ Q → Q ~ R → P ~ R
~-trans {P} {Q} {R}
        (P-Q , (P-QisSS , P-Q˘isSS) , PQ)
        (Q-R , (Q-RisSS , Q-R˘isSS) , QR) =
    P-R , (P-RisSS , P-R˘isSS) , lem {r = P-Q} {s = Q-R} PQ QR
    where P-R = Q-R ○ P-Q
          P-RisSS : StrongSimulation P-R
          P-RisSS = compose-ss P-QisSS Q-RisSS
          P-R˘isSS : StrongSimulation (P-R ˘)
          P-R˘isSS = compose-ss˘ P-Q˘isSS Q-R˘isSS
          lem : {A B C : Set} {a : A} {b : B} {c : C} {r : B ← A} {s : C ← B} →
                r a b → s b c → (s ○ r) a c
          lem {b = b} r0 r1 = b , r0 , r1

SBisEquivalence : IsEquivalence _~_
SBisEquivalence = record
  { refl = ~-refl
  ; sym = ~-sym
  ; trans = ~-trans
  }