SearchTreeBinary Search Trees
- Section 3.2 of Algorithms, Fourth Edition, by Sedgewick and
Wayne, Addison Wesley 2011; or
- Chapter 12 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009.
BST Implementation
E represents the empty map. T l k v r represents the
map that binds k to v, along with all the bindings in l and
r. No key may be bound more than once in the map.
Inductive tree (V : Type) : Type :=
| E
| T (l : tree V) (k : key) (v : V) (r : tree V).
Arguments E {V}.
Arguments T {V}.
An example tree:
4 -> "four" / \ / \ 2 -> "two" 5 -> "five"
empty_tree contains no bindings.
bound k t is whether k is bound in t.
Fixpoint bound {V : Type} (x : key) (t : tree V) :=
match t with
| E ⇒ false
| T l y v r ⇒ if x <? y then bound x l
else if x >? y then bound x r
else true
end.
lookup d k t is the value bound to k in t, or is default
value d if k is not bound in t.
Fixpoint lookup {V : Type} (d : V) (x : key) (t : tree V) : V :=
match t with
| E ⇒ d
| T l y v r ⇒ if x <? y then lookup d x l
else if x >? y then lookup d x r
else v
end.
insert k v t is the map containing all the bindings of t along
with a binding of k to v.
Fixpoint insert {V : Type} (x : key) (v : V) (t : tree V) : tree V :=
match t with
| E ⇒ T E x v E
| T l y v' r ⇒ if x <? y then T (insert x v l) y v' r
else if x >? y then T l y v' (insert x v r)
else T l x v r
end.
Note that insert is a functional aka persistent
implementation: t is not changed.
Here are some unit tests to check that BSTs behave the way we
expect.
Open Scope string_scope.
Example bst_ex1 :
insert 5 "five" (insert 2 "two" (insert 4 "four" empty_tree)) = ex_tree.
Proof. reflexivity. Qed.
Example bst_ex2 : lookup "" 5 ex_tree = "five".
Proof. reflexivity. Qed.
Example bst_ex3 : lookup "" 3 ex_tree = "".
Proof. reflexivity. Qed.
Example bst_ex4 : bound 3 ex_tree = false.
Proof. reflexivity. Qed.
End Tests.
Although we can spot-check the behavior of BST operations with
unit tests like these, we of course should prove general theorems
about their correctness. We will do that later in the chapter.
BST Invariant
Module NotBst.
Open Scope string_scope.
Definition t : tree string :=
T (T E 5 "five" E) 4 "four" (T E 2 "two" E).
The insert function we wrote above would never produce
such a tree, but we can still construct it by manually applying
T. When we try to lookup 2 in that tree, we get the wrong
answer, because lookup assumes 2 is in the left subtree:
Example not_bst_lookup_wrong :
lookup "" 2 t ≠ "two".
Proof.
simpl. unfold not. intros contra. discriminate.
Qed.
End NotBst.
So, let's formalize the BST invariant. Here's one way to do
so. First, we define a helper ForallT to express that idea that
a predicate holds at every node of a tree:
Fixpoint ForallT {V : Type} (P: key → V → Prop) (t: tree V) : Prop :=
match t with
| E ⇒ True
| T l k v r ⇒ P k v ∧ ForallT P l ∧ ForallT P r
end.
Second, we define the BST invariant:
- An empty tree is a BST.
- A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.
Inductive BST {V : Type} : tree V → Prop :=
| BST_E : BST E
| BST_T : ∀ l x v r,
ForallT (fun y _ ⇒ y < x) l →
ForallT (fun y _ ⇒ y > x) r →
BST l →
BST r →
BST (T l x v r).
Hint Constructors BST.
Let's check that BST correctly classifies a couple of example
trees:
Example is_BST_ex :
BST ex_tree.
Proof.
unfold ex_tree.
repeat (constructor; try lia).
Qed.
Example not_BST_ex :
¬ BST NotBst.t.
Proof.
unfold NotBst.t. intros contra.
inv contra. inv H3. lia.
Qed.
Exercise: 4 stars, standard (insert_BST)
Lemma ForallT_insert : ∀ (V : Type) (P : key → V → Prop) (t : tree V),
ForallT P t → ∀ (k : key) (v : V),
P k v → ForallT P (insert k v t).
Proof.
(* FILL IN HERE *) Admitted.
Now prove the main theorem. Proceed by induction on the evidence
that t is a BST.
Theorem insert_BST : ∀ (V : Type) (k : key) (v : V) (t : tree V),
BST t → BST (insert k v t).
Proof.
(* FILL IN HERE *) Admitted.
☐
Correctness of BST Operations
(a + b) + c = a + (b + c)
a + b = b + a
a + 0 = a
(a × b) × c = a × (b × c)
a × b = b × a
a × 1 = a
a × 0 = 0
a × (b + c) = a × b + a × c
lookup d k empty_tree = d
lookup d k (insert k v t) = v
lookup d k' (insert k v t) = lookup d k' t if k ≠ k'
Theorem lookup_empty : ∀ (V : Type) (d : V) (k : key),
lookup d k empty_tree = d.
Proof.
auto.
Qed.
Theorem lookup_insert_eq : ∀ (V : Type) (t : tree V) (d : V) (k : key) (v : V),
lookup d k (insert k v t) = v.
Proof.
induction t; intros; simpl.
- bdestruct (k <? k); try lia; auto.
- bdestruct (k <? k0); bdestruct (k0 <? k); simpl; try lia; auto.
+ bdestruct (k <? k0); bdestruct (k0 <? k); try lia; auto.
+ bdestruct (k <? k0); bdestruct (k0 <? k); try lia; auto.
+ bdestruct (k0 <? k0); try lia; auto.
Qed.
The basic method of that proof is to repeatedly bdestruct
everything in sight, followed by generous use of lia and
auto. Let's automate that.
Ltac bdestruct_guard :=
match goal with
| ⊢ context [ if ?X =? ?Y then _ else _ ] ⇒ bdestruct (X =? Y)
| ⊢ context [ if ?X <=? ?Y then _ else _ ] ⇒ bdestruct (X <=? Y)
| ⊢ context [ if ?X <? ?Y then _ else _ ] ⇒ bdestruct (X <? Y)
end.
Ltac bdall :=
repeat (simpl; bdestruct_guard; try lia; auto).
Theorem lookup_insert_eq' :
∀ (V : Type) (t : tree V) (d : V) (k : key) (v : V),
lookup d k (insert k v t) = v.
Proof.
induction t; intros; bdall.
Qed.
The tactic immediately pays off in proving the third
equation.
Theorem lookup_insert_neq :
∀ (V : Type) (t : tree V) (d : V) (k k' : key) (v : V),
k ≠ k' → lookup d k' (insert k v t) = lookup d k' t.
Proof.
induction t; intros; bdall.
Qed.
Perhaps surprisingly, the proofs of these results do not
depend on whether t satisfies the BST invariant. That's because
lookup and insert follow the same path through the tree, so
even if nodes are in the "wrong" place, they are consistently
"wrong".
Specify and prove the correctness of bound. State and prove
three theorems, inspired by those we just proved for lookup. If
you have the right theorem statements, the proofs should all be
quite easy -- thanks to bdall.
Exercise: 3 stars, standard, optional (bound_correct)
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_bound_correct : option (nat×string) := None.
☐
Exercise: 3 stars, standard, optional (bound_default)
Theorem bound_default :
∀ (V : Type) (k : key) (d : V) (t : tree V),
bound k t = false →
lookup d k t = d.
Proof.
(* FILL IN HERE *) Admitted.
☐
BSTs vs. Higher-order Functions (Optional)
- lookup_empty and t_apply_empty both state that the empty map binds all keys to the default value.
Check lookup_empty : ∀ (V : Type) (d : V) (k : key),
lookup d k empty_tree = d.
Check t_apply_empty : ∀ (V : Type) (k : key) (d : V),
t_empty d k = d.
- lookup_insert_eq and t_update_eq both state that updating a map then looking for the updated key produces the updated value.
Check lookup_insert_eq : ∀ (V : Type) (t : tree V) (d : V) (k : key) (v : V),
lookup d k (insert k v t) = v.
Check t_update_eq : ∀ (V : Type) (m : total_map V) (k : key) (v : V),
(t_update m k v) k = v.
- lookup_insert_neq and t_update_neq both state that updating a map then looking for a different key produces the same value as the original map.
Check lookup_insert_neq :
∀ (V : Type) (t : tree V) (d : V) (k k' : key) (v : V),
k ≠ k' → lookup d k' (insert k v t) = lookup d k' t.
Check t_update_neq : ∀ (V : Type) (v : V) (k k' : key) (m : total_map V),
k ≠ k' → (t_update m k v) k' = m k'.
In Maps, we also proved three other theorems about the
behavior of functional maps on various combinations of updates and
lookups:
Check t_update_shadow : ∀ (V : Type) (m : total_map V) (v1 v2 : V) (k : key),
t_update (t_update m k v1) k v2 = t_update m k v2.
Check t_update_same : ∀ (V : Type) (k : key) (m : total_map V),
t_update m k (m k) = m.
Check t_update_permute :
∀ (V : Type) (v1 v2 : V) (k1 k2 : key) (m : total_map V),
k2 ≠ k1 →
t_update (t_update m k2 v2) k1 v1 = t_update (t_update m k1 v1) k2 v2.
Let's prove analogues to these three theorems for search trees.
Hint: you do not need to unfold the definitions of empty_tree,
insert, or lookup. Instead, use lookup_insert_eq and
lookup_insert_neq.
Exercise: 2 stars, standard, optional (lookup_insert_shadow)
Lemma lookup_insert_shadow :
∀ (V : Type) (t : tree V) (v v' d: V) (k k' : key),
lookup d k' (insert k v (insert k v' t)) = lookup d k' (insert k v t).
Proof.
intros. bdestruct (k =? k').
(* FILL IN HERE *) Admitted.
☐
Lemma lookup_insert_same :
∀ (V : Type) (k k' : key) (d : V) (t : tree V),
lookup d k' (insert k (lookup d k t) t) = lookup d k' t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma lookup_insert_permute :
∀ (V : Type) (v1 v2 d : V) (k1 k2 k': key) (t : tree V),
k1 ≠ k2 →
lookup d k' (insert k1 v1 (insert k2 v2 t))
= lookup d k' (insert k2 v2 (insert k1 v1 t)).
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma insert_shadow_equality : ∀ (V : Type) (t : tree V) (k : key) (v v' : V),
insert k v (insert k v' t) = insert k v t.
Proof.
induction t; intros; bdall.
- rewrite IHt1; auto.
- rewrite IHt2; auto.
Qed.
But the other two direct equalities on BSTs do not necessarily
hold.
Prove that the other equalities do not hold. Hint: find a counterexample
first on paper, then use the ∃ tactic to instantiate the theorem
on your counterexample. The simpler your counterexample, the simpler
the rest of the proof will be.
Exercise: 3 stars, standard, optional (direct_equalities_break)
Lemma insert_same_equality_breaks :
∃ (V : Type) (d : V) (t : tree V) (k : key),
insert k (lookup d k t) t ≠ t.
Proof.
(* FILL IN HERE *) Admitted.
Lemma insert_permute_equality_breaks :
∃ (V : Type) (v1 v2 : V) (k1 k2 : key) (t : tree V),
k1 ≠ k2 ∧ insert k1 v1 (insert k2 v2 t) ≠ insert k2 v2 (insert k1 v1 t).
Proof.
(* FILL IN HERE *) Admitted.
☐
Converting a BST to a List
Fixpoint elements {V : Type} (t : tree V) : list (key × V) :=
match t with
| E ⇒ []
| T l k v r ⇒ elements l ++ [(k, v)] ++ elements r
end.
Example elements_ex :
elements ex_tree = [(2, "two"); (4, "four"); (5, "five")]%string.
Proof. reflexivity. Qed.
Here are three desirable properties for elements:
1. The list has the same bindings as the tree.
2. The list is sorted by keys.
3. The list contains no duplicate keys.
Let's formally specify and verify them.
We want to show that a binding is in elements t iff it's in
t. We'll prove the two directions of that bi-implication
separately:
Getting the specification of completeness right is a little
tricky. It's tempting to start off with something too simple like
this:
Part 1: Same Bindings
- elements is complete: if a binding is in t then it's in
elements t.
- elements is correct: if a binding is in elements t then it's in t.
Definition elements_complete_broken_spec :=
∀ (V : Type) (k : key) (v d : V) (t : tree V),
BST t →
lookup d k t = v →
In (k, v) (elements t).
The problem with that specification is how it handles the default
element d: the specification would incorrectly require elements
t to contain a binding (k, d) for all keys k unbound in
t. That would force elements t to be infinitely long, since
it would have to contain a binding for every natural number. We can
observe this problem right away if we begin the proof:
Theorem elements_complete_broken : elements_complete_broken_spec.
Proof.
unfold elements_complete_broken_spec. intros. induction t.
- (* t = E *) simpl.
We have nothing to work with, since elements E is [].
Abort.
The solution is to check first to see whether k is bound in t.
Only bound keys need be in the list of elements:
Definition elements_complete_spec :=
∀ (V : Type) (k : key) (v d : V) (t : tree V),
bound k t = true →
lookup d k t = v →
In (k, v) (elements t).
Exercise: 3 stars, standard (elements_complete)
Definition elements_correct_spec :=
∀ (V : Type) (k : key) (v d : V) (t : tree V),
BST t →
In (k, v) (elements t) →
bound k t = true ∧ lookup d k t = v.
Proving correctness requires more work than completeness.
BST uses ForallT to say that all nodes in the left/right
subtree have smaller/greater keys than the root. We need to
relate ForallT, which expresses that all nodes satisfy a
property, to Forall, which expresses that all list elements
satisfy a property.
The standard library contains a helpful lemma about Forall:
Exercise: 2 stars, standard (elements_preserves_forall)
Definition uncurry {X Y Z : Type} (f : X → Y → Z) '(a, b) :=
f a b.
Hint Transparent uncurry.
Lemma elements_preserves_forall : ∀ (V : Type) (P : key → V → Prop) (t : tree V),
ForallT P t →
Forall (uncurry P) (elements t).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (elements_preserves_relation)
Lemma elements_preserves_relation :
∀ (V : Type) (k k' : key) (v : V) (t : tree V) (R : key → key → Prop),
ForallT (fun y _ ⇒ R y k') t
→ In (k, v) (elements t)
→ R k k'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard (elements_correct)
- inverse completeness: if a binding is not in t then it's not
in elements t.
- inverse correctness: if a binding is not in elements t then it's not in t.
Exercise: 2 stars, advanced (elements_complete_inverse)
Theorem elements_complete_inverse :
∀ (V : Type) (k : key) (v : V) (t : tree V),
BST t →
bound k t = false →
¬ In (k, v) (elements t).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, advanced (elements_correct_inverse)
Lemma bound_value : ∀ (V : Type) (k : key) (t : tree V),
bound k t = true → ∃ v, ∀ d, lookup d k t = v.
Proof.
(* FILL IN HERE *) Admitted.
Prove the main result. You don't need induction.
Theorem elements_correct_inverse :
∀ (V : Type) (k : key) (t : tree V),
(∀ v, ¬ In (k, v) (elements t)) →
bound k t = false.
Proof.
(* FILL IN HERE *) Admitted.
☐
Part 2: Sorted (Advanced)
Exercise: 3 stars, advanced (sorted_app)
Lemma sorted_app: ∀ l1 l2 x,
Sort.sorted l1 → Sort.sorted l2 →
Forall (fun n ⇒ n < x) l1 → Forall (fun n ⇒ n > x) l2 →
Sort.sorted (l1 ++ x :: l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, advanced (sorted_elements)
Prove that elements t is sorted by keys. Proceed by induction
on the evidence that t is a BST.
Theorem sorted_elements : ∀ (V : Type) (t : tree V),
BST t → Sort.sorted (list_keys (elements t)).
Proof.
(* FILL IN HERE *) Admitted.
☐
Part 3: No Duplicates (Advanced and Optional)
The library is missing a theorem, though, about NoDup and ++.
To state that theorem, we first need to formalize what it means
for two lists to be disjoint:
Exercise: 3 stars, advanced, optional (NoDup_append)
Lemma NoDup_append : ∀ (X:Type) (l1 l2: list X),
NoDup l1 → NoDup l2 → disjoint l1 l2 →
NoDup (l1 ++ l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, advanced, optional (elements_nodup_keys)
Theorem elements_nodup_keys : ∀ (V : Type) (t : tree V),
BST t →
NoDup (list_keys (elements t)).
Proof.
(* FILL IN HERE *) Admitted.
☐
A Faster elements Implementation
Fixpoint fast_elements_tr {V : Type} (t : tree V)
(acc : list (key × V)) : list (key × V) :=
match t with
| E ⇒ acc
| T l k v r ⇒ fast_elements_tr l ((k, v) :: fast_elements_tr r acc)
end.
Definition fast_elements {V : Type} (t : tree V) : list (key × V) :=
fast_elements_tr t [].
Exercise: 3 stars, standard (fast_elements_eq_elements)
Lemma fast_elements_tr_helper :
∀ (V : Type) (t : tree V) (lst : list (key × V)),
fast_elements_tr t lst = elements t ++ lst.
Proof.
(* FILL IN HERE *) Admitted.
Lemma fast_elements_eq_elements : ∀ (V : Type) (t : tree V),
fast_elements t = elements t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Corollary fast_elements_correct :
∀ (V : Type) (k : key) (v d : V) (t : tree V),
BST t →
In (k, v) (fast_elements t) →
bound k t = true ∧ lookup d k t = v.
Proof.
intros. rewrite fast_elements_eq_elements in ×.
apply elements_correct; assumption.
Qed.
This corollary illustrates a general technique: prove the correctness
of a simple, slow implementation; then prove that the slow version
is functionally equivalent to a fast implementation. The proof of
correctness for the fast implementation then comes "for free".
An Algebraic Specification of elements
elements empty_tree = ...
elements (insert k v t) = ... (elements t) ...
Lemma elements_empty : ∀ (V : Type),
@elements V empty_tree = [].
Proof.
intros. simpl. reflexivity.
Qed.
But for the second equation, we have to express the result of
inserting (k, v) into the elements list for t, accounting for
ordering and the possibility that t may already contain a pair
(k, v') which must be replaced. The following rather ugly
function will do the trick:
Fixpoint kvs_insert {V : Type} (k : key) (v : V) (kvs : list (key × V)) :=
match kvs with
| [] ⇒ [(k, v)]
| (k', v') :: kvs' ⇒
if k <? k' then (k, v) :: kvs
else if k >? k' then (k', v') :: kvs_insert k v kvs'
else (k, v) :: kvs'
end.
That's not satisfactory, because the definition of
kvs_insert is so complex. Moreover, this equation doesn't tell
us anything directly about the overall properties of elements t
for a given tree t. Nonetheless, we can proceed with a rather
ugly verification.
Exercise: 3 stars, standard, optional (kvs_insert_split)
Lemma kvs_insert_split :
∀ (V : Type) (v v0 : V) (e1 e2 : list (key × V)) (k k0 : key),
Forall (fun '(k',_) ⇒ k' < k0) e1 →
Forall (fun '(k',_) ⇒ k' > k0) e2 →
kvs_insert k v (e1 ++ (k0,v0):: e2) =
if k <? k0 then
(kvs_insert k v e1) ++ (k0,v0)::e2
else if k >? k0 then
e1 ++ (k0,v0)::(kvs_insert k v e2)
else
e1 ++ (k,v)::e2.
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ (V : Type) (v v0 : V) (e1 e2 : list (key × V)) (k k0 : key),
Forall (fun '(k',_) ⇒ k' < k0) e1 →
Forall (fun '(k',_) ⇒ k' > k0) e2 →
kvs_insert k v (e1 ++ (k0,v0):: e2) =
if k <? k0 then
(kvs_insert k v e1) ++ (k0,v0)::e2
else if k >? k0 then
e1 ++ (k0,v0)::(kvs_insert k v e2)
else
e1 ++ (k,v)::e2.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma kvs_insert_elements : ∀ (V : Type) (t : tree V),
BST t →
∀ (k : key) (v : V),
elements (insert k v t) = kvs_insert k v (elements t).
Proof.
(* FILL IN HERE *) Admitted.
☐
BST t →
∀ (k : key) (v : V),
elements (insert k v t) = kvs_insert k v (elements t).
Proof.
(* FILL IN HERE *) Admitted.
☐
Model-based Specifications
- Any search tree corresponds to some functional partial map,
using a function or relation that we write down.
- The lookup operation on trees gives the same result as the
find operation on the corresponding map.
- Given a tree and corresponding map, if we insert on the tree and update the map with the same key and value, the resulting tree and map are in correspondence.
Fixpoint map_of_list {V : Type} (el : list (key × V)) : partial_map V :=
match el with
| [] ⇒ empty
| (k, v) :: el' ⇒ update (map_of_list el') k v
end.
Definition Abs {V : Type} (t : tree V) : partial_map V :=
map_of_list (elements t).
In general, model-based specifications may use an abstraction
relation, allowing each concrete value to be related to multiple
abstract values. But in this case a simple abstraction function
will do, assigning a unique abstract value to each concrete
one.
One small difference between trees and functional maps is that
applying the latter returns an option V which might be None,
whereas lookup returns a default value if key is not bound
lookup fails. We can easily provide a function on functional
partial maps having the latter behavior.
Definition find {V : Type} (d : V) (k : key) (m : partial_map V) : V :=
match m k with
| Some v ⇒ v
| None ⇒ d
end.
We also need a bound operation on maps.
Definition map_bound {V : Type} (k : key) (m : partial_map V) : bool :=
match m k with
| Some _ ⇒ true
| None ⇒ false
end.
We now proceed to prove that each operation preserves (or establishes)
the abstraction relationship in an appropriate way:
concrete abstract
-------- --------
empty_tree empty
bound map_bound
lookup find
insert update
The following lemmas will be useful, though you are not required
to prove them. They can all be proved by induction on the list.
concrete abstract
-------- --------
empty_tree empty
bound map_bound
lookup find
insert update
Exercise: 2 stars, standard, optional (in_fst)
Lemma in_fst : ∀ (X Y : Type) (lst : list (X × Y)) (x : X) (y : Y),
In (x, y) lst → In x (map fst lst).
Proof.
(* FILL IN HERE *) Admitted.
☐
In (x, y) lst → In x (map fst lst).
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma in_map_of_list : ∀ (V : Type) (el : list (key × V)) (k : key) (v : V),
NoDup (map fst el) →
In (k,v) el → (map_of_list el) k = Some v.
Proof.
(* FILL IN HERE *) Admitted.
☐
NoDup (map fst el) →
In (k,v) el → (map_of_list el) k = Some v.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma not_in_map_of_list : ∀ (V : Type) (el : list (key × V)) (k : key),
¬ In k (map fst el) → (map_of_list el) k = None.
Proof.
(* FILL IN HERE *) Admitted.
☐
¬ In k (map fst el) → (map_of_list el) k = None.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem bound_relate : ∀ (V : Type) (t : tree V) (k : key),
BST t →
map_bound k (Abs t) = bound k t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma lookup_relate : ∀ (V : Type) (t : tree V) (d : V) (k : key),
BST t → find d k (Abs t) = lookup d k t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma insert_relate : ∀ (V : Type) (t : tree V) (k : key) (v : V),
BST t → Abs (insert k v t) = update (Abs t) k v.
Proof.
(* TODO: find a direct proof that doesn't rely on kvs_insert_elements *)
unfold Abs.
intros.
rewrite kvs_insert_elements; auto.
remember (elements t) as l.
clear -l. (* clear everything not about l *)
(* Hint: proceed by induction on l. *)
(* FILL IN HERE *) Admitted.
☐
BST t → Abs (insert k v t) = update (Abs t) k v.
Proof.
(* TODO: find a direct proof that doesn't rely on kvs_insert_elements *)
unfold Abs.
intros.
rewrite kvs_insert_elements; auto.
remember (elements t) as l.
clear -l. (* clear everything not about l *)
(* Hint: proceed by induction on l. *)
(* FILL IN HERE *) Admitted.
☐
bound k t -------------------+ | | Abs | | V V m -----------------> b map_bound k lookup d k t -----------------> v | | Abs | | Some V V m -----------------> Some v find d k insert k v t -----------------> t' | | Abs | | Abs V V m -----------------> m' update' k v
update' k v m = update m k v
Lemma elements_relate : ∀ (V : Type) (t : tree V),
BST t →
map_of_list (elements t) = Abs t.
Proof.
unfold Abs. intros. reflexivity.
Qed.
An Alternative Abstraction Relation (Optional, Advanced)
Definition union {X} (m1 m2: partial_map X) : partial_map X :=
fun k ⇒
match (m1 k, m2 k) with
| (None, None) ⇒ None
| (None, Some v) ⇒ Some v
| (Some v, None) ⇒ Some v
| (Some _, Some _) ⇒ None
end.
We can prove some simple properties of lookup and update on unions,
which will prove useful later.
Exercise: 2 stars, standard, optional (union_collapse)
Lemma union_left : ∀ {X} (m1 m2: partial_map X) k,
m2 k = None → union m1 m2 k = m1 k.
Proof.
(* FILL IN HERE *) Admitted.
Lemma union_right : ∀ {X} (m1 m2: partial_map X) k,
m1 k = None →
union m1 m2 k = m2 k.
Proof.
(* FILL IN HERE *) Admitted.
Lemma union_both : ∀ {X} (m1 m2 : partial_map X) k v1 v2,
m1 k = Some v1 →
m2 k = Some v2 →
union m1 m2 k = None.
Proof.
(* FILL IN HERE *) Admitted.
☐
m2 k = None → union m1 m2 k = m1 k.
Proof.
(* FILL IN HERE *) Admitted.
Lemma union_right : ∀ {X} (m1 m2: partial_map X) k,
m1 k = None →
union m1 m2 k = m2 k.
Proof.
(* FILL IN HERE *) Admitted.
Lemma union_both : ∀ {X} (m1 m2 : partial_map X) k v1 v2,
m1 k = Some v1 →
m2 k = Some v2 →
union m1 m2 k = None.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma union_update_right : ∀ {X} (m1 m2: partial_map X) k v,
m1 k = None →
update (union m1 m2) k v = union m1 (update m2 k v).
Proof.
(* FILL IN HERE *) Admitted.
Lemma union_update_left : ∀ {X} (m1 m2: partial_map X) k v,
m2 k = None →
update (union m1 m2) k v = union (update m1 k v) m2.
Proof.
(* FILL IN HERE *) Admitted.
☐
m1 k = None →
update (union m1 m2) k v = union m1 (update m2 k v).
Proof.
(* FILL IN HERE *) Admitted.
Lemma union_update_left : ∀ {X} (m1 m2: partial_map X) k v,
m2 k = None →
update (union m1 m2) k v = union (update m1 k v) m2.
Proof.
(* FILL IN HERE *) Admitted.
☐
Fixpoint map_of_tree {V : Type} (t: tree V) : partial_map V :=
match t with
| E ⇒ empty
| T l k v r ⇒ update (union (map_of_tree l) (map_of_tree r)) k v
end.
Lemma map_of_tree_prop : ∀ (V : Type) (P : key → V → Prop) (t : tree V),
ForallT P t →
∀ k v, (map_of_tree t) k = Some v →
P k v.
Proof.
(* FILL IN HERE *) Admitted.
☐
ForallT P t →
∀ k v, (map_of_tree t) k = Some v →
P k v.
Proof.
(* FILL IN HERE *) Admitted.
☐
Definition Abs' {V : Type} (t: tree V) : partial_map V :=
map_of_tree t.
Lemma empty_relate' : ∀ (V : Type),
@Abs' V empty_tree = empty.
Proof.
reflexivity.
Qed.
Theorem bound_relate' : ∀ (V : Type) (t : tree V) (k : key),
BST t →
map_bound k (Abs' t) = bound k t.
Proof.
(* FILL IN HERE *) Admitted.
☐
BST t →
map_bound k (Abs' t) = bound k t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma lookup_relate' : ∀ (V : Type) (d : V) (t : tree V) (k : key),
BST t → find d k (Abs' t) = lookup d k t.
Proof.
(* FILL IN HERE *) Admitted.
☐
BST t → find d k (Abs' t) = lookup d k t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma insert_relate' : ∀ (V : Type) (k : key) (v : V) (t : tree V),
BST t → Abs' (insert k v t) = update (Abs' t) k v.
Proof.
(* FILL IN HERE *) Admitted.
☐
BST t → Abs' (insert k v t) = update (Abs' t) k v.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, advanced, optional (map_of_list_app)
Lemma map_of_list_app : ∀ (V : Type) (el1 el2: list (key × V)),
disjoint (map fst el1) (map fst el2) →
map_of_list (el1 ++ el2) = union (map_of_list el1) (map_of_list el2).
Proof.
(* FILL IN HERE *) Admitted.
☐
disjoint (map fst el1) (map fst el2) →
map_of_list (el1 ++ el2) = union (map_of_list el1) (map_of_list el2).
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma elements_relate' : ∀ (V : Type) (t : tree V),
BST t →
map_of_list (elements t) = Abs' t.
Proof.
(* FILL IN HERE *) Admitted.
☐
BST t →
map_of_list (elements t) = Abs' t.
Proof.
(* FILL IN HERE *) Admitted.
☐
Efficiency of Search Trees
- SOLUTION: use an algorithm that ensures the trees stay balanced. We'll do that in Redblack.
- SOLUTION: represent keys by a data type that has a more efficient comparison operator. We used nat in this chapter because it's something easy to work with.
- SOLUTION 1: Don't prove (in Coq) that they're efficient;
just prove that they are correct. Prove things about their
efficiency the old-fashioned way, on pencil and paper.
- SOLUTION 2: Prove in Coq some facts about the height of the
trees, which have direct bearing on their efficiency. We'll
explore that in Redblack.
- SOLUTION 3: Apply bleeding-edge frameworks for reasoning about run-time of programs represented in Coq.
- SOLUTION: Use Coq's extraction feature to derive the real implementation (in Ocaml or Haskell) automatically from the Coq function. Or, use Coq's Compute or Eval native_compute feature to compile and run the programs efficiently inside Coq. We'll explore extraction in a Extract.
(* 2021-05-04 07:54 *)