# SearchTreeBinary Search Trees

*binary search trees*(BSTs). Insert and lookup operations on BSTs take time proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.

- 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}.

| 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.

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.

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.

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_ex

insert 5 "five" (insert 2 "two" (insert 4 "four" empty_tree)) = ex_tree.

Proof. reflexivity. Qed.

Example bst_ex

Proof. reflexivity. Qed.

Example bst_ex

Proof. reflexivity. Qed.

Example bst_ex

Proof. reflexivity. Qed.

End Tests.

Example bst_ex

_{1}:insert 5 "five" (insert 2 "two" (insert 4 "four" empty_tree)) = ex_tree.

Proof. reflexivity. Qed.

Example bst_ex

_{2}: lookup "" 5 ex_tree = "five".Proof. reflexivity. Qed.

Example bst_ex

_{3}: lookup "" 3 ex_tree = "".Proof. reflexivity. Qed.

Example bst_ex

_{4}: 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

*BST invariant*: for any non-empty node with key k, all the values of the left subtree are less than k and all the values of the right subtree are greater than k. But that invariant is not part of the definition of tree. For example, the following tree is not a BST:

Module NotBst.

Open Scope string_scope.

Definition t : tree string :=

T (T E 5 "five" E) 4 "four" (T E 2 "two" E).

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.

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.

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.

| 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 H

Qed.

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 H

_{3}. 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.

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.

☐

BST t → BST (insert k v t).

Proof.

(* FILL IN HERE *) Admitted.

☐

# Correctness of BST Operations

*algebraic specification*. With it, we write down equations relating the results of operations. For example, we could write down equations like the following to specify the + and × 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 <? k

+ bdestruct (k <? k

+ bdestruct (k <? k

+ bdestruct (k

Qed.

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 <? k

_{0}); bdestruct (k_{0}<? k); simpl; try lia; auto.+ bdestruct (k <? k

_{0}); bdestruct (k_{0}<? k); try lia; auto.+ bdestruct (k <? k

_{0}); bdestruct (k_{0}<? k); try lia; auto.+ bdestruct (k

_{0}<? k_{0}); 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.

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.

∀ (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.

☐

(* 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.

☐

∀ (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 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 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'.

∀ (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) (v

t_update (t_update m k v

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) (v

k

t_update (t_update m k

_{1}v_{2}: V) (k : key),t_update (t_update m k v

_{1}) k v_{2}= t_update m k v_{2}.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) (v

_{1}v_{2}: V) (k_{1}k_{2}: key) (m : total_map V),k

_{2}≠ k_{1}→t_update (t_update m k

_{2}v_{2}) k_{1}v_{1}= t_update (t_update m k_{1}v_{1}) k_{2}v_{2}.
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.

☐

∀ (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.

☐

∀ (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) (v

k

lookup d k' (insert k

= lookup d k' (insert k

Proof.

(* FILL IN HERE *) Admitted.

☐

∀ (V : Type) (v

_{1}v_{2}d : V) (k_{1}k_{2}k': key) (t : tree V),k

_{1}≠ k_{2}→lookup d k' (insert k

_{1}v_{1}(insert k_{2}v_{2}t))= lookup d k' (insert k

_{2}v_{2}(insert k_{1}v_{1}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.

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) (v

k

Proof.

(* FILL IN HERE *) Admitted.

☐

∃ (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) (v

_{1}v_{2}: V) (k_{1}k_{2}: key) (t : tree V),k

_{1}≠ k_{2}∧ insert k_{1}v_{1}(insert k_{2}v_{2}t) ≠ insert k_{2}v_{2}(insert k_{1}v_{1}t).Proof.

(* FILL IN HERE *) Admitted.

☐

# Converting a BST to a List

*association list*that contains the key--value bindings from the tree stored as pairs. If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list. Here's a function that does so with an in-order traversal of the tree:

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.

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).

∀ (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.

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).

∀ (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.

∀ (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)

*uncurry*P when we pass it to Forall. (See Poly for more about uncurrying.) The single quote used below is the Coq syntax for doing a pattern match in the function arguments.

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.

☐

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.

☐

∀ (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.

☐

∀ (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.

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.

☐

∀ (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)

_{1}is sorted.

Lemma sorted_app: ∀ l

Sort.sorted l

Forall (fun n ⇒ n < x) l

Sort.sorted (l

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}l_{2}x,Sort.sorted l

_{1}→ Sort.sorted l_{2}→Forall (fun n ⇒ n < x) l

_{1}→ Forall (fun n ⇒ n > x) l_{2}→Sort.sorted (l

_{1}++ x :: l_{2}).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.

☐

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) (l

NoDup l

NoDup (l

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}l_{2}: list X),NoDup l

_{1}→ NoDup l_{2}→ disjoint l_{1}l_{2}→NoDup (l

_{1}++ l_{2}).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.

☐

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 [].

(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.

☐

∀ (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.

∀ (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.

@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.

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 v

Forall (fun '(k',_) ⇒ k' < k

Forall (fun '(k',_) ⇒ k' > k

kvs_insert k v (e

if k <? k

(kvs_insert k v e

else if k >? k

e

else

e

Proof.

(* FILL IN HERE *) Admitted.

☐

∀ (V : Type) (v v

_{0}: V) (e_{1}e_{2}: list (key × V)) (k k_{0}: key),Forall (fun '(k',_) ⇒ k' < k

_{0}) e_{1}→Forall (fun '(k',_) ⇒ k' > k

_{0}) e_{2}→kvs_insert k v (e

_{1}++ (k_{0},v_{0}):: e_{2}) =if k <? k

_{0}then(kvs_insert k v e

_{1}) ++ (k_{0},v_{0})::e_{2}else if k >? k

_{0}thene

_{1}++ (k_{0},v_{0})::(kvs_insert k v e_{2})else

e

_{1}++ (k,v)::e_{2}.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.

*model-based specification*: we show that our implementation of a data type corresponds to a more more abstract

*model*type that we already understand. To reason about programs that use the implementation, it suffices to reason about the behavior of the abstract type, which may be significantly easier. For example, we can take advantage of laws that we proved for the abstract type, like update_eq for functional maps, without having to prove them again for the concrete tree type.

*abstraction*relation between trees and maps, and show that it is maintained by all operations. In the end, about the same amount of work is needed to show correctness, though the work shows up in different places depending on how the abstraction relation is defined.

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).

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
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.

*function*will do, assigning a unique abstract value to each concrete one.
Definition find {V : Type} (d : V) (k : key) (m : partial_map V) : V :=

match m k with

| Some v ⇒ v

| None ⇒ d

end.

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.

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.

☐

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.

☐

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.

BST t →

map_of_list (elements t) = Abs t.

Proof.

unfold Abs. intros. reflexivity.

Qed.

# An Alternative Abstraction Relation (Optional, Advanced)

Definition union {X} (m

fun k ⇒

match (m

| (None, None) ⇒ None

| (None, Some v) ⇒ Some v

| (Some v, None) ⇒ Some v

| (Some _, Some _) ⇒ None

end.

_{1}m_{2}: partial_map X) : partial_map X :=fun k ⇒

match (m

_{1}k, m_{2}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} (m

m

Proof.

(* FILL IN HERE *) Admitted.

Lemma union_right : ∀ {X} (m

m

union m

Proof.

(* FILL IN HERE *) Admitted.

Lemma union_both : ∀ {X} (m

m

m

union m

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}m_{2}: partial_map X) k,m

_{2}k = None → union m_{1}m_{2}k = m_{1}k.Proof.

(* FILL IN HERE *) Admitted.

Lemma union_right : ∀ {X} (m

_{1}m_{2}: partial_map X) k,m

_{1}k = None →union m

_{1}m_{2}k = m_{2}k.Proof.

(* FILL IN HERE *) Admitted.

Lemma union_both : ∀ {X} (m

_{1}m_{2}: partial_map X) k v_{1}v_{2},m

_{1}k = Some v_{1}→m

_{2}k = Some v_{2}→union m

_{1}m_{2}k = None.Proof.

(* FILL IN HERE *) Admitted.

☐

Lemma union_update_right : ∀ {X} (m

m

update (union m

Proof.

(* FILL IN HERE *) Admitted.

Lemma union_update_left : ∀ {X} (m

m

update (union m

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}m_{2}: partial_map X) k v,m

_{1}k = None →update (union m

_{1}m_{2}) k v = union m_{1}(update m_{2}k v).Proof.

(* FILL IN HERE *) Admitted.

Lemma union_update_left : ∀ {X} (m

_{1}m_{2}: partial_map X) k v,m

_{2}k = None →update (union m

_{1}m_{2}) k v = union (update m_{1}k v) m_{2}.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.

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.

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) (el

disjoint (map fst el

map_of_list (el

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}el_{2}: list (key × V)),disjoint (map fst el

_{1}) (map fst el_{2}) →map_of_list (el

_{1}++ el_{2}) = union (map_of_list el_{1}) (map_of_list el_{2}).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-08-11 15:15 *)