Library Coq.MSets.MSetRBT
MSetRBT : Implementation of MSetInterface via Red-Black trees
Initial author: Andrew W. Appel, 2011.
Extra modifications by: Pierre Letouzey
The design decisions behind this implementation are described here:
- Efficient Verified Red-Black Trees, by Andrew W. Appel, September 2011.
http://www.cs.princeton.edu/~appel/papers/redblack.pdf
Additional suggested reading:
- Red-Black Trees in a Functional Setting by Chris Okasaki.
Journal of Functional Programming, 9(4):471-477, July 1999.
http://www.eecs.usma.edu/webs/people/okasaki/jfp99redblack.pdf
- Red-black trees with types, by Stefan Kahrs.
Journal of Functional Programming, 11(4), 425-432, 2001.
- Functors for Proofs and Programs, by J.-C. Filliatre and P. Letouzey.
ESOP'04: European Symposium on Programming, pp. 370-384, 2004.
http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz
An extra function not (yet?) in MSetInterface.S
The type of color annotation.
Generic trees instantiated with color
We reuse a generic definition of trees where the information
parameter is a color. Functions like mem or fold are also
provided by this generic functor.
Balancing
We adapt when one side is not a true red-black tree.
Both sides have the same black depth.
Definition lbal l k r :=
match l with
|
Rd (
Rd a x b)
y c =>
Rd (
Bk a x b)
y (
Bk c k r)
|
Rd a x (
Rd b y c) =>
Rd (
Bk a x b)
y (
Bk c k r)
|
_ =>
Bk l k r
end.
Definition rbal l k r :=
match r with
|
Rd (
Rd b y c)
z d =>
Rd (
Bk l k b)
y (
Bk c z d)
|
Rd b y (
Rd c z d) =>
Rd (
Bk l k b)
y (
Bk c z d)
|
_ =>
Bk l k r
end.
A variant of rbal, with reverse pattern order.
Is it really useful ? Should we always use it ?
Definition rbal' l k r :=
match r with
|
Rd b y (
Rd c z d) =>
Rd (
Bk l k b)
y (
Bk c z d)
|
Rd (
Rd b y c)
z d =>
Rd (
Bk l k b)
y (
Bk c z d)
|
_ =>
Bk l k r
end.
Balancing with different black depth.
One side is almost a red-black tree, while the other is
a true red-black tree, but with black depth + 1.
Used in deletion.
Tree-ification
We rebuild a tree of size
if pred then n-1 else n as soon
as the list
l has enough elements
Union, intersection, difference
union of the elements of
l1 and
l2 into a third
acc list.
compare_height returns:
- Lt if height s2 is at least twice height s1;
- Gt if height s1 is at least twice height s2;
- Eq if heights are approximately equal.
Warning: this is not an equivalence relation! but who cares....
Definition skip_red t :=
match t with
|
Rd t' _ _ =>
t'
|
_ =>
t
end.
Definition skip_black t :=
match skip_red t with
|
Bk t' _ _ =>
t'
|
t' =>
t'
end.
Fixpoint compare_height (
s1x s1 s2 s2x:
tree) :
comparison :=
match skip_red s1x,
skip_red s1,
skip_red s2,
skip_red s2x with
|
Node _ s1x' _ _,
Node _ s1' _ _,
Node _ s2' _ _,
Node _ s2x' _ _ =>
compare_height (
skip_black s2x')
s1' s2' (
skip_black s2x')
|
_,
Leaf,
_,
Node _ _ _ _ =>
Lt
|
Node _ _ _ _,
_,
Leaf,
_ =>
Gt
|
Node _ s1x' _ _,
Node _ s1' _ _,
Node _ s2' _ _,
Leaf =>
compare_height (
skip_black s1x')
s1' s2' Leaf
|
Leaf,
Node _ s1' _ _,
Node _ s2' _ _,
Node _ s2x' _ _ =>
compare_height Leaf s1' s2' (
skip_black s2x')
|
_,
_,
_,
_ =>
Eq
end.
When one tree is quite smaller than the other, we simply
adds repeatively all its elements in the big one.
For trees of comparable height, we rather use linear_union.
MakeRaw : the pure functions and their specifications
Generic definition of binary-search-trees and proofs of
specifications for generic functions such as mem or fold.
Generic handling for red-matching and red-red-matching
Balancing operations are instances of generic match
Removing the minimal element
An invariant for binary list functions with accumulator.
Balancing properties
We now prove that all operations preserve a red-black invariant,
and that trees have hence a logarithmic depth.
Red-Black invariants
In a red-black tree :
- a red node has no red children
- the black depth at each node is the same along all paths.
The black depth is here an argument of the predicate.
A red-red tree is almost a red-black tree, except that it has
a red root node which may have red children. Note that a
red-red tree is hence non-empty, and all its strict subtrees
are red-black.
An almost-red-black tree is almost a red-black tree, except that
it's permitted to have two red nodes in a row at the very root (only).
We implement this notion by saying that a quasi-red-black tree
is either a red-black tree or a red-red tree.
The main exported invariant : being a red-black tree for some
black depth.
Basic tactics and results about red-black
A Red-Black tree has indeed a logarithmic depth
Insertion
The next lemmas combine simultaneous results about rbt and arbt.
A first solution here: statement with
if ... then ... else
Deletion
A second approach here: statement with ... /\ ...
A third approach : Lemma ... with ...
The black depth of treeify l is actually a log2, but
we don't need to mention that.
Union, intersection, difference
Final Encapsulation
Now, in order to really provide a functor implementing
S, we
need to encapsulate everything into a type of binary search trees.
They also happen to be well-balanced, but this has no influence
on the correctness of operations, so we won't state this here,
see
BalanceProps if you need more than just the MSet interface.