Library FSetRBT

Red-black trees

  Inductive color : Set := red : color | black : color.

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

Occurrence in a tree

  Inductive In_tree [x:elt] : tree -> Prop :=
  | IsRoot : (l,r:tree)(c:color)(y:elt)
             (X.eq x y) -> (In_tree x (Node c l y r))
  | InLeft : (l,r:tree)(c:color)(y:elt)
             (In_tree x l) -> (In_tree x (Node c l y r))
  | InRight : (l,r:tree)(c:color)(y:elt)
              (In_tree x r) -> (In_tree x (Node c l y r)).

   Hint In_tree := Constructors In_tree.

In_tree is color-insensitive

  Lemma In_color : (c,c':color)(x,y:elt)(l,r:tree)
    (In_tree y (Node c l x r)) -> (In_tree y (Node c' l x r)).
   Hints Resolve In_color.

Binary search trees

lt_tree x s: all elements in s are smaller than x (resp. greater for gt_tree)

  Definition lt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt y x).
  Definition gt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt x y).

   Hints Unfold lt_tree gt_tree.

Results about lt_tree and gt_tree

  Lemma lt_leaf : (x:elt)(lt_tree x Leaf).

  Lemma gt_leaf : (x:elt)(gt_tree x Leaf).

  Lemma lt_tree_node : (x,y:elt)(l,r:tree)(c:color)
    (lt_tree x l) -> (lt_tree x r) -> (X.lt y x) ->
    (lt_tree x (Node c l y r)).

  Lemma gt_tree_node : (x,y:elt)(l,r:tree)(c:color)
    (gt_tree x l) -> (gt_tree x r) -> (E.lt x y) ->
    (gt_tree x (Node c l y r)).

   Hints Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.

  Lemma lt_node_lt : (x,y:elt)(l,r:tree)(c:color)
     (lt_tree x (Node c l y r)) -> (E.lt y x).

  Lemma gt_node_gt : (x,y:elt)(l,r:tree)(c:color)
     (gt_tree x (Node c l y r)) -> (E.lt x y).

  Lemma lt_left : (x,y:elt)(l,r:tree)(c:color)
     (lt_tree x (Node c l y r)) -> (lt_tree x l).

  Lemma lt_right : (x,y:elt)(l,r:tree)(c:color)
     (lt_tree x (Node c l y r)) -> (lt_tree x r).

  Lemma gt_left : (x,y:elt)(l,r:tree)(c:color)
     (gt_tree x (Node c l y r)) -> (gt_tree x l).

  Lemma gt_right : (x,y:elt)(l,r:tree)(c:color)
     (gt_tree x (Node c l y r)) -> (gt_tree x r).

   Hints Resolve lt_node_lt gt_node_gt
                lt_left lt_right gt_left gt_right.

  Lemma lt_tree_not_in :
    (x:elt)(t:tree)(lt_tree x t) -> ~(In_tree x t).

  Lemma lt_tree_trans :
    (x,y:elt)(X.lt x y) -> (t:tree)(lt_tree x t) -> (lt_tree y t).

  Lemma gt_tree_not_in :
    (x:elt)(t:tree)(gt_tree x t) -> ~(In_tree x t).

  Lemma gt_tree_trans :
    (x,y:elt)(X.lt y x) -> (t:tree)(gt_tree x t) -> (gt_tree y t).

   Hints Resolve lt_tree_not_in lt_tree_trans
                gt_tree_not_in gt_tree_trans.

bst t : t is a binary search tree

  Inductive bst : tree -> Prop :=
  | BSLeaf :
      (bst Leaf)
  | BSNode : (x:elt)(l,r:tree)(c:color)
      (bst l) -> (bst r) ->
      (lt_tree x l) -> (gt_tree x r) ->
      (bst (Node c l x r)).

   Hint bst := Constructors bst.

Results about bst


 
  Lemma bst_left : (x:elt)(l,r:tree)(c:color)
    (bst (Node c l x r)) -> (bst l).

  Lemma bst_right : (x:elt)(l,r:tree)(c:color)
    (bst (Node c l x r)) -> (bst r).

   Implicits bst_left. Implicits bst_right.
   Hints Resolve bst_left bst_right.

  Lemma bst_color : (c,c':color)(x:elt)(l,r:tree)
    (bst (Node c l x r)) -> (bst (Node c' l x r)).
   Hints Resolve bst_color.

Key fact about binary search trees: rotations preserve the bst property

  Lemma rotate_left : (x,y:elt)(a,b,c:tree)(c1,c2,c3,c4:color)
    (bst (Node c1 a x (Node c2 b y c))) ->
    (bst (Node c3 (Node c4 a x b) y c)).

  Lemma rotate_right : (x,y:elt)(a,b,c:tree)(c1,c2,c3,c4:color)
    (bst (Node c3 (Node c4 a x b) y c)) ->
    (bst (Node c1 a x (Node c2 b y c))).

   Hints Resolve rotate_left rotate_right.

Balanced red-black trees

rbtree n t: t is a properly balanced red-black tree, i.e. it satisfies the following two invariants: a red node has no red son any path from the root to a leaf has exactly n black nodes


       
  Definition is_not_red [t:tree] := Cases t of
  | Leaf => True
  | (Node black x0 x1 x2) => True
  | (Node red x0 x1 x2) => False
  end.

   Hints Unfold is_not_red.

  Inductive rbtree : nat -> tree -> Prop :=
  | RBLeaf :
      (rbtree O Leaf)
  | RBRed : (x:elt)(l,r:tree)(n:nat)
      (rbtree n l) -> (rbtree n r) ->
      (is_not_red l) -> (is_not_red r) ->
      (rbtree n (Node red l x r))
  | RBBlack : (x:elt)(l,r:tree)(n:nat)
      (rbtree n l) -> (rbtree n r) ->
      (rbtree (S n) (Node black l x r)).

   Hint rbtree := Constructors rbtree.

Results about rbtree

  Lemma rbtree_left :
    (x:elt)(l,r:tree)(c:color)
    (EX n:nat | (rbtree n (Node c l x r))) ->
    (EX n:nat | (rbtree n l)).

  Lemma rbtree_right :
    (x:elt)(l,r:tree)(c:color)
    (EX n:nat | (rbtree n (Node c l x r))) ->
    (EX n:nat | (rbtree n r)).

   Implicits rbtree_left. Implicits rbtree_right.
   Hints Resolve rbtree_left rbtree_right.

Sets as red-black trees

A set is implement as a record t, containing a tree, a proof that it is a binary search tree and a proof that it is a properly balanced red-black tree

  Record t_ : Set := t_intro {
    the_tree :> tree;
    is_bst : (bst the_tree);
    is_rbtree : (EX n:nat | (rbtree n the_tree)) }.
  Definition t := t_.

Projections

  Lemma t_is_bst : (s:t)(bst s).
   Hints Resolve t_is_bst.

Logical appartness

  Definition In : elt -> t -> Prop := [x:elt][s:t](In_tree x s).

  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
  Definition Empty := [s](a:elt)~(In a s).
  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).

  Lemma eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s).

   Hints Resolve eq_In.

Empty set

  Definition t_empty : t.

  Definition empty : { s:t | (x:elt)~(In x s) }.

Emptyness test

  Definition is_empty : (s:t){ Empty s }+{ ~(Empty s) }.

Appartness

The mem function is deciding appartness. It exploits the bst property to achieve logarithmic complexity.

  Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.

Singleton set

  Definition singleton_tree [x:elt] := (Node red Leaf x Leaf).

  Lemma singleton_bst : (x:elt)(bst (singleton_tree x)).

  Lemma singleton_rbtree : (x:elt)(EX n:nat | (rbtree n (singleton_tree x))).

  Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.

Insertion

almost_rbtree n t: t may have one red-red conflict at its root; it satisfies rbtree n everywhere else

  Inductive almost_rbtree : nat -> tree -> Prop :=
  | ARBLeaf :
      (almost_rbtree O Leaf)
  | ARBRed : (x:elt)(l,r:tree)(n:nat)
      (rbtree n l) -> (rbtree n r) ->
      (almost_rbtree n (Node red l x r))
  | ARBBlack : (x:elt)(l,r:tree)(n:nat)
      (rbtree n l) -> (rbtree n r) ->
      (almost_rbtree (S n) (Node black l x r)).

   Hint almost_rbtree := Constructors almost_rbtree.

Results about almost_rbtree

  Lemma rbtree_almost_rbtree :
    (n:nat)(t:tree)(rbtree n t) -> (almost_rbtree n t).

   Hints Resolve rbtree_almost_rbtree.

  Lemma rbtree_almost_rbtree_ex : (s:tree)
    (EX n:nat | (rbtree n s)) -> (EX n:nat | (almost_rbtree n s)).

   Hints Resolve rbtree_almost_rbtree_ex.

  Lemma almost_rbtree_rbtree_black : (x:elt)(l,r:tree)(n:nat)
    (almost_rbtree n (Node black l x r)) ->
    (rbtree n (Node black l x r)).
   Hints Resolve almost_rbtree_rbtree_black.

Balancing functions lbalance and rbalance (see below) require a rather complex pattern-matching; it is realized by the following function conflict which returns in the sum type Conflict

  Inductive Conflict [s:tree] : Set :=
  | NoConflict :
      ((n:nat) (almost_rbtree n s) -> (rbtree n s)) ->
      (Conflict s)
  | RedRedConflict :
      (a,b,c:tree)(x,y:elt)
      (bst a) -> (bst b) -> (bst c) ->
      (lt_tree x a) -> (gt_tree x b) ->
      (lt_tree y b) -> (gt_tree y c) -> (X.lt x y) ->
      ((z:elt)(In_tree z s) <->
        ((X.eq z x) \/ (X.eq z y) \/
         (In_tree z a) \/ (In_tree z b) \/ (In_tree z c))) ->
      ((n:nat)(almost_rbtree n s) ->
              ((rbtree n a) /\ (rbtree n b) /\ (rbtree n c))) ->
      (Conflict s).

  Definition conflict : (s:tree)(bst s) -> (Conflict s).

lbalance c x l r acts as a black node constructor, solving a possible red-red conflict on l, using the following schema: B (R (R a x b) y c) z d B (R a x (R b y c)) z d -> R (B a x b) y (R c z d) B a x b -> B a x b The result is not necessarily a black node.

  Definition lbalance :
    (l:tree)(x:elt)(r:tree)
    (lt_tree x l) -> (gt_tree x r) ->
    (bst l) -> (bst r) ->
    { s:tree |
        (bst s) /\
        ((n:nat)((almost_rbtree n l) /\ (rbtree n r)) ->
                (rbtree (S n) s)) /\
        (y:elt)(In_tree y s) <-> ((E.eq y x)\/(In_tree y l)\/(In_tree y r)) }.

rbalance l x r is similar to lbalance, solving a possible red-red conflict on r. The balancing schema is similar: B a x (R (R b y c) z d) B a x (R b y (R c z d)) -> R (B a x b) y (R c z d) B a x b -> B a x b

  Definition rbalance :
     (l:tree)(x:elt)(r:tree)
     (lt_tree x l) -> (gt_tree x r) ->
     (bst l) -> (bst r) ->
     { s:tree |
        (bst s) /\
        ((n:nat)((almost_rbtree n r) /\ (rbtree n l)) ->
                (rbtree (S n) s)) /\
        (y:elt)(In_tree y s) <-> ((E.eq y x)\/(In_tree y l)\/(In_tree y r)) }.

insert x s inserts x in tree s, resulting in a possible top red-red conflict when s is red. Its code is: insert x Empty = Node red Empty x Empty insert x (Node red a y b) = if lt x y then Node red (insert x a) y b else if lt y x then Node red a y (insert x b) else (Node c a y b) insert x (Node black a y b) = if lt x y then lbalance (insert x a) y b else if lt y x then rbalance a y (insert x b) else (Node c a y b)

  Definition insert :
    (x:elt) (s:t)
    { s':tree | (bst s') /\
                ((n:nat)(rbtree n s) ->
                   ((almost_rbtree n s') /\
                    ((is_not_red s) -> (rbtree n s')))) /\
                (y:elt)(In_tree y s') <-> ((E.eq y x) \/ (In_tree y s)) }.

Finally add x s calls insert and recolors the root as black: add x s = match insert x s with | Node _ a y b -> Node black a y b | Empty -> assert false (* absurd *)

  Definition add : (x:elt) (s:t) { s':t | (Add x s s') }.

Deletion

UnbalancedLeft n t: t is a tree of black height S n on its left side and n on its right side (the root color is taken into account, whathever it is)


     
  Inductive UnbalancedLeft : nat -> tree -> Prop :=
  | ULRed : (x:elt)(l,r:tree)(n:nat)
      (rbtree (S n) l) -> (rbtree n r) ->
      (is_not_red l) ->
      (UnbalancedLeft n (Node red l x r))
  | ULBlack : (x:elt)(l,r:tree)(n:nat)
      (rbtree (S n) l) -> (rbtree n r) ->
      (UnbalancedLeft (S n) (Node black l x r)).

when a tree is unbalanced on its left, it can be repared

  Definition unbalanced_left :
    (s:tree)(bst s) ->
    { r : tree * bool |
        let (s',b) = r in
        (bst s') /\
        ((is_not_red s) /\ b=false -> (is_not_red s')) /\
        ((n:nat)(UnbalancedLeft n s) ->
                (if b then (rbtree n s') else (rbtree (S n) s'))) /\
        ((y:elt)(In_tree y s') <-> (In_tree y s)) }.

UnbalancedRight n t: t is a tree of black height S n on its right side and n on its left side (the root color is taken into account, whathever it is)


     
  Inductive UnbalancedRight : nat -> tree -> Prop :=
  | URRed : (x:elt)(l,r:tree)(n:nat)
      (rbtree n l) -> (rbtree (S n) r) ->
      (is_not_red r) ->
      (UnbalancedRight n (Node red l x r))
  | URBlack : (x:elt)(l,r:tree)(n:nat)
      (rbtree n l) -> (rbtree (S n) r) ->
      (UnbalancedRight (S n) (Node black l x r)).

when a tree is unbalanced on its right, it can be repared

  Definition unbalanced_right :
    (s:tree)(bst s) ->
    { r : tree * bool |
        let (s',b) = r in
        (bst s') /\
        ((is_not_red s) /\ b=false -> (is_not_red s')) /\
        ((n:nat)(UnbalancedRight n s) ->
                (if b then (rbtree n s') else (rbtree (S n) s'))) /\
        ((y:elt)(In_tree y s') <-> (In_tree y s)) }.

remove_min s extracts the minimum elements of s and indicates whether the black height has decreased.

  Definition remove_min :
    (s:tree)(bst s) -> ~s=Leaf ->
    { r : tree * elt * bool |
        let (s',r') = r in
        let (m,b) = r' in
        (bst s') /\
        ((is_not_red s) /\ b=false -> (is_not_red s')) /\
        ((n:nat) (rbtree n s) ->
                 (if b then (lt O n) /\ (rbtree (pred n) s') else (rbtree n s'))) /\
        ((y:elt)(In_tree y s') -> (E.lt m y)) /\
        ((y:elt)(In_tree y s) <-> (E.eq y m) \/ (In_tree y s')) }.

blackify colors the root node in Black

  Definition blackify :
    (s:tree)(bst s) ->
    { r : tree * bool |
        let (s',b) = r in
        (is_not_red s') /\ (bst s') /\
        ((n:nat)(rbtree n s) ->
                if b then (rbtree n s') else (rbtree (S n) s')) /\
        ((y:elt)(In_tree y s) <-> (In_tree y s')) }.

remove_aux x s removes x from s and indicates whether the black height has decreased.

  Definition remove_aux :
    (x:elt)(s:tree)(bst s) ->
    { r : tree * bool |
        let (s',b) = r in
        (bst s') /\
        ((is_not_red s) /\ b=false -> (is_not_red s')) /\
        ((n:nat) (rbtree n s) ->
                 (if b then (lt O n) /\ (rbtree (pred n) s') else (rbtree n s'))) /\
        ((y:elt)(In_tree y s') <-> (~(E.eq y x) /\ (In_tree y s))) }.

remove is just a call to remove_aux

  Definition remove : (x:elt)(s:t)
                      { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.

From lists to red-black trees


  


of_list builds a red-black tree from a sorted list

  Set Implicit Arguments.
  Record of_list_aux_Invariant [k,n:Z; l,l':(list elt); r:tree] : Prop :=
  make_olai
  { olai_bst : (bst r);
    olai_rb : (EX kn:nat | (inject_nat kn)=k /\ (rbtree kn r));
    olai_sort : (sort E.lt l');
    olai_length : (Zlength l')=(Zlength l)-n;
    olai_same :
      ((x:elt)(InList E.eq x l) <-> (In_tree x r) \/ (InList E.eq x l'));
    olai_order :
      ((x,y:elt)(In_tree x r) -> (InList E.eq y l') -> (E.lt x y)) }.
  Unset Implicit Arguments.

  Lemma power_invariant :
    (n,k:Z)0<k ->
    (two_p k) <= n +1 <= (two_p (Zs k)) ->
    let (nn,_) = (Zsplit2 (n-1)) in let (n1,n2) = nn in
    (two_p (Zpred k)) <= n1+1 <= (two_p k) /\
    (two_p (Zpred k)) <= n2+1 <= (two_p k).

  Definition of_list_aux :
    (k:Z) 0<=k ->
    (n:Z) (two_p k) <= n+1 <= (two_p (Zs k)) ->
    (l:(list elt)) (sort E.lt l) -> n <= (Zlength l) ->
    { rl' : tree * (list elt)
    | let (r,l')=rl' in (of_list_aux_Invariant k n l l' r) }.

  Definition of_list : (l:(list elt))(sort E.lt l) ->
    { s : t | (x:elt)(In x s) <-> (InList E.eq x l) }.
  


Elements

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

  Fixpoint elements_tree_aux [acc:(list X.t); t:tree] : (list X.t) :=
    Cases t of
    | Leaf =>
        acc
    | (Node _ l x r) =>
        (elements_tree_aux (x :: (elements_tree_aux acc r)) l)
    end.

then elements_tree is an instanciation with an empty acc

  Definition elements_tree := (elements_tree_aux []).

  Lemma elements_tree_aux_acc_1 :
    (s:tree)(acc:(list elt))
    (x:elt)(InList E.eq x acc)->(InList E.eq x (elements_tree_aux acc s)).
   Hints Resolve elements_tree_aux_acc_1.

  Lemma elements_tree_aux_1 :
    (s:tree)(acc:(list elt))
    (x:elt)(In_tree x s)->(InList E.eq x (elements_tree_aux acc s)).

  Lemma elements_tree_1 :
    (s:tree)
    (x:elt)(In_tree x s)->(InList E.eq x (elements_tree s)).
   Hints Resolve elements_tree_1.

  Lemma elements_tree_aux_acc_2 :
    (s:tree)(acc:(list elt))
    (x:elt)(InList E.eq x (elements_tree_aux acc s)) ->
      (InList E.eq x acc) \/ (In_tree x s).
   Hints Resolve elements_tree_aux_acc_2.

  Lemma elements_tree_2 :
   (s:tree)
    (x:elt)(InList E.eq x (elements_tree s)) -> (In_tree x s).
   Hints Resolve elements_tree_2.

  Lemma elements_tree_aux_sort :
    (s:tree)(bst s) -> (acc:(list elt))
    (sort E.lt acc) ->
    ((x:elt)(InList E.eq x acc) -> (y:elt)(In_tree y s) -> (E.lt y x)) ->
    (sort E.lt (elements_tree_aux acc s)).

  Lemma elements_tree_sort :
    (s:tree)(bst s) -> (sort E.lt (elements_tree s)).
   Hints Resolve elements_tree_sort.

  Definition elements :
    (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}.

Isomorphism with FSetList

  Module Lists := FSetList.Make(X).

  Definition of_slist : (l:Lists.t) { s : t | (x:elt)(Lists.In x l)<->(In x s) }.

  Definition to_slist : (s:t) { l : Lists.t | (x:elt)(In x s)<->(Lists.In x l) }.

Union

  Definition union : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.

Intersection

  Lemma inter : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.

Difference

  Lemma diff : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.

Equality test

Set Ground Depth 5.

  Lemma equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.

Inclusion test

  Lemma subset : (s,s':t){ Subset s s' } + { ~(Subset s s') }.

Fold

  Fixpoint fold_tree [A:Set; f:elt->A->A; s:tree] : A -> A :=
    Cases s of
    | Leaf => [a]a
    | (Node _ l x r) => [a](fold_tree A f l (f x (fold_tree A f r a)))
    end.
   Implicits fold_tree [1].

  Definition fold_tree' :=
   [A:Set; f:elt->A->A; s:tree] (Lists.Raw.fold f (elements_tree s)).
   Implicits fold_tree' [1].

  Lemma fold_tree_equiv_aux :
     (A:Set)(s:tree)(f:elt->A->A)(a:A; acc : (list elt))
     (Lists.Raw.fold f (elements_tree_aux acc s) a)
     = (fold_tree f s (Lists.Raw.fold f acc a)).

  Lemma fold_tree_equiv :
     (A:Set)(s:tree)(f:elt->A->A; a:A)
     (fold_tree f s a)=(fold_tree' f s a).

  Definition fold :
   (A:Set)(f:elt->A->A)(s:t)(i:A)
   { r : A | (EX l:(list elt) |
                  (Unique E.eq l) /\
                  ((x:elt)(In x s)<->(InList E.eq x l)) /\
                  r = (fold_right f i l)) }.

Cardinal

  Definition cardinal :
     (s:t) { r : nat | (EX l:(list elt) |
                              (Unique E.eq l) /\
                              ((x:elt)(In x s)<->(InList E.eq x l)) /\
                              r = (length l)) }.

Filter

  Module DLists := DepOfNodep(Lists).

  Definition filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
     { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.

  Lemma for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
     { (compat_P E.eq P) -> (For_all P s) } +
     { (compat_P E.eq P) -> ~(For_all P s) }.

  Lemma exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
     { (compat_P E.eq P) -> (Exists P s) } +
     { (compat_P E.eq P) -> ~(Exists P s) }.

  Lemma partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
     { partition : t*t |
        let (s1,s2) = partition in
        (compat_P E.eq P) ->
        ((For_all P s1) /\
         (For_all ([x]~(P x)) s2) /\
         (x:elt)(In x s)<->((In x s1)\/(In x s2))) }.

Minimum element

  Definition min_elt :
     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.

Maximum element

  Definition max_elt :
     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.

Any element

  Definition choose : (s:t) { x:elt | (In x s)} + { Empty s }.

Comparison


  
  Definition eq : t -> t -> Prop := Equal.

  Definition lt : t -> t -> Prop :=
    [s,s':t]let (l,_) = (to_slist s) in
            let (l',_) = (to_slist s') in
            (Lists.lt l l').

  Lemma eq_refl: (s:t)(eq s s).

  Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s).

  Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').

  Lemma lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').

  Definition eql : t -> t -> Prop :=
    [s,s':t]let (l,_) = (to_slist s) in
            let (l',_) = (to_slist s') in
            (Lists.eq l l').

  Lemma eq_eql : (s,s':t)(eq s s') -> (eql s s').

  Lemma eql_eq : (s,s':t)(eql s s') -> (eq s s').

  Lemma lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s').
  
  Definition compare: (s,s':t)(Compare lt eq s s').

End Make.