The Coq Proof Assistant

# 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

Require MSetGenTree.
Require Import Bool List BinPos Pnat Setoid SetoidList PeanoNat.
Local Open Scope list_scope.
An extra function not (yet?) in MSetInterface.S
Module Type MSetRemoveMin (Import M:MSetInterface.S).
Parameter remove_min : t -> option (elt * t).
Axiom remove_min_spec1 : forall s k s',
remove_min s = Some (k,s') ->
min_elt s = Some k /\ remove k s [=] s'.
Axiom remove_min_spec2 : forall s, remove_min s = None -> Empty s.
End MSetRemoveMin.
The type of color annotation.
Inductive color := Red | Black.
Module Color.
Definition t := color.
End Color.

# Ops : the pure functions

Module Ops (X:Orders.OrderedType) <: MSetInterface.Ops X.

## 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.
Include MSetGenTree.Ops X Color.
Definition t := tree.
Local Notation Rd := (Node Red).
Local Notation Bk := (Node Black).

## Basic tree

Definition singleton (k: elt) : tree := Bk Leaf k Leaf.

## Changing root color

Definition makeBlack t :=
match t with
| Leaf => Leaf
| Node _ a x b => Bk a x b
end.
Definition makeRed t :=
match t with
| Leaf => Leaf
| Node _ a x b => Rd a x b
end.

## 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.
Definition lbalS l k r :=
match l with
| Rd a x b => Rd (Bk a x b) k r
| _ =>
match r with
| Bk a y b => rbal' l k (Rd a y b)
| Rd (Bk a y b) z c => Rd (Bk l k a) y (rbal' b z (makeRed c))
| _ => Rd l k r
end
end.
Definition rbalS l k r :=
match r with
| Rd b y c => Rd l k (Bk b y c)
| _ =>
match l with
| Bk a x b => lbal (Rd a x b) k r
| Rd a x (Bk b y c) => Rd (lbal (makeRed a) x b) y (Bk c k r)
| _ => Rd l k r
end
end.

## Insertion

Fixpoint ins x s :=
match s with
| Leaf => Rd Leaf x Leaf
| Node c l y r =>
match X.compare x y with
| Eq => s
| Lt =>
match c with
| Red => Rd (ins x l) y r
| Black => lbal (ins x l) y r
end
| Gt =>
match c with
| Red => Rd l y (ins x r)
| Black => rbal l y (ins x r)
end
end
end.
Definition add x s := makeBlack (ins x s).

## Deletion

Fixpoint append (l:tree) : tree -> tree :=
match l with
| Leaf => fun r => r
| Node lc ll lx lr =>
fix append_l (r:tree) : tree :=
match r with
| Leaf => l
| Node rc rl rx rr =>
match lc, rc with
| Red, Red =>
let lrl := append lr rl in
match lrl with
| Rd lr' x rl' => Rd (Rd ll lx lr') x (Rd rl' rx rr)
| _ => Rd ll lx (Rd lrl rx rr)
end
| Black, Black =>
let lrl := append lr rl in
match lrl with
| Rd lr' x rl' => Rd (Bk ll lx lr') x (Bk rl' rx rr)
| _ => lbalS ll lx (Bk lrl rx rr)
end
| Black, Red => Rd (append_l rl) rx rr
| Red, Black => Rd ll lx (append lr r)
end
end
end.
Fixpoint del x t :=
match t with
| Leaf => Leaf
| Node _ a y b =>
match X.compare x y with
| Eq => append a b
| Lt =>
match a with
| Bk _ _ _ => lbalS (del x a) y b
| _ => Rd (del x a) y b
end
| Gt =>
match b with
| Bk _ _ _ => rbalS a y (del x b)
| _ => Rd a y (del x b)
end
end
end.
Definition remove x t := makeBlack (del x t).

## Removing minimal element

Fixpoint delmin l x r : (elt * tree) :=
match l with
| Leaf => (x,r)
| Node lc ll lx lr =>
let (k,l') := delmin ll lx lr in
match lc with
| Black => (k, lbalS l' x r)
| Red => (k, Rd l' x r)
end
end.
Definition remove_min t : option (elt * tree) :=
match t with
| Leaf => None
| Node _ l x r =>
let (k,t) := delmin l x r in
Some (k, makeBlack t)
end.

## Tree-ification

We rebuild a tree of size if pred then n-1 else n as soon as the list l has enough elements
Definition bogus : tree * list elt := (Leaf, nil).
Notation treeify_t := (list elt -> tree * list elt).
Definition treeify_zero : treeify_t :=
fun acc => (Leaf,acc).
Definition treeify_one : treeify_t :=
fun acc => match acc with
| x::acc => (Rd Leaf x Leaf, acc)
| _ => bogus
end.
Definition treeify_cont (f g : treeify_t) : treeify_t :=
fun acc =>
match f acc with
| (l, x::acc) =>
match g acc with
| (r, acc) => (Bk l x r, acc)
end
| _ => bogus
end.
Fixpoint treeify_aux (pred:bool)(n: positive) : treeify_t :=
match n with
| xH => if pred then treeify_zero else treeify_one
| xO n => treeify_cont (treeify_aux pred n) (treeify_aux true n)
| xI n => treeify_cont (treeify_aux false n) (treeify_aux pred n)
end.
Fixpoint plength_aux (l:list elt)(p:positive) := match l with
| nil => p
| _::l => plength_aux l (Pos.succ p)
end.
Definition plength l := plength_aux l 1.
Definition treeify (l:list elt) :=
fst (treeify_aux true (plength l) l).

## Filtering

Fixpoint filter_aux (f: elt -> bool) s acc :=
match s with
| Leaf => acc
| Node _ l k r =>
let acc := filter_aux f r acc in
if f k then filter_aux f l (k::acc)
else filter_aux f l acc
end.
Definition filter (f: elt -> bool) (s: t) : t :=
treeify (filter_aux f s nil).
Fixpoint partition_aux (f: elt -> bool) s acc1 acc2 :=
match s with
| Leaf => (acc1,acc2)
| Node _ sl k sr =>
let (acc1, acc2) := partition_aux f sr acc1 acc2 in
if f k then partition_aux f sl (k::acc1) acc2
else partition_aux f sl acc1 (k::acc2)
end.
Definition partition (f: elt -> bool) (s:t) : t*t :=
let (ok,ko) := partition_aux f s nil nil in
(treeify ok, treeify ko).

## Union, intersection, difference

union of the elements of l1 and l2 into a third acc list.
Fixpoint union_list l1 : list elt -> list elt -> list elt :=
match l1 with
| nil => @rev_append _
| x::l1' =>
fix union_l1 l2 acc :=
match l2 with
| nil => rev_append l1 acc
| y::l2' =>
match X.compare x y with
| Eq => union_list l1' l2' (x::acc)
| Lt => union_l1 l2' (y::acc)
| Gt => union_list l1' l2 (x::acc)
end
end
end.
Definition linear_union s1 s2 :=
treeify (union_list (rev_elements s1) (rev_elements s2) nil).
Fixpoint inter_list l1 : list elt -> list elt -> list elt :=
match l1 with
| nil => fun _ acc => acc
| x::l1' =>
fix inter_l1 l2 acc :=
match l2 with
| nil => acc
| y::l2' =>
match X.compare x y with
| Eq => inter_list l1' l2' (x::acc)
| Lt => inter_l1 l2' acc
| Gt => inter_list l1' l2 acc
end
end
end.
Definition linear_inter s1 s2 :=
treeify (inter_list (rev_elements s1) (rev_elements s2) nil).
Fixpoint diff_list l1 : list elt -> list elt -> list elt :=
match l1 with
| nil => fun _ acc => acc
| x::l1' =>
fix diff_l1 l2 acc :=
match l2 with
| nil => rev_append l1 acc
| y::l2' =>
match X.compare x y with
| Eq => diff_list l1' l2' acc
| Lt => diff_l1 l2' acc
| Gt => diff_list l1' l2 (x::acc)
end
end
end.
Definition linear_diff s1 s2 :=
treeify (diff_list (rev_elements s1) (rev_elements s2) nil).
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 s1x') 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.
Definition union (t1 t2: t) : t :=
match compare_height t1 t1 t2 t2 with
| Lt => fold add t1 t2
| Gt => fold add t2 t1
| Eq => linear_union t1 t2
end.
Definition diff (t1 t2: t) : t :=
match compare_height t1 t1 t2 t2 with
| Lt => filter (fun k => negb (mem k t2)) t1
| Gt => fold remove t2 t1
| Eq => linear_diff t1 t2
end.
Definition inter (t1 t2: t) : t :=
match compare_height t1 t1 t2 t2 with
| Lt => filter (fun k => mem k t2) t1
| Gt => filter (fun k => mem k t1) t2
| Eq => linear_inter t1 t2
end.
End Ops.

# MakeRaw : the pure functions and their specifications

Module Type MakeRaw (X:Orders.OrderedType) <: MSetInterface.RawSets X.
Include Ops X.
Generic definition of binary-search-trees and proofs of specifications for generic functions such as mem or fold.
Include MSetGenTree.Props X Color.
Local Notation Rd := (Node Red).
Local Notation Bk := (Node Black).
Local Hint Immediate MX.eq_sym : core.
Local Hint Unfold In lt_tree gt_tree Ok : core.
Local Hint Constructors InT bst : core.
Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core.
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
Local Hint Resolve elements_spec2 : core.

## Singleton set

Lemma singleton_spec x y : InT y (singleton x) <-> X.eq y x.
#[global]
Instance singleton_ok x : Ok (singleton x).

## makeBlack, MakeRed

Lemma makeBlack_spec s x : InT x (makeBlack s) <-> InT x s.
Lemma makeRed_spec s x : InT x (makeRed s) <-> InT x s.
#[global]
Instance makeBlack_ok s `{Ok s} : Ok (makeBlack s).
#[global]
Instance makeRed_ok s `{Ok s} : Ok (makeRed s).

## Generic handling for red-matching and red-red-matching

Definition isblack t :=
match t with Bk _ _ _ => True | _ => False end.
Definition notblack t :=
match t with Bk _ _ _ => False | _ => True end.
Definition notred t :=
match t with Rd _ _ _ => False | _ => True end.
Definition rcase {A} f g t : A :=
match t with
| Rd a x b => f a x b
| _ => g t
end.
Inductive rspec {A} f g : tree -> A -> Prop :=
| rred a x b : rspec f g (Rd a x b) (f a x b)
| relse t : notred t -> rspec f g t (g t).
Fact rmatch {A} f g t : rspec (A:=A) f g t (rcase f g t).
Definition rrcase {A} f g t : A :=
match t with
| Rd (Rd a x b) y c => f a x b y c
| Rd a x (Rd b y c) => f a x b y c
| _ => g t
end.
Notation notredred := (rrcase (fun _ _ _ _ _ => False) (fun _ => True)).
Inductive rrspec {A} f g : tree -> A -> Prop :=
| rrleft a x b y c : rrspec f g (Rd (Rd a x b) y c) (f a x b y c)
| rrright a x b y c : rrspec f g (Rd a x (Rd b y c)) (f a x b y c)
| rrelse t : notredred t -> rrspec f g t (g t).
Fact rrmatch {A} f g t : rrspec (A:=A) f g t (rrcase f g t).
Definition rrcase' {A} f g t : A :=
match t with
| Rd a x (Rd b y c) => f a x b y c
| Rd (Rd a x b) y c => f a x b y c
| _ => g t
end.
Fact rrmatch' {A} f g t : rrspec (A:=A) f g t (rrcase' f g t).
Balancing operations are instances of generic match
Fact lbal_match l k r :
rrspec
(fun a x b y c => Rd (Bk a x b) y (Bk c k r))
(fun l => Bk l k r)
l
(lbal l k r).
Fact rbal_match l k r :
rrspec
(fun a x b y c => Rd (Bk l k a) x (Bk b y c))
(fun r => Bk l k r)
r
(rbal l k r).
Fact rbal'_match l k r :
rrspec
(fun a x b y c => Rd (Bk l k a) x (Bk b y c))
(fun r => Bk l k r)
r
(rbal' l k r).
Fact lbalS_match l x r :
rspec
(fun a y b => Rd (Bk a y b) x r)
(fun l =>
match r with
| Bk a y b => rbal' l x (Rd a y b)
| Rd (Bk a y b) z c => Rd (Bk l x a) y (rbal' b z (makeRed c))
| _ => Rd l x r
end)
l
(lbalS l x r).
Fact rbalS_match l x r :
rspec
(fun a y b => Rd l x (Bk a y b))
(fun r =>
match l with
| Bk a y b => lbal (Rd a y b) x r
| Rd a y (Bk b z c) => Rd (lbal (makeRed a) y b) z (Bk c x r)
| _ => Rd l x r
end)
r
(rbalS l x r).

## Balancing for insertion

Lemma lbal_spec l x r y :
InT y (lbal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
#[global]
Instance lbal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
Ok (lbal l x r).
Lemma rbal_spec l x r y :
InT y (rbal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
#[global]
Instance rbal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
Ok (rbal l x r).
Lemma rbal'_spec l x r y :
InT y (rbal' l x r) <-> X.eq y x \/ InT y l \/ InT y r.
#[global]
Instance rbal'_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
Ok (rbal' l x r).
Global Hint Rewrite In_node_iff In_leaf_iff
makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb.
Ltac descolor := destruct_all Color.t.
Ltac destree t := destruct t as [|[|] ? ? ?].
Ltac autorew := autorewrite with rb.
Tactic Notation "autorew" "in" ident(H) := autorewrite with rb in H.

## Insertion

Lemma ins_spec : forall s x y,
InT y (ins x s) <-> X.eq y x \/ InT y s.
Global Hint Rewrite ins_spec : rb.
#[global]
Instance ins_ok s x `{Ok s} : Ok (ins x s).
Lemma add_spec' s x y :
InT y (add x s) <-> X.eq y x \/ InT y s.
Global Hint Rewrite add_spec' : rb.
Lemma add_spec s x y `{Ok s} :
InT y (add x s) <-> X.eq y x \/ InT y s.
#[global]
Instance add_ok s x `{Ok s} : Ok (add x s).

## Balancing for deletion

Lemma lbalS_spec l x r y :
InT y (lbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
#[global]
Instance lbalS_ok l x r :
forall `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (lbalS l x r).
Lemma rbalS_spec l x r y :
InT y (rbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
#[global]
Instance rbalS_ok l x r :
forall `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (rbalS l x r).
Global Hint Rewrite lbalS_spec rbalS_spec : rb.

## Append for deletion

Ltac append_tac l r :=
induction l as [| lc ll _ lx lr IHlr];
[intro r; simpl
|induction r as [| rc rl IHrl rx rr _];
[simpl
|destruct lc, rc;
[specialize (IHlr rl); clear IHrl
|simpl;
assert (Hr:notred (Bk rl rx rr)) by (simpl; trivial);
set (r:=Bk rl rx rr) in *; clearbody r; clear IHrl rl rx rr;
specialize (IHlr r)
|change (append _ _) with (Rd (append (Bk ll lx lr) rl) rx rr);
assert (Hl:notred (Bk ll lx lr)) by (simpl; trivial);
set (l:=Bk ll lx lr) in *; clearbody l; clear IHlr ll lx lr
|specialize (IHlr rl); clear IHrl]]].
Fact append_rr_match ll lx lr rl rx rr :
rspec
(fun a x b => Rd (Rd ll lx a) x (Rd b rx rr))
(fun t => Rd ll lx (Rd t rx rr))
(append lr rl)
(append (Rd ll lx lr) (Rd rl rx rr)).
Fact append_bb_match ll lx lr rl rx rr :
rspec
(fun a x b => Rd (Bk ll lx a) x (Bk b rx rr))
(fun t => lbalS ll lx (Bk t rx rr))
(append lr rl)
(append (Bk ll lx lr) (Bk rl rx rr)).
Lemma append_spec l r x :
InT x (append l r) <-> InT x l \/ InT x r.
Global Hint Rewrite append_spec : rb.
Lemma append_ok : forall x l r `{Ok l, Ok r},
lt_tree x l -> gt_tree x r -> Ok (append l r).

## Deletion

Lemma del_spec : forall s x y `{Ok s},
InT y (del x s) <-> InT y s /\ ~X.eq y x.
Global Hint Rewrite del_spec : rb.
#[global]
Instance del_ok s x `{Ok s} : Ok (del x s).
Lemma remove_spec s x y `{Ok s} :
InT y (remove x s) <-> InT y s /\ ~X.eq y x.
Global Hint Rewrite remove_spec : rb.
#[global]
Instance remove_ok s x `{Ok s} : Ok (remove x s).

## Removing the minimal element

Lemma delmin_spec l y r c x s' `{O : Ok (Node c l y r)} :
delmin l y r = (x,s') ->
min_elt (Node c l y r) = Some x /\ del x (Node c l y r) = s'.
Lemma remove_min_spec1 s x s' `{Ok s}:
remove_min s = Some (x,s') ->
min_elt s = Some x /\ remove x s = s'.
Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
Lemma remove_min_ok (s:t) `{Ok s}:
match remove_min s with
| Some (_,s') => Ok s'
| None => True
end.

## Treeify

Notation ifpred p n := (if p then pred n else n%nat).
Definition treeify_invariant size (f:treeify_t) :=
forall acc,
size <= length acc ->
let (t,acc') := f acc in
cardinal t = size /\ acc = elements t ++ acc'.
Lemma treeify_zero_spec : treeify_invariant 0 treeify_zero.
Lemma treeify_one_spec : treeify_invariant 1 treeify_one.
Lemma treeify_cont_spec f g size1 size2 size :
treeify_invariant size1 f ->
treeify_invariant size2 g ->
size = S (size1 + size2) ->
treeify_invariant size (treeify_cont f g).
Lemma treeify_aux_spec n (p:bool) :
treeify_invariant (ifpred p (Pos.to_nat n)) (treeify_aux p n).
Lemma plength_aux_spec l p :
Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p.
Lemma plength_spec l : Pos.to_nat (plength l) = S (length l).
Lemma treeify_elements l : elements (treeify l) = l.
Lemma treeify_spec x l : InT x (treeify l) <-> InA X.eq x l.
Lemma treeify_ok l : sort X.lt l -> Ok (treeify l).

## Filter

Lemma filter_aux_elements s f acc :
filter_aux f s acc = List.filter f (elements s) ++ acc.
Lemma filter_elements s f :
elements (filter f s) = List.filter f (elements s).
Lemma filter_spec s x f :
Proper (X.eq==>Logic.eq) f ->
(InT x (filter f s) <-> InT x s /\ f x = true).
#[global]
Instance filter_ok s f `(Ok s) : Ok (filter f s).

## Partition

Lemma partition_aux_spec s f acc1 acc2 :
partition_aux f s acc1 acc2 =
(filter_aux f s acc1, filter_aux (fun x => negb (f x)) s acc2).
Lemma partition_spec s f :
partition f s = (filter f s, filter (fun x => negb (f x)) s).
Lemma partition_spec1 s f :
Proper (X.eq==>Logic.eq) f ->
Equal (fst (partition f s)) (filter f s).
Lemma partition_spec2 s f :
Proper (X.eq==>Logic.eq) f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
#[global]
Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
#[global]
Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).

## An invariant for binary list functions with accumulator.

Ltac inA :=
rewrite ?InA_app_iff, ?InA_cons, ?InA_nil, ?InA_rev in *; auto_tc.
Record INV l1 l2 acc : Prop := {
l1_sorted : sort X.lt (rev l1);
l2_sorted : sort X.lt (rev l2);
acc_sorted : sort X.lt acc;
l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y;
l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}.
Local Hint Resolve l1_sorted l2_sorted acc_sorted : core.
Lemma INV_init s1 s2 `(Ok s1, Ok s2) :
INV (rev_elements s1) (rev_elements s2) nil.
Lemma INV_sym l1 l2 acc : INV l1 l2 acc -> INV l2 l1 acc.
Lemma INV_drop x1 l1 l2 acc :
INV (x1 :: l1) l2 acc -> INV l1 l2 acc.
Lemma INV_eq x1 x2 l1 l2 acc :
INV (x1 :: l1) (x2 :: l2) acc -> X.eq x1 x2 ->
INV l1 l2 (x1 :: acc).
Lemma INV_lt x1 x2 l1 l2 acc :
INV (x1 :: l1) (x2 :: l2) acc -> X.lt x1 x2 ->
INV (x1 :: l1) l2 (x2 :: acc).
Lemma INV_rev l1 l2 acc :
INV l1 l2 acc -> Sorted X.lt (rev_append l1 acc).

## union

Lemma union_list_ok l1 l2 acc :
INV l1 l2 acc -> sort X.lt (union_list l1 l2 acc).
#[global]
Instance linear_union_ok s1 s2 `(Ok s1, Ok s2) :
Ok (linear_union s1 s2).
#[global]
Instance fold_add_ok s1 s2 `(Ok s1, Ok s2) :
Ok (fold add s1 s2).
#[global]
Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2).
Lemma union_list_spec x l1 l2 acc :
InA X.eq x (union_list l1 l2 acc) <->
InA X.eq x l1 \/ InA X.eq x l2 \/ InA X.eq x acc.
Lemma linear_union_spec s1 s2 x :
InT x (linear_union s1 s2) <-> InT x s1 \/ InT x s2.
Lemma fold_add_spec s1 s2 x :
InT x (fold add s1 s2) <-> InT x s1 \/ InT x s2.
Lemma union_spec' s1 s2 x :
InT x (union s1 s2) <-> InT x s1 \/ InT x s2.
Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2},
(InT y (union s1 s2) <-> InT y s1 \/ InT y s2).

## inter

Lemma inter_list_ok l1 l2 acc :
INV l1 l2 acc -> sort X.lt (inter_list l1 l2 acc).
#[global]
Instance linear_inter_ok s1 s2 `(Ok s1, Ok s2) :
Ok (linear_inter s1 s2).
#[global]
Instance inter_ok s1 s2 `(Ok s1, Ok s2) : Ok (inter s1 s2).
Lemma inter_list_spec x l1 l2 acc :
sort X.lt (rev l1) ->
sort X.lt (rev l2) ->
(InA X.eq x (inter_list l1 l2 acc) <->
(InA X.eq x l1 /\ InA X.eq x l2) \/ InA X.eq x acc).
Lemma linear_inter_spec s1 s2 x `(Ok s1, Ok s2) :
InT x (linear_inter s1 s2) <-> InT x s1 /\ InT x s2.
Local Instance mem_proper s `(Ok s) :
Proper (X.eq ==> Logic.eq) (fun k => mem k s).
Lemma inter_spec s1 s2 y `{Ok s1, Ok s2} :
InT y (inter s1 s2) <-> InT y s1 /\ InT y s2.

## difference

Lemma diff_list_ok l1 l2 acc :
INV l1 l2 acc -> sort X.lt (diff_list l1 l2 acc).
#[global]
Instance diff_inter_ok s1 s2 `(Ok s1, Ok s2) :
Ok (linear_diff s1 s2).
#[global]
Instance fold_remove_ok s1 s2 `(Ok s2) :
Ok (fold remove s1 s2).
#[global]
Instance diff_ok s1 s2 `(Ok s1, Ok s2) : Ok (diff s1 s2).
Lemma diff_list_spec x l1 l2 acc :
sort X.lt (rev l1) ->
sort X.lt (rev l2) ->
(InA X.eq x (diff_list l1 l2 acc) <->
(InA X.eq x l1 /\ ~InA X.eq x l2) \/ InA X.eq x acc).
Lemma linear_diff_spec s1 s2 x `(Ok s1, Ok s2) :
InT x (linear_diff s1 s2) <-> InT x s1 /\ ~InT x s2.
Lemma fold_remove_spec s1 s2 x `(Ok s2) :
InT x (fold remove s1 s2) <-> InT x s2 /\ ~InT x s1.
Lemma diff_spec s1 s2 y `{Ok s1, Ok s2} :
InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2.
End MakeRaw.

# Balancing properties

We now prove that all operations preserve a red-black invariant, and that trees have hence a logarithmic depth.
Module BalanceProps(X:Orders.OrderedType)(Import M : MakeRaw X).
Local Notation Rd := (Node Red).
Local Notation Bk := (Node Black).
Import M.MX.

## 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.
Inductive rbt : nat -> tree -> Prop :=
| RB_Leaf : rbt 0 Leaf
| RB_Rd n l k r :
notred l -> notred r -> rbt n l -> rbt n r -> rbt n (Rd l k r)
| RB_Bk n l k r : rbt n l -> rbt n r -> rbt (S n) (Bk l k r).
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.
Inductive rrt (n:nat) : tree -> Prop :=
| RR_Rd l k r : rbt n l -> rbt n r -> rrt n (Rd l k r).
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.
Inductive arbt (n:nat)(t:tree) : Prop :=
| ARB_RB : rbt n t -> arbt n t
| ARB_RR : rrt n t -> arbt n t.
The main exported invariant : being a red-black tree for some black depth.
Class Rbt (t:tree) := RBT : exists d, rbt d t.

## Basic tactics and results about red-black

Scheme rbt_ind := Induction for rbt Sort Prop.
Local Hint Constructors rbt rrt arbt : core.
Local Hint Extern 0 (notred _) => (exact I) : core.
Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction.
Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end.
Ltac nonzero n := destruct n as [|n]; [try split; invrb|].
Lemma rr_nrr_rb n t :
rrt n t -> notredred t -> rbt n t.
Local Hint Resolve rr_nrr_rb : core.
Lemma arb_nrr_rb n t :
arbt n t -> notredred t -> rbt n t.
Lemma arb_nr_rb n t :
arbt n t -> notred t -> rbt n t.
Local Hint Resolve arb_nrr_rb arb_nr_rb : core.

## A Red-Black tree has indeed a logarithmic depth

Definition redcarac s := rcase (fun _ _ _ => 1) (fun _ => 0) s.
Lemma rb_maxdepth s n : rbt n s -> maxdepth s <= 2*n + redcarac s.
Lemma rb_mindepth s n : rbt n s -> n + redcarac s <= mindepth s.
Lemma maxdepth_upperbound s : Rbt s ->
maxdepth s <= 2 * Nat.log2 (S (cardinal s)).
Lemma maxdepth_lowerbound s : s<>Leaf ->
Nat.log2 (cardinal s) < maxdepth s.

## Singleton

Lemma singleton_rb x : Rbt (singleton x).

## makeBlack and makeRed

Lemma makeBlack_rb n t : arbt n t -> Rbt (makeBlack t).
Lemma makeRed_rr t n :
rbt (S n) t -> notred t -> rrt n (makeRed t).

## Balancing

Lemma lbal_rb n l k r :
arbt n l -> rbt n r -> rbt (S n) (lbal l k r).
Lemma rbal_rb n l k r :
rbt n l -> arbt n r -> rbt (S n) (rbal l k r).
Lemma rbal'_rb n l k r :
rbt n l -> arbt n r -> rbt (S n) (rbal' l k r).
Lemma lbalS_rb n l x r :
arbt n l -> rbt (S n) r -> notred r -> rbt (S n) (lbalS l x r).
Lemma lbalS_arb n l x r :
arbt n l -> rbt (S n) r -> arbt (S n) (lbalS l x r).
Lemma rbalS_rb n l x r :
rbt (S n) l -> notred l -> arbt n r -> rbt (S n) (rbalS l x r).
Lemma rbalS_arb n l x r :
rbt (S n) l -> arbt n r -> arbt (S n) (rbalS l x r).

## Insertion

The next lemmas combine simultaneous results about rbt and arbt. A first solution here: statement with if ... then ... else
Definition ifred s (A B:Prop) := rcase (fun _ _ _ => A) (fun _ => B) s.
Lemma ifred_notred s A B : notred s -> (ifred s A B <-> B).
Lemma ifred_or s A B : ifred s A B -> A\/B.
Lemma ins_rr_rb x s n : rbt n s ->
ifred s (rrt n (ins x s)) (rbt n (ins x s)).
Lemma ins_arb x s n : rbt n s -> arbt n (ins x s).
#[global]
Instance add_rb x s : Rbt s -> Rbt (add x s).

## Deletion

A second approach here: statement with ... /\ ...
Lemma append_arb_rb n l r : rbt n l -> rbt n r ->
(arbt n (append l r)) /\
(notred l -> notred r -> rbt n (append l r)).
A third approach : Lemma ... with ...
Lemma del_arb s x n : rbt (S n) s -> isblack s -> arbt n (del x s)
with del_rb s x n : rbt n s -> notblack s -> rbt n (del x s).
#[global]
Instance remove_rb s x : Rbt s -> Rbt (remove x s).

## Treeify

Definition treeify_rb_invariant size depth (f:treeify_t) :=
forall acc,
size <= length acc ->
rbt depth (fst (f acc)) /\
size + length (snd (f acc)) = length acc.
Lemma treeify_zero_rb : treeify_rb_invariant 0 0 treeify_zero.
Lemma treeify_one_rb : treeify_rb_invariant 1 0 treeify_one.
Lemma treeify_cont_rb f g size1 size2 size d :
treeify_rb_invariant size1 d f ->
treeify_rb_invariant size2 d g ->
size = S (size1 + size2) ->
treeify_rb_invariant size (S d) (treeify_cont f g).
Lemma treeify_aux_rb n :
exists d, forall (b:bool),
treeify_rb_invariant (ifpred b (Pos.to_nat n)) d (treeify_aux b n).
The black depth of treeify l is actually a log2, but we don't need to mention that.
#[global]
Instance treeify_rb l : Rbt (treeify l).

## Filtering

#[global]
Instance filter_rb f s : Rbt (filter f s).
#[global]
Instance partition_rb1 f s : Rbt (fst (partition f s)).
#[global]
Instance partition_rb2 f s : Rbt (snd (partition f s)).

## Union, intersection, difference

#[global]
Instance fold_add_rb s1 s2 : Rbt s2 -> Rbt (fold add s1 s2).
#[global]
Instance fold_remove_rb s1 s2 : Rbt s2 -> Rbt (fold remove s1 s2).
Lemma union_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (union s1 s2).
Lemma inter_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (inter s1 s2).
Lemma diff_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (diff s1 s2).
End BalanceProps.

# 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.
Module Type MSetInterface_S_Ext := MSetInterface.S <+ MSetRemoveMin.
Module Make (X: Orders.OrderedType) <:
MSetInterface_S_Ext with Module E := X.
Module Raw. Include MakeRaw X. End Raw.
Include MSetInterface.Raw2Sets X Raw.
Definition opt_ok (x:option (elt * Raw.t)) :=
match x with Some (_,s) => Raw.Ok s | None => True end.
Definition mk_opt_t (x: option (elt * Raw.t))(P: opt_ok x) :
option (elt * t) :=
match x as o return opt_ok o -> option (elt * t) with
| Some (k,s') => fun P : Raw.Ok s' => Some (k, Mkt s')
| None => fun _ => None
end P.
Definition remove_min s : option (elt * t) :=
mk_opt_t (Raw.remove_min (this s)) (Raw.remove_min_ok s).
Lemma remove_min_spec1 s x s' :
remove_min s = Some (x,s') ->
min_elt s = Some x /\ Equal (remove x s) s'.
Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
End Make.