```------------------------------------------------------------------------
-- 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.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.Weak.Alternative.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Bisimilarity.Weak.Equivalent
open import Equational-reasoning

open import Bisimilarity delay-monad using ([_]_∼_)
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 _ , _ =

... | 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 _ , _ =

...   | 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′)
```