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

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

open import Labelled-transition-system

module Bisimilarity.Coinductive.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 hiding (Extensionality)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F 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 (S̲t̲e̲p̲)
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 4 _∼_ _∼′_ [_]_∼_ [_]_∼′_

Bisimilarity : Size  Rel₂ (# 0) Proc
Bisimilarity i = ν S̲t̲e̲p̲ i

Bisimilarity′ : Size  Rel₂ (# 0) Proc
Bisimilarity′ i = ν′ S̲t̲e̲p̲ i

[_]_∼_ : 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-∼ =
    S̲t̲e̲p̲.⟨  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 4 [_]_≡_ [_]_≡′_

[_]_≡_ :  {p q}  Size  (_ _ : ν S̲t̲e̲p̲  (p , q))  Set
[_]_≡_ = curry  ν-bisimilar

[_]_≡′_ :  {p q}  Size  (_ _ : ν′ S̲t̲e̲p̲  (p , q))  Set
[_]_≡′_ = curry  ν′-bisimilar

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

[]≡↔ :
   {p q} {i : Size} (p∼q₁ p∼q₂ : ν S̲t̲e̲p̲  (p , q)) 

  [ i ] p∼q₁  p∼q₂

    

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ , p′∼q′₁ = S̲t̲e̲p̲.left-to-right p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ = S̲t̲e̲p̲.left-to-right p∼q₂ p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        [ i ] subst (ν′ S̲t̲e̲p̲   (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) 
   let p′₁ , p⟶p′₁ , p′∼q′₁ = S̲t̲e̲p̲.right-to-left p∼q₁ q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ = S̲t̲e̲p̲.right-to-left p∼q₂ q⟶q′
   in  λ (p′₁≡p′₂ : p′₁  p′₂) 
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁  p⟶p′₂
          ×
        [ i ] subst (ν′ S̲t̲e̲p̲   (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)

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

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

   S̲t̲e̲p̲₁  S̲t̲e̲p̲₂ ⟧₂ (ν′-bisimilar i) (p∼q₁ , p∼q₂)                     ↝⟨ ⟦⟷⟧₂↔ S̲t̲e̲p̲₁ S̲t̲e̲p̲₂ (ν′-bisimilar i) p∼q₁ p∼q₂ 

   S̲t̲e̲p̲₁ ⟧₂ (ν′-bisimilar i)
    ((proj₁ s₁ , f₁  inj₁) , (proj₁ s₂ , f₂  inj₁))
    ×
   S̲t̲e̲p̲₂ ⟧₂ (ν′-bisimilar i)
    ( (proj₂ s₁ , λ p  f₁ (inj₂ (_ , refl , p)))
    , (proj₂ s₂ , λ p  f₂ (inj₂ (_ , refl , p)))
    )                                                                   ↝⟨ Step₁.⟦S̲t̲e̲p̲⟧₂↔ (ν′-bisimilar i) (proj₁ s₁ , f₁  inj₁)
                                                                                                           (proj₁ s₂ , f₂  inj₁)
                                                                             ×-cong
                                                                           Step₂.⟦S̲t̲e̲p̲⟧₂↔ (ν′-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₁.S̲t̲e̲p̲.challenge (proj₁ s₁ , f₁  inj₁) p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ =
         Step₁.S̲t̲e̲p̲.challenge (proj₁ s₂ , f₂  inj₁) p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        [ i ] subst (ν′ S̲t̲e̲p̲   (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  ((∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) 
   let p′₁ , p⟶p′₁ , p′∼q′₁ =
          Step₂.S̲t̲e̲p̲.challenge
             (proj₂ s₁ , λ p  f₁ (inj₂ (_ , refl , p))) q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ =
          Step₂.S̲t̲e̲p̲.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 (ν′ S̲t̲e̲p̲   (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂))    ↔⟨⟩

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ , p′∼q′₁ = S̲t̲e̲p̲.left-to-right p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′∼q′₂ = S̲t̲e̲p̲.left-to-right p∼q₂ p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        [ i ] subst (ν′ S̲t̲e̲p̲   (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂)
    ×
  (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) 
   let p′₁ , p⟶p′₁ , p′∼q′₁ = S̲t̲e̲p̲.right-to-left p∼q₁ q⟶q′
       p′₂ , p⟶p′₂ , p′∼q′₂ = S̲t̲e̲p̲.right-to-left p∼q₂ q⟶q′
   in  λ (p′₁≡p′₂ : p′₁  p′₂) 
        subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁  p⟶p′₂
          ×
        [ i ] subst (ν′ S̲t̲e̲p̲   (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂)     

  where
  open Container

  S̲t̲e̲p̲₁ = Step₁.S̲t̲e̲p̲
  S̲t̲e̲p̲₂ = Step₂.S̲t̲e̲p̲

module Bisimilarity-of-∼
         {p q} {i : Size}
         (p∼q₁ p∼q₂ : ν S̲t̲e̲p̲  (p , q))
         where

  -- A "constructor".

  ⟨_,_,_,_⟩ :
    (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
     let q′₁ , q⟶q′₁ , p′∼q′₁ = S̲t̲e̲p̲.left-to-right p∼q₁ p⟶p′
         q′₂ , q⟶q′₂ , p′∼q′₂ = S̲t̲e̲p̲.left-to-right p∼q₂ p⟶p′
     in  λ (q′₁≡q′₂ : q′₁  q′₂) 
          subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
            ×
          [ i ] subst (ν′ S̲t̲e̲p̲   (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂) 
    (∀ {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) 
     let p′₁ , p⟶p′₁ , p′∼q′₁ = S̲t̲e̲p̲.right-to-left p∼q₁ q⟶q′
         p′₂ , p⟶p′₂ , p′∼q′₂ = S̲t̲e̲p̲.right-to-left p∼q₂ q⟶q′
     in  λ (p′₁≡p′₂ : p′₁  p′₂) 
          subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁  p⟶p′₂
            ×
          [ i ] subst (ν′ S̲t̲e̲p̲   (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂) 
    [ i ] p∼q₁  p∼q₂
  ⟨_,_,_,_⟩ = curry (_↔_.from ([]≡↔ 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′₁ = S̲t̲e̲p̲.left-to-right p∼q₁ p⟶p′
        q′₂ , q⟶q′₂ , p′∼q′₂ = S̲t̲e̲p̲.left-to-right p∼q₂ p⟶p′
    in  λ (q′₁≡q′₂ : q′₁  q′₂) 
         subst (q [ μ ]↝₁_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
           ×
         [ i ] subst (ν′ S̲t̲e̲p̲   (p′ ,_)) q′₁≡q′₂ p′∼q′₁ ≡′ p′∼q′₂
  left-to-right = proj₁  _↔_.to ([]≡↔ p∼q₁ p∼q₂)

  right-to-left :
    [ i ] p∼q₁  p∼q₂ 
     {q′ μ} (q⟶q′ : q [ μ ]⟶ q′) 
    let p′₁ , p⟶p′₁ , p′∼q′₁ = S̲t̲e̲p̲.right-to-left p∼q₁ q⟶q′
        p′₂ , p⟶p′₂ , p′∼q′₂ = S̲t̲e̲p̲.right-to-left p∼q₂ q⟶q′
    in  λ (p′₁≡p′₂ : p′₁  p′₂) 
         subst (p [ μ ]↝₂_) p′₁≡p′₂ p⟶p′₁  p⟶p′₂
           ×
         [ i ] subst (ν′ S̲t̲e̲p̲   (_, q′)) p′₁≡p′₂ p′∼q′₁ ≡′ p′∼q′₂
  right-to-left = proj₂  _↔_.to ([]≡↔ p∼q₁ p∼q₂)

-- A statement of extensionality for bisimilarity.

Extensionality : Set
Extensionality = ν′-extensionality S̲t̲e̲p̲

-- This form of extensionality can be used to derive another form.

extensionality :
  Extensionality 
   {p q} {p∼q₁ p∼q₂ : ν S̲t̲e̲p̲  (p , q)} 
  [  ] p∼q₁  p∼q₂  p∼q₁  p∼q₂
extensionality ext = ν-extensionality ext

open S̲t̲e̲p̲ public using (⟨_,_⟩; left-to-right; right-to-left)