Binary search trees are an efficient data structure for lookup tables, that is, mappings from keys to values. The total_map type from Maps.v is an inefficient implementation: if you add N items to your total_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 one can implement binary search trees (BSTs). 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 binary search trees.

Total and Partial Maps

Recall the Maps chapter of Volume 1 (Logical Foundations), describing functions from identifiers to some arbitrary type A. VFA's Maps module is almost exactly the same, except that it implements functions from nat to some arbitrary type A.

Sections

We will use Coq's Section feature to structure this development, so first a brief introduction to Sections. We'll use the example of lookup tables implemented by lists.

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 have been generalized to take them as parameters:

We can even prove that the two definitions are equivalent, as follows.

For lookup, the proof is a bit harder. The problem is that the two lookup functions are not implemented in quite the same way:

When the Section added parameters to SectionExample2.lookup, they came as a result of function fun (V : Type) (default : V) ... wrapped around the actual lookup function. So, reflexivity isn't enough to complete the proof.

Instead, we need to prove that the two lookup functions compute the same result when applied to the same arguments. That is, we want to use the Axiom of Functional Extensionality, which is discussed in Logic and provided by the standard library's Logic.FunctionalExentionality module. Recall that functions f and g are extensionally equal if, for every argument x, it holds that f x = g x. The Axiom of Functional Extensionality says that if two functions are extensionally equal, then they are equal. The extensionality tactic, which we use next, is a convenient way of applying the axiom.

Binary Search Tree Implementation

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

Efficiency of BSTs

We use binary search trees because they are efficient. That is, if there are N elements in a (reasonably well balanced) BST, each insertion or lookup takes about log N 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. We have no formalization of running time or time complexity 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.

What Should We Prove About Search trees?

Search trees are meant to be an implementation of maps. That is, they have an insert function that corresponds to the update function of a map, and a lookup function that corresponds to applying the map to an argument. To prove the correctness of a search-tree algorithm, we can prove:

• Any search tree corresponds to some map, using a function or relation that we demonstrate.
• The lookup function gives the same result as applying the map.
• The insert function returns a corresponding map.
• Maps have the properties we actually want.
  What properties do we want search trees to have? If I insert the binding (k,v) into a search tree t, then look up k, I should get v. If I look up k' in insert (k,v) t, where k'≠k, then I should get the same result as lookup k t. There are several more such properties, which are already proved about total_map in the Maps module:

So, if we like those properties that total_map is proved to have, and we can prove that search trees behave like maps, then we don't have to reprove each individual property about search trees. More generally: a job worth doing is worth doing well. It does no good to prove the "correctness" of a program, if you prove that it satisfies a wrong or useless specification.

Abstraction Relation

We claim that a tree "corresponds" to a total_map. So we must exhibit an abstraction relation Abs: tree → total_map V → Prop. The idea is that Abs t m says that tree t is a representation of map m; or that map m is an abstraction of tree t. How should we define this abstraction relation? The empty tree is easy: Abs E (fun x ⇒ default). Now, what about this tree?:

Exercise: 2 stars, standard (example_map)

Fill in the definition of example_map with a total_map that you think example_tree should correspond to. Use t_update and (t_empty default). When you are finished, the unit tests below should all be provable with reflexivity.

Exercise: 3 stars, standard (check_example_map)

Prove that your example_map is the right one. Start by proving the following auxiliary lemma that will make Abs_T easier to work with.

Now proceed with the proof about your example_map. Hint: to prove the equality of two non-empty maps, use functional extensionality to make the argument to the map (that is, a key) manifest. Reduce both maps to expressions involving just functions, if expressions, and Boolean comparisons. Then you can repeatedly destruct the key argument and simplify.

       lookup k
    t ----------+
    |            \
Abs |             +--> v
    V            /
    m ----------+
       lookup k

        insert k v
    t --------------> t'
    |                 |
Abs |                 | Abs
    V                 V
    m --------------> m'
        update k v

Exercise: 3 stars, standard, optional (elements_relate_informal)

Don't prove this yet. Instead, explain in your own words, with examples, why this ought to be true. It's OK if your explanation is not a formal proof; it's even OK if your explanation is subtly wrong! Just make it convincing.

To prove the first subgoal, prove that m=m' (by extensionality) and then use H. To prove the second subgoal, do an intro so that you can assume update_list (t_empty default) (elements bogus) = m, then show that update_list (t_empty default) (elements bogus) 3 ≠ m 3. That's a contradiction. To prove the third subgoal, just destruct Paradox and use the contradiction. In all 3 goals, when you need to unfold local definitions such as bogus you can use unfold bogus or subst bogus.

This is probably provable. But the SearchTreeX property is quite unwieldy, with its two Fixpoints nested inside a Fixpoint.

Instead of using SearchTreeX, let's reformulate the search tree property as an inductive proposition without any nested induction. SearchTree' lo t hi will hold of a tree t satisfying the BST invariant whose keys are between lo (inclusive) and hi (exclusive), where lo may not be greater than hi.

It's easy to show that the definition prohibits lo from being greater than hi.

To be a SearchTree, a tree must satisfy SearchTree' for some upper bound hi.

Before we prove that elements is correct, 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 quadratic, because at each of the T nodes it does a linear-time list concatentation. The original elements function takes linear time overall; that's much 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 quadratic, 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)

Exercise: 3 stars, standard, optional (elements_relate)

In general, to prove that a function satisfies the abstraction relation, one also needs to use the representation invariant. That was certainly the case with elements_relate:

To put that another way, the general form of lookup_relate should be:

That is certainly provable, since it's a weaker statement than what we proved:

The question is, why did we not need the representation invariant in the proof of lookup_relate? The answer is that our particular Abs relation is much more clever than necessary:

Because the combine function is chosen very carefully, it turns out that this abstraction relation even works on bogus trees!

Step through the proof to LOOK HERE, and notice what's going on. Just when it seems that (T (T E 3 v₃ E) 2 v₂ E) is about to produce v₃ while (t_update (t_empty default) 2 v₂) is about to produce default, omega finds a contradiction. What's happening is that combine 2 is careful to ignore any keys >= 2 in the left-hand subtree. For that reason, Abs matches the actual behavior of lookup, even on bogus trees. But that's a really strong condition! We should not have to care about the behavior of lookup (and insert) on bogus trees. We should not need to prove anything about it, either. Sure, it's convenient in this case that the abstraction relation is able to cope with ill-formed trees. But in general, when proving correctness of abstract-data-type (ADT) implementations, it may be a lot of extra effort to make the abstraction relation as heavy-duty as that. It's often much easier for the abstraction relation to assume that the representation is well formed. Thus, the general statement of our correctness theorems will be more like lookup_relate' than like lookup_relate.

Every Well-Formed Tree Does Actually Relate to an Abstraction

We're not quite done yet. We would like to know that every tree that satisfies the representation invariant, means something. So as a general sanity check, we need the following theorem:

Exercise: 2 stars, standard, optional (can_relate)

It's easy to prove that elements respects this abstraction relation:

But it's not so easy to prove that lookup and insert respect this relation. For example, the following claim is not true.

In fact, naive_lookup_relateX is provably false, as long as the type V contains at least two different values.

Exercise: 4 stars, standard, optional (lookup_relateX)

To prove this, you'll need to use this collection of facts: In_decidable, list2map_app_left, list2map_app_right, list2map_not_in_default, slow_elements_range. The point is, it's not very pretty.

Implementation

What if we want an implementation of search trees in another language, such as OCaml or Haskell? That new implementation would potentially be different than the Coq implementation we have verified. Perhaps some bugs will be introduced in the new implementation. The solution will be to use Coq's extraction feature to derive the real implementation (in OCaml or Haskell) automatically from the Coq function. We'll explore extraction in a later chapter.