-
Notifications
You must be signed in to change notification settings - Fork 7
/
priority.v
183 lines (137 loc) · 4.84 KB
/
priority.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import eqtype order seq path.
From favssr Require Import prelude bintree.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.POrderTheory.
Import Order.TotalTheory.
Open Scope order_scope.
Module APQ.
Structure APQ (disp : unit) (T : orderType disp): Type :=
make {tp :> Type;
empty : tp;
insert : T -> tp -> tp;
del_min : tp -> tp;
get_min : T -> tp -> T;
mset : tp -> seq T;
invar : tp -> bool;
_ : invar empty;
_ : mset empty = [::];
_ : forall x s, invar s -> invar (insert x s);
_ : forall x s, invar s ->
perm_eq (mset (insert x s)) (x :: mset s);
_ : forall s, invar s -> ~~ nilp (mset s) -> invar (del_min s);
_ : forall x0 s, invar s -> ~~ nilp (mset s) ->
perm_eq (mset (del_min s)) (rem (get_min x0 s) (mset s));
(* we don't need non-emptiness here since we've made both sides total *)
_ : forall s x0, invar s ->
get_min x0 s = mins x0 (mset s)
}.
End APQ.
Module APQM.
Structure APQ (disp : unit) (T : orderType disp): Type :=
make {tp :> Type;
empty : tp;
insert : T -> tp -> tp;
del_min : tp -> tp;
get_min : T -> tp -> T;
meld : tp -> tp -> tp;
mset : tp -> seq T;
invar : tp -> bool;
_ : invar empty;
_ : mset empty = [::];
_ : forall x s, invar s -> invar (insert x s);
_ : forall x s, invar s ->
perm_eq (mset (insert x s)) (x :: mset s);
_ : forall s, invar s -> ~~ nilp (mset s) -> invar (del_min s);
_ : forall x0 s, invar s -> ~~ nilp (mset s) ->
perm_eq (mset (del_min s)) (rem (get_min x0 s) (mset s));
_ : forall s x0, invar s ->
get_min x0 s = mins x0 (mset s);
_ : forall s1 s2, invar s1 -> invar s2 -> invar (meld s1 s2);
_ : forall s1 s2, invar s1 -> invar s2 ->
perm_eq (mset (meld s1 s2)) (mset s1 ++ mset s2)
}.
End APQM.
(* Exercise 14.1 *)
Section Exercise.
Context {disp : unit} {T : orderType disp}.
Definition empty_list : seq T := [::].
Fixpoint ins_list (x : T) (xs : seq T) : seq T := xs. (* FIXME *)
Definition del_min_list (xs : seq T) : seq T := xs. (* FIXME *)
Definition get_min_list (x0 : T) (xs : seq T) : T := x0. (* FIXME *)
Definition invar_list (t : seq T) : bool := true. (* FIXME *)
Definition merge_list (xs1 xs2 : seq T) : seq T := xs1. (* FIXME *)
(* PROVE PROPERTIES *)
Definition ListPQM :=
@APQM.make _ _ (seq T)
empty_list ins_list del_min_list get_min_list merge_list
id invar_list
(* use proved lemmas *)
.
End Exercise.
Section Heaps.
Context {disp : unit} {T : orderType disp}.
Fixpoint heap (t : tree T) : bool :=
if t is Node l m r
then [&& all (>= m) (inorder l ++ inorder r), heap l & heap r]
else true.
Definition mset_tree : tree T -> seq T := preorder.
Definition empty : tree T := leaf.
Definition get_min (x0 : T) (t : tree T) : T :=
if t is Node _ x _
then x else x0.
Fixpoint meld (t1 : tree T) :=
if t1 is Node l1 a1 r1 then
let fix meld_t1 t2 :=
if t2 is Node l2 a2 r2 then
if a1 <= a2 then Node l1 a1 (meld r1 t2) else Node l2 a2 (meld_t1 r2)
else t1 in
meld_t1
else id.
Definition insert x t := meld (Node leaf x leaf) t.
Definition del_min (t : tree T) : tree T :=
if t is Node l _ r then meld l r else leaf.
(* Exercise 14.2 *)
Lemma invar_empty : heap empty.
Proof. Admitted.
Lemma mset_empty : mset_tree empty = [::].
Proof. Admitted.
Lemma invar_meld t1 t2 : heap t1 -> heap t2 -> heap (meld t1 t2).
Proof.
Admitted.
Lemma mset_meld t1 t2 : heap t1 -> heap t2 ->
perm_eq (mset_tree (meld t1 t2)) (mset_tree t1 ++ mset_tree t2).
Proof.
Admitted.
Corollary invar_insert_heap x t : heap t -> heap (insert x t).
Proof. by rewrite /insert=>H; apply: invar_meld. Qed.
Corollary mset_insert x t : heap t ->
perm_eq (mset_tree (insert x t)) (x :: mset_tree t).
Proof. by rewrite /insert=>H; apply: perm_trans; first by apply: mset_meld. Qed.
Corollary invar_delmin_heap t : heap t -> ~~ nilp (mset_tree t) -> heap (del_min t).
Proof.
case: t=>//=l a r; case/and3P=>_ Hl Hr _.
by apply: invar_meld.
Qed.
Corollary mset_delmin_heap x0 t : heap t -> ~~ nilp (mset_tree t) ->
perm_eq (mset_tree (del_min t)) (rem (get_min x0 t) (mset_tree t)).
Proof.
case: t=>//=l a r; case/and3P=>_ Hl Hr _; rewrite eq_refl.
by apply: mset_meld.
Qed.
Lemma mins_getmin_heap t x0 : heap t ->
get_min x0 t = mins x0 (mset_tree t).
Proof.
Admitted.
Definition HeapPQM :=
@APQM.make _ _ (tree T)
empty insert del_min get_min meld
mset_tree heap
invar_empty mset_empty
invar_insert_heap mset_insert
invar_delmin_heap mset_delmin_heap
mins_getmin_heap
invar_meld mset_meld.
End Heaps.