------------------------------------------------------------------------
-- Lemmas related to bisimilarity and CCS, implemented using the
-- classical definition of bisimilarity
------------------------------------------------------------------------

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

module Bisimilarity.CCS.Classical {ℓ} {Name : Set ℓ} where

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

import Bisimilarity.CCS.General
import Bisimilarity.Classical.Equational-reasoning-instances
open import Equational-reasoning
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity.Classical CCS

------------------------------------------------------------------------
-- Various lemmas related to _∣_

-- _∣_ is commutative.

∣-comm : ∀ {P Q} → P ∣ Q ∼ Q ∣ P
∣-comm = ⟨ R , R-is-a-bisimulation , base ⟩
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P Q} → R (P ∣ Q , Q ∣ P)

  R-is-symmetric : ∀ {P Q} → R (P , Q) → R (Q , P)
  R-is-symmetric base = base

  R-is-a-bisimulation : Bisimulation R
  R-is-a-bisimulation =
    ⟪ lr , (λ PRQ tr →
              Σ-map id (Σ-map id R-is-symmetric)
                (lr (R-is-symmetric PRQ) tr)) ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × R (P′ , Q′)
    lr base (par-left  tr)  = _ , par-right tr , base
    lr base (par-right tr)  = _ , par-left  tr , base
    lr base (par-τ tr₁ tr₂) =
        _
      , par-τ tr₂ (subst (λ a → _ [ name a ]⟶ _)
                         (sym $ co-involutive _)
                         tr₁)
      , base

-- _∣_ is associative.

∣-assoc : ∀ {P Q R} → P ∣ (Q ∣ R) ∼ (P ∣ Q) ∣ R
∣-assoc = ⟨ S , S-is-a-bisimulation , base ⟩
  where
  data S : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P Q R} → S (P ∣ (Q ∣ R) , (P ∣ Q) ∣ R)

  S-is-a-bisimulation : Bisimulation S
  S-is-a-bisimulation = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         S (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × S (P′ , Q′)
    lr base (par-left tr)               = _ , par-left (par-left tr)    , base
    lr base (par-right (par-left tr))   = _ , par-left (par-right tr)   , base
    lr base (par-right (par-right tr))  = _ , par-right tr              , base
    lr base (par-right (par-τ tr₁ tr₂)) = _ , par-τ (par-right tr₁) tr₂ , base
    lr base (par-τ tr₁ (par-left tr₂))  = _ , par-left (par-τ tr₁ tr₂)  , base
    lr base (par-τ tr₁ (par-right tr₂)) = _ , par-τ (par-left tr₁) tr₂  , base

    rl : ∀ {P Q Q′ μ} →
         S (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × S (P′ , Q′)
    rl base (par-left (par-left tr))    = _ , par-left tr               , base
    rl base (par-left (par-right tr))   = _ , par-right (par-left tr)   , base
    rl base (par-left (par-τ tr₁ tr₂))  = _ , par-τ tr₁ (par-left tr₂)  , base
    rl base (par-right tr)              = _ , par-right (par-right tr)  , base
    rl base (par-τ (par-left tr₁) tr₂)  = _ , par-τ tr₁ (par-right tr₂) , base
    rl base (par-τ (par-right tr₁) tr₂) = _ , par-right (par-τ tr₁ tr₂) , base

-- ∅ is a left identity of _∣_.

∣-left-identity : ∀ {P} → ∅ ∣ P ∼ P
∣-left-identity = ⟨ R , R-is-a-bisimulation , base ⟩
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P} → R (∅ ∣ P , P)

  R-is-a-bisimulation : Bisimulation R
  R-is-a-bisimulation = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × R (P′ , Q′)
    lr base (par-right tr) = _ , tr , base
    lr base (par-left ())
    lr base (par-τ () _)

    rl : ∀ {P Q Q′ μ} →
         R (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × R (P′ , Q′)
    rl base tr = _ , par-right tr , base

-- ∅ is a right identity of _∣_.

∣-right-identity : ∀ {P} → P ∣ ∅ ∼ P
∣-right-identity {P} =
  P ∣ ∅  ∼⟨ ∣-comm ⟩
  ∅ ∣ P  ∼⟨ ∣-left-identity ⟩■
  P

-- _∣_ preserves bisimilarity.

_∣-cong_ : ∀ {P P′ Q Q′} → P ∼ P′ → Q ∼ Q′ → P ∣ Q ∼ P′ ∣ Q′
P∼P′ ∣-cong Q∼Q′ with _⇔_.to (Bisimilarity↔ _) P∼P′
                    | _⇔_.to (Bisimilarity↔ _) Q∼Q′
... | L , L-bisim , PLP′
    | R , R-bisim , QRQ′ = ⟨ LR , ⟪ lr , rl ⟫ , base PLP′ QRQ′ ⟩
  where
  data LR : Rel₂ ℓ (Proc ∞) where
    base : ∀ {P P′ Q Q′} →
           L (P , P′) → R (Q , Q′) → LR (P ∣ Q , P′ ∣ Q′)

  lr : ∀ {P P′ Q μ} →
       LR (P , Q) → P [ μ ]⟶ P′ →
       ∃ λ Q′ → Q [ μ ]⟶ Q′ × LR (P′ , Q′)
  lr (base PLP′ QRQ′) (par-left tr) =
    Σ-map (_∣ _) (Σ-map par-left (flip base QRQ′))
      (left-to-right L-bisim PLP′ tr)

  lr (base PLP′ QRQ′) (par-right tr) =
    Σ-map (_ ∣_) (Σ-map par-right (base PLP′))
      (left-to-right R-bisim QRQ′ tr)

  lr (base PLP′ QRQ′) (par-τ tr₁ tr₂) =
    Σ-zip _∣_ (Σ-zip par-τ base)
      (left-to-right L-bisim PLP′ tr₁)
      (left-to-right R-bisim QRQ′ tr₂)

  rl : ∀ {P Q Q′ μ} →
       LR (P , Q) → Q [ μ ]⟶ Q′ →
       ∃ λ P′ → P [ μ ]⟶ P′ × LR (P′ , Q′)
  rl (base PLP′ QRQ′) (par-left tr) =
    Σ-map (_∣ _) (Σ-map par-left (flip base QRQ′))
      (right-to-left L-bisim PLP′ tr)

  rl (base PLP′ QRQ′) (par-right tr) =
    Σ-map (_ ∣_) (Σ-map par-right (base PLP′))
      (right-to-left R-bisim QRQ′ tr)

  rl (base PLP′ QRQ′) (par-τ tr₁ tr₂) =
    Σ-zip _∣_ (Σ-zip par-τ base)
      (right-to-left L-bisim PLP′ tr₁)
      (right-to-left R-bisim QRQ′ tr₂)

------------------------------------------------------------------------
-- Exercise 6.1.2 from "Enhancements of the bisimulation proof method"
-- by Pous and Sangiorgi

6-1-2 : ∀ {P} → ! P ∣ P ∼ ! P
6-1-2 {P} = ⟨ R , R-is-a-bisimulation , base ⟩
  where
  data R : Rel₂ ℓ (Proc ∞) where
    base : R (! P ∣ P , ! P)
    refl : ∀ {P} → R (P , P)

  R-is-a-bisimulation : Bisimulation R
  R-is-a-bisimulation = ⟪ lr , rl ⟫
    where
    lr : ∀ {P P′ Q μ} →
         R (P , Q) → P [ μ ]⟶ P′ →
         ∃ λ Q′ → Q [ μ ]⟶ Q′ × R (P′ , Q′)
    lr base tr = _ , replication tr , refl
    lr refl tr = _ , tr             , refl

    rl : ∀ {P Q Q′ μ} →
         R (P , Q) → Q [ μ ]⟶ Q′ →
         ∃ λ P′ → P [ μ ]⟶ P′ × R (P′ , Q′)
    rl base (replication tr) = _ , tr , refl
    rl refl tr               = _ , tr , refl

------------------------------------------------------------------------
-- Exercise 6.1.3 (2) from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi

open Bisimilarity.CCS.General.6-1-3-2 (record
       { _∼_       = _∼_
       ; step-∼    = step-∼
       ; finally-∼ = Equational-reasoning.finally₂
       ; reflexive = reflexive
       ; symmetric = symmetric
       ; ∣-comm    = ∣-comm
       ; ∣-assoc   = ∣-assoc
       ; _∣-cong_  = _∣-cong_
       ; 6-1-2     = 6-1-2
       })
       public using (swap-rightmost; 6-1-3-2)