Skip to content

Commit e20265f

Browse files
damhiyadamhiya
committed
PriorityQueue interface
1 parent b09525c commit e20265f

File tree

3 files changed

+216
-0
lines changed

3 files changed

+216
-0
lines changed

‎src/Data/Maybe/Properties.agda

+3
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,9 @@ private
3131
------------------------------------------------------------------------
3232
-- Equality
3333

34+
just≢nothing : ∀ {x} → (Maybe A ∋ just x) ≢ nothing
35+
just≢nothing ()
36+
3437
just-injective : ∀ {x y} → (Maybe A ∋ just x) ≡ just y → x ≡ y
3538
just-injective refl = refl
3639

‎src/Data/PriorityQueue/Base.agda

+138
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
open import Relation.Binary using (TotalOrder)
4+
5+
module Data.PriorityQueue.Base
6+
{a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
7+
8+
open import Data.Empty
9+
open import Data.Maybe as Maybe
10+
open import Data.Maybe.Properties
11+
open import Data.Nat using (ℕ; zero; suc; _+_)
12+
open import Data.Nat.Properties
13+
open import Data.Product
14+
open import Data.List
15+
open import Data.List.Relation.Binary.Permutation.Propositional
16+
open import Data.List.Relation.Unary.All using (All)
17+
open import Function.Base
18+
open import Level renaming (suc to ℓ-suc)
19+
open import Relation.Binary
20+
open import Relation.Binary.PropositionalEquality as P
21+
open import Relation.Unary hiding (Empty)
22+
open import Relation.Nullary
23+
open import Induction.WellFounded
24+
25+
open TotalOrder totalOrder renaming (Carrier to A)
26+
27+
record RawPriorityQueue b ℓ : Set (a ⊔ ℓ-suc (b ⊔ ℓ)) where
28+
field
29+
Queue : Set b
30+
size : Queue → ℕ
31+
empty : Queue
32+
insert : A → Queue → Queue
33+
meld : Queue → Queue → Queue
34+
popMin : Queue → Maybe (A × Queue)
35+
36+
singleton : A → Queue
37+
singleton x = insert x empty
38+
39+
findMin : Queue → Maybe A
40+
findMin = Maybe.map proj₁ ∘ popMin
41+
42+
deleteMin : Queue → Maybe Queue
43+
deleteMin = Maybe.map proj₂ ∘ popMin
44+
45+
Empty : Pred Queue (a ⊔ b)
46+
Empty q = popMin q ≡ nothing
47+
48+
¬Empty : Pred Queue (a ⊔ b)
49+
¬Empty q = ¬ Empty q
50+
51+
PopMin : Queue → A → Queue → Set (a ⊔ b)
52+
PopMin q x q' = popMin q ≡ just (x , q')
53+
54+
FindMin : REL Queue A a
55+
FindMin q x = findMin q ≡ just x
56+
57+
DeleteMin : Rel Queue b
58+
DeleteMin q q' = deleteMin q ≡ just q'
59+
60+
_≺_ : Rel Queue b
61+
q' ≺ q = DeleteMin q q'
62+
63+
_⊀_ : Rel Queue b
64+
q' ⊀ q = ¬ (q' ≺ q)
65+
66+
Empty⇒⊀ : ∀ {q} → Empty q → (∀ q' → q' ⊀ q)
67+
Empty⇒⊀ {q} ≡nothing q' ≡just = just≢nothing $ begin
68+
just q' ≡˘⟨ ≡just ⟩
69+
deleteMin q ≡⟨ P.cong (Maybe.map proj₂) ≡nothing ⟩
70+
nothing ∎
71+
where open P.≡-Reasoning
72+
73+
74+
record SizeLaws {b ℓ} (rawPriorityQueue : RawPriorityQueue b ℓ) : Set (a ⊔ b) where
75+
open RawPriorityQueue rawPriorityQueue
76+
77+
field
78+
Empty⇒size≡0 : ∀ q → Empty q → size q ≡ 0
79+
≺-size : ∀ q q' → q' ≺ q → size q ≡ 1 + size q'
80+
size-empty : size empty ≡ 0
81+
size-insert : ∀ x q → size (insert x q) ≡ 1 + size q
82+
size-meld : ∀ q₁ q₂ → size (meld q₁ q₂) ≡ size q₁ + size q₂
83+
84+
size≡0⇒Empty : ∀ q → size q ≡ 0 → Empty q
85+
size≡0⇒Empty q #q≡0 with popMin q in eq
86+
... | nothing = P.refl
87+
... | just (x , q') = ⊥-elim ∘ 0≢1+n $ begin
88+
0 ≡˘⟨ #q≡0 ⟩
89+
size q ≡⟨ ≺-size q q' (P.cong (Maybe.map proj₂) eq) ⟩
90+
1 + size q' ∎
91+
where open P.≡-Reasoning
92+
93+
≺-wellFounded : WellFounded _≺_
94+
≺-wellFounded = λ q → Size⇒Acc _ q P.refl
95+
where
96+
Size⇒Acc : ∀ n q → size q ≡ n → Acc _≺_ q
97+
Size⇒Acc zero q #q≡0 = acc λ q' q'≺q →
98+
⊥-elim (Empty⇒⊀ (size≡0⇒Empty q #q≡0) q' q'≺q)
99+
Size⇒Acc (suc m) q #q≡n = acc λ q' q'≺q →
100+
Size⇒Acc m q' ∘ suc-injective $ begin
101+
1 + size q' ≡˘⟨ ≺-size q q' q'≺q ⟩
102+
size q ≡⟨ #q≡n ⟩
103+
1 + m ∎
104+
where open P.≡-Reasoning
105+
106+
toListAux : ∀ q → @0 Acc _≺_ q → List A
107+
toListAux q (acc rs) with popMin q
108+
... | nothing = []
109+
... | just (x , q') = x ∷ toListAux q' (rs q' P.refl)
110+
111+
toList : Queue → List A
112+
toList q = toListAux q (≺-wellFounded q)
113+
114+
115+
record ElementLaws
116+
{b ℓ}
117+
(rawPriorityQueue : RawPriorityQueue b ℓ)
118+
(sizeLaws : SizeLaws rawPriorityQueue)
119+
: Set (a ⊔ b ⊔ ℓ₂) where
120+
121+
open RawPriorityQueue rawPriorityQueue
122+
open SizeLaws sizeLaws
123+
124+
field
125+
toList-insert : ∀ q x → toList (insert x q) ↭ x ∷ toList q
126+
toList-meld : ∀ q₁ q₂ → toList (meld q₁ q₂) ↭ toList q₁ ++ toList q₂
127+
toList-FindMin : ∀ q x → FindMin q x → All (x ≤_) (toList q)
128+
129+
130+
record PriorityQueue b ℓ : Set (a ⊔ ℓ-suc (b ⊔ ℓ) ⊔ ℓ₂) where
131+
field
132+
rawPriorityQueue : RawPriorityQueue b ℓ
133+
sizeLaws : SizeLaws rawPriorityQueue
134+
elementLaws : ElementLaws rawPriorityQueue sizeLaws
135+
136+
open RawPriorityQueue rawPriorityQueue public
137+
open SizeLaws sizeLaws public
138+
open ElementLaws elementLaws public

‎src/Data/PriorityQueue/Properties.agda

+75
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
open import Relation.Binary using (TotalOrder)
4+
open import Data.PriorityQueue.Base
5+
6+
module Data.PriorityQueue.Properties
7+
{a ℓ₁ ℓ₂} {b ℓ}
8+
(totalOrder : TotalOrder a ℓ₁ ℓ₂)
9+
(priorityQueue : PriorityQueue totalOrder b ℓ)
10+
where
11+
12+
open import Data.Empty
13+
import Data.Empty.Irrelevant as Irrelevant
14+
open import Data.List
15+
open import Data.Maybe as Maybe
16+
open import Data.Nat
17+
open import Data.Product
18+
open import Relation.Binary.PropositionalEquality as P
19+
open import Induction.WellFounded
20+
21+
open TotalOrder totalOrder renaming (Carrier to A)
22+
open PriorityQueue priorityQueue
23+
24+
popMin⇒deleteMin : ∀ {q t} → popMin q ≡ t → deleteMin q ≡ Maybe.map proj₂ t
25+
popMin⇒deleteMin = P.cong (Maybe.map proj₂)
26+
27+
popMin′ : ∀ q → .(¬Empty q) → A × Queue
28+
popMin′ q q≢∅ with popMin q
29+
... | nothing = Irrelevant.⊥-elim (q≢∅ P.refl)
30+
... | just p = p
31+
32+
findMin′ : ∀ q → .(¬Empty q) → A
33+
findMin′ q q≢∅ = proj₁ (popMin′ q q≢∅)
34+
35+
deleteMin′ : ∀ q → .(¬Empty q) → Queue
36+
deleteMin′ q q≢∅ = proj₂ (popMin′ q q≢∅)
37+
38+
Empty-empty : Empty empty
39+
Empty-empty = size≡0⇒Empty empty size-empty
40+
41+
toListAux-irrelevant : ∀ q (rec₁ rec₂ : Acc _≺_ q) → toListAux q rec₁ ≡ toListAux q rec₂
42+
toListAux-irrelevant q (acc rs₁) (acc rs₂) with popMin q
43+
... | nothing = P.refl
44+
... | just (x , q') = P.cong (x ∷_) (toListAux-irrelevant q' (rs₁ q' P.refl) (rs₂ q' P.refl))
45+
46+
toListAux-length : ∀ q (@0 rec : Acc _≺_ q) → length (toListAux q rec) ≡ size q
47+
toListAux-length q (acc rs) with popMin q in eq
48+
... | nothing = P.sym (Empty⇒size≡0 q eq)
49+
... | just (x , q') = begin
50+
1 + length (toListAux q' (rs q' P.refl)) ≡⟨ P.cong suc (toListAux-length q' (rs q' P.refl)) ⟩
51+
1 + size q' ≡˘⟨ ≺-size q q' (popMin⇒deleteMin eq) ⟩
52+
size q ∎
53+
where open P.≡-Reasoning
54+
55+
toList-length : ∀ q → length (toList q) ≡ size q
56+
toList-length q = toListAux-length q (≺-wellFounded q)
57+
58+
toListAux-Empty : ∀ q (@0 rec : Acc _≺_ q) → Empty q → toListAux q rec ≡ []
59+
toListAux-Empty q (acc rs) q≡∅ with popMin q
60+
toListAux-Empty q (acc rs) refl | nothing = P.refl
61+
62+
toList-Empty : ∀ q → Empty q → toList q ≡ []
63+
toList-Empty q = toListAux-Empty q (≺-wellFounded q)
64+
65+
toList-empty : toList empty ≡ []
66+
toList-empty = toList-Empty empty (Empty-empty)
67+
68+
toList-unfold : ∀ q x q' → PopMin q x q' → toList q ≡ x ∷ toList q'
69+
toList-unfold q x q' p with ≺-wellFounded q
70+
toList-unfold q x q' p | acc rs with popMin q in eq
71+
toList-unfold q x q' refl | acc rs | just (x , q') =
72+
P.cong (x ∷_) (toListAux-irrelevant q' rec₁ rec₂)
73+
where
74+
rec₁ = rs q' P.refl
75+
rec₂ = ≺-wellFounded q'

0 commit comments

Comments
 (0)