# Library Coq.MSets.MSetGenTree

# MSetGenTree : sets via generic trees

This module factorizes common parts in implementations of finite sets as AVL trees and as Red-Black trees. The nodes of the trees defined here include an generic information parameter, that will be the heigth in AVL trees and the color in Red-Black trees. Without more details here about these information parameters, trees here are not known to be well-balanced, but simply binary-search-trees.
The operations we could define and prove correct here are the one that do not build non-empty trees, but only analyze them :

- empty is_empty
- mem
- compare equal subset
- fold cardinal elements
- for_all exists - min_elt max_elt choose

Require Import Orders OrdersFacts MSetInterface NPeano.
Local Open Scope list_scope.
Local Open Scope lazy_bool_scope.
LocalLocal
Module Type InfoTyp.
Parameter t : Set.
End InfoTyp.

# Ops : the pure functions

Module Type Ops (X:OrderedType)(Info:InfoTyp).
Definition elt := X.t.
Hint Transparent elt.
Inductive tree : Type :=
| Leaf : tree
| Node : Info.t -> tree -> X.t -> tree -> tree.

## The empty set and emptyness test

Definition empty := Leaf.
Definition is_empty t :=
match t with
| Leaf => true
| _ => false
end.

## Membership test

The mem function is deciding membership. It exploits the binary search tree invariant to achieve logarithmic complexity.
Fixpoint mem x t :=
match t with
| Leaf => false
| Node _ l k r =>
match X.compare x k with
| Lt => mem x l
| Eq => true
| Gt => mem x r
end
end.

## Minimal, maximal, arbitrary elements

Fixpoint min_elt (t : tree) : option elt :=
match t with
| Leaf => None
| Node _ Leaf x r => Some x
| Node _ l x r => min_elt l
end.
Fixpoint max_elt (t : tree) : option elt :=
match t with
| Leaf => None
| Node _ l x Leaf => Some x
| Node _ l x r => max_elt r
end.
Definition choose := min_elt.

## Iteration on elements

Fixpoint fold {A: Type} (f: elt -> A -> A) (t: tree) (base: A) : A :=
match t with
| Leaf => base
| Node _ l x r => fold f r (f x (fold f l base))
end.
Fixpoint elements_aux acc s :=
match s with
| Leaf => acc
| Node _ l x r => elements_aux (x :: elements_aux acc r) l
end.
Definition elements := elements_aux nil.
Fixpoint rev_elements_aux acc s :=
match s with
| Leaf => acc
| Node _ l x r => rev_elements_aux (x :: rev_elements_aux acc l) r
end.
Definition rev_elements := rev_elements_aux nil.
Fixpoint cardinal (s : tree) : nat :=
match s with
| Leaf => 0
| Node _ l _ r => S (cardinal l + cardinal r)
end.
Fixpoint maxdepth s :=
match s with
| Leaf => 0
| Node _ l _ r => S (max (maxdepth l) (maxdepth r))
end.
Fixpoint mindepth s :=
match s with
| Leaf => 0
| Node _ l _ r => S (min (mindepth l) (mindepth r))
end.

## Testing universal or existential properties.

We do not use the standard boolean operators of Coq, but lazy ones.
Fixpoint for_all (f:elt->bool) s := match s with
| Leaf => true
| Node _ l x r => f x &&& for_all f l &&& for_all f r
end.
Fixpoint exists_ (f:elt->bool) s := match s with
| Leaf => false
| Node _ l x r => f x ||| exists_ f l ||| exists_ f r
end.

## Comparison of trees

The algorithm here has been suggested by Xavier Leroy, and transformed into c.p.s. by Benjamin Grégoire. The original ocaml code (with non-structural recursive calls) has also been formalized (thanks to Function+measure), see ocaml_compare in MSetFullAVL. The following code with continuations computes dramatically faster in Coq, and should be almost as efficient after extraction.
Enumeration of the elements of a tree. This corresponds to the "samefringe" notion in the litterature.
Inductive enumeration :=
| End : enumeration
| More : elt -> tree -> enumeration -> enumeration.
cons t e adds the elements of tree t on the head of enumeration e.
Fixpoint cons s e : enumeration :=
match s with
| Leaf => e
| Node _ l x r => cons l (More x r e)
end.
One step of comparison of elements
Definition compare_more x1 (cont:enumeration->comparison) e2 :=
match e2 with
| End => Gt
| More x2 r2 e2 =>
match X.compare x1 x2 with
| Eq => cont (cons r2 e2)
| Lt => Lt
| Gt => Gt
end
end.
Comparison of left tree, middle element, then right tree
Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 :=
match s1 with
| Leaf => cont e2
| Node _ l1 x1 r1 =>
compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2
end.
Initial continuation
Definition compare_end e2 :=
match e2 with End => Eq | _ => Lt end.
The complete comparison
Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End).
Definition equal s1 s2 :=
match compare s1 s2 with Eq => true | _ => false end.

## Subset test

In ocaml, recursive calls are made on "half-trees" such as (Node _ l1 x1 Leaf) and (Node _ Leaf x1 r1). Instead of these non-structural calls, we propose here two specialized functions for these situations. This version should be almost as efficient as the one of ocaml (closures as arguments may slow things a bit), it is simply less compact. The exact ocaml version has also been formalized (thanks to Function+measure), see ocaml_subset in MSetFullAVL.
Fixpoint subsetl (subset_l1 : tree -> bool) x1 s2 : bool :=
match s2 with
| Leaf => false
| Node _ l2 x2 r2 =>
match X.compare x1 x2 with
| Eq => subset_l1 l2
| Lt => subsetl subset_l1 x1 l2
| Gt => mem x1 r2 &&& subset_l1 s2
end
end.
Fixpoint subsetr (subset_r1 : tree -> bool) x1 s2 : bool :=
match s2 with
| Leaf => false
| Node _ l2 x2 r2 =>
match X.compare x1 x2 with
| Eq => subset_r1 r2
| Lt => mem x1 l2 &&& subset_r1 s2
| Gt => subsetr subset_r1 x1 r2
end
end.
Fixpoint subset s1 s2 : bool := match s1, s2 with
| Leaf, _ => true
| Node _ _ _ _, Leaf => false
| Node _ l1 x1 r1, Node _ l2 x2 r2 =>
match X.compare x1 x2 with
| Eq => subset l1 l2 &&& subset r1 r2
| Lt => subsetl (subset l1) x1 l2 &&& subset r1 s2
| Gt => subsetr (subset r1) x1 r2 &&& subset l1 s2
end
end.
End Ops.

# Props : correctness proofs of these generic operations

Module Type Props (X:OrderedType)(Info:InfoTyp)(Import M:Ops X Info).

## Occurrence in a tree

Inductive InT (x : elt) : tree -> Prop :=
| IsRoot : forall c l r y, X.eq x y -> InT x (Node c l y r)
| InLeft : forall c l r y, InT x l -> InT x (Node c l y r)
| InRight : forall c l r y, InT x r -> InT x (Node c l y r).
Definition In := InT.

## Some shortcuts

Definition Equal s s' := forall a : elt, InT a s <-> InT a s'.
Definition Subset s s' := forall a : elt, InT a s -> InT a s'.
Definition Empty s := forall a : elt, ~ InT a s.
Definition For_all (P : elt -> Prop) s := forall x, InT x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x , InT x s /\ P x.

## Binary search trees

lt_tree x s: all elements in s are smaller than x (resp. greater for gt_tree)
Definition lt_tree x s := forall y, InT y s -> X.lt y x.
Definition gt_tree x s := forall y, InT y s -> X.lt x y.
bst t : t is a binary search tree
Inductive bst : tree -> Prop :=
| BSLeaf : bst Leaf
| BSNode : forall c x l r, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (Node c l x r).
bst is the (decidable) invariant our trees will have to satisfy.
Definition IsOk := bst.
Class Ok (s:tree) : Prop := ok : bst s.
Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }.
Fixpoint ltb_tree x s :=
match s with
| Leaf => true
| Node _ l y r =>
match X.compare x y with
| Gt => ltb_tree x l && ltb_tree x r
| _ => false
end
end.
Fixpoint gtb_tree x s :=
match s with
| Leaf => true
| Node _ l y r =>
match X.compare x y with
| Lt => gtb_tree x l && gtb_tree x r
| _ => false
end
end.
Fixpoint isok s :=
match s with
| Leaf => true
| Node _ l x r => isok l && isok r && ltb_tree x l && gtb_tree x r
end.

## Known facts about ordered types

Module Import MX := OrderedTypeFacts X.

## Automation and dedicated tactics

Scheme tree_ind := Induction for tree Sort Prop.
Scheme bst_ind := Induction for bst Sort Prop.
Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree.
Local Hint Constructors InT bst.
Local Hint Unfold Ok.
Automatic treatment of Ok hypothesis
Ltac clear_inversion H := inversion H; clear H; subst.
Ltac inv_ok := match goal with
| H:Ok (Node _ _ _ _) |- _ => clear_inversion H; inv_ok
| H:Ok Leaf |- _ => clear H; inv_ok
| H:bst ?x |- _ => change (Ok x) in H; inv_ok
| _ => idtac
end.
A tactic to repeat inversion_clear on all hyps of the form (f (Node _ _ _ _))
Ltac is_tree_constr c :=
match c with
| Leaf => idtac
| Node _ _ _ _ => idtac
| _ => fail
end.
Ltac invtree f :=
match goal with
| H:f ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
| H:f _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
| H:f _ _ ?s |- _ => is_tree_constr s; clear_inversion H; invtree f
| _ => idtac
end.
Ltac inv := inv_ok; invtree InT.
Ltac intuition_in := repeat progress (intuition; inv).
Helper tactic concerning order of elements.
Ltac order := match goal with
| U: lt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
| U: gt_tree _ ?s, V: InT _ ?s |- _ => generalize (U _ V); clear U; order
| _ => MX.order
end.
isok is indeed a decision procedure for Ok
Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true.
Lemma gtb_tree_iff : forall x s, gt_tree x s <-> gtb_tree x s = true.
Lemma isok_iff : forall s, Ok s <-> isok s = true.
Instance isok_Ok s : isok s = true -> Ok s | 10.

## Basic results about In

Lemma In_1 :
forall s x y, X.eq x y -> InT x s -> InT y s.
Local Hint Immediate In_1.
Instance In_compat : Proper (X.eq ==> eq ==> iff) InT.
Lemma In_node_iff :
forall c l x r y,
InT y (Node c l x r) <-> InT y l \/ X.eq y x \/ InT y r.
Lemma In_leaf_iff : forall x, InT x Leaf <-> False.
Results about lt_tree and gt_tree
Lemma lt_leaf : forall x : elt, lt_tree x Leaf.
Lemma gt_leaf : forall x : elt, gt_tree x Leaf.
Lemma lt_tree_node :
forall (x y : elt) (l r : tree) (i : Info.t),
lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node i l y r).
Lemma gt_tree_node :
forall (x y : elt) (l r : tree) (i : Info.t),
gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node i l y r).
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
Lemma lt_tree_not_in :
forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t.
Lemma lt_tree_trans :
forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t.
Lemma gt_tree_not_in :
forall (x : elt) (t : tree), gt_tree x t -> ~ InT x t.
Lemma gt_tree_trans :
forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t.
Instance lt_tree_compat : Proper (X.eq ==> Logic.eq ==> iff) lt_tree.
Instance gt_tree_compat : Proper (X.eq ==> Logic.eq ==> iff) gt_tree.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
Ltac induct s x :=
induction s as [|i l IHl x' r IHr]; simpl; intros;
[|elim_compare x x'; intros; inv].
Ltac auto_tc := auto with typeclass_instances.
Ltac ok :=
inv; change bst with Ok in *;
match goal with
| |- Ok (Node _ _ _ _) => constructor; auto_tc; ok
| |- lt_tree _ (Node _ _ _ _) => apply lt_tree_node; ok
| |- gt_tree _ (Node _ _ _ _) => apply gt_tree_node; ok
| _ => eauto with typeclass_instances
end.

## Empty set

Lemma empty_spec : Empty empty.
Instance empty_ok : Ok empty.

## Emptyness test

Lemma is_empty_spec : forall s, is_empty s = true <-> Empty s.

## Membership

Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.

## Minimal and maximal elements

Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.
Lemma min_elt_spec1 s x : min_elt s = Some x -> InT x s.
Lemma min_elt_spec2 s x y `{Ok s} :
min_elt s = Some x -> InT y s -> ~ X.lt y x.
Lemma min_elt_spec3 s : min_elt s = None -> Empty s.
Lemma max_elt_spec1 s x : max_elt s = Some x -> InT x s.
Lemma max_elt_spec2 s x y `{Ok s} :
max_elt s = Some x -> InT y s -> ~ X.lt x y.
Lemma max_elt_spec3 s : max_elt s = None -> Empty s.
Lemma choose_spec1 : forall s x, choose s = Some x -> InT x s.
Lemma choose_spec2 : forall s, choose s = None -> Empty s.
Lemma choose_spec3 : forall s s' x x' `{Ok s, Ok s'},
choose s = Some x -> choose s' = Some x' ->
Equal s s' -> X.eq x x'.

## Elements

Lemma elements_spec1' : forall s acc x,
InA X.eq x (elements_aux acc s) <-> InT x s \/ InA X.eq x acc.
Lemma elements_spec1 : forall s x, InA X.eq x (elements s) <-> InT x s.
Lemma elements_spec2' : forall s acc `{Ok s}, sort X.lt acc ->
(forall x y : elt, InA X.eq x acc -> InT y s -> X.lt y x) ->
sort X.lt (elements_aux acc s).
Lemma elements_spec2 : forall s `(Ok s), sort X.lt (elements s).
Local Hint Resolve elements_spec2.
Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s).
Lemma elements_aux_cardinal :
forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s).
Lemma elements_cardinal : forall s : tree, cardinal s = length (elements s).
Definition cardinal_spec (s:tree)(Hs:Ok s) := elements_cardinal s.
Lemma elements_app :
forall s acc, elements_aux acc s = elements s ++ acc.
Lemma elements_node c l x r :
elements (Node c l x r) = elements l ++ x :: elements r.
Lemma rev_elements_app :
forall s acc, rev_elements_aux acc s = rev_elements s ++ acc.
Lemma rev_elements_node c l x r :
rev_elements (Node c l x r) = rev_elements r ++ x :: rev_elements l.
Lemma rev_elements_rev s : rev_elements s = rev (elements s).
The converse of elements_spec2, used in MSetRBT
Lemma sorted_app_inv l1 l2 :
sort X.lt (l1++l2) ->
sort X.lt l1 /\ sort X.lt l2 /\
forall x1 x2, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2.
Lemma elements_sort_ok s : sort X.lt (elements s) -> Ok s.

## for_all and exists

Lemma for_all_spec s f : Proper (X.eq==>eq) f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Lemma exists_spec s f : Proper (X.eq==>eq) f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).

## Fold

Lemma fold_spec' {A} (f : elt -> A -> A) (s : tree) (i : A) (acc : list elt) :
fold_left (flip f) (elements_aux acc s) i = fold_left (flip f) acc (fold f s i).
Lemma fold_spec (s:tree) {A} (i : A) (f : elt -> A -> A) :
fold f s i = fold_left (flip f) (elements s) i.

## Subset

Lemma subsetl_spec : forall subset_l1 l1 x1 c1 s2
`{Ok (Node c1 l1 x1 Leaf), Ok s2},
(forall s `{Ok s}, (subset_l1 s = true <-> Subset l1 s)) ->
(subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2 ).
Lemma subsetr_spec : forall subset_r1 r1 x1 c1 s2,
bst (Node c1 Leaf x1 r1) -> bst s2 ->
(forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) ->
(subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) s2).
Lemma subset_spec : forall s1 s2 `{Ok s1, Ok s2},
(subset s1 s2 = true <-> Subset s1 s2).

## Comparison

Relations eq and lt over trees
Module L := MSetInterface.MakeListOrdering X.
Definition eq := Equal.
Instance eq_equiv : Equivalence eq.
Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
Definition lt (s1 s2 : tree) : Prop :=
exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
/\ L.lt (elements s1') (elements s2').
Instance lt_strorder : StrictOrder lt.
Instance lt_compat : Proper (eq==>eq==>iff) lt.
Proof of the comparison algorithm
flatten_e e returns the list of elements of e i.e. the list of elements actually compared
Fixpoint flatten_e (e : enumeration) : list elt := match e with
| End => nil
| More x t r => x :: elements t ++ flatten_e r
end.
Lemma flatten_e_elements :
forall l x r c e,
elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e.
Lemma cons_1 : forall s e,
flatten_e (cons s e) = elements s ++ flatten_e e.
Correctness of this comparison
Definition Cmp c x y := CompSpec L.eq L.lt x y c.
Local Hint Unfold Cmp flip.
Lemma compare_end_Cmp :
forall e2, Cmp (compare_end e2) nil (flatten_e e2).
Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
(flatten_e (More x2 r2 e2)).
Lemma compare_cont_Cmp : forall s1 cont e2 l,
(forall e, Cmp (cont e) l (flatten_e e)) ->
Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
Lemma compare_Cmp : forall s1 s2,
Cmp (compare s1 s2) (elements s1) (elements s2).
Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
CompSpec eq lt s1 s2 (compare s1 s2).

## Equality test

Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2},
equal s1 s2 = true <-> eq s1 s2.

## A few results about mindepth and maxdepth

Lemma mindepth_maxdepth s : mindepth s <= maxdepth s.
Lemma maxdepth_cardinal s : cardinal s < 2^(maxdepth s).
Lemma mindepth_cardinal s : 2^(mindepth s) <= S (cardinal s).
Lemma maxdepth_log_cardinal s : s <> Leaf ->
log2 (cardinal s) < maxdepth s.
Lemma mindepth_log_cardinal s : mindepth s <= log2 (S (cardinal s)).
End Props.