{-# OPTIONS --sized-types #-}
open import Prelude
module Bisimilarity.Delay-monad {a} {A : Type a} where
open import Delay-monad
open import Delay-monad.Bisimilarity as D using (force)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Labelled-transition-system
open import Labelled-transition-system.Delay-monad A
open import Bisimilarity delay-monad
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
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 })
⟩
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) }
indirect→direct : ∀ {i} x y → [ i ] x ∼ y → D.[ i ] x ∼ y
indirect→direct (now x) (now y) nx∼ny
with left-to-right nx∼ny now
... | _ , now , _ = D.now
indirect→direct (later x) (later y) lx∼ly
with left-to-right lx∼ly later
... | _ , later , x∼′y = D.later λ { .force →
indirect→direct _ _ (force x∼′y) }
indirect→direct (now x) (later y) nx∼ly
with left-to-right nx∼ly now
... | _ , () , _
indirect→direct (later x) (now y) lx∼ny
with left-to-right lx∼ny later
... | _ , () , _
direct⇔indirect : ∀ {i x y} → D.[ i ] x ∼ y ⇔ [ i ] x ∼ y
direct⇔indirect = record
{ to = direct→indirect
; from = indirect→direct _ _
}