------------------------------------------------------------------------
-- Some results about various forms of coinductively defined weak
-- bisimilarity for the delay monad
------------------------------------------------------------------------

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

module Bisimilarity.Weak.Delay-monad {a} {A : Set a} where

open import Delay-monad
import Delay-monad.Expansion as DE
open import Delay-monad.Weak-bisimilarity as DW using (force)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.Delay-monad as SD
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Bisimilarity.Weak.Equivalent
open import Equational-reasoning
import Expansion.Delay-monad as ED
open import Labelled-transition-system.Delay-monad A

open import Bisimilarity delay-monad using ([_]_∼_)
open import Bisimilarity.Weak delay-monad
open import Bisimilarity.Weak.Alternative delay-monad as AW
  using (force)
open import Expansion delay-monad as BE using ([_]_≳_; _≳_)

------------------------------------------------------------------------
-- Several definitions of weak bisimilarity are pointwise logically
-- equivalent

-- Emulations of the constructors DW.later, DW.laterˡ and DW.laterʳ.

later-cong : ∀ {i x y} →
             [ i ] force x ≈′ force y → [ i ] later x ≈ later y
later-cong x≈′y =
  ⟨ (λ { later → _ , ⟶→⇒̂ later , x≈′y })
  , (λ { later → _ , ⟶→⇒̂ later , x≈′y })
  ⟩

laterˡ : ∀ {i x y} → [ i ] force x ≈ y → [ i ] later x ≈ y
laterˡ x≈y =
  ⟨ (λ { later → _ , silent _ done , convert {a = a} x≈y })
  , Σ-map id (Σ-map later⇒̂ id) ∘ right-to-left x≈y
  ⟩

laterʳ : ∀ {i x y} → [ i ] x ≈ force y → [ i ] x ≈ later y
laterʳ x≈y =
  ⟨ Σ-map id (Σ-map later⇒̂ id) ∘ left-to-right x≈y
  , (λ { later → _ , silent _ done , convert {a = a} x≈y })
  ⟩

-- The direct definition of weak bisimilarity is contained in the form
-- of weak bisimilarity obtained from the transition relation.

direct→indirect : ∀ {i x y} →
                  DW.[ i ] x ≈ y → [ i ] x ≈ y
direct→indirect DW.now        = reflexive
direct→indirect (DW.later  p) = later-cong λ { .force →
                                  direct→indirect (force p) }
direct→indirect (DW.laterˡ p) = laterˡ (direct→indirect p)
direct→indirect (DW.laterʳ p) = laterʳ (direct→indirect p)

mutual

  -- The definition of weak bisimilarity obtained from the transition
  -- relation is contained in the direct one.

  indirect→direct : ∀ {i} x y → [ i ] x ≈ y → DW.[ i ] x ≈ y
  indirect→direct {i} (now x) y =
    [ i ] now x ≈ y                                  ↝⟨ (λ p → left-to-right p now) ⟩
    (∃ λ y′ → y [ just x ]⇒̂ y′ × [ i ] now x ≈′ y′)  ↝⟨ DE.≳→≈ ∘ ED.[just]⇒̂→≳now ∘ proj₁ ∘ proj₂ ⟩
    DW.[ i ] y ≈ now x                               ↝⟨ DW.symmetric ⟩□
    DW.[ i ] now x ≈ y                               □

  indirect→direct {i} x (now y) =
    [ i ] x ≈ now y                                  ↝⟨ (λ p → right-to-left p now) ⟩
    (∃ λ x′ → x [ just y ]⇒̂ x′ × [ i ] x′ ≈′ now y)  ↝⟨ DE.≳→≈ ∘ ED.[just]⇒̂→≳now ∘ proj₁ ∘ proj₂ ⟩□
    DW.[ i ] x ≈ now y                               □

  indirect→direct (later x) (later y) lx≈ly
    with left-to-right lx≈ly later

  ... | y′ , non-silent contradiction _ , _ =
    ⊥-elim (contradiction _)

  ... | y′ , silent _ (step _ later y⇒y′) , x≈′y′ =
    DW.later λ { .force →
      indirect→direct′ y⇒y′ (force x≈′y′) }

  ... | y′ , silent _ done , x≈′ly
    with right-to-left lx≈ly later

  ...   | x′ , non-silent contradiction _ , _ =
    ⊥-elim (contradiction _)

  ...   | x′ , silent _ (step _ later x⇒x′) , x′≈′y =
    DW.later λ { .force →
      DW.symmetric $
      indirect→direct′ x⇒x′ $
      symmetric (force x′≈′y) }

  ...   | x′ , silent _ done , lx≈′y =
    DW.later λ { .force →
      DW.laterˡʳ⁻¹
        (indirect→direct _ _ (force lx≈′y))
        (indirect→direct _ _ (force x≈′ly)) }

  private

    -- A lemma used by indirect→direct.

    indirect→direct′ : ∀ {i x y y′} →
                       y ⇒ y′ → [ i ] x ≈ y′ → DW.[ i ] x ≈ y
    indirect→direct′ done               p = indirect→direct _ _ p
    indirect→direct′ (step _  later tr) p = DW.laterʳ (indirect→direct′ tr p)
    indirect→direct′ (step () now   _)

-- The direct definition of weak bisimilarity is logically equivalent
-- to the one obtained from the transition relation.
--
-- TODO: Are the two definitions isomorphic?

direct⇔indirect : ∀ {i x y} → DW.[ i ] x ≈ y ⇔ [ i ] x ≈ y
direct⇔indirect = record
  { to   = direct→indirect
  ; from = indirect→direct _ _
  }

-- The direct definition of weak bisimilarity is logically equivalent
-- to the alternative, coinductive form of weak bisimilarity obtained
-- from the transition relation. Note that this proof is not
-- size-preserving.

direct⇔alternative : ∀ {x y} → x DW.≈ y ⇔ x AW.≈ y
direct⇔alternative {x} {y} =
  x DW.≈ y  ↝⟨ direct⇔indirect ⟩
  x ≈ y     ↝⟨ inverse alternative⇔ ⟩□
  x AW.≈ y  □

------------------------------------------------------------------------
-- A non-existence result for the alternative, coinductive indirect
-- definition of weak bisimilarity

private

  -- If A is uninhabited, then AW._≈_ is trivial.

  uninhabited→trivial : ¬ A → ∀ x y → x AW.≈ y
  uninhabited→trivial =
    ¬ A                 ↝⟨ DW.uninhabited→trivial ⟩
    (∀ x y → x DW.≈ y)  ↝⟨ ∀-cong _ (λ _ → ∀-cong _ λ _ → _⇔_.to direct⇔alternative) ⟩
    (∀ x y → x AW.≈ y)  □

-- One can define a size-preserving "later-cong" function iff A is
-- uninhabited.

Later-cong =
  ∀ {i x y} →
  AW.[ i ] force x ≈′ force y → AW.[ i ] later x ≈ later y

size-preserving-later-cong⇔uninhabited : Later-cong ⇔ ¬ A
size-preserving-later-cong⇔uninhabited = record
  { to   = Later-cong                ↝⟨ (λ later-cong → now≈never (λ {i} → later-cong {i})) ⟩
           (∀ x → now x AW.≈ never)  ↝⟨ ∀-cong _ (λ _ → _⇔_.from direct⇔alternative) ⟩
           (∀ x → now x DW.≈ never)  ↝⟨ (λ hyp → DW.now≉never ∘ hyp) ⟩□
           ¬ A                       □
  ; from = ¬ A                 ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x AW.≈ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
           Later-cong          □
  }
  where

  module _ (later-cong : Later-cong) where

    now≈never : ∀ {i} x → AW.[ i ] now x ≈ never
    now≈never x =
      now x                         ∼⟨ ⇒alternative (laterʳ reflexive) ⟩
      later (λ { .force → now x })  ∼⟨ later-cong (λ { .force → now≈never x }) ⟩■
      never

------------------------------------------------------------------------
-- Some non-existence results for the standard indirect definition of
-- weak bisimilarity

-- There is a transitivity proof that takes weak bisimilarity and
-- expansion to expansion iff A is uninhabited.

Transitivity-≈≳≳ = {x y z : Delay A ∞} → x ≈ y → y ≳ z → x ≳ z
Transitivity-≳≈≳ = {x y z : Delay A ∞} → x ≳ y → y ≈ z → x ≳ z

transitive-≈≳≳⇔uninhabited : Transitivity-≈≳≳ ⇔ ¬ A
transitive-≈≳≳⇔uninhabited =
  Transitivity-≈≳≳     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect ED.direct⇔indirect) ⟩
  DE.Transitivity-≈≳≳  ↝⟨ DE.transitive-≈≳≳⇔uninhabited ⟩□
  ¬ A                  □

transitive-≳≈≳⇔uninhabited : Transitivity-≳≈≳ ⇔ ¬ A
transitive-≳≈≳⇔uninhabited =
  Transitivity-≳≈≳     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ ED.direct⇔indirect (→-cong _ direct⇔indirect ED.direct⇔indirect) ⟩
  DE.Transitivity-≳≈≳  ↝⟨ DE.transitive-≳≈≳⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity proof that preserves the size of the second
-- argument iff A is uninhabited.

Transitivityʳ =
  ∀ {i} {x y z : Delay A ∞} →
  x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivityʳ⇔uninhabited : Transitivityʳ ⇔ ¬ A
size-preserving-transitivityʳ⇔uninhabited =
  Transitivityʳ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                       →-cong _ direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DW.Transitivityʳ  ↝⟨ DW.size-preserving-transitivityʳ⇔uninhabited ⟩□
  ¬ A               □

-- There is a transitivity proof that preserves the size of the first
-- argument iff A is uninhabited.

Transitivityˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivityˡ⇔uninhabited : Transitivityˡ ⇔ ¬ A
size-preserving-transitivityˡ⇔uninhabited =
  Transitivityˡ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                       →-cong _ direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DW.Transitivityˡ  ↝⟨ DW.size-preserving-transitivityˡ⇔uninhabited ⟩□
  ¬ A               □

-- There is a transitivity proof that preserves the size of the second
-- argument, a strong bisimilarity, iff A is uninhabited.

Transitivity-≈∼ʳ =
  ∀ {i} {x y z : Delay A ∞} →
  x ≈ y → [ i ] y ∼ z → [ i ] x ≈ z

size-preserving-transitivity-≈∼ʳ⇔uninhabited : Transitivity-≈∼ʳ ⇔ ¬ A
size-preserving-transitivity-≈∼ʳ⇔uninhabited =
  Transitivity-≈∼ʳ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect $ →-cong _ SD.direct⇔indirect direct⇔indirect ⟩
  DW.Transitivity-≈∼ʳ  ↝⟨ DW.size-preserving-transitivity-≈∼ʳ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity proof that preserves the size of the first
-- argument, a strong bisimilarity, iff A is uninhabited.

Transitivity-∼≈ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ∼ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-∼≈ˡ⇔uninhabited : Transitivity-∼≈ˡ ⇔ ¬ A
size-preserving-transitivity-∼≈ˡ⇔uninhabited =
  Transitivity-∼≈ˡ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ SD.direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DW.Transitivity-∼≈ˡ  ↝⟨ DW.size-preserving-transitivity-∼≈ˡ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity-like proof that preserves the size of the
-- first argument, an expansion, iff A is uninhabited.

Transitivity-≳≈ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈ˡ⇔uninhabited : Transitivity-≳≈ˡ ⇔ ¬ A
size-preserving-transitivity-≳≈ˡ⇔uninhabited =
  Transitivity-≳≈ˡ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ ED.direct⇔indirect (→-cong _ direct⇔indirect direct⇔indirect) ⟩
  DE.Transitivity-≳≈ˡ  ↝⟨ DE.size-preserving-transitivity-≳≈ˡ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity-like proof that takes an expansion as the
-- first argument, and preserves the size of both arguments, iff A is
-- uninhabited.

Transitivity-≳≈ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈⇔uninhabited : Transitivity-≳≈ ⇔ ¬ A
size-preserving-transitivity-≳≈⇔uninhabited =
  Transitivity-≳≈     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ ED.direct⇔indirect (→-cong _ direct⇔indirect direct⇔indirect) ⟩
  DE.Transitivity-≳≈  ↝⟨ DE.size-preserving-transitivity-≳≈⇔uninhabited ⟩□
  ¬ A                 □

-- There is a transitivity-like proof that preserves the size of the
-- second argument, an expansion (with the arguments swapped), iff A
-- is uninhabited.

Transitivity-≈≲ʳ =
  ∀ {i} {x y z : Delay A ∞} →
  x ≈ y → [ i ] z ≳ y → [ i ] x ≈ z

size-preserving-transitivity-≈≲ʳ⇔uninhabited : Transitivity-≈≲ʳ ⇔ ¬ A
size-preserving-transitivity-≈≲ʳ⇔uninhabited =
  Transitivity-≈≲ʳ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect direct⇔indirect) ⟩
  DE.Transitivity-≈≲ʳ  ↝⟨ DE.size-preserving-transitivity-≈≲ʳ⇔uninhabited ⟩□
  ¬ A                  □

-- There is a transitivity-like proof that takes an expansion (with
-- the arguments swapped) as the second argument, and preserves the
-- size of both arguments, iff A is uninhabited.

Transitivity-≈≲ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → [ i ] z ≳ y → [ i ] x ≈ z

size-preserving-transitivity-≈≲⇔uninhabited : Transitivity-≈≲ ⇔ ¬ A
size-preserving-transitivity-≈≲⇔uninhabited =
  Transitivity-≈≲     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect direct⇔indirect) ⟩
  DE.Transitivity-≈≲  ↝⟨ DE.size-preserving-transitivity-≈≲⇔uninhabited ⟩□
  ¬ A                 □

-- There is a transitivity-like proof that preserves the size of the
-- first argument, and takes an expansion as the second argument, iff
-- A is uninhabited.

Transitivity-≈≳ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≈ y → y ≳ z → [ i ] x ≈ z

size-preserving-transitivity-≈≳ˡ⇔uninhabited : Transitivity-≈≳ˡ ⇔ ¬ A
size-preserving-transitivity-≈≳ˡ⇔uninhabited =
  Transitivity-≈≳ˡ     ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ direct⇔indirect (→-cong _ ED.direct⇔indirect direct⇔indirect) ⟩
  DE.Transitivity-≈≳ˡ  ↝⟨ DE.size-preserving-transitivity-≈≳ˡ⇔uninhabited ⟩□
  ¬ A                  □

------------------------------------------------------------------------
-- A non-existence result for both indirect definitions of weak
-- bisimilarity

-- The function ⇒alternative translating from the standard indirect
-- definition of weak bisimilarity to the alternative, coinductive one
-- can be made size-preserving iff A is uninhabited.

size-preserving-⇒alternative⇔uninhabited :
  (∀ {i p q} → [ i ] p ≈ q → AW.[ i ] p ≈ q) ⇔ ¬ A
size-preserving-⇒alternative⇔uninhabited = record
  { to =
      (∀ {i p q} → [ i ] p ≈ q → AW.[ i ] p ≈ q)  ↝⟨ (λ ⇒alternative x≈y y≈z →
                                                        alternative⇒ (transitive {a = a} (⇒alternative x≈y) (⇒alternative y≈z))) ⟩
      Transitivityʳ                               ↝⟨ _⇔_.to size-preserving-transitivityʳ⇔uninhabited ⟩□
      ¬ A                                         □
  ; from =
      ¬ A                                         ↝⟨ uninhabited→trivial ⟩
      (∀ x y → x AW.≈ y)                          ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
      (∀ {i p q} → [ i ] p ≈ q → AW.[ i ] p ≈ q)  □
  }

------------------------------------------------------------------------
-- More lemmas

-- If x and y both make non-silent transitions of the same kind,
-- then they are weakly bisimilar.

⟶-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⟶ x′ → y [ μ ]⟶ y′ → x ≈ y
⟶-with-equal-labels→≈ _  now   now = reflexive
⟶-with-equal-labels→≈ ¬s later _   = ⊥-elim (¬s _)

[]⇒-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⇒ x′ → y [ μ ]⇒ y′ → x ≈ y
[]⇒-with-equal-labels→≈
  {x = x} {y = y} ¬s
  (steps {p′ = x′} x⇒x′ x′⟶x″ x″⇒x‴)
  (steps {p′ = y′} y⇒y′ y′⟶y″ y″⇒y‴) =

  x   ∼⟨ direct→indirect (DE.≳→≈ (ED.⇒→≳ x⇒x′)) ⟩
  x′  ∼⟨ ⟶-with-equal-labels→≈ ¬s x′⟶x″ y′⟶y″ ⟩
  y′  ∼⟨ symmetric (direct→indirect (DE.≳→≈ (ED.⇒→≳ y⇒y′))) ⟩■
  y

⇒̂-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⇒̂ x′ → y [ μ ]⇒̂ y′ → x ≈ y
⇒̂-with-equal-labels→≈ ¬s (non-silent _ x⇒x′) (non-silent _ y⇒y′) =
  []⇒-with-equal-labels→≈ ¬s x⇒x′ y⇒y′
⇒̂-with-equal-labels→≈ ¬s   (silent s _) = ⊥-elim (¬s s)
⇒̂-with-equal-labels→≈ ¬s _ (silent s _) = ⊥-elim (¬s s)

⟶̂-with-equal-labels→≈ :
  ∀ {x x′ y y′ μ} →
  ¬ Silent μ → x [ μ ]⟶̂ x′ → y [ μ ]⟶̂ y′ → x ≈ y
⟶̂-with-equal-labels→≈ ¬s x⟶̂x′ y⟶̂y′ =
  ⇒̂-with-equal-labels→≈ ¬s (⟶̂→⇒̂ x⟶̂x′) (⟶̂→⇒̂ y⟶̂y′)