{-# OPTIONS --cubical --safe #-}
open import Equality
module Queue.Truncated
{c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where
open Derived-definitions-and-properties eq
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Bijection eq as Bijection using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Erased.Cubical eq hiding (map)
open import Function-universe eq as F hiding (id; _∘_)
open import List eq as L hiding (map)
open import H-level eq
open import H-level.Closure eq
open import H-level.Truncation.Propositional eq as Trunc
import Queue eq as Q
open import Sum eq
open import Surjection eq using (_↠_)
open import Tactic.By.Parametrised eq
private
variable
a b : Level
A B : Set a
p q x : A
f : A → B
xs : List A
s s₁ s₂ : Very-stable-≡ A
module _
(Q : ∀ {ℓ} → @0 Set ℓ → Set ℓ)
⦃ is-queue : ∀ {ℓ} → Q.Is-queue Q (λ _ → ↑ _ ⊤) ℓ ⦄
where
abstract
Queue_⟪_⟫ : {@0 A : Set a} → @0 List A → Set a
Queue_⟪_⟫ {A = A} xs =
∥ (∃ λ (q : Q A) → Erased (Q.to-List _ q ≡ xs)) ∥
Queue : Set a → Set a
Queue A = ∃ λ (xs : Erased (List A)) → Queue_⟪_⟫ (erased xs)
module _
{Q : ∀ {ℓ} → @0 Set ℓ → Set ℓ}
⦃ is-queue : ∀ {ℓ} → Q.Is-queue Q (λ _ → ↑ _ ⊤) ℓ ⦄
⦃ is-queue-with-map : ∀ {ℓ₁ ℓ₂} → Q.Is-queue-with-map Q ℓ₁ ℓ₂ ⦄
where
abstract
Queue-⟪⟫-propositional :
{@0 xs : List A} →
Is-proposition (Queue Q ⟪ xs ⟫)
Queue-⟪⟫-propositional = truncation-is-proposition
@0 ⌊_⌋ : Queue Q A → List A
⌊_⌋ = erased ∘ proj₁
≡-for-indices↔≡ :
{xs ys : Queue Q A} →
Erased (⌊ xs ⌋ ≡ ⌊ ys ⌋) ↔ xs ≡ ys
≡-for-indices↔≡ {xs = xs} {ys = ys} =
Erased (⌊ xs ⌋ ≡ ⌊ ys ⌋) ↝⟨ Erased-≡↔[]≡[] ⟩
proj₁ xs ≡ proj₁ ys ↝⟨ ignore-propositional-component Queue-⟪⟫-propositional ⟩□
xs ≡ ys □
strengthen-queue-equality :
{q₁ q₂ : Queue Q A} → (Very-stable-≡ A → q₁ ≡ q₂) → q₁ ≡ q₂
strengthen-queue-equality {q₁ = q₁} {q₂ = q₂} eq =
_↔_.to ≡-for-indices↔≡
[ ⌊ q₁ ⌋ ≡⟨ cong ⌊_⌋ (eq (Very-stable→Very-stable-≡ 0 (erased Erased-Very-stable))) ⟩∎
⌊ q₂ ⌋ ∎
]
mutual
abstract
Σ-List→Queue-⟪⟫ :
{@0 ys : List A} →
(∃ λ xs → Erased (xs ≡ ys)) → Queue Q ⟪ ys ⟫
Σ-List→Queue-⟪⟫ = _
Queue-⟪⟫↔Σ-List :
{@0 ys : List A} →
Very-stable-≡ A →
Queue Q ⟪ ys ⟫ ↔ ∃ λ xs → Erased (xs ≡ ys)
Queue-⟪⟫↔Σ-List {ys = ys} s = Bijection.with-other-inverse
Queue-⟪⟫↔Σ-List′
Σ-List→Queue-⟪⟫
(λ _ → from-Queue-⟪⟫↔Σ-List′)
where
abstract
Queue-⟪⟫↔Σ-List′ : Queue Q ⟪ ys ⟫ ↔ ∃ λ xs → Erased (xs ≡ ys)
Queue-⟪⟫↔Σ-List′ = ↠→↔Erased-singleton
(Q.Queue↠List _)
(Very-stable-≡-List 0 s)
from-Queue-⟪⟫↔Σ-List′ :
_≡_ {A = Queue Q ⟪ ys ⟫}
(_↔_.from Queue-⟪⟫↔Σ-List′ p)
(Σ-List→Queue-⟪⟫ p)
from-Queue-⟪⟫↔Σ-List′ = refl _
Queue↔List : Very-stable-≡ A → Queue Q A ↔ List A
Queue↔List {A = A} s =
Queue Q A ↔⟨⟩
(∃ λ (xs : Erased (List A)) → Queue Q ⟪ erased xs ⟫) ↝⟨ (∃-cong λ _ → Queue-⟪⟫↔Σ-List s) ⟩
(∃ λ (xs : Erased (List A)) → ∃ λ ys → Erased (ys ≡ erased xs)) ↝⟨ Σ-Erased-Erased-singleton↔ ⟩□
List A □
mutual
from-List : List A → Queue Q A
from-List = _
_ : _↔_.from (Queue↔List s) ≡ from-List
_ = refl _
to-List : Very-stable-≡ A → Queue Q A → List A
to-List s = _↔_.to (Queue↔List s)
abstract
private
to-List-, :
∀ {A : Set a} {s : Very-stable-≡ A} {xs q p} →
to-List s ([ xs ] , ∣ q , p ∣) ≡ Q.to-List _ q
to-List-, = refl _
@0 ≡⌊⌋ : to-List s q ≡ ⌊ q ⌋
≡⌊⌋ {s = s} {q = q} =
to-Σ-Erased-∥-Σ-Erased-≡-∥↔≡
(Q.Queue↠List _) (Very-stable-≡-List 0 s) q
@0 Queue↔Listⁱ : Queue Q A ↔ List A
Queue↔Listⁱ {A = A} =
Queue Q A ↔⟨⟩
(∃ λ (xs : Erased (List A)) → Queue Q ⟪ erased xs ⟫) ↝⟨ drop-⊤-right (λ _ → _⇔_.to contractible⇔↔⊤ $
propositional⇒inhabited⇒contractible Queue-⟪⟫-propositional $
_↔_.from (Queue-⟪⟫↔Σ-List (Very-stable→Very-stable-≡ 0 $ erased Erased-Very-stable))
(_ , [ refl _ ])) ⟩
Erased (List A) ↝⟨ Very-stable→Stable 0 $ erased Erased-Very-stable ⟩□
List A □
private
@0 to-Queue↔Listⁱ-, : _↔_.to Queue↔Listⁱ q ≡ ⌊ q ⌋
to-Queue↔Listⁱ-, = refl _
@0 to-Queue↔List : _↔_.to (Queue↔List s) q ≡ _↔_.to Queue↔Listⁱ q
to-Queue↔List = ≡⌊⌋
Maybe[×Queue]↔List :
Very-stable-≡ A →
Maybe (A × Queue Q A) ↔ List A
Maybe[×Queue]↔List {A = A} s =
Maybe (A × Queue Q A) ↝⟨ F.id ⊎-cong F.id ×-cong Queue↔List s ⟩
Maybe (A × List A) ↝⟨ inverse List↔Maybe[×List] ⟩□
List A □
@0 Maybe[×Queue]↔Listⁱ :
Maybe (A × Queue Q A) ↔ List A
Maybe[×Queue]↔Listⁱ {A = A} =
Maybe (A × Queue Q A) ↝⟨ F.id ⊎-cong F.id ×-cong Queue↔Listⁱ ⟩
Maybe (A × List A) ↝⟨ inverse List↔Maybe[×List] ⟩□
List A □
@0 to-Maybe[×Queue]↔List :
∀ xs →
_↔_.to (Maybe[×Queue]↔List s) xs ≡
_↔_.to Maybe[×Queue]↔Listⁱ xs
to-Maybe[×Queue]↔List {s = s} xs =
_↔_.from List↔Maybe[×List]
(⊎-map id (Σ-map id (_↔_.to (Queue↔List s))) xs) ≡⟨ cong (λ f → _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id f) xs)) (⟨ext⟩ λ _ →
to-Queue↔List) ⟩∎
_↔_.from List↔Maybe[×List]
(⊎-map id (Σ-map id (_↔_.to Queue↔Listⁱ)) xs) ∎
⌊⌋≡→to-List≡ :
Erased (⌊ q ⌋ ≡ xs) →
to-List s q ≡ xs
⌊⌋≡→to-List≡ {q = q} {xs = xs} {s = s} eq =
to-List s q ≡⟨ cong (to-List _) (_↔_.to ≡-for-indices↔≡ eq) ⟩
to-List s (from-List xs) ≡⟨ _↔_.right-inverse-of (Queue↔List _) _ ⟩∎
xs ∎
module Indexed where
abstract
private
unary :
{@0 A : Set a} {@0 B : Set b}
{@0 xs : List A} {@0 f : List A → List B}
(g : Q A → Q B) →
@0 (∀ {q} → Q.to-List _ (g q) ≡ f (Q.to-List _ q)) →
Queue Q ⟪ xs ⟫ → Queue Q ⟪ f xs ⟫
unary {xs = xs} {f = f} g hyp = Trunc.rec
truncation-is-proposition
(uncurry λ q p →
∣ g q
, [ Q.to-List _ (g q) ≡⟨ hyp ⟩
f (Q.to-List _ q) ≡⟨ cong f (erased p) ⟩∎
f xs ∎
]
∣)
enqueue :
{@0 xs : List A}
(x : A) → Queue Q ⟪ xs ⟫ → Queue Q ⟪ xs ++ x ∷ [] ⟫
enqueue x = unary (Q.enqueue x) Q.to-List-enqueue
map :
{@0 xs : List A} →
(f : A → B) → Queue Q ⟪ xs ⟫ → Queue Q ⟪ L.map f xs ⟫
map f = unary (Q.map f) Q.to-List-map
Result-⟪_⟫ : {A : Set a} → @0 List A → Set a
Result-⟪_⟫ {A = A} xs =
∃ λ (q : Maybe (A × Queue Q A)) →
Erased (_↔_.to Maybe[×Queue]↔Listⁱ q ≡ xs)
Result-⟪⟫-propositional :
{@0 xs : List A} →
Very-stable-≡ A →
Is-proposition Result-⟪ xs ⟫
Result-⟪⟫-propositional {A = A} {xs = xs} s =
$⟨ erased-singleton-with-erased-center-propositional (Very-stable-≡-List 0 s) ⟩
Is-proposition (Erased-singleton xs) ↝⟨ H-level-cong _ 1 (inverse lemma) ⦂ (_ → _) ⟩□
Is-proposition Result-⟪ xs ⟫ □
where
lemma : _ ↔ _
lemma =
Result-⟪ xs ⟫ ↔⟨⟩
(∃ λ (ys : Maybe (A × Queue Q A)) →
Erased (_↔_.to Maybe[×Queue]↔Listⁱ ys ≡ xs)) ↝⟨ ∃-cong (λ ys → Erased-cong (≡⇒↝ _ $ cong (_≡ xs) $ sym $
to-Maybe[×Queue]↔List ys)) ⟩
(∃ λ (ys : Maybe (A × Queue Q A)) →
Erased (_↔_.to (Maybe[×Queue]↔List s) ys ≡ xs)) ↝⟨ Σ-cong (Maybe[×Queue]↔List s) (λ _ → F.id) ⟩
(∃ λ (ys : List A) → Erased (ys ≡ xs)) ↔⟨⟩
Erased-singleton xs □
abstract
dequeue :
{@0 xs : List A} →
Very-stable-≡ A →
Queue Q ⟪ xs ⟫ →
Result-⟪ xs ⟫
dequeue {xs = xs} s = Trunc.rec
(Result-⟪⟫-propositional s)
(λ (q , [ eq ]) →
⊎-map id (Σ-map id λ q → _ , ∣ q , [ refl _ ] ∣)
(Q.dequeue _ q)
, [ _↔_.to Maybe[×Queue]↔Listⁱ
(⊎-map id (Σ-map id (λ q → _ , ∣ q , [ refl _ ] ∣))
(Q.dequeue _ q)) ≡⟨⟩
_↔_.from List↔Maybe[×List]
⟨ ⊎-map id (Σ-map id (_↔_.to Queue↔Listⁱ))
(⊎-map id (Σ-map id (λ q → _ , ∣ q , [ refl _ ] ∣))
(Q.dequeue _ q)) ⟩ ≡⟨ ⟨by⟩ 8 (sym $ ⊎-map-∘ (Q.dequeue _ q)) ⟩
_↔_.from List↔Maybe[×List]
⟨ ⊎-map id (Σ-map id (Q.to-List _)) (Q.dequeue _ q) ⟩ ≡⟨ ⟨by⟩ 8 (Q.to-List-dequeue {q = q}) ⟩
_↔_.from List↔Maybe[×List]
(_↔_.to List↔Maybe[×List] (Q.to-List _ q)) ≡⟨ _↔_.left-inverse-of List↔Maybe[×List] _ ⟩
Q.to-List _ q ≡⟨ eq ⟩∎
xs ∎
])
dequeue⁻¹ :
{@0 xs : List A} →
Result-⟪ xs ⟫ → Queue Q ⟪ xs ⟫
dequeue⁻¹ {xs = xs} (nothing , eq) =
∣ Q.empty
, [ Q.to-List _ (Q.empty ⦂ Q _) ≡⟨ Q.to-List-empty ⟩
[] ≡⟨ erased eq ⟩∎
xs ∎
]
∣
dequeue⁻¹ {xs = xs} (just (x , ys , q) , eq) =
∥∥-map (Σ-map (Q.cons x)
(λ {q′} → Erased-cong λ eq′ →
Q.to-List _ (Q.cons x q′) ≡⟨ Q.to-List-cons ⟩
x ∷ Q.to-List _ q′ ≡⟨ cong (x ∷_) eq′ ⟩
x ∷ erased ys ≡⟨ erased eq ⟩∎
xs ∎))
q
Queue-⟪⟫↔Result-⟪⟫ :
{@0 xs : List A} →
Very-stable-≡ A →
Queue Q ⟪ xs ⟫ ↔ Result-⟪ xs ⟫
Queue-⟪⟫↔Result-⟪⟫ s = record
{ surjection = record
{ logical-equivalence = record
{ to = dequeue s
; from = dequeue⁻¹
}
; right-inverse-of = λ _ → Result-⟪⟫-propositional s _ _
}
; left-inverse-of = λ _ → Queue-⟪⟫-propositional _ _
}
module Non-indexed where
enqueue : A → Queue Q A → Queue Q A
enqueue x = Σ-map _ (Indexed.enqueue x)
to-List-enqueue : to-List s (enqueue x q) ≡ to-List s q ++ x ∷ []
to-List-enqueue {s = s} {x = x} {q = q} = ⌊⌋≡→to-List≡
[ ⌊ q ⌋ ++ x ∷ [] ≡⟨ cong (_++ _) $ sym ≡⌊⌋ ⟩∎
to-List s q ++ x ∷ [] ∎
]
map : (A → B) → Queue Q A → Queue Q B
map f = Σ-map _ (Indexed.map f)
to-List-map : to-List s₁ (map f q) ≡ L.map f (to-List s₂ q)
to-List-map {f = f} {q = q} {s₂ = s₂} = ⌊⌋≡→to-List≡
[ L.map f ⌊ q ⌋ ≡⟨ cong (L.map f) $ sym ≡⌊⌋ ⟩∎
L.map f (to-List s₂ q) ∎
]
private
Result : Set a → Set a
Result A =
∃ λ (xs : Erased (List A)) → Indexed.Result-⟪ erased xs ⟫
Result↠Maybe[×Queue] : Result A ↠ Maybe (A × Queue Q A)
Result↠Maybe[×Queue] = record
{ logical-equivalence = record
{ to = proj₁ ∘ proj₂
; from = λ q → _ , q , [ refl _ ]
}
; right-inverse-of = refl
}
Result↔Maybe[×Queue] :
Very-stable-≡ A →
Result A ↔ Maybe (A × Queue Q A)
Result↔Maybe[×Queue] s = record
{ surjection = Result↠Maybe[×Queue]
; left-inverse-of = λ r → $⟨ from∘to r ⟩
Erased (⌊ from (to r) ⌋ʳ ≡ ⌊ r ⌋ʳ) ↝⟨ Erased-≡↔[]≡[] ⟩
proj₁ (from (to r)) ≡ proj₁ r ↝⟨ ignore-propositional-component (Indexed.Result-⟪⟫-propositional s) ⟩□
from (to r) ≡ r □
}
where
open _↠_ Result↠Maybe[×Queue]
@0 ⌊_⌋ʳ : Result A → List A
⌊_⌋ʳ = erased ∘ proj₁
from∘to : ∀ r → Erased (⌊ from (to r) ⌋ʳ ≡ ⌊ r ⌋ʳ)
from∘to (_ , _ , eq) = eq
Queue↔Maybe[×Queue] :
Very-stable-≡ A →
Queue Q A ↔ Maybe (A × Queue Q A)
Queue↔Maybe[×Queue] {A = A} s =
Queue Q A ↝⟨ ∃-cong (λ _ → Indexed.Queue-⟪⟫↔Result-⟪⟫ s) ⟩
Result A ↝⟨ Result↔Maybe[×Queue] s ⟩□
Maybe (A × Queue Q A) □
mutual
dequeue⁻¹ : Maybe (A × Queue Q A) → Queue Q A
dequeue⁻¹ q = _
_ : _↔_.from (Queue↔Maybe[×Queue] s) ≡ dequeue⁻¹
_ = refl _
to-List-dequeue⁻¹ :
to-List s (dequeue⁻¹ x) ≡
_↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id (to-List s)) x)
to-List-dequeue⁻¹ {x = nothing} = ⌊⌋≡→to-List≡ [ refl _ ]
to-List-dequeue⁻¹ {s = s} {x = just (x , q)} = ⌊⌋≡→to-List≡
[ x ∷ ⌊ q ⌋ ≡⟨ cong (_ ∷_) $ sym ≡⌊⌋ ⟩∎
x ∷ to-List s q ∎
]
dequeue : Very-stable-≡ A → Queue Q A → Maybe (A × Queue Q A)
dequeue s = _↔_.to (Queue↔Maybe[×Queue] s)
to-List-dequeue :
⊎-map id (Σ-map id (to-List s)) (dequeue s q) ≡
_↔_.to List↔Maybe[×List] (to-List s q)
to-List-dequeue {s = s} {q = q} =
⊎-map id (Σ-map id (to-List s)) (dequeue s q) ≡⟨ _↔_.to (from≡↔≡to (from-isomorphism List↔Maybe[×List])) $
sym to-List-dequeue⁻¹ ⟩
_↔_.to List↔Maybe[×List] (to-List s (dequeue⁻¹ (dequeue s q))) ≡⟨ cong (_↔_.to List↔Maybe[×List] ∘ to-List s) $
_↔_.left-inverse-of (Queue↔Maybe[×Queue] _) _ ⟩∎
_↔_.to List↔Maybe[×List] (to-List s q) ∎