------------------------------------------------------------------------
-- The Step function, used to define strong and weak bisimilarity as
-- well as expansion
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Step
         {ℓ}
         (lts : LTS ℓ)
         (open LTS lts)
         (_[_]↝₁_ _[_]↝₂_ : Proc → Label → Proc → Set ℓ)
         where

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

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

import Similarity.Step lts as One-sided
open import Indexed-container hiding (⟨_⟩)
open import Indexed-container.Combinators hiding (_∘_)
open import Relation

private
 module Temporarily-private where

  -- If _[_]↝₁_ and _[_]↝₂_ are instantiated with _[_]⟶_, then this is
  -- basically the function from Definition 6.3.1 in Pous and
  -- Sangiorgi's "Enhancements of the bisimulation proof method",
  -- except that clause (3) is omitted.
  --
  -- Similarly, if the relations are instantiated with _[_]⇒̂_, then
  -- this is basically the function wb₁, again with the exception that
  -- clause (3) is omitted.
  --
  -- Finally, if _[_]↝₁_ is instantiated with _[_]⟶̂_ and _[_]↝₂_ is
  -- instantiated with _[_]⇒_, then we get the expansion relation's
  -- "step" function.

  record Step {r} (R : Rel₂ r Proc) (pq : Proc × Proc) :
              Set (ℓ ⊔ r) where
    constructor ⟨_,_⟩

    private
      p = proj₁ pq
      q = proj₂ pq

    field
      left-to-right : ∀ {p′ μ} →
                      p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′ × R (p′ , q′)
      right-to-left : ∀ {q′ μ} →
                      q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′ × R (p′ , q′)

open Temporarily-private using (Step)

-- The Step function, expressed as an indexed container.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = One-sided.StepC _[_]↝₁_ ⟷ One-sided.StepC _[_]↝₂_

-- The strong bisimilarity container presented in the paper,
-- generalised to use _[_]↝₁_ and _[_]↝₂_.

StepC′ : Container (Proc × Proc) (Proc × Proc)
StepC′ =
  (λ { (p , q) → (∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′) ×
                 (∀ {q′ μ} → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′)
     })
    ◁
  (λ { {(p , q)} (lr , rl) (p′ , q′) →
       (∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) → proj₁ (lr p⟶p′) ≡ q′) ⊎
       (∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ q′) → proj₁ (rl q⟶q′) ≡ p′)
     })

-- The interpretations of the two containers above are pointwise
-- logically equivalent, and in the presence of extensionality they
-- are pointwise isomorphic.

StepC↔StepC′ :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  ⟦ StepC ⟧ R pq ↝[ k ] ⟦ StepC′ ⟧ R pq
StepC↔StepC′ {pq = p , q} =
  inverse-ext? λ {k} ext →
  Σ-cong (inverse $
          drop-⊤-left-Σ (One-sided.Magic↔⊤ _)
            ×-cong
          drop-⊤-left-Σ (One-sided.Magic↔⊤ _)) λ { (lr , rl) →
  implicit-∀-cong ext λ { {p′ , q′} →
  Π-cong (lower-extensionality? k lzero ℓ ext)
    (F.id ⊎-cong (

       (∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ q′) →
            proj₁ (rl q⟶q′) ≡ p′)                            ↝⟨ inverse $ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩

       (∃ λ (q′p′≡ : ∃ λ q′p′ → q′p′ ≡ (q′ , p′)) →
        ∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ proj₁ (proj₁ q′p′≡)) →
          proj₁ (rl q⟶q′) ≡ proj₂ (proj₁ q′p′≡))             ↝⟨ inverse Σ-assoc ⟩

       (∃ λ q′p′ → q′p′ ≡ (q′ , p′) ×
        ∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ proj₁ q′p′) →
          proj₁ (rl q⟶q′) ≡ proj₂ q′p′)                      ↔⟨ (∃-cong λ _ → (inverse $ Eq.≃-≡ (Eq.↔⇒≃ ×-comm)) ×-cong F.id) ⟩□

       (∃ λ q′p′ → swap q′p′ ≡ (p′ , q′) ×
        ∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ proj₁ q′p′) →
          proj₁ (rl q⟶q′) ≡ proj₂ q′p′)                      □))

    (λ _ → F.id) }}

-- The definition of Step in terms of a container is pointwise
-- logically equivalent to the direct definition, and in the presence
-- of extensionality it is pointwise isomorphic to the direct
-- definition.

Step↔StepC :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  Step R pq ↝[ k ] ⟦ StepC ⟧ R pq
Step↔StepC {R = R} {pq} ext =
  Step R pq                                     ↔⟨ lemma ⟩

  One-sided.Step _[_]↝₁_ R pq
    ×
  One-sided.Step _[_]↝₂_ (R ⁻¹) (swap pq)       ↝⟨ One-sided.Step↔StepC _ ext ×-cong One-sided.Step↔StepC _ ext ⟩

  ⟦ One-sided.StepC _[_]↝₁_ ⟧ R pq
    ×
  ⟦ One-sided.StepC _[_]↝₂_ ⟧ (R ⁻¹) (swap pq)  ↝⟨ inverse-ext? (λ ext → ⟦⟷⟧↔ ext (One-sided.StepC _[_]↝₁_) (One-sided.StepC _[_]↝₂_)) ext ⟩□

  ⟦ StepC ⟧ R pq                                □
  where
  lemma : _ ↔ _
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ s → One-sided.Step.⟨ Step.left-to-right s ⟩
                     , One-sided.Step.⟨ Step.right-to-left s ⟩
        ; from = λ { (lr , rl) → Step.⟨ One-sided.Step.challenge lr
                                      , One-sided.Step.challenge rl
                                      ⟩
                   }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }

-- A variant of the previous lemma, stated for StepC′ instead of
-- StepC.

Step↔StepC′ :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  Step R pq ↝[ k ] ⟦ StepC′ ⟧ R pq
Step↔StepC′ {R = R} {pq} ext =
  Step R pq        ↝⟨ Step↔StepC   ext ⟩
  ⟦ StepC  ⟧ R pq  ↝⟨ StepC↔StepC′ ext ⟩□
  ⟦ StepC′ ⟧ R pq  □

module StepC {r} {R : Rel₂ r Proc} {p q} where

  -- A "constructor".

  ⟨_,_⟩ :
    (∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′ × R (p′ , q′)) →
    (∀ {q′ μ} → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′ × R (p′ , q′)) →
    ⟦ StepC ⟧ R (p , q)
  ⟨ lr , rl ⟩ = _⇔_.to (Step↔StepC _) Step.⟨ lr , rl ⟩

  -- Some "projections".

  left-to-right :
    ⟦ StepC ⟧ R (p , q) →
    ∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′ × R (p′ , q′)
  left-to-right = Step.left-to-right ∘ _⇔_.from (Step↔StepC _)

  right-to-left :
    ⟦ StepC ⟧ R (p , q) →
    ∀ {q′ μ} → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′ × R (p′ , q′)
  right-to-left = Step.right-to-left ∘ _⇔_.from (Step↔StepC _)

open Temporarily-private public