{-# OPTIONS --without-K #-}
module Delay-monad.Alternative.Equivalence {a} {A : Set a} where
open import Equality.Propositional
open import Interval
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (↑)
open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Delay-monad as D hiding (Delay)
open import Delay-monad.Alternative
open import Delay-monad.Alternative.Properties
open import Delay-monad.Strong-bisimilarity as Strong-bisimilarity
module Delay⇔Delay where
mutual
to₁ : (ℕ → Maybe A) → D.Delay A ∞
to₁ f = to′ (f 0)
module To where
to′ : Maybe A → D.Delay A ∞
to′ (just x) = now x
to′ nothing =
later (∞to₁ (f ∘ suc))
∞to₁ : (ℕ → Maybe A) → D.∞Delay A ∞
force (∞to₁ x) = to₁ x
to : Delay A → D.Delay A ∞
to = to₁ ∘ proj₁
from : D.Delay A ∞ → Delay A
from = λ x → from₁ x , from₂ x
where
from₁ : D.Delay A ∞ → ℕ → Maybe A
from₁ (now x) _ = just x
from₁ (later x) zero = nothing
from₁ (later x) (suc n) = from₁ (force x) n
from₂ : ∀ x → Increasing (from₁ x)
from₂ (now x) _ = inj₁ refl
from₂ (later x) zero = proj₁ LE-nothing-contractible
from₂ (later x) (suc n) = from₂ (force x) n
Delay⇔Delay : Delay A ⇔ D.Delay A ∞
Delay⇔Delay = record { to = Delay⇔Delay.to; from = Delay⇔Delay.from }
Delay↠Delay : D.Delay A ∞ ↠ Delay A
Delay↠Delay = record
{ logical-equivalence = inverse Delay⇔Delay
; right-inverse-of = from∘to
}
where
open Delay⇔Delay
from∘to : ∀ x → from (to x) ≡ x
from∘to x = Σ-≡,≡→≡
(ext (proj₁∘from∘to x))
(ext λ n →
subst Increasing
(ext (proj₁∘from∘to x))
(proj₂ (from (to x)))
n ≡⟨ sym $ push-subst-application (ext (proj₁∘from∘to x)) (flip Increasing-at) ⟩
subst (Increasing-at n)
(ext (proj₁∘from∘to x))
(proj₂ (from (to x)) n) ≡⟨ uncurry proj₂∘from∘to x n _ refl ⟩∎
proj₂ x n ∎)
where
proj₁∘from∘to′ :
(g : ℕ → Maybe A) →
Increasing g →
∀ x → g 0 ≡ x → ∀ n →
proj₁ (from (To.to′ g x)) n ≡ g n
proj₁∘from∘to′ g g-inc (just x) g0↓x n = sym $ ↓-upwards-closed₀ g-inc g0↓x n
proj₁∘from∘to′ g g-inc nothing g0↑ zero = sym g0↑
proj₁∘from∘to′ g g-inc nothing g0↑ (suc n) =
proj₁∘from∘to′ (g ∘ suc) (g-inc ∘ suc) _ refl n
proj₁∘from∘to :
(x : Delay A) →
∀ n → proj₁ (from (to x)) n ≡ proj₁ x n
proj₁∘from∘to (g , g-inc) = proj₁∘from∘to′ g g-inc (g 0) refl
↓-lemma :
(g : ℕ → Maybe A) →
(g-increasing : Increasing g) →
∀ n x (g0↓x : g 0 ↓ x) p → p ≡ g-increasing 0 →
subst (Increasing-at n)
(ext (sym ∘ ↓-upwards-closed₀ g-increasing g0↓x))
(inj₁ refl)
≡
g-increasing n
↓-lemma g _ _ x g0↓x (inj₂ (g0↑ , _)) _ =
⊥-elim $ ⊎.inj₁≢inj₂ (
nothing ≡⟨ sym g0↑ ⟩
g 0 ≡⟨ g0↓x ⟩∎
just x ∎)
↓-lemma g g-inc zero x g0↓x (inj₁ g0≡g1) ≡g-inc0 =
subst (Increasing-at zero)
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
(inj₁ refl) ≡⟨ push-subst-inj₁
{y≡z = ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x)}
(λ f → f 0 ≡ f 1) (λ f → f 0 ↑ × ¬ f 1 ↑) ⟩
inj₁ (subst (λ f → f 0 ≡ f 1)
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
refl) ≡⟨ cong inj₁ lemma ⟩
inj₁ g0≡g1 ≡⟨ ≡g-inc0 ⟩∎
g-inc zero ∎
where
eq = ↓-upwards-closed₀ g-inc g0↓x
lemma =
subst (λ f → f 0 ≡ f 1) (ext (sym ∘ eq)) refl ≡⟨ subst-in-terms-of-trans-and-cong {x≡y = ext (sym ∘ eq)} ⟩
trans (sym (cong (_$ 0) (ext (sym ∘ eq))))
(trans refl (cong (_$ 1) (ext (sym ∘ eq)))) ≡⟨ cong (trans (sym (cong (_$ 0) (ext (sym ∘ eq))))) $
trans-reflˡ (cong (_$ 1) (ext (sym ∘ eq))) ⟩
trans (sym (cong (_$ 0) (ext (sym ∘ eq))))
(cong (_$ 1) (ext (sym ∘ eq))) ≡⟨ cong₂ (λ p q → trans (sym p) q) (cong-ext (sym ∘ eq)) (cong-ext (sym ∘ eq)) ⟩
trans (sym $ sym $ eq 0) (sym $ eq 1) ≡⟨ cong (λ eq′ → trans eq′ (sym $ eq 1)) $ sym-sym _ ⟩
trans (eq 0) (sym $ eq 1) ≡⟨⟩
trans g0↓x (sym $ ↓.step g-inc g0↓x (g-inc 0)) ≡⟨ cong (λ eq′ → trans g0↓x (sym $ ↓.step g-inc g0↓x eq′)) $ sym $ ≡g-inc0 ⟩
trans g0↓x (sym $ ↓.step g-inc g0↓x (inj₁ g0≡g1)) ≡⟨⟩
trans g0↓x (sym $ trans (sym g0≡g1) g0↓x) ≡⟨ cong (trans g0↓x) $ sym-trans (sym g0≡g1) g0↓x ⟩
trans g0↓x (trans (sym g0↓x) (sym (sym g0≡g1))) ≡⟨ trans--[trans-sym] _ _ ⟩
sym (sym g0≡g1) ≡⟨ sym-sym _ ⟩∎
g0≡g1 ∎
↓-lemma g g-inc (suc n) x g0↓x (inj₁ g0≡g1) ≡g-inc0 =
subst (Increasing-at (suc n))
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
(inj₁ refl) ≡⟨⟩
subst (Increasing-at n ∘ (_∘ suc))
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
(inj₁ refl) ≡⟨ subst-∘ (Increasing-at n) (_∘ suc)
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x)) ⟩
subst (Increasing-at n)
(cong (_∘ suc)
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x)))
(inj₁ refl) ≡⟨ cong (λ eq → subst (Increasing-at n) eq _) $
cong-pre-∘-ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x) ⟩
subst (Increasing-at n)
(ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x ∘ suc))
(inj₁ refl) ≡⟨⟩
subst (Increasing-at n)
(ext (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
(↓.step g-inc g0↓x (g-inc 0))))
(inj₁ refl) ≡⟨ cong (λ p → subst (Increasing-at n)
(ext (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
(↓.step g-inc g0↓x p)))
(inj₁ refl))
(sym ≡g-inc0) ⟩
subst (Increasing-at n)
(ext (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
(↓.step g-inc g0↓x (inj₁ g0≡g1))))
(inj₁ refl) ≡⟨⟩
subst (Increasing-at n)
(ext (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
(trans (sym g0≡g1) g0↓x)))
(inj₁ refl) ≡⟨ ↓-lemma (g ∘ suc) (g-inc ∘ suc) n _ _ _ refl ⟩∎
g-inc (suc n) ∎
proj₂∘from∘to :
(g : ℕ → Maybe A) →
(g-increasing : Increasing g) →
∀ n y (g0≡y : g 0 ≡ y) →
subst (Increasing-at n)
(ext (proj₁∘from∘to′ g g-increasing y g0≡y))
(proj₂ (from (To.to′ g y)) n)
≡
g-increasing n
proj₂∘from∘to g g-inc n (just y) g0↓y =
↓-lemma g g-inc n y g0↓y _ refl
proj₂∘from∘to g g-inc zero nothing g0↑ =
_⇔_.to propositional⇔irrelevant
( $⟨ mono₁ 0 LE-nothing-contractible ⟩
Is-proposition (LE nothing (g 1)) ↝⟨ subst (λ x → Is-proposition (LE x (g 1))) (sym g0↑) ⟩□
Is-proposition (LE (g 0) (g 1)) □)
_ _
proj₂∘from∘to g g-inc (suc n) nothing g0↑ =
subst (Increasing-at (suc n))
(ext (proj₁∘from∘to′ g g-inc nothing g0↑))
(proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n) ≡⟨⟩
subst (Increasing-at n ∘ (_∘ suc))
(ext (proj₁∘from∘to′ g g-inc nothing g0↑))
(proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n) ≡⟨ subst-∘ (Increasing-at n) (_∘ suc)
(ext (proj₁∘from∘to′ g g-inc nothing g0↑)) ⟩
subst (Increasing-at n)
(cong (_∘ suc) (ext (proj₁∘from∘to′ g g-inc nothing g0↑)))
(proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n) ≡⟨ cong (λ eq → subst (Increasing-at n) eq
(proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)) $
cong-pre-∘-ext (proj₁∘from∘to′ g g-inc nothing g0↑) ⟩
subst (Increasing-at n)
(ext (proj₁∘from∘to′ g g-inc nothing g0↑ ∘ suc))
(proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n) ≡⟨⟩
subst (Increasing-at n)
(ext (proj₁∘from∘to′ (g ∘ suc) (g-inc ∘ suc) _ refl))
(proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n) ≡⟨ proj₂∘from∘to (g ∘ suc) (g-inc ∘ suc) n _ refl ⟩∎
g-inc (suc n) ∎
Delay↔Delay : Strong-bisimilarity.Extensionality a →
Delay A ↔ D.Delay A ∞
Delay↔Delay delay-ext = record
{ surjection = record
{ logical-equivalence = Delay⇔Delay
; right-inverse-of = delay-ext ∘ to∘from
}
; left-inverse-of = _↠_.right-inverse-of Delay↠Delay
}
where
open Delay⇔Delay
mutual
to∘from : ∀ x → to (from x) ∼ x
to∘from (now x) = now-cong
to∘from (later x) = later-cong (∞to∘from (force x))
∞to∘from : ∀ x → to (from x) ∞∼ x
force (∞to∘from x) = to∘from x
→↠Delay-coinductive : Strong-bisimilarity.Extensionality a →
(ℕ → Maybe A) ↠ D.Delay A ∞
→↠Delay-coinductive delay-ext = record
{ logical-equivalence = record
{ to = Delay⇔Delay.to₁
; from = proj₁ ∘ Delay⇔Delay.from
}
; right-inverse-of = _↔_.right-inverse-of (Delay↔Delay delay-ext)
}
→↠Delay-function : (ℕ → Maybe A) ↠ Delay A
→↠Delay-function = record
{ logical-equivalence = record
{ to = Delay⇔Delay.from ∘ Delay⇔Delay.to₁
; from = proj₁
}
; right-inverse-of = _↠_.right-inverse-of Delay↠Delay
}