```------------------------------------------------------------------------
-- Some results related to expansion for the delay monad
------------------------------------------------------------------------

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

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

open import Delay-monad.Expansion as D using (force)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

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

open import Equational-reasoning
import Expansion.Equational-reasoning-instances

open import Bisimilarity delay-monad using ([_]_∼_)

------------------------------------------------------------------------
-- The direct and the indirect definitions of expansion are pointwise
-- logically equivalent

-- Emulations of the constructors D.later and D.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 → _ , done _ , convert {a = a} x≳y })
, Σ-map id (Σ-map later[]⇒ id) ∘ right-to-left x≳y
⟩

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

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

-- If x makes a sequence of zero or more silent transitions to y, then
-- x is an expansion of y.

⇒→≳ : ∀ {i x y} → x ⇒ y → D.[ i ] x ≳ y
⇒→≳ done               = D.reflexive _
⇒→≳ (step _  later tr) = D.laterˡ (⇒→≳ tr)
⇒→≳ (step () now   tr)

-- If x makes a non-silent transition with the label y, then x is an
-- expansion of now y.

[just]⟶→≳now : ∀ {i x x′ y} → x [ just y ]⟶ x′ → D.[ i ] x ≳ now y
[just]⟶→≳now now = D.reflexive _

[just]⇒→≳now : ∀ {i x x′ y} → x [ just y ]⇒ x′ → D.[ i ] x ≳ now y
[just]⇒→≳now (steps tr now _) = ⇒→≳ tr

[just]⇒̂→≳now : ∀ {i x x′ y} → x [ just y ]⇒̂ x′ → D.[ i ] x ≳ now y
[just]⇒̂→≳now (silent () _)
[just]⇒̂→≳now (non-silent _ tr) = [just]⇒→≳now tr

[just]⟶̂→≳now : ∀ {i x x′ y} → x [ just y ]⟶̂ x′ → D.[ i ] x ≳ now y
[just]⟶̂→≳now (done ())
[just]⟶̂→≳now (step tr) = [just]⇒̂→≳now (⟶→⇒̂ tr)

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

indirect→direct : ∀ {i} x y → [ i ] x ≳ y → D.[ 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′)  ↝⟨ sym ∘ [just]⟶̂→≡now ∘ proj₁ ∘ proj₂ ⟩
now x ≡ y                                        ↝⟨ (λ { refl → D.reflexive _ }) ⟩□
D.[ 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)  ↝⟨ [just]⇒→≳now ∘ proj₁ ∘ proj₂ ⟩□
D.[ i ] x ≳ now y                                □

indirect→direct (later x) (later y) lx≳ly =
case left-to-right lx≳ly later of λ where
(_ , step later , x≳′y) → D.later λ { .force {j} →
indirect→direct _ _
(force x≳′y {j = j}) }
(_ , done _     , x≳′ly) →
let x′ , lx⇒x′ , x′≳′y = right-to-left lx≳ly later
in lemma x≳′ly ([]⇒→⇒ _ lx⇒x′) x′≳′y
where
indirect→direct′ : ∀ {i x x′ y} →
x ⇒ x′ → [ i ] x′ ≳ y → D.[ i ] x ≳ y
indirect→direct′ done               p = indirect→direct _ _ p
indirect→direct′ (step _  later tr) p = D.laterˡ
(indirect→direct′ tr p)
indirect→direct′ (step () now   _)

lemma :
∀ {i x x′} →
[ i ] force x ≳′ later y →
later x ⇒ x′ → [ i ] x′ ≳′ force y →
D.[ i ] later x ≳ later y
lemma x≳′ly done lx≳′y =
D.later λ { .force →
D.laterˡʳ⁻¹
(indirect→direct _ _ (force lx≳′y))
(indirect→direct _ _ (force x≳′ly)) }
lemma x≳′ly (step _ later x⇒x′) x′≳′y =
D.later λ { .force →
indirect→direct′ x⇒x′ (force x′≳′y) }

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

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

------------------------------------------------------------------------
-- Some non-existence results

Laterˡ⁻¹′ = ∀ {x} →
later (record { force = now x }) ≳
later (record { force = now x }) →
now x ≳ later (record { force = now x })

laterˡ⁻¹′⇔uninhabited : Laterˡ⁻¹′ ⇔ ¬ A
laterˡ⁻¹′⇔uninhabited =
Laterˡ⁻¹′    ↝⟨ inverse \$ implicit-∀-cong _ \$ →-cong _ direct⇔indirect direct⇔indirect ⟩
D.Laterˡ⁻¹′  ↝⟨ D.laterˡ⁻¹′⇔uninhabited ⟩□
¬ A          □

Laterˡ⁻¹ = ∀ {x y} → later x ≳ y → force x ≳ y

laterˡ⁻¹⇔uninhabited : Laterˡ⁻¹ ⇔ ¬ A
laterˡ⁻¹⇔uninhabited =
Laterˡ⁻¹    ↝⟨ inverse \$ implicit-∀-cong _ \$ implicit-∀-cong _ \$ →-cong _ direct⇔indirect direct⇔indirect ⟩
D.Laterˡ⁻¹  ↝⟨ D.laterˡ⁻¹⇔uninhabited ⟩□
¬ A         □

Laterʳ⁻¹-∼≳ =
∀ {i x} →
[ i ] never ∼ later (record { force = now x }) →
[ i ] never ≳ now x

size-preserving-laterʳ⁻¹-∼≳⇔uninhabited : Laterʳ⁻¹-∼≳ ⇔ ¬ A
size-preserving-laterʳ⁻¹-∼≳⇔uninhabited =
Laterʳ⁻¹-∼≳    ↝⟨ inverse \$ implicit-∀-cong _ \$ implicit-∀-cong _ \$ →-cong _ SD.direct⇔indirect direct⇔indirect ⟩
D.Laterʳ⁻¹-∼≳  ↝⟨ D.size-preserving-laterʳ⁻¹-∼≳⇔uninhabited ⟩□
¬ A            □

Laterʳ⁻¹ = ∀ {i x y} → [ i ] x ≳ later y → [ i ] x ≳ force y

size-preserving-laterʳ⁻¹⇔uninhabited : Laterʳ⁻¹ ⇔ ¬ A
size-preserving-laterʳ⁻¹⇔uninhabited =
Laterʳ⁻¹    ↝⟨ inverse \$ implicit-∀-cong _ \$ implicit-∀-cong _ \$ implicit-∀-cong _ \$ →-cong _ direct⇔indirect direct⇔indirect ⟩
D.Laterʳ⁻¹  ↝⟨ D.size-preserving-laterʳ⁻¹⇔uninhabited ⟩□
¬ A         □

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) ⟩
D.Transitivity-∼≳ˡ  ↝⟨ D.size-preserving-transitivity-∼≳ˡ⇔uninhabited ⟩□
¬ A                 □

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) ⟩
D.Transitivityˡ  ↝⟨ D.size-preserving-transitivityˡ⇔uninhabited ⟩□
¬ A              □

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 _ direct⇔indirect \$ →-cong _ direct⇔indirect direct⇔indirect ⟩
D.Transitivity  ↝⟨ D.size-preserving-transitivity⇔uninhabited ⟩□
¬ A             □
```