{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

-------------------------------------------------
-- direct proof that bisimulation is symmetric --
-------------------------------------------------

open import dtt
open import equality
open import Bisimulation


module Bisimulation.symmetry {I : Set} (w : IS I) where

private
  module symmetry (R : Pow (states w)) (coalg : R ⊂ Φ w R) where
    open IS w renaming (Command to A ; Response to D ; next to n)

    -- the converse relation
    private R~ : Pow (states w)
    R~ ( i , ( T₁ , T₂ ) ) = R ( i , ( T₂ , T₁ ) )

    private lemma : {i : I} {a₁ a₂ : A i}
             {nT₁ : (d₁ : D i a₁) → ν w (n a₁ d₁)}
             {nT₂ : (d₂ : D i a₂) → ν w (n a₂ d₂)}
             (eq : a₂ ≡ a₁) →
             (r₂ : Π (D i a₂)        λ d₂ →
                  let d₁ : D i a₁
                      d₁ = transport-d w eq d₂
                      eqi : n a₂ d₂ ≡ n a₁ d₁
                      eqi = transport-n w eq d₂
                      newT₁ : ν w (n a₂ d₂)
                      newT₁ = transport (ν w) (sym eqi) (nT₁ d₁) in
                   R ( n a₂ d₂ , ( nT₂ d₂ , newT₁ ) )) →
             (d₁ : D i a₁) →
             let newT₁ : ν w (n a₁ d₁)
                 newT₁ = nT₁ d₁
                 d₂ : D i a₂
                 d₂ = transport-d w (sym eq) d₁
                 newT₂' : ν w (n a₂ d₂)
                 newT₂' = nT₂ d₂
                 eqi : n a₁ d₁ ≡ n a₂ d₂
                 eqi = transport-n w (sym eq) d₁
                 newT₂ : ν w (n a₁ d₁)
                 newT₂ = transport (ν w) (sym eqi) newT₂' in
             R ( n a₁ d₁ , ( newT₂ , newT₁ ) )
    lemma refl r d₁ = r d₁

    coalg-sym : R~ ⊂ Φ w R~
    coalg-sym {( i , ( T₁ , T₂ ) )} r =
      let a₁ : A i
          a₁ = fst (νElim T₁)
          a₂ : A i
          a₂ = fst (νElim T₂) in
      let eq : a₁ ≡ a₂
          eq = sym (fst (coalg r)) in
      ( eq ,  (λ d₁ →
          lemma {i} {a₁} {a₂} {snd (νElim T₁)} {snd (νElim T₂)} (fst (coalg r)) (snd (coalg r)) d₁) )

----------------------------------------
-- proof that bisimilarity is reflexive:
symmetry : {i : I} {T₁ T₂ : ν w i} → T₁ ≈ T₂ → T₂ ≈ T₁
symmetry {T₁} {T₂} B =
        let open Bisimilar B in
        record { carrier = λ s → carrier ( (fst s) , ( (snd (snd s)) , (fst (snd s)) ) );
                 coalg   = symmetry.coalg-sym carrier coalg;
                 init    = init }