Library Coq.MSets.MSetAVL


MSetAVL : Implementation of MSetInterface via AVL trees

This module implements finite sets using AVL trees. It follows the implementation from Ocaml's standard library,
All operations given here expect and produce well-balanced trees (in the ocaml sense: heigths of subtrees shouldn't differ by more than 2), and hence has low complexities (e.g. add is logarithmic in the size of the set). But proving these balancing preservations is in fact not necessary for ensuring correct operational behavior and hence fulfilling the MSet interface. As a consequence, balancing results are not part of this file anymore, they can now be found in MSetFullAVL.
Four operations (union, subset, compare and equal) have been slightly adapted in order to have only structural recursive calls. The precise ocaml versions of these operations have also been formalized (thanks to Function+measure), see ocaml_union, ocaml_subset, ocaml_compare and ocaml_equal in MSetFullAVL. The structural variants compute faster in Coq, whereas the other variants produce nicer and/or (slightly) faster code after extraction.

Require Import MSetInterface ZArith Int.

LocalLocal

Ops : the pure functions


Module Ops (Import I:Int)(X:OrderedType) <: WOps X.
Local Open Scope Int_scope.
Local Open Scope lazy_bool_scope.

Definition elt := X.t.
Hint Transparent elt.

Trees

The fourth field of Node is the height of the tree

Inductive tree :=
  | Leaf : tree
  | Node : tree -> X.t -> tree -> int -> tree.

Definition t := tree.

Basic functions on trees: height and cardinal


Definition height (s : t) : int :=
  match s with
  | Leaf => 0
  | Node _ _ _ h => h
  end.

Fixpoint cardinal (s : t) : nat :=
  match s with
   | Leaf => 0%nat
   | Node l _ r _ => S (cardinal l + cardinal r)
  end.

Empty Set


Definition empty := Leaf.

Emptyness test


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

Membership

The mem function is deciding membership. It exploits the binary search tree invariant to achieve logarithmic complexity.

Fixpoint mem x s :=
   match s with
     | Leaf => false
     | Node l y r _ => match X.compare x y with
             | Lt => mem x l
             | Eq => true
             | Gt => mem x r
         end
   end.

Singleton set


Definition singleton x := Node Leaf x Leaf 1.

Helper functions

create l x r creates a node, assuming l and r to be balanced and |height l - height r| <= 2.

Definition create l x r :=
   Node l x r (max (height l) (height r) + 1).

bal l x r acts as create, but performs one step of rebalancing if necessary, i.e. assumes |height l - height r| <= 3.

Definition assert_false := create.

Definition bal l x r :=
  let hl := height l in
  let hr := height r in
  if gt_le_dec hl (hr+2) then
    match l with
     | Leaf => assert_false l x r
     | Node ll lx lr _ =>
       if ge_lt_dec (height ll) (height lr) then
         create ll lx (create lr x r)
       else
         match lr with
          | Leaf => assert_false l x r
          | Node lrl lrx lrr _ =>
              create (create ll lx lrl) lrx (create lrr x r)
         end
    end
  else
    if gt_le_dec hr (hl+2) then
      match r with
       | Leaf => assert_false l x r
       | Node rl rx rr _ =>
         if ge_lt_dec (height rr) (height rl) then
            create (create l x rl) rx rr
         else
           match rl with
            | Leaf => assert_false l x r
            | Node rll rlx rlr _ =>
                create (create l x rll) rlx (create rlr rx rr)
           end
      end
    else
      create l x r.

Insertion


Fixpoint add x s := match s with
   | Leaf => Node Leaf x Leaf 1
   | Node l y r h =>
      match X.compare x y with
         | Lt => bal (add x l) y r
         | Eq => Node l y r h
         | Gt => bal l y (add x r)
      end
  end.

Join

Same as bal but does not assume anything regarding heights of l and r.

Fixpoint join l : elt -> t -> t :=
  match l with
    | Leaf => add
    | Node ll lx lr lh => fun x =>
       fix join_aux (r:t) : t := match r with
          | Leaf => add x l
          | Node rl rx rr rh =>
               if gt_le_dec lh (rh+2) then bal ll lx (join lr x r)
               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr
               else create l x r
          end
  end.

Extraction of minimum element

Morally, remove_min is to be applied to a non-empty tree t = Node l x r h. Since we can't deal here with assert false for t=Leaf, we pre-unpack t (and forget about h).

Fixpoint remove_min l x r : t*elt :=
  match l with
    | Leaf => (r,x)
    | Node ll lx lr lh =>
       let (l',m) := remove_min ll lx lr in (bal l' x r, m)
  end.

Merging two trees

merge t1 t2 builds the union of t1 and t2 assuming all elements of t1 to be smaller than all elements of t2, and |height t1 - height t2| <= 2.

Definition merge s1 s2 := match s1,s2 with
  | Leaf, _ => s2
  | _, Leaf => s1
  | _, Node l2 x2 r2 h2 =>
        let (s2',m) := remove_min l2 x2 r2 in bal s1 m s2'
end.

Deletion


Fixpoint remove x s := match s with
  | Leaf => Leaf
  | Node l y r h =>
      match X.compare x y with
         | Lt => bal (remove x l) y r
         | Eq => merge l r
         | Gt => bal l y (remove x r)
      end
   end.

Minimum element


Fixpoint min_elt s := match s with
   | Leaf => None
   | Node Leaf y _ _ => Some y
   | Node l _ _ _ => min_elt l
end.

Maximum element


Fixpoint max_elt s := match s with
   | Leaf => None
   | Node _ y Leaf _ => Some y
   | Node _ _ r _ => max_elt r
end.

Any element


Definition choose := min_elt.

Concatenation

Same as merge but does not assume anything about heights.

Definition concat s1 s2 :=
   match s1, s2 with
      | Leaf, _ => s2
      | _, Leaf => s1
      | _, Node l2 x2 r2 _ =>
            let (s2',m) := remove_min l2 x2 r2 in
            join s1 m s2'
   end.

Splitting

split x s returns a triple (l, present, r) where
  • l is the set of elements of s that are < x
  • r is the set of elements of s that are > x
  • present is true if and only if s contains x.

Record triple := mktriple { t_left:t; t_in:bool; t_right:t }.
Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).

Fixpoint split x s : triple := match s with
  | Leaf => << Leaf, false, Leaf >>
  | Node l y r h =>
     match X.compare x y with
      | Lt => let (ll,b,rl) := split x l in << ll, b, join rl y r >>
      | Eq => << l, true, r >>
      | Gt => let (rl,b,rr) := split x r in << join l y rl, b, rr >>
     end
 end.

Intersection


Fixpoint inter s1 s2 := match s1, s2 with
    | Leaf, _ => Leaf
    | _, Leaf => Leaf
    | Node l1 x1 r1 h1, _ =>
            let (l2',pres,r2') := split x1 s2 in
            if pres then join (inter l1 l2') x1 (inter r1 r2')
            else concat (inter l1 l2') (inter r1 r2')
    end.

Difference


Fixpoint diff s1 s2 := match s1, s2 with
 | Leaf, _ => Leaf
 | _, Leaf => s1
 | Node l1 x1 r1 h1, _ =>
    let (l2',pres,r2') := split x1 s2 in
    if pres then concat (diff l1 l2') (diff r1 r2')
    else join (diff l1 l2') x1 (diff r1 r2')
end.

Union

In ocaml, heights of s1 and s2 are compared each time in order to recursively perform the split on the smaller set. Unfortunately, this leads to a non-structural algorithm. The following code is a simplification of the ocaml version: no comparison of heights. It might be slightly slower, but experimentally all the tests I've made in ocaml have shown this potential slowdown to be non-significant. Anyway, the exact code of ocaml has also been formalized thanks to Function+measure, see ocaml_union in MSetFullAVL.

Fixpoint union s1 s2 :=
 match s1, s2 with
  | Leaf, _ => s2
  | _, Leaf => s1
  | Node l1 x1 r1 h1, _ =>
     let (l2',_,r2') := split x1 s2 in
     join (union l1 l2') x1 (union r1 r2')
 end.

Elements

elements_tree_aux acc t catenates the elements of t in infix order to the list acc

Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t :=
  match s with
   | Leaf => acc
   | Node l x r _ => elements_aux (x :: elements_aux acc r) l
  end.

then elements is an instanciation with an empty acc

Definition elements := elements_aux nil.

Filter


Fixpoint filter_acc (f:elt->bool) acc s := match s with
  | Leaf => acc
  | Node l x r h =>
     filter_acc f (filter_acc f (if f x then add x acc else acc) l) r
 end.

Definition filter f := filter_acc f Leaf.

Partition


Fixpoint partition_acc (f:elt->bool)(acc : t*t)(s : t) : t*t :=
  match s with
   | Leaf => acc
   | Node l x r _ =>
      let (acct,accf) := acc in
      partition_acc f
        (partition_acc f
           (if f x then (add x acct, accf) else (acct, add x accf)) l) r
  end.

Definition partition f := partition_acc f (Leaf,Leaf).

for_all and exists


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.

Fold


Fixpoint fold (A : Type) (f : elt -> A -> A)(s : t) : A -> A :=
 fun a => match s with
  | Leaf => a
  | Node l x r _ => fold f r (f x (fold f l a))
 end.

Subset

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:t->bool) x1 s2 : bool :=
 match s2 with
  | Leaf => false
  | Node l2 x2 r2 h2 =>
     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:t->bool) x1 s2 : bool :=
 match s2 with
  | Leaf => false
  | Node l2 x2 r2 h2 =>
     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 h1, Node l2 x2 r2 h2 =>
     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.

A new comparison algorithm suggested by Xavier Leroy

Transformation in C.P.S. suggested 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

Inductive enumeration :=
 | End : enumeration
 | More : elt -> t -> 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 h => 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).

Equality test


Definition equal s1 s2 : bool :=
 match compare s1 s2 with
  | Eq => true
  | _ => false
 end.

End Ops.

MakeRaw

Functor of pure functions + a posteriori proofs of invariant preservation

Module MakeRaw (Import I:Int)(X:OrderedType) <: RawSets X.
Include Ops I X.

Invariants

Occurrence in a tree


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

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 x l r h, bst l -> bst r ->
     lt_tree x l -> gt_tree x r -> bst (Node l x r h).

bst is the (decidable) invariant our trees will have to satisfy.

Definition IsOk := bst.

Class Ok (s:t) : 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.

Correctness proofs


Module Import MX := OrderedTypeFacts X.

Automation and dedicated tactics


Scheme tree_ind := Induction for tree 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.

Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
 "as" ident(s) :=
 set (s:=Node l x r h) in *; clearbody s; clear l x r h.

Automatic treatment of Ok hypothesis

Ltac inv_ok := match goal with
 | H:Ok (Node _ _ _ _) |- _ => inversion_clear 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; inversion_clear H; invtree f
     | H:f _ ?s |- _ => is_tree_constr s; inversion_clear H; invtree f
     | H:f _ _ ?s |- _ => is_tree_constr s; inversion_clear 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, lt_tree, gt_tree, height

In is compatible with X.eq

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 l x r h y,
  InT y (Node l x r h) <-> InT y l \/ X.eq y x \/ InT y r.

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) (h : int),
 lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y r h).

Lemma gt_tree_node :
 forall (x y : elt) (l r : tree) (h : int),
 gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y r h).

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.

Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.

Inductions principles for some of the set operators


Functional Scheme bal_ind := Induction for bal Sort Prop.
Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
Functional Scheme merge_ind := Induction for merge Sort Prop.
Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.
Functional Scheme max_elt_ind := Induction for max_elt Sort Prop.
Functional Scheme concat_ind := Induction for concat Sort Prop.
Functional Scheme inter_ind := Induction for inter Sort Prop.
Functional Scheme diff_ind := Induction for diff Sort Prop.
Functional Scheme union_ind := Induction for union Sort Prop.

Ltac induct s x :=
 induction s as [|l IHl x' r IHr h]; simpl; intros;
 [|elim_compare x x'; intros; inv].

Notations and helper lemma about pairs and triples


Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope.
Notation "t #b" := (t_in t) (at level 9, format "t '#b'") : pair_scope.
Notation "t #r" := (t_right t) (at level 9, format "t '#r'") : pair_scope.

Open Local Scope pair_scope.

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.

Singleton set


Lemma singleton_spec : forall x y, InT y (singleton x) <-> X.eq y x.

Instance singleton_ok x : Ok (singleton x).

Helper functions


Lemma create_spec :
 forall l x r y, InT y (create l x r) <-> X.eq y x \/ InT y l \/ InT y r.

Instance create_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
 Ok (create l x r).

Lemma bal_spec : forall l x r y,
 InT y (bal l x r) <-> X.eq y x \/ InT y l \/ InT y r.

Instance bal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
 Ok (bal l x r).

Insertion


Lemma add_spec' : forall s x y,
 InT y (add x s) <-> X.eq y x \/ InT y s.

Lemma add_spec : forall s x y `{Ok s},
 InT y (add x s) <-> X.eq y x \/ InT y s.

Instance add_ok s x `(Ok s) : Ok (add x s).

Open Scope Int_scope.

Join



Ltac join_tac :=
 intro l; induction l as [| ll _ lx lr Hlr lh];
   [ | intros x r; induction r as [| rl Hrl rx rr _ rh]; unfold join;
     [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
       [ match goal with |- context b [ bal ?a ?b ?c] =>
           replace (bal a b c)
           with (bal ll lx (join lr x (Node rl rx rr rh))); [ | auto]
         end
       | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
         [ match goal with |- context b [ bal ?a ?b ?c] =>
             replace (bal a b c)
             with (bal (join (Node ll lx lr lh) x rl) rx rr); [ | auto]
           end
         | ] ] ] ]; intros.

Lemma join_spec : forall l x r y,
 InT y (join l x r) <-> X.eq y x \/ InT y l \/ InT y r.

Instance join_ok : forall l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r),
 Ok (join l x r).

Extraction of minimum element


Lemma remove_min_spec : forall l x r h y,
 InT y (Node l x r h) <->
  X.eq y (remove_min l x r)#2 \/ InT y (remove_min l x r)#1.

Instance remove_min_ok l x r : forall h `(Ok (Node l x r h)),
 Ok (remove_min l x r)#1.

Lemma remove_min_gt_tree : forall l x r h `{Ok (Node l x r h)},
 gt_tree (remove_min l x r)#2 (remove_min l x r)#1.
Local Hint Resolve remove_min_gt_tree.

Merging two trees


Lemma merge_spec : forall s1 s2 y,
 InT y (merge s1 s2) <-> InT y s1 \/ InT y s2.

Instance merge_ok s1 s2 : forall `(Ok s1, Ok s2)
 `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
 Ok (merge s1 s2).

Deletion


Lemma remove_spec : forall s x y `{Ok s},
 (InT y (remove x s) <-> InT y s /\ ~ X.eq y x).

Instance remove_ok s x `(Ok s) : Ok (remove x s).

Minimum element


Lemma min_elt_spec1 : forall s x, min_elt s = Some x -> InT x s.

Lemma min_elt_spec2 : forall s x y `{Ok s},
 min_elt s = Some x -> InT y s -> ~ X.lt y x.

Lemma min_elt_spec3 : forall s, min_elt s = None -> Empty s.

Maximum element


Lemma max_elt_spec1 : forall s x, max_elt s = Some x -> InT x s.

Lemma max_elt_spec2 : forall s x y `{Ok s},
 max_elt s = Some x -> InT y s -> ~ X.lt x y.

Lemma max_elt_spec3 : forall s, max_elt s = None -> Empty s.

Any element


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

Concatenation


Lemma concat_spec : forall s1 s2 y,
 InT y (concat s1 s2) <-> InT y s1 \/ InT y s2.

Instance concat_ok s1 s2 : forall `(Ok s1, Ok s2)
 `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
 Ok (concat s1 s2).

Splitting


Lemma split_spec1 : forall s x y `{Ok s},
 (InT y (split x s)#l <-> InT y s /\ X.lt y x).

Lemma split_spec2 : forall s x y `{Ok s},
 (InT y (split x s)#r <-> InT y s /\ X.lt x y).

Lemma split_spec3 : forall s x `{Ok s},
 ((split x s)#b = true <-> InT x s).

Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r.

Instance split_ok1 s x `(Ok s) : Ok (split x s)#l.

Instance split_ok2 s x `(Ok s) : Ok (split x s)#r.

Intersection


Ltac destruct_split := match goal with
 | H : split ?x ?s = << ?u, ?v, ?w >> |- _ =>
   assert ((split x s)#l = u) by (rewrite H; auto);
   assert ((split x s)#b = v) by (rewrite H; auto);
   assert ((split x s)#r = w) by (rewrite H; auto);
   clear H; subst u w
 end.

Lemma inter_spec_ok : forall s1 s2 `{Ok s1, Ok s2},
 Ok (inter s1 s2) /\ (forall y, InT y (inter s1 s2) <-> InT y s1 /\ InT y s2).

Lemma inter_spec : forall s1 s2 y `{Ok s1, Ok s2},
 (InT y (inter s1 s2) <-> InT y s1 /\ InT y s2).

Instance inter_ok s1 s2 `(Ok s1, Ok s2) : Ok (inter s1 s2).

Difference


Lemma diff_spec_ok : forall s1 s2 `{Ok s1, Ok s2},
 Ok (diff s1 s2) /\ (forall y, InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2).

Lemma diff_spec : forall s1 s2 y `{Ok s1, Ok s2},
 (InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2).

Instance diff_ok s1 s2 `(Ok s1, Ok s2) : Ok (diff s1 s2).

Union


Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2},
 (InT y (union s1 s2) <-> InT y s1 \/ InT y s2).

Instance union_ok s1 s2 : forall `(Ok s1, Ok s2), Ok (union s1 s2).

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:t)(Hs:Ok s) := elements_cardinal s.

Lemma elements_app :
 forall s acc, elements_aux acc s = elements s ++ acc.

Lemma elements_node :
 forall l x r h acc,
 elements l ++ x :: elements r ++ acc =
 elements (Node l x r h) ++ acc.

Filter


Lemma filter_spec' : forall s x acc f,
 Proper (X.eq==>eq) f ->
 (InT x (filter_acc f acc s) <-> InT x acc \/ InT x s /\ f x = true).

Instance filter_ok' : forall s acc f `(Ok s, Ok acc),
 Ok (filter_acc f acc s).

Lemma filter_spec : forall s x f,
 Proper (X.eq==>eq) f ->
 (InT x (filter f s) <-> InT x s /\ f x = true).

Instance filter_ok s f `(Ok s) : Ok (filter f s).

Partition


Lemma partition_spec1' : forall s acc f,
 Proper (X.eq==>eq) f -> forall x : elt,
 InT x (partition_acc f acc s)#1 <->
 InT x acc#1 \/ InT x s /\ f x = true.

Lemma partition_spec2' : forall s acc f,
 Proper (X.eq==>eq) f -> forall x : elt,
 InT x (partition_acc f acc s)#2 <->
 InT x acc#2 \/ InT x s /\ f x = false.

Lemma partition_spec1 : forall s f,
 Proper (X.eq==>eq) f ->
 Equal (partition f s)#1 (filter f s).

Lemma partition_spec2 : forall s f,
 Proper (X.eq==>eq) f ->
 Equal (partition f s)#2 (filter (fun x => negb (f x)) s).

Instance partition_ok1' : forall s acc f `(Ok s, Ok acc#1),
 Ok (partition_acc f acc s)#1.

Instance partition_ok2' : forall s acc f `(Ok s, Ok acc#2),
 Ok (partition_acc f acc s)#2.

Instance partition_ok1 s f `(Ok s) : Ok (partition f s)#1.

Instance partition_ok2 s f `(Ok s) : Ok (partition f s)#2.

for_all and exists


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

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

Fold


Lemma fold_spec' :
 forall (A : Type) (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 :
 forall (s:t) (A : Type) (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 h1 s2
 `{Ok (Node l1 x1 Leaf h1), Ok s2},
 (forall s `{Ok s}, (subset_l1 s = true <-> Subset l1 s)) ->
 (subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ).

Lemma subsetr_spec : forall subset_r1 r1 x1 h1 s2,
 bst (Node Leaf x1 r1 h1) -> bst s2 ->
 (forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) ->
 (subsetr subset_r1 x1 s2 = true <-> Subset (Node Leaf x1 r1 h1) 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 := 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 : t) : 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 h e,
 elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ 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.

End MakeRaw.

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 MSetFullAVL if you need more than just the MSet interface.

Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 Module Raw := MakeRaw I X.
 Include Raw2Sets X Raw.
End IntMake.


Module Make (X: OrderedType) <: S with Module E := X
 :=IntMake(Z_as_Int)(X).