Skip to content

Commit fa001af

Browse files
damhiyadamhiya
committed
PriorityQueue interface
1 parent b09525c commit fa001af

File tree

4 files changed

+239
-0
lines changed

4 files changed

+239
-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.agda

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Priority queue
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.PriorityQueue where
10+
11+
open import Data.PriorityQueue.Base public

‎src/Data/PriorityQueue/Base.agda

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

‎src/Data/PriorityQueue/Properties.agda

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

0 commit comments

Comments
 (0)