Maps (also called dictionaries, lookup tables, associative arrays, etc.) are a fundamental data structure in computing; they maintain an association between keys and values. At a minimum, a map implementation should support operations to create a new empty map, to look up the value corresponding to a key, and to insert a new key-to-value association into the map. Map implementations might also support other operations, such as returning a list of all key-to-value associations in the map, removing a key, etc. Binary search trees are an efficient data structure for implementing maps. We have already seen other map representations, including lists (the type partial_map from the Lists chapter) and functions (the types total_map and partial_map in the Maps chapter). Both of these are inefficient implementations: if you add N items to your map, then looking them up takes N comparisons in the worst case, and N/2 comparisons in the average case. In contrast, if your key type is a total order -- that is, if it has a less-than comparison that's transitive and antisymmetric a<b ↔ ~(b<a) then you can implement maps using binary search trees (BSTs). Insert and lookup operations on BSTs take time proportional to the height of the tree, which will be proportional to logN if the trees are roughly balanced. We will assume you know how BSTs work; you can learn this from:

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

Our focus here is to prove the correctness of an implementation of maps using binary search trees. For this purpose, we will consider partial maps containing a finite number of keys, and the lookup operation will take an extra argument giving a default value to be returned if the desired key is not present. (This behavior is a bit different from that of the partial maps defined in Maps, as we will discuss further below.) Finally, we will fix our keys to be of type nat, which is certainly a total order.

Sections

We will use Coq's Section feature to structure this development, so first a brief introduction to Sections. We'll use as example a fragment of a list-based implementation of maps.

It sure is tedious to repeat the V and default parameters in every definition and every theorem. The Section feature allows us to declare them as parameters to every definition and theorem in the entire section:

At the close of the section, this produces exactly the same result: the functions that "need" to be parametrized by V or default are given extra parameters:

==>
   SectionExample2.mymap = fun V : Type ⇒ list (nat × V)
    : Type → Type

==>
SectionExample2.empty
     : ∀ V : Type, SectionExample2.mymap V

==>
SectionExample2.lookup
     : ∀ V : Type, V → nat → SectionExample2.mymap V → V

Program for Binary Search Trees

Now we introduce a tree-based representation for maps, with nat keys and and values drawn from some arbitrary type V, and these operations:

• empty_tree returns a new empty tree
• lookup d k t returns the value corresponding to key k in tree t, or returns default value d if k is not in the tree.
• insert k v t returns a new tree formed by inserting a mapping from k to v into tree t. Note that tree t itself is not changed.
• elements t returns a list of (key,value) mappings contained in t.

Our assumption is that our binary search trees will only be constructed or inspected using these operations; in other words, we want to treat them as an abstract data type for maps, whose internal representation is not visible to clients making use of maps. (This assumption is not enforced by the Coq code in this chapter; we will see how it can be in a future chapter.)

We could also add a section Variable default, but it is clearer to keep it as an explicit parameter where needed.

We expect these trees to be Binary Search Trees (BST)'s, i.e.: 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. However, this fact is not encoded in the tree inductive definition. And as we'll see shortly, it is not actually essential for making lookup and insert work correctly!

If you're wondering why we didn't implement elements more simply with ++, we'll return to that question below when we discuss a function named slow_elements; feel free to peek ahead now if you're curious.

Search Tree Examples

Properties of lookup and insert

Now that we have our definitions, what should we formally prove about them? How can we even go about determining what a satisfactory specification looks like? There are several well-established approaches to specifying abstract data types. They share the goal of describing the behavior of the operations without reference to the internal representation of the type (in this case, as a tree). In algebraic specification, we write down equations relating the results of different operations. More specifically, we divide the operations into two classes: constructors create new instances of the type and observers extract information from existing instances. We then write down equations describing the behavior of each observer on each possible combination of constructors. In the present case, our constructors are empty_tree and insert, and our observers are lookup and elements. Let's first focus on lookup, and how it should behave on different combinations of constructors. It is easy to see what needs to be true for empty_tree: looking up any value at all in the empty tree should fail and return the default value: ∀ d k, lookup d k empty_tree = d What about non-empty trees? The essential observation here is that the only way to build a non-empty tree is by applying insert k v t to an existing tree t. So it suffices to describe the behavior of lookup on the result of an arbitrary insert operation. There are two cases. If we look up the same key that was just inserted, we should get the value that was inserted with it: ∀ d k v t, lookup d k (insert k v t) = v On the hand, if we look up a different key than was just inserted, the insert should not affect the answer, which should be the same as if we did the lookup in the original dictionary before the insert occured: ∀ d k k' v t, k ≠ k' → lookup d k' (insert k v t) = lookup d k' t It turns out that these three rules are all that is necessary to fully characterize a map-like type with the functions empty, insert, and lookup. They have the nice feature of explaining the behavior of the "type of interest" (maps) in terms of simple equality statements on the type V of values, which we presumably already understand. Let's prove these three basic laws!

It seems like the basic method of this proof is simply to bdestruct everything in sight. This calls for automation!.

Exercise: 2 stars, standard (lookup_insert_neq)

First, prove this without bdall, just using induction, simpl, bd₁, auto, omega, and auto. In the process, try to understand the case analysis used in this proof.

Now, make a more automated proof using bdall.

Perhaps surprisingly, the proofs of these results do not depend on knowing that the tree t actually has the BST property! That is, even if we start with a tree that has values "in the wrong order" the above theorems hold. Intuitively, that's because lookup and insert follow the same path through the tree, so even if that path is "wrong" it will be consistently "wrong".

Derived Properties

The three rules proved here may look familiar, because we developed and proved very similar rules in Maps for maps defined as functions, where tree insert corresponds to functional map update and tree lookup corresponds to applying the functional map to an argument. The corresponding rules we defined there for partial maps were:

The similarity of these laws is no accident! Since we claimed that our three laws were fundamental to map-like structures, they should certainly be true of functional maps. In Maps, we also proved several other useful lemmas about the behavior of functional maps on various combinations of updates and lookups:

To provide some evidence for our claim that the three laws we have already proved on search trees are sufficient to characterize all operations on empty_tree, insert, and lookup, let's prove analogs to these three lemmas for search trees, using only the three basic rules that we have already proven. That is, in the following proofs, you should not use the definition of empty_tree, insert, or lookup, only the three lemmas lookup_empty (not actually needed), lookup_insert_eq, and lookup_insert_neq. Our ability to prove these lemmas without reference to the underlying map implementation (trees) demonstrates they hold for any map implementation for which the three basic rules hold.

Exercise: 2 stars, standard (lookup_insert_shadow)

Exercise: 2 stars, standard (lookup_insert_same)

Exercise: 2 stars, standard (lookup_insert_permute)

You may have noticed that each of these lemmas was phrased as an equality between the results of looking up an arbitrary key k' in two maps, rather than as a direct equality between the maps themselves, as was the case for the function-based map lemmas update_shadow, etc. There's a good reason for this: the more direct equalities on search trees are not all true! Can you figure out which ones are false? It is quite common for the concrete realization of an abstract data type to allow multiple concrete values to correspond to a single abstract value. In such situations, there are quite likely to be equalities between abstract values that are not necessarily true on (all) the corresponding concrete ones. The way to work around this situation is to phrase specifications in terms of an observer function, like lookup in this case.

Exercise: 3 stars, standard, optional (direct_equalities)

Determine which of the following properties are actually true. For the ones that are not, explain what goes wrong.

Properties of elements

Now let's consider how to specify and prove correctness of elements. Actually, before we do that, let's consider a simpler version.

This one is easier to understand than the elements function, because it doesn't carry the base list around in its recursion. Unfortunately, its running time is NlogN even if the tree is roughly balanced, because it does a linear number of list concatentation steps for each level of the tree. The original elements function takes linear time overall (even if the tree is unbalanced), which is a more efficient. To prove correctness of elements, it's actually easier to first prove that it's equivalent to slow_elements, then prove the correctness of slow_elements. We don't care that slow_elements is a bit slow, because we're never going to really run it; it's just there to support the proof.

Exercise: 3 stars, standard, optional (elements_slow_elements)

Now, what should we prove about elements (or slow_elements) ? The algrebraic specification approach would suggest that we look for equations of the form elements empty_tree = ... and elements (insert k v t) = ...(elements t)... The first of these is easy; we can trivially prove

For the second, 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. I claim that the following function will do the trick:

However, this is not terribly satisfactory. First of all, proving that elements (insert k v t) = kvs_insert k v (elements t) is not trivial, although you'll be given an opportunity to do so later on. But more importantly, the definition of kvs_insert is sufficiently complex that it is hard to see exactly what it does without thinking a bit. Moreover, this equation doesn't tell us anything directly about the overall properties of elements t for a given tree t. So for now, let's take a more ad hoc approach to coming up with suitable properties. Surely one requirement is that if looking up a value in the search tree produces a value, then that value should be in the result list of elements. Let's try to prove that:

==>
fix In (a : A) (l : list A) {struct l} : Prop :=
  match l with
  | [] ⇒ False
  | b :: m ⇒ b = a ∨ In a m
  end
     : ∀ A : Type, A → list A → Prop

We forgot that lookup might return the default value d for some k, which typically will not be in the elements list (although it might be!). Let's try again:

We were successful this time, but this theorem is just a little weaker than we might like in practice. We'll see a way to strengthen it further below. Meanwhile, how about a converse property: if a (key,value) pair appears in elements then looking up that key in the search tree should produce that value.

The problem is that we need to know we are working with a properly formed binary search tree! Otherwise, we don't know that the lookup path will sucessfully find every key in the tree. Let's recall the definition of BSTs over natural numbers:

• An empty tree is a binary search tree.
• A nonempty tree is a binary search tree if the root element is greater than every element in the left sub-tree and less than every element in the right sub-tree, and the left and right subtrees are themselves binary search trees.

Here is one way to formalize this property in Coq: ForallT P t holds if P k v holds for every (k,v) node of the tree t.

BST t holds if t is a BST.

Exercise: 1 star, standard (is_bst)

Exercise: 1 star, standard (is_not_bst)

How do we know that all the trees we will encounter (particularly, that the elements function will encounter), have the BST property? Well, the empty tree is a BST; and if you insert into a tree that's a BST, then the result is a BST; and these are the only ways that you're supposed to build trees. So we need to prove those two theorems.

Exercise: 1 star, standard (empty_tree_BST)

Exercise: 3 stars, standard (insert_BST)

You may want to start with an auxiliary lemma relating ForallT and insert

Now that we're equipped with BSTs, let us return to proving In_elements_lookup, i.e. that if a (key,value) pair appears in elements then looking up that key in the search tree should produce that value. We will find it very useful to relate the ForallT predicate on trees with the standard Forall predicate on the lists produced by slow_elements.

This lemma is apparently missing from the standard library.

Here's the key connection between trees and their elements. (The tick mark in the lambda-expression fun '(k,v) ⇒ P k v is needed to allow pattern matching against a pair.)

Exercise: 3 stars, standard (In_elements_lookup)

Finally, we're in a position to prove our theorem. This is easiest done by induction on evidence that t is a BST.

Now let's return briefly to our lookup_In_elements theorem.

==>
lookup_In_elements_second_try
     : ∀ (d: V) (t : tree) (k : key) (v : V),
       lookup d k t = v → In (k, v) (elements t) ∨ v = d

This result is not quite strong enough to characterize elements the way we will need later on, because in the case lookup d k t returns d, it says nothing about whether elements t has an entry with key k or not! In particular, elements t might contain an entry (k,v') for some v' different from d, without violating this theorem. What we really want is to say that if v = d then elements t either contains (k,d) or no entry for with key k at all. It turns out that a theorem along these lines is also provable, but only if we know that t is a BST. (That's why we didn't try to prove something like this earlier.) In fact, we can prove it from the lemmas we already have, without reference to the definitions of lookup and elements. The proof uses a trick we haven't seen before: since membership in a list of nats is a decidable proposition, we can do a case split on the two possibilities.

Another important fact about elements is that it contains no duplicate keys. This is something we surely want to be true for any implementation of maps.

Exercise: 3 stars, standard, optional (NoDup_append)

Exercise: 3 stars, standard, optional (elements_keys_distinct)

There is at least one more simple and interesting fact about our implementation of elements, which we might perhaps want to include in its specification, but is not implied by the specification we have so far. The next exercise encourages you to think about this.

Exercise: 4 stars, advanced, optional (elements_spec)

State and prove a nontrivial fact about elements that is not implied by In_elements_lookup, lookup_In_elements and elements_keys_distinct.

Finally, let's return to our equation connecting slow_elements, insert, and kvs_insert. The auxiliary ideas and lemmas developed above should be helpful in proving this. Note that it is only true for trees having the BST property. The suggested approach is to first prove an auxiliary lemma about the behavior of kvs_insert; with this in hand, the main lemma is straightforward. Hint: remember the bdall tactic!

Exercise: 3 stars, standard, optional (kvs_insert_split)

Exercise: 3 stars, standard, optional (kvs_insert_elements)

Efficiency of Search Trees

All the theory we've developed so far has been about correctness. But the reason we use binary search trees is that they are efficient. That is, if there are N elements in a (reasonably well balanced) BST, each insertion or lookup takes about logN time. What could go wrong? 1. The search tree might not be balanced. In that case, each insertion or lookup will take as much as linear time.

• SOLUTION: use an algorithm, such as "red-black trees", that ensures the trees stay balanced. We'll do that in Chapter RedBlack.

2. Our keys are natural numbers, and Coq's nat type takes linear time per comparison. That is, computing (j <? k) takes time proportional to the value of k-j.

• SOLUTION: represent keys by a data type that has a more efficient comparison operator. We just use nat in this chapter because it's something you're already familiar with.

3. There's no notion of "run time" in Coq. That is, we can't say what it means that a Coq function "takes N steps to evaluate." Therefore, we can't prove that binary search trees are efficient.

• 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 later chapters.
• SOLUTION 3: Apply bleeding-edge frameworks for reasoning about run-time of programs represented in Coq.

4. Our functions in Coq aren't real implementations; they are just pretend models of real implementations. What if there are bugs in the correspondence between the Coq function and the real implementation?

• 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 later chapter.

Model-based specifications

Another approach to proving correctness of search trees might be to relate them to our existing implementation of functional partial maps, as developed in Maps. To prove the correctness of a search-tree algorithm, we can prove:

• 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.
• Functional maps have the properties we actually wanted. It would do no good to prove that searchtrees correspond to some abstract type X, if X didn't have useful properties!

This approach is sometimes called 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. We also need to be careful here, because the type of functional maps as defined in Maps do not actually behave quite like our tree-based maps. For one thing, functional maps can be defined on an infinite number of keys, and there is no mechanism for enumerating over the key set. To maintain correspondence with our finite trees, we need to make sure that we consider only functional maps built by finitely many applications of constructor functions (empty and update). Also, thanks to functional extensionality, functional maps obey stronger equality laws than our trees do (as we investigated in the direct_equalities exercise), so we should not be misled into thinking that every fact we can prove about abstract maps necessarily holds for concrete ones. Compared to the algebraic specification approach described earlier in this chapter, the model based approach can save some proof effort, especially if we already have a well-developed theory for the abstract model type. On the other hand, we have to give an explicit 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. For search trees, it is not clear that model-based specification is worth the effort. The simple algebraic rules for lookup and the indirect characterization of elements by its properties are simpler and adequate to support reasoning by clients of the type. However, we will find the model-based approach very useful in later chapters where we deal with data types that do not enjoy simple algebraic laws. So, in order to prepare for that, we will give a model-based specification for trees in terms of functional partial maps. It is based on a simple abstraction relation that builds a functional map element by element:

The following utility functions will prove useful. They are simple to prove by induction on el, using the basic laws on functional partial maps.

Exercise: 2 stars, standard (list2map_yes)

Exercise: 2 stars, standard (list2map_no)

In general, model-based specifications may use an abstraction relation, allowing each concrete value to be related to multiple abstract values. But often, as 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 our lookup operation returns a default value if the lookup fails. We can easily provide a function on functional partial maps having the latter behavior.

We now proceed to prove that each operation preserves (or establishes) the abstraction relationship in an appropriate way:
    concrete abstract
    -------- --------
    empty_tree empty
    lookup find
    insert update
    elements (see below)

Since functional partial maps lack a way to extract or iterate over their elements, we cannot give an analogous abstract operation for elements, but the abstraction function itself gives a strong relationship that we can take as a (trivially satisfiable) part of the specification. Thanks to various lemmas we proved earlier about elements, the following results are quite straightforward. Note that they do require the trees to be BSTs. It is quite typical that a model-based specification only works when we restrict the concrete reprsentation to obey some invariant.

Exercise: 3 stars, standard (lookup_relate)

Exercise: 3 stars, standard (insert_relate)

An alternative abstraction relation (Optional, Advanced)

There is often more than one way to specify a suitable Abstraction relation between given concrete and abstract datatypes. The following exercises explore another way to relate search trees to functional partial maps without using elements as an intermediate step. We extend our definition of functional partial maps by adding a new primitive for combining two partial maps, which we call union. Our intention is that it only be used to combine maps with disjoint key sets; to keep the operation symmetric, we make the result be undefined on any key they have in common.

We can prove some simple properties of lookup and update on unions, which will prove useful later.

Exercise: 2 stars, standard, optional (union_collapse)

Exercise: 3 stars, standard, optional (union_update)

We can now write a direct conversion function from trees to maps based on the structure of the tree, and prove a basic property preservation result.

Exercise: 3 stars, advanced, optional (tree2map_prop)

Finally, we define our new abstraction function, and prove the same commutation lemmas as before.

Exercise: 3 stars, advanced, optional (lookup_relate')

Exercise: 4 stars, advanced, optional (insert_relate')

The elements_relate lemma, which was trivial for our previous Abs function, is considerably harder this time. We suggest starting with an auxiliary lemma.

Exercise: 3 stars, advanced, optional (list2map_app)

Exercise: 4 stars, advanced, optional (elements_relate')