{-# OPTIONS --sized-types #-}
open import Prelude
module Delay-monad.Bisimilarity.Alternative {a} {A : Type a} where
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size
import Extensionality equality-with-J as E
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Termination
infix 4 _≈₂_
_≈₂_ : Delay A ∞ → Delay A ∞ → Type a
x ≈₂ y = ∀ z → x ⇓ z ⇔ y ⇓ z
≈₂-propositional :
E.Extensionality a a →
Is-set A → ∀ {x y} → Is-proposition (x ≈₂ y)
≈₂-propositional ext A-set =
Π-closure ext 1 λ _ →
⇔-closure ext 1 (Terminates-propositional A-set)
(Terminates-propositional A-set)
infix 4 [_]_≈₃_ [_]_≈₃′_ _≈₃_
mutual
data [_]_≈₃_ (i : Size) : Delay A ∞ → Delay A ∞ → Type a where
both-terminate : ∀ {x y v} → x ⇓ v → y ⇓ v → [ i ] x ≈₃ y
later : ∀ {x y} →
[ i ] force x ≈₃′ force y →
[ i ] later x ≈₃ later y
record [_]_≈₃′_ (i : Size) (x y : Delay A ∞) : Type a where
coinductive
field
force : {j : Size< i} → [ j ] x ≈₃ y
open [_]_≈₃′_ public
_≈₃_ : Delay A ∞ → Delay A ∞ → Type a
_≈₃_ = [ ∞ ]_≈₃_
¬-≈₃-propositional : A → ¬ (∀ {x y} → Is-proposition (x ≈₃ y))
¬-≈₃-propositional x =
(∀ {x y} → Is-proposition (x ≈₃ y)) ↝⟨ (λ prop → prop) ⟩
Is-proposition (y ≈₃ y) ↝⟨ (_$ _) ∘ (_$ _) ⟩
proof₁ ≡ proof₂ ↝⟨ (λ ()) ⟩□
⊥ □
where
y : Delay A ∞
y = later λ { .force → now x }
proof₁ : y ≈₃ y
proof₁ = both-terminate (laterʳ now) (laterʳ now)
proof₂ : y ≈₃ y
proof₂ = later λ { .force → both-terminate now now }
≈⇔≈₃ : ∀ {i x y} → [ i ] x ≈ y ⇔ [ i ] x ≈₃ y
≈⇔≈₃ = record { to = to; from = from }
where
mutual
laterˡ′ : ∀ {i x x′ y} →
x′ ≡ force x →
[ i ] x′ ≈₃ y →
[ i ] later x ≈₃ y
laterˡ′ eq (both-terminate x⇓ y⇓) = both-terminate
(laterʳ (subst (_⇓ _) eq x⇓))
y⇓
laterˡ′ eq (later p) = later (laterˡ″ eq p)
laterˡ″ : ∀ {i x x′ y} →
later x′ ≡ x →
[ i ] force x′ ≈₃′ y →
[ i ] x ≈₃′ y
force (laterˡ″ refl p) = laterˡ′ refl (force p)
mutual
laterʳ′ : ∀ {i x y y′} →
y′ ≡ force y →
[ i ] x ≈₃ y′ →
[ i ] x ≈₃ later y
laterʳ′ eq (both-terminate x⇓ y⇓) = both-terminate
x⇓
(laterʳ (subst (_⇓ _) eq y⇓))
laterʳ′ eq (later p) = later (laterʳ″ eq p)
laterʳ″ : ∀ {i x y y′} →
later y′ ≡ y →
[ i ] x ≈₃′ force y′ →
[ i ] x ≈₃′ y
force (laterʳ″ refl p) = laterʳ′ refl (force p)
to : ∀ {i x y} → [ i ] x ≈ y → [ i ] x ≈₃ y
to now = both-terminate now now
to (later p) = later λ { .force → to (force p) }
to (laterˡ p) = laterˡ′ refl (to p)
to (laterʳ p) = laterʳ′ refl (to p)
from⇓ : ∀ {i x y v} → x ⇓ v → y ⇓ v → [ i ] x ≈ y
from⇓ now now = now
from⇓ p (laterʳ q) = laterʳ (from⇓ p q)
from⇓ (laterʳ p) q = laterˡ (from⇓ p q)
from : ∀ {i x y} → [ i ] x ≈₃ y → [ i ] x ≈ y
from (both-terminate x⇓v y⇓v) = from⇓ x⇓v y⇓v
from (later p) = later λ { .force → from (force p) }