------------------------------------------------------------------------
-- A parametrised coinductive definition that can be used to define
-- strong and weak bisimilarity as well as expansion
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.General
         {ℓ}
         (lts : LTS ℓ)
         (open LTS lts)
         (_[_]↝₁_ _[_]↝₂_ : Proc → Label → Proc → Set ℓ)
         (⟶→↝₁ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝₁ q)
         (⟶→↝₂ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝₂ q)
         where

open import Equality.Propositional as Eq hiding (Extensionality)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Bisimilarity.Step lts _[_]↝₁_ _[_]↝₂_ as Step public
  using (StepC)
open import Indexed-container hiding (⟨_⟩; Bisimilarity)
open import Indexed-container.Combinators hiding (id; _∘_)
open import Relation
import Similarity.Step lts _[_]↝₁_ as Step₁
import Similarity.Step lts _[_]↝₂_ as Step₂

open Indexed-container public using (force)

------------------------------------------------------------------------
-- Bisimilarity

-- Bisimilarity. Note that this definition is small.

infix  _∼_ _∼′_ [_]_∼_ [_]_∼′_

Bisimilarity : Size → Rel₂ ℓ Proc
Bisimilarity = ν StepC

Bisimilarity′ : Size → Rel₂ ℓ Proc
Bisimilarity′ = ν′ StepC

[_]_∼_ : Size → Proc → Proc → Set ℓ
[_]_∼_ = curry ∘ Bisimilarity

[_]_∼′_ : Size → Proc → Proc → Set ℓ
[_]_∼′_ = curry ∘ Bisimilarity′

_∼_ : Proc → Proc → Set ℓ
_∼_ = [ ∞ ]_∼_

_∼′_ : Proc → Proc → Set ℓ
_∼′_ = [ ∞ ]_∼′_

-- Bisimilarity is reflexive.

mutual

  reflexive-∼ : ∀ {p i} → [ i ] p ∼ p
  reflexive-∼ =
    StepC.⟨ (λ p⟶p′ → _ , ⟶→↝₁ p⟶p′ , reflexive-∼′)
          , (λ q⟶q′ → _ , ⟶→↝₂ q⟶q′ , reflexive-∼′)
          ⟩

  reflexive-∼′ : ∀ {p i} → [ i ] p ∼′ p
  force reflexive-∼′ = reflexive-∼

≡⇒∼ : ∀ {p q} → p ≡ q → p ∼ q
≡⇒∼ refl = reflexive-∼

-- Functions that can be used to aid the instance resolution
-- mechanism.

infix -2 ∼:_ ∼′:_

∼:_ : ∀ {i p q} → [ i ] p ∼ q → [ i ] p ∼ q
∼:_ = id

∼′:_ : ∀ {i p q} → [ i ] p ∼′ q → [ i ] p ∼′ q
∼′:_ = id

------------------------------------------------------------------------
-- Bisimilarity for bisimilarity

-- Bisimilarity of bisimilarity proofs.

infix  [_]_≡_ [_]_≡′_

[_]_≡_ : ∀ {p q} → Size → (_ _ : ν StepC ∞ (p , q)) → Set ℓ
[_]_≡_ = curry ∘ ν-bisimilar

[_]_≡′_ : ∀ {p q} → Size → (_ _ : ν′ StepC ∞ (p , q)) → Set ℓ
[_]_≡′_ = curry ∘ ν′-bisimilar

-- An alternative characterisation of bisimilarity of bisimilarity
-- proofs.

[]≡↔ :
  Eq.Extensionality ℓ ℓ →
  ∀ {p q} {i : Size} (p∼q₁ p∼q₂ : ν StepC ∞ (p , q)) →

  [ i ] p∼q₁ ≡ p∼q₂

    ↔

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
   let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
   in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)

[]≡↔ ext {p} {q} {i} p∼q₁@(s₁ , f₁) p∼q₂@(s₂ , f₂) =

  [ i ] p∼q₁ ≡ p∼q₂                                                    ↝⟨ ν-bisimilar↔ ext p∼q₁ p∼q₂ ⟩

  ⟦ StepC₁ ⟷ StepC₂ ⟧₂ (ν′-bisimilar i) (p∼q₁ , p∼q₂)                  ↝⟨ ⟦⟷⟧₂↔ ext StepC₁ StepC₂ (ν′-bisimilar i) p∼q₁ p∼q₂ ⟩

  ⟦ StepC₁ ⟧₂ (ν′-bisimilar i)
    ((proj₁ s₁ , f₁ ∘ inj₁) , (proj₁ s₂ , f₂ ∘ inj₁))
    ×
  ⟦ StepC₂ ⟧₂ (ν′-bisimilar i)
    ( (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p)))
    , (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p)))
    )                                                                  ↝⟨ Step₁.⟦StepC⟧₂↔ ext (ν′-bisimilar i) (proj₁ s₁ , f₁ ∘ inj₁)
                                                                                                               (proj₁ s₂ , f₂ ∘ inj₁)
                                                                            ×-cong
                                                                          Step₂.⟦StepC⟧₂↔ ext (ν′-bisimilar i)
                                                                            (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p)))
                                                                            (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p))) ⟩
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′∼q′₁ =
         Step₁.StepC.challenge (proj₁ s₁ , f₁ ∘ inj₁) p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ =
         Step₁.StepC.challenge (proj₁ s₂ , f₂ ∘ inj₁) p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  ((∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
   let p′₁ , p⟶p′₁ , p′∼q′₁ =
          Step₂.StepC.challenge
             (proj₂ s₁ , λ p → f₁ (inj₂ (_ , refl , p))) q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ =
          Step₂.StepC.challenge
             (proj₂ s₂ , λ p → f₂ (inj₂ (_ , refl , p))) q⟶q′
   in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂))  ↔⟨⟩

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
   let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
   in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)   □

  where
  open Container

  StepC₁ = Step₁.StepC
  StepC₂ = Step₂.StepC

module Bisimilarity-of-∼
         (ext : Eq.Extensionality ℓ ℓ)
         {p q} {i : Size}
         (p∼q₁ p∼q₂ : ν StepC ∞ (p , q))
         where

  -- A "constructor".

  ⟨_,_,_,_,_⟩ :
    (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
     let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
         q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
     in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
          subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
            ×
          [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂) →
    (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
     let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
         p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
     in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
          subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
            ×
          [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂) →
    [ i ] p∼q₁ ≡ p∼q₂
  ⟨_,_,_,_,_⟩ = curry (_↔_.from ([]≡↔ ext p∼q₁ p∼q₂))

  -- Some "projections".

  left-to-right :
    [ i ] p∼q₁ ≡ p∼q₂ →
    ∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
    let q′₁ , q⟶q′₁ , p′∼q′₁ = StepC.left-to-right p∼q₁ p⟶p′
        q′₂ , q⟶q′₂ , p′∼q′₂ = StepC.left-to-right p∼q₂ p⟶p′
    in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
         subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
           ×
         [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂
  left-to-right = proj₁ ∘ _↔_.to ([]≡↔ ext p∼q₁ p∼q₂)

  right-to-left :
    [ i ] p∼q₁ ≡ p∼q₂ →
    ∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) →
    let p′₁ , p⟶p′₁ , p′∼q′₁ = StepC.right-to-left p∼q₁ q⟶q′
        p′₂ , p⟶p′₂ , p′∼q′₂ = StepC.right-to-left p∼q₂ q⟶q′
    in ∃ λ (p′₁≡p′₂ : p′₁ ≡ p′₂) →
         subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁ ≡ p⟶p′₂
           ×
         [ i ] subst (ν′ StepC ∞ ∘ (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂
  right-to-left = proj₂ ∘ _↔_.to ([]≡↔ ext p∼q₁ p∼q₂)

-- A statement of extensionality for bisimilarity.

Extensionality : Set ℓ
Extensionality = ν′-extensionality StepC

-- This form of extensionality can be used to derive another form
-- (in the presence of extensionality for functions).

extensionality :
  Eq.Extensionality ℓ ℓ →
  Extensionality →
  ∀ {p q} {p∼q₁ p∼q₂ : ν StepC ∞ (p , q)} →
  [ ∞ ] p∼q₁ ≡ p∼q₂ → p∼q₁ ≡ p∼q₂
extensionality ext ν-ext = ν-extensionality ext ν-ext

open StepC public using (⟨_,_⟩; left-to-right; right-to-left)