Required Reading

(1) General background on red-black trees,

• Section 3.3 of Algorithms, Fourth Edition, by Sedgewick and Wayne, Addison Wesley 2011; or
• Chapter 13 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009
• or Wikipedia.

(2) an explanation of the particular implementation we use here. Red-Black Trees in a Functional Setting, by Chris Okasaki. Journal of Functional Programming, 9(4):471-477, July 1999. https://www.cs.tufts.edu/~nr/cs257/archive/chris-okasaki/redblack99.pdf (3) Optional reading: Efficient Verified Red-Black Trees, by Andrew W. Appel, September 2011. http://www.cs.princeton.edu/~appel/papers/redblack.pdf

Implementation

Red-black trees are a form of binary search tree (BST), but with balance. Recall that the depth of a node in a tree is the distance from the root to that node. The height of a tree is the depth of the deepest node. The insert or lookup function of the BST algorithm (Chapter SearchTree) takes time proportional to the depth of the node that is found (or inserted). To make these functions run fast, we want trees where the worst-case depth (or the average depth) is as small as possible. In a perfectly balanced tree of N nodes, every node has depth less than or or equal to log N, using logarithms base 2. In an approximately balanced tree, every node has depth less than or equal to 2 log N. That's good enough to make insert and lookup run in time proportional to log N. The trick is to mark the nodes Red and Black, and by these marks to know when to locally rebalance the tree. For more explanation and pictures, see the Required Reading above. We will use the same framework as in Extract: keys are Ocaml integers. We don't repeat the Extract commands, because they are imported implicitly from Extract.v

lookup is exactly as in our (unbalanced) search-tree algorithm in Extract, except that the T constructor carries a color component, which we can ignore here.

The balance function is copied directly from Okasaki's paper. Now, the nice thing about machine-checked proof in Coq is that you can prove this correct without actually understanding it! So, do read Okasaki's paper, but don't worry too much about the details of this balance function. In contrast, Sedgewick has proposed left-leaning red-black trees, which have a simpler balance function (but a more complicated invariant). He does this in order to make the proof of correctness easier: there are fewer cases in the balance function, and therefore fewer cases in the case-analysis of the proof of correctness of balance. But as you will see, our proofs about balance will have automated case analyses, so we don't care how many cases there are!

(In contrast, Sedgewick has proposed left-leaning red-black trees, which have a simpler balance function (but a more complicated invariant). He does this in order to make the proof of correctness easier: there are fewer cases in the balance function, and therefore fewer cases in the case-analysis of the proof of correctness of balance. But as you will see, our proofs about balance will have automated case analyses, so we don't care how many cases there are!) The insert operation uses a helper function ins to do the insertion, and another function makeBlack to color the resulting tree's root black.

The elements function does not change except to ignore the color component of T.

Now that the program has been defined, it's time to prove its properties. A red-black tree has two kinds of invariants:

• BST: the keys in each left subtree are all less than the node's key, and the keys in each right subtree are greater
• Balanced: there is the same number of black nodes on any path from the root to each leaf; and there are never two red nodes in a row.

First, we'll look at some automation methodology.

Proof Automation for Case-Analysis Proofs.

Let's start by proving a seemingly obvious fact about ins, namely that the result of any ins operation is a non-empty tree. (We don't actually need this fact, but it makes a good example.) The proof turns out to be surprisingly complicated, because of the need for a big case analysis over all the clauses of the balance function. These proofs are very tedious to do "by hand," but are easy to automate.

Proof Automation for Case-Analysis Proofs.

Several of the proofs for red-black trees require a big case analysis over all the clauses of the balance function. These proofs are very tedious to do by hand, but are easy to automate. Let's get some practice by automating a proof that insertion produces a non-empty tree.

Let's destruct on the topmost case, ltb x k. We can use destruct instead of bdestruct because we don't need to remember whether x<k or x≥k.

How long will this go on? A long time! But it will terminate. Just keep typing. Better yet, let's automate. The following tactic applies whenever the current goal looks like match ?c with Red ⇒ _ | Black ⇒ _ end ≠ _ and what it does in that case is destruct c

The following tactic applies whenever the current goal looks like match ?s with E ⇒ _ | T _ _ _ _ _ ⇒ _ end ≠ _ and what it does in that case is destruct s

Let's apply that tactic again, and then try it on the subgoals, recursively. Recall that the repeat tactical keeps trying the same tactic on subgoals.

This seems promising. Let's start the proof all over again and incorporate this automation.

This is the beginning of the big case analysis. This time, let's combine several tactics together:

What we have left is 117 cases, every one of which can be proved the same way:

Only 111 cases to go...

Only 107 cases to go... There has to be a better way, and there is:

The all: goal selector applies a tactic to all remaining subgoals. Alternatively, we can restart the proof yet again, and add one more clause to the match goal tactic...

Let's start over again, adding that apply to the case analysis.

The BST Property

The Binary Seach Tree (BST) property for red-black trees is exactly the same as for ordinary searchtrees (we just ignore the color of each node). We copy the relevant definitions from SearchTree, also changing to use int rather than nat. ForallT P t holds if P k v holds for every (k,v) node of the tree t.

Exercise: 1 star, standard (empty_tree_BST)

Now, let's proceed to show that insert preserves the BST property. This is a really important result, because it turns out that for red-black trees (unlike the simpler searchtrees in SearchTree) the BST property is required to make insert and lookup interact correctly. We'll address this task in easy stages. First we prove that if t is a BST, then the rebalanced version of t is also a BST. This turns out to be quite a bit of work, but automation helps a great deal.

Use proof automation for this case analysis.

58 cases to consider!

To prove this one, we need to destruct a hypothesis above the line.

And for this one, we first need to both invert and destruct above the line.

This time, let's do the inversion and destruction before deconstructing.

Hmm. Another complicated case. Rather than working through it, let's try the proof again with stronger automation based on what we learned above. Whenever we have a hypothesis above the line that looks like

• H: BST (T _ _ _ _ _)
• H: ForallT _ (T _ _ _ _ _)

we should invert or destruct it, and if we have a goal below the line of the form ForallT _ (T _ _ _ _ _) we should split it up. Otherwise we try try constructor; auto; try omega

Use heavier-duty proof automation for this case analysis.

(Only) 41 cases to consider now! A little disappointing that we didn't clear more cases, but let's look at why are we stuck. The first goal follows from the hypotheses [ ForallT (fun (k' : int) (_ : V) ⇒ int2Z k' > int2Z k₀) r₂ ] and [ int2Z k₁ < int2Z k₀ ] but we need a lemma about >, to be proved inductively over r₂. The other goals look similar.

We can predict that we'll need a matching lemma for <

Use same heavier-duty proof automation as before.

Use our lemmas on everything that is left.

With that fact about balance established, let's take a moment to prove that insertion preserves universal properties of tree nodes. As before, the balance pattern matching will generate lots of cases, so automation is essential.

Exercise: 2 stars, standard (balanceP)

Exercise: 2 stars, standard (insP)

Now to the main results on insertion. Again, all the hard work was done in proving balance_BST, so no automated case analysis should be needed here -- just a simple induction. Remember bdall!

Exercise: 3 stars, standard (ins_BST)

Exercise: 2 stars, standard (insert_BST)

Proving fundamental laws relating insert and lookup.

Next, we want to show the fundamental laws for maps hold on red-black trees. The empty_tree case is trivial.

As above, the hard work will be in handling balance. The following intermediate lemma is useful to characterize the interaction of lookup and balance, and is not too hard to prove with automation.

Exercise: 3 stars, standard (balance_lookup)

Now we can easily prove the main laws relating lookup and ins. Note that unlike for the search trees in SearchTree, these laws are only true for trees that have the BST property; without it, lookup might fail to find an inserted item moved by a balance operation. Neither of these lemmas requires any automation; the hard case analysis work has all been done in balance_lookup.

Exercise: 2 stars, standard (lookup_ins_eq)

Exercise: 3 stars, standard (lookup_ins_neq)

Finally, the main theorems relating lookup and insert. The proofs of these two are almost identical.

Exercise: 3 stars, standard (lookup_insert)

OK, we're almost done! We have proved all these main theorems:

We could now proceed to reprove all the facts about elements that we developed in SearchTrees. Since elements does not not pay attention to colors, and does not rebalance the tree, these proofs should be a simple copy-paste from that chapter, with only minor edits. This would not be a very interesting exercise, so we don't pursue it here.

Proving Efficiency

Red-black trees are supposed to be more efficient than ordinary search trees, because they stay balanced. In a perfectly balanced tree, any two leaves have exactly the same depth, or the difference in depth is at most 1. In an approximately balanced tree, no leaf is more than twice as deep as another leaf. Red-black trees are approximately balanced. Consequently, no node is more then 2logN deep, and the run time for insert or lookup is bounded by a constant times 2logN. We can't prove anything directly about the run time, because we don't have a cost model for Coq functions. But we can prove that the trees stay approximately balanced; this tells us important information about their efficiency.

Exercise: 4 stars, standard (is_redblack_properties)

The relation is_redblack ensures that there are exactly n black nodes in every path from the root to a leaf, and that there are never two red nodes in a row.

nearly_redblack expresses, "the tree is a red-black tree, except that it's nonempty and it is permitted to have two red nodes in a row at the very root (only)."

You will need proof automation, in a similar style to the proofs of ins_not_E and balance_lookup.

Exercise: 3 stars, standard, optional (redblack_bound)

To confirm that red-black trees really are roughly balanced, define functions to compute the height (maximum depth) and minimum depth of a red-black tree, and prove that the height is bounded by twice the minimum depth + 1.

Extracting and Measuring Red-Black Trees

You can run this inside the OCaml top level by:

#use "redblack.ml";;
#use "test_searchtree.ml";;

On my machine, in the byte-code interpreter this prints,

Insert and lookup 1000000 random integers in 0.889 seconds.
Insert and lookup 20000 random integers in 0.016 seconds.
Insert and lookup 20000 consecutive integers in 0.015 seconds.

You can compile and run this with the ocaml native-code compiler by:

$ ocamlopt -c redblack.mli redblack.ml
$ ocamlopt redblack.cmx -open Redblack test_searchtree.ml -o test_redblack
$ ./test_redblack

On my machine this prints,

Insert and lookup 1000000 random integers in 0.436 seconds.
Insert and lookup 20000 random integers in 0. seconds.
Insert and lookup 20000 consecutive integers in 0. seconds.

Success!

The benchmark measurements above (and in Extract.v) demonstrate that:

• On random insertions, red-black trees are slightly faster than ordinary BSTs (red-black 0.436 seconds, vs ordinary 0.468 seconds)
• On consecutive insertions, red-black trees are much faster than ordinary BSTs (red-black 0. seconds, vs ordinary 0.374 seconds)

In particular, red-black trees are almost exactly as fast on the consecutive insertions (0.015 seconds) as on the random (0.016 seconds).