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 height 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 FunInd Orders OrdersFacts MSetInterface PeanoNat.
Require Arith. Local Open Scope list_scope.
Local Open Scope lazy_bool_scope.


Module Type InfoTyp.
 Parameter t : Set.
End InfoTyp.

Ops : the pure functions


Module Type Ops (X:OrderedType)(Info:InfoTyp).

Definition elt := X.t.
#[global]
Hint Transparent elt : core.

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 literature.

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.

#[global]
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 : core.
Local Hint Immediate MX.eq_sym : core.
Local Hint Unfold In lt_tree gt_tree : core.
Local Hint Constructors InT bst : core.
Local Hint Unfold Ok : core.

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 (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.

#[global]
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 : core.

#[global]
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 : core.

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.

#[global]
Instance lt_tree_compat : Proper (X.eq ==> Logic.eq ==> iff) lt_tree.

#[global]
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 : core.

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.

#[global]
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 : core.

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.
#[global]
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').


#[global]
Instance lt_strorder : StrictOrder lt.

#[global]
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 : core.

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 ->
 Nat.log2 (cardinal s) < maxdepth s.

Lemma mindepth_log_cardinal s : mindepth s <= Nat.log2 (S (cardinal s)).

End Props.