forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
simple_bstScript.sml
262 lines (219 loc) · 7.12 KB
/
simple_bstScript.sml
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
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
(*
Simple binary search tree.
This file defines a datatype for binary search trees, plus insert and lookup
operations It then proves functional correctness of these operations.
It is a simplified version of the balanced binary tree example found in
$HOLDIR/examples/balanced_bst
*)
(*
A script file begins with a descriptive comment like the above, then opens
the structures whose contents will be used. When working within the CakeML
repository, it is usually sufficient to open preamble. Otherwise, one would
typically open HolKernel boolLib bossLib and Parse (at least). CakeML's
preamble wrapper includes all of those structures and more.
*)
open preamble comparisonTheory
(*
Create the logical theory in which we will work. Its name should match the name
of this file, before the "Script.sml" suffix.
*)
val _ = new_theory "simple_bst";
(*
Define the binary tree type.
It is polymorphic with two type variables, 'k for the key type and 'v for the
value type.
*)
val _ = Datatype`
btree = Leaf | Node 'k 'v btree btree`;
(*
Try, for example
type_of ``Node``;
*)
(*
Now we define some basic binary search tree operations.
The operations are parameterised by a comparison function on the tree data,
which is of type 'a -> 'a -> cpn. The cpn type is an enumeration of three
constructors: Less, Equal, Greater; it is predefined in totoTheory (included
within preamble).
Try, for example
TypeBase.constructors_of``:cpn``;
*)
val singleton_def = Define`
singleton k v = Node k v Leaf Leaf`;
val lookup_def = Define`
lookup cmp k Leaf = NONE ∧
lookup cmp k (Node k' v' l r) =
case cmp k k' of
| Less => lookup cmp k l
| Greater => lookup cmp k r
| Equal => SOME v'`;
val insert_def =
(* EXERCISE: fill in your definition here *)
(*
Since we are working with an abstract comparison function, different keys (k,
k') may be considered equivalent (cmp k k' = Equal).
We will assume good_cmp of the comparison function cmp.
Try:
DB.find"good_cmp";
which reveals that this is defined in comparisonTheory
*)
val key_set_def = Define`
key_set cmp k = { k' | cmp k k' = Equal } `;
(*
For a good comparison function cmp, the key_set cmp relation should be an
equivalence relation (reflexive, symmetric, and transitive): this is because
key_set cmp k is supposed to be the set of keys equivalent to k under cmp.
Let's prove this.
*)
Theorem key_set_equiv:
∀cmp.
good_cmp cmp
⇒
(∀k. k ∈ key_set cmp k) ∧
(∀k1 k2. k1 ∈ key_set cmp k2 ⇒ k2 ∈ key_set cmp k1) ∧
(∀k1 k2 k3. k1 ∈ key_set cmp k2 ∧ k2 ∈ key_set cmp k3 ⇒ k1 ∈ key_set cmp k3)
Proof
rw [key_set_def] >>
metis_tac [good_cmp_def]
QED
(* A corollary of this: if two keys have the same key_set, they must be
equivalent *)
Theorem key_set_eq:
∀cmp k1 k2.
good_cmp cmp
⇒
(key_set cmp k1 = key_set cmp k2 ⇔ cmp k1 k2 = Equal)
Proof
(* EXERCISE: prove this *)
(* hint: consider the tactics used above *)
(* hint: remember DB.match and DB.find to find useful theorems *)
(* hint: set extensionality theorem is called EXTENSION *)
QED
(* A helper theorem, expanding out the definition of key_set, for use with
metis_tac later. *)
val IN_key_set = save_thm("IN_key_set",
``k' ∈ key_set cmp k`` |> SIMP_CONV (srw_ss()) [key_set_def]);
(*
Now let us define the (abstract) finite map from key-equivalence-classes to
values, obtained by considering every (key,value) pair in a tree. This is the
standard against which we can verify correctness of the operations.
*)
val to_fmap_def = Define`
to_fmap cmp Leaf = FEMPTY ∧
to_fmap cmp (Node k v l r) =
to_fmap cmp l ⊌ to_fmap cmp r |+ (key_set cmp k, v)`;
Theorem to_fmap_key_set:
∀ks t.
ks ∈ FDOM (to_fmap cmp t) ⇒ ∃k. ks = key_set cmp k
Proof
Induct_on `t` >>
(* EXERCISE: finish this proof *)
(* hint: the same tactic probably works for both subgoals *)
QED
(*
Now some proofs about the basic tree operations.
*)
(*
We start by defining what a predicate on trees indicating
whether they have the binary search tree property
*)
val key_ordered_def = Define`
(key_ordered cmp k Leaf res ⇔ T) ∧
(key_ordered cmp k (Node k' _ l r) res ⇔
cmp k k' = res ∧
key_ordered cmp k l res ∧
key_ordered cmp k r res)`;
(* We make this definition an automatic rewrite, so it is expanded
automatically by simplification tactics (such as rw, fs, and simp) *)
val _ = export_rewrites["key_ordered_def"];
val wf_tree_def = Define`
(wf_tree cmp Leaf ⇔ T) ∧
(wf_tree cmp (Node k _ l r) ⇔
key_ordered cmp k l Greater ∧
key_ordered cmp k r Less ∧
wf_tree cmp l ∧
wf_tree cmp r)`;
(*
We can prove that all the operations preserve wf_tree
The aim here is to prove:
- wf_tree_singleton
- wf_tree_insert
Figuring out the lemmas required along the way
should probably be part of the exercise
*)
Theorem wf_tree_singleton[simp]:
wf_tree cmp (singleton k v)
Proof
EVAL_TAC
QED
(* The [simp] annotation above is equivalent to calling
export_rewrites["wf_tree_singleton"] after storing this theorem. *)
Theorem key_ordered_singleton[simp]:
(* EXERCISE: you might want to prove a lemma about key_ordered and singleton *)
(* skip ahead to wf_tree_insert first *)
Theorem key_ordered_insert[simp]:
(* ∀t. ????? ⇒ *)
key_ordered cmp k (insert cmp k' v' t) res
Proof
(* EXERCISE: you might want to prove a lemma about key_ordered and insert *)
(* skip ahead to wf_tree_insert first *)
(* hint: this lemma might need induction *)
QED
Theorem wf_tree_insert[simp]:
good_cmp cmp ⇒
∀t k v. wf_tree cmp t ⇒ wf_tree cmp (insert cmp k v t)
Proof
strip_tac \\
Induct \\
rw[insert_def] \\
CASE_TAC \\ fs[wf_tree_def] \\
(* EXERCISE: fill in the rest of the proof *)
(* hint: you might want to prove the key_ordered_insert lemma above at this point
then you can continue with:
match_mp_tac key_ordered_insert
( or: match_mp_tac (MP_CANON key_ordered_insert) )*)
QED
(*
Correctness of lookup
*)
Theorem key_ordered_to_fmap:
good_cmp cmp ⇒
∀t k res. key_ordered cmp k t res ⇔
(∀ks k'. ks ∈ FDOM (to_fmap cmp t) ∧ k' ∈ ks ⇒ cmp k k' = res)
Proof
strip_tac \\
Induct \\
rw[to_fmap_def] \\
eq_tac \\ rw[] \\
metis_tac[IN_key_set,cmp_thms]
QED
Theorem wf_tree_Node_imp:
good_cmp cmp ∧
wf_tree cmp (Node k v l r) ⇒
DISJOINT (FDOM (to_fmap cmp l)) (FDOM (to_fmap cmp r)) ∧
(∀x. key_set cmp x ∈ FDOM (to_fmap cmp l) ⇒ cmp k x = Greater) ∧
(∀x. key_set cmp x ∈ FDOM (to_fmap cmp r) ⇒ cmp k x = Less)
Proof
rw[IN_DISJOINT,wf_tree_def] \\
spose_not_then strip_assume_tac \\
imp_res_tac to_fmap_key_set \\
imp_res_tac key_ordered_to_fmap \\
metis_tac[cmp_thms,IN_key_set]
QED
Theorem lookup_to_fmap:
good_cmp cmp ⇒
∀t k. wf_tree cmp t ⇒
lookup cmp k t = FLOOKUP (to_fmap cmp t) (key_set cmp k)
Proof
strip_tac \\
Induct \\
rw[lookup_def,to_fmap_def] \\
fs[] \\
(*
Try, for example,
DB.match[] ``FLOOKUP (_ |+ _)``;
DB.match[] ``FLOOKUP (_ ⊌ _)``;
*)
(* EXERCISE: fill in the rest of this proof *)
QED
val _ = export_theory();