diff options
Diffstat (limited to 'theories/FSets/FSetAVL.v')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 3351 |
1 files changed, 1253 insertions, 2098 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index d5ce54d9..faa705f6 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) @@ -12,41 +11,555 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL.v 9862 2007-05-25 16:57:06Z letouzey $ *) +(* $Id: FSetAVL.v 10811 2008-04-17 16:29:49Z letouzey $ *) + +(** * FSetAVL *) (** This module implements sets using AVL trees. - It follows the implementation from Ocaml's standard library. *) + 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 FSet interface. As a consequence, + balancing results are not part of this file anymore, they can + now be found in [FSetFullAVL]. + + 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 + [FSetFullAVL]. The structural variants compute faster in Coq, + whereas the other variants produce nicer and/or (slightly) faster + code after extraction. +*) -Require Import FSetInterface. -Require Import FSetList. -Require Import ZArith. -Require Import Int. +Require Import FSetInterface FSetList ZArith Int. -Set Firstorder Depth 3. +Set Implicit Arguments. +Unset Strict Implicit. -Module Raw (I:Int)(X:OrderedType). -Import I. -Module II:=MoreInt(I). -Import II. -Open Local Scope Int_scope. +(** Notations and helper lemma about pairs *) + +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. -Module E := X. -Module MX := OrderedTypeFacts X. +(** * Raw + + Functor of pure functions + a posteriori proofs of invariant + preservation *) + +Module Raw (Import I:Int)(X:OrderedType). +Open Local Scope pair_scope. +Open Local Scope lazy_bool_scope. +Open Local Scope Int_scope. Definition elt := X.t. -(** * Trees *) +(** * Trees -Inductive tree : Set := + The fourth field of [Node] is the height of the tree *) + +Inductive tree := | Leaf : tree | Node : tree -> X.t -> tree -> int -> tree. Notation t := tree. -(** The fourth field of [Node] is the height of the tree *) +(** * Basic functions on trees: height and cardinal *) + +Definition height (s : tree) : int := + match s with + | Leaf => 0 + | Node _ _ _ h => h + end. + +Fixpoint cardinal (s : tree) : 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. + +(** * Appartness *) + +(** The [mem] function is deciding appartness. 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). +Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). +Notation "t #b" := (t_in t) (at level 9, format "t '#b'"). +Notation "t #r" := (t_right t) (at level 9, format "t '#r'"). + +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 [FSetFullAVL]. +*) + +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) (t : tree) : list X.t := + match t 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 : tree) : A -> A := + fun a => match s with + | Leaf => a + | Node l x r _ => fold f r (f x (fold f l a)) + end. +Implicit Arguments fold [A]. + + +(** * 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 + [FSetFullAVL]. + *) + +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 [FSetFullAVL]. 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 -> 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 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. + + + + +(** * Invariants *) + +(** ** Occurrence in a tree *) + +Inductive In (x : elt) : tree -> Prop := + | IsRoot : forall l r h y, X.eq x y -> In x (Node l y r h) + | InLeft : forall l r h y, In x l -> In x (Node l y r h) + | InRight : forall l r h y, In x r -> In x (Node l y r h). + +(** ** 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, In y s -> X.lt y x. +Definition gt_tree x s := forall y, In 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). + + + + +(** * Some shortcuts *) + +Definition Equal s s' := forall a : elt, In a s <-> In a s'. +Definition Subset s s' := forall a : elt, In a s -> In a s'. +Definition Empty s := forall a : elt, ~ In a s. +Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x. +Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x. + + + +(** * Correctness proofs, isolated in a sub-module *) + +Module Proofs. + Module MX := OrderedTypeFacts X. + Module L := FSetList.Raw X. + +(** * Automation and dedicated tactics *) + +Hint Constructors In bst. +Hint Unfold lt_tree gt_tree. + +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. (** A tactic to repeat [inversion_clear] on all hyps of the form [(f (Node _ _ _ _))] *) + Ltac inv f := match goal with | H:f Leaf |- _ => inversion_clear H; inv f @@ -56,30 +569,18 @@ Ltac inv f := | _ => idtac end. -(** Same, but with a backup of the original hypothesis. *) +Ltac intuition_in := repeat progress (intuition; inv In). -Ltac safe_inv f := match goal with - | H:f (Node _ _ _ _) |- _ => - generalize H; inversion_clear H; safe_inv f - | _ => intros - end. +(** Helper tactic concerning order of elements. *) -(** * Occurrence in a tree *) +Ltac order := match goal with + | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order + | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order + | _ => MX.order +end. -Inductive In (x : elt) : tree -> Prop := - | IsRoot : - forall (l r : tree) (h : int) (y : elt), - X.eq x y -> In x (Node l y r h) - | InLeft : - forall (l r : tree) (h : int) (y : elt), - In x l -> In x (Node l y r h) - | InRight : - forall (l r : tree) (h : int) (y : elt), - In x r -> In x (Node l y r h). - -Hint Constructors In. -Ltac intuition_in := repeat progress (intuition; inv In). +(** * Basic results about [In], [lt_tree], [gt_tree], [height] *) (** [In] is compatible with [X.eq] *) @@ -90,48 +591,37 @@ Proof. Qed. Hint Immediate In_1. -(** * 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) := - forall y:elt, In y s -> X.lt y x. -Definition gt_tree (x : elt) (s : tree) := - forall y:elt, In y s -> X.lt x y. - -Hint Unfold lt_tree gt_tree. - -Ltac order := match goal with - | H: lt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order - | H: gt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order - | _ => MX.order -end. +Lemma In_node_iff : + forall l x r h y, + In y (Node l x r h) <-> In y l \/ X.eq y x \/ In y r. +Proof. + intuition_in. +Qed. (** Results about [lt_tree] and [gt_tree] *) Lemma lt_leaf : forall x : elt, lt_tree x Leaf. Proof. - unfold lt_tree in |- *; intros; inversion H. + red; inversion 1. Qed. Lemma gt_leaf : forall x : elt, gt_tree x Leaf. Proof. - unfold gt_tree in |- *; intros; inversion H. + red; inversion 1. Qed. 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). Proof. - unfold lt_tree in *; intuition_in; order. + unfold lt_tree; intuition_in; order. Qed. 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). Proof. - unfold gt_tree in *; intuition_in; order. + unfold gt_tree; intuition_in; order. Qed. Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. @@ -145,7 +635,7 @@ Qed. Lemma lt_tree_trans : forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t. Proof. - firstorder eauto. + eauto. Qed. Lemma gt_tree_not_in : @@ -157,120 +647,43 @@ Qed. Lemma gt_tree_trans : forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t. Proof. - firstorder eauto. + eauto. Qed. Hint 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 : - forall (x : elt) (l r : tree) (h : int), - bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (Node l x r h). +(** * Inductions principles *) -Hint Constructors bst. +Functional Scheme mem_ind := Induction for mem Sort Prop. +Functional Scheme bal_ind := Induction for bal Sort Prop. +Functional Scheme add_ind := Induction for add Sort Prop. +Functional Scheme remove_min_ind := Induction for remove_min Sort Prop. +Functional Scheme merge_ind := Induction for merge Sort Prop. +Functional Scheme remove_ind := Induction for remove 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 split_ind := Induction for split 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. -(** * AVL trees *) -(** [avl s] : [s] is a properly balanced AVL tree, - i.e. for any node the heights of the two children - differ by at most 2 *) - -Definition height (s : tree) : int := - match s with - | Leaf => 0 - | Node _ _ _ h => h - end. - -Inductive avl : tree -> Prop := - | RBLeaf : avl Leaf - | RBNode : - forall (x : elt) (l r : tree) (h : int), - avl l -> - avl r -> - -(2) <= height l - height r <= 2 -> - h = max (height l) (height r) + 1 -> - avl (Node l x r h). - -Hint Constructors avl. - -(** Results about [avl] *) - -Lemma avl_node : - forall (x : elt) (l r : tree), - avl l -> - avl r -> - -(2) <= height l - height r <= 2 -> - avl (Node l x r (max (height l) (height r) + 1)). -Proof. - intros; auto. -Qed. -Hint Resolve avl_node. - -(** The tactics *) +(** * Empty set *) -Lemma height_non_negative : forall s : tree, avl s -> height s >= 0. +Lemma empty_1 : Empty empty. Proof. - induction s; simpl; intros; auto with zarith. - inv avl; intuition; omega_max. + intro; intro. + inversion H. Qed. -Implicit Arguments height_non_negative. - -(** When [H:avl r], typing [avl_nn H] or [avl_nn r] adds [height r>=0] *) - -Ltac avl_nn_hyp H := - let nz := fresh "nz" in assert (nz := height_non_negative H). - -Ltac avl_nn h := - let t := type of h in - match type of t with - | Prop => avl_nn_hyp h - | _ => match goal with H : avl h |- _ => avl_nn_hyp H end - end. - -(* Repeat the previous tactic. - Drawback: need to clear the [avl _] hyps ... Thank you Ltac *) - -Ltac avl_nns := - match goal with - | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns - | _ => idtac - end. - -(** * Some shortcuts. *) - -Definition Equal s s' := forall a : elt, In a s <-> In a s'. -Definition Subset s s' := forall a : elt, In a s -> In a s'. -Definition Empty s := forall a : elt, ~ In a s. -Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x. -Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x. - -(** * Empty set *) - -Definition empty := Leaf. Lemma empty_bst : bst empty. Proof. auto. Qed. -Lemma empty_avl : avl empty. -Proof. - auto. -Qed. - -Lemma empty_1 : Empty empty. -Proof. - intro; intro. - inversion H. -Qed. - (** * Emptyness test *) -Definition is_empty (s:t) := match s with Leaf => true | _ => false end. - Lemma is_empty_1 : forall s, Empty s -> is_empty s = true. Proof. destruct s as [|r x l h]; simpl; auto. @@ -282,54 +695,28 @@ Proof. destruct s; simpl; intros; try discriminate; red; auto. Qed. -(** * Appartness *) -(** The [mem] function is deciding appartness. It exploits the [bst] property - to achieve logarithmic complexity. *) -Function mem (x:elt)(s:t) { struct s } : bool := - 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. +(** * Appartness *) Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. -Proof. - intros s x. - functional induction (mem x s); inversion_clear 1; auto. - inversion_clear 1. - inversion_clear 1; auto; absurd (X.lt x y); eauto. - inversion_clear 1; auto; absurd (X.lt y x); eauto. +Proof. + intros s x; functional induction mem x s; auto; intros; try clear e0; + inv bst; intuition_in; order. Qed. Lemma mem_2 : forall s x, mem x s = true -> In x s. Proof. - intros s x. - functional induction (mem x s); auto; intros; try discriminate. + intros s x; functional induction mem x s; auto; intros; discriminate. Qed. -(** * Singleton set *) -Definition singleton (x : elt) := Node Leaf x Leaf 1. - -Lemma singleton_bst : forall x : elt, bst (singleton x). -Proof. - unfold singleton; auto. -Qed. -Lemma singleton_avl : forall x : elt, avl (singleton x). -Proof. - unfold singleton; intro. - constructor; auto; try red; simpl; omega_max. -Qed. +(** * Singleton set *) Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y. Proof. - unfold singleton; inversion_clear 1; auto; inversion_clear H0. + unfold singleton; intros; inv In; order. Qed. Lemma singleton_2 : forall x y, X.eq x y -> In y (singleton x). @@ -337,35 +724,14 @@ Proof. unfold singleton; auto. Qed. -(** * 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). - -Lemma create_bst : - forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> - bst (create l x r). +Lemma singleton_bst : forall x : elt, bst (singleton x). Proof. - unfold create; auto. + unfold singleton; auto. Qed. -Hint Resolve create_bst. -Lemma create_avl : - forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> - avl (create l x r). -Proof. - unfold create; auto. -Qed. -Lemma create_height : - forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> - height (create l x r) = max (height l) (height r) + 1. -Proof. - unfold create; intros; auto. -Qed. + +(** * Helper functions *) Lemma create_in : forall l x r y, In y (create l x r) <-> X.eq y x \/ In y l \/ In y r. @@ -373,196 +739,69 @@ Proof. unfold create; split; [ inversion_clear 1 | ]; intuition. Qed. -(** trick for emulating [assert false] in Coq *) - -Definition assert_false := Leaf. - -(** [bal l x r] acts as [create], but performs one step of - rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) - -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 - | 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 - | 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 - | 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 - | Node rll rlx rlr _ => - create (create l x rll) rlx (create rlr rx rr) - end - end - else - create l x r. - -Ltac bal_tac := - intros l x r; - unfold bal; - destruct (gt_le_dec (height l) (height r + 2)); - [ destruct l as [ |ll lx lr lh]; - [ | destruct (ge_lt_dec (height ll) (height lr)); - [ | destruct lr ] ] - | destruct (gt_le_dec (height r) (height l + 2)); - [ destruct r as [ |rl rx rr rh]; - [ | destruct (ge_lt_dec (height rr) (height rl)); - [ | destruct rl ] ] - | ] ]; intros. - -Lemma bal_bst : forall l x r, bst l -> bst r -> - lt_tree x l -> gt_tree x r -> bst (bal l x r). -Proof. - (* intros l x r; functional induction bal l x r. MARCHE PAS !*) - bal_tac; - inv bst; repeat apply create_bst; auto; unfold create; - apply lt_tree_node || apply gt_tree_node; auto; - eapply lt_tree_trans || eapply gt_tree_trans || eauto; eauto. -Qed. - -Lemma bal_avl : forall l x r, avl l -> avl r -> - -(3) <= height l - height r <= 3 -> avl (bal l x r). +Lemma create_bst : + forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> + bst (create l x r). Proof. - bal_tac; inv avl; repeat apply create_avl; simpl in *; auto; omega_max. + unfold create; auto. Qed. +Hint Resolve create_bst. -Lemma bal_height_1 : forall l x r, avl l -> avl r -> - -(3) <= height l - height r <= 3 -> - 0 <= height (bal l x r) - max (height l) (height r) <= 1. +Lemma bal_in : forall l x r y, + In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r. Proof. - bal_tac; inv avl; avl_nns; simpl in *; omega_max. + intros l x r; functional induction bal l x r; intros; try clear e0; + rewrite !create_in; intuition_in. Qed. -Lemma bal_height_2 : - forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> - height (bal l x r) == max (height l) (height r) +1. +Lemma bal_bst : forall l x r, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (bal l x r). Proof. - bal_tac; inv avl; simpl in *; omega_max. + intros l x r; functional induction bal l x r; intros; + inv bst; repeat apply create_bst; auto; unfold create; + (apply lt_tree_node || apply gt_tree_node); auto; + (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. +Hint Resolve bal_bst. -Lemma bal_in : forall l x r y, avl l -> avl r -> - (In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r). -Proof. - bal_tac; - solve [repeat rewrite create_in; intuition_in - |inv avl; avl_nns; simpl in *; false_omega]. -Qed. -Ltac omega_bal := match goal with - | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] => - generalize (bal_height_1 l x r H H') (bal_height_2 l x r H H'); - omega_max - end. (** * Insertion *) -Function add (x:elt)(s:t) { struct s } : t := 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. - -Lemma add_avl_1 : forall s x, avl s -> - avl (add x s) /\ 0 <= height (add x s) - height s <= 1. -Proof. - intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *. - intuition; try constructor; simpl; auto; try omega_max. - (* LT *) - destruct IHt; auto. - split. - apply bal_avl; auto; omega_max. - omega_bal. - (* EQ *) - intuition; omega_max. - (* GT *) - destruct IHt; auto. - split. - apply bal_avl; auto; omega_max. - omega_bal. -Qed. - -Lemma add_avl : forall s x, avl s -> avl (add x s). -Proof. - intros; generalize (add_avl_1 s x H); intuition. -Qed. -Hint Resolve add_avl. - -Lemma add_in : forall s x y, avl s -> - (In y (add x s) <-> X.eq y x \/ In y s). +Lemma add_in : forall s x y, + In y (add x s) <-> X.eq y x \/ In y s. Proof. - intros s x; functional induction (add x s); auto; intros. - intuition_in. - (* LT *) - inv avl. - rewrite bal_in; auto. - rewrite (IHt y0 H0); intuition_in. - (* EQ *) - inv avl. - intuition. + intros s x; functional induction (add x s); auto; intros; + try rewrite bal_in, IHt; intuition_in. eapply In_1; eauto. - (* GT *) - inv avl. - rewrite bal_in; auto. - rewrite (IHt y0 H1); intuition_in. Qed. -Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s). +Lemma add_bst : forall s x, bst s -> bst (add x s). Proof. - intros s x; functional induction (add x s); auto; intros. - inv bst; inv avl; apply bal_bst; auto. + intros s x; functional induction (add x s); auto; intros; + inv bst; apply bal_bst; auto. (* lt_tree -> lt_tree (add ...) *) - red; red in H4. + red; red in H3. intros. - rewrite (add_in l x y0 H) in H0. + rewrite add_in in H. intuition. eauto. - inv bst; inv avl; apply bal_bst; auto. + inv bst; auto using bal_bst. (* gt_tree -> gt_tree (add ...) *) - red; red in H4. + red; red in H3. intros. - rewrite (add_in r x y0 H5) in H0. + rewrite add_in in H. intuition. apply MX.lt_eq with x; auto. Qed. +Hint Resolve add_bst. -(** * Join - Same as [bal] but does not assume anything regarding heights - of [l] and [r]. -*) -Fixpoint join (l:t) : 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. +(** * Join *) + +(* Function/Functional Scheme can't deal with internal fix. + Let's do its job by hand: *) Ltac join_tac := intro l; induction l as [| ll _ lx lr Hlr lh]; @@ -579,437 +818,200 @@ Ltac join_tac := end | ] ] ] ]; intros. -Lemma join_avl_1 : forall l x r, avl l -> avl r -> avl (join l x r) /\ - 0<= height (join l x r) - max (height l) (height r) <= 1. -Proof. - (* intros l x r; functional induction join l x r. AUTRE PROBLEME! *) - join_tac. - - split; simpl; auto. - destruct (add_avl_1 r x H0). - avl_nns; omega_max. - split; auto. - set (l:=Node ll lx lr lh) in *. - destruct (add_avl_1 l x H). - simpl (height Leaf). - avl_nns; omega_max. - - inversion_clear H. - assert (height (Node rl rx rr rh) = rh); auto. - set (r := Node rl rx rr rh) in *; clearbody r. - destruct (Hlr x r H2 H0); clear Hrl Hlr. - set (j := join lr x r) in *; clearbody j. - simpl. - assert (-(3) <= height ll - height j <= 3) by omega_max. - split. - apply bal_avl; auto. - omega_bal. - - inversion_clear H0. - assert (height (Node ll lx lr lh) = lh); auto. - set (l := Node ll lx lr lh) in *; clearbody l. - destruct (Hrl H H1); clear Hrl Hlr. - set (j := join l x rl) in *; clearbody j. - simpl. - assert (-(3) <= height j - height rr <= 3) by omega_max. - split. - apply bal_avl; auto. - omega_bal. - - clear Hrl Hlr. - assert (height (Node ll lx lr lh) = lh); auto. - assert (height (Node rl rx rr rh) = rh); auto. - set (l := Node ll lx lr lh) in *; clearbody l. - set (r := Node rl rx rr rh) in *; clearbody r. - assert (-(2) <= height l - height r <= 2) by omega_max. - split. - apply create_avl; auto. - rewrite create_height; auto; omega_max. -Qed. - -Lemma join_avl : forall l x r, avl l -> avl r -> avl (join l x r). -Proof. - intros; generalize (join_avl_1 l x r H H0); intuition. -Qed. -Hint Resolve join_avl. - -Lemma join_in : forall l x r y, avl l -> avl r -> - (In y (join l x r) <-> X.eq y x \/ In y l \/ In y r). +Lemma join_in : forall l x r y, + In y (join l x r) <-> X.eq y x \/ In y l \/ In y r. Proof. join_tac. simpl. rewrite add_in; intuition_in. - rewrite add_in; intuition_in. - - inv avl. - rewrite bal_in; auto. - rewrite Hlr; clear Hlr Hrl; intuition_in. - - inv avl. - rewrite bal_in; auto. - rewrite Hrl; clear Hlr Hrl; intuition_in. - + rewrite bal_in, Hlr; clear Hlr Hrl; intuition_in. + rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in. apply create_in. Qed. -Lemma join_bst : forall l x r, bst l -> avl l -> bst r -> avl r -> +Lemma join_bst : forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (join l x r). Proof. - join_tac. - apply add_bst; auto. - apply add_bst; auto. - - inv bst; safe_inv avl. - apply bal_bst; auto. - clear Hrl Hlr H13 H14 H16 H17 z; intro; intros. - set (r:=Node rl rx rr rh) in *; clearbody r. - rewrite (join_in lr x r y) in H13; auto. - intuition. - apply MX.lt_eq with x; eauto. - eauto. - - inv bst; safe_inv avl. - apply bal_bst; auto. - clear Hrl Hlr H13 H14 H16 H17 z; intro; intros. - set (l:=Node ll lx lr lh) in *; clearbody l. - rewrite (join_in l x rl y) in H13; auto. - intuition. - apply MX.eq_lt with x; eauto. - eauto. - - apply create_bst; auto. + join_tac; auto; inv bst; apply bal_bst; auto; + clear Hrl Hlr z; intro; intros; rewrite join_in in *. + intuition; [ apply MX.lt_eq with x | ]; eauto. + intuition; [ apply MX.eq_lt with x | ]; eauto. Qed. +Hint Resolve join_bst. -(** * 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]). -*) - -Function remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := - match l with - | Leaf => (r,x) - | Node ll lx lr lh => let (l',m) := (remove_min ll lx lr : t*elt) in (bal l' x r, m) - end. - -Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> - avl (fst (remove_min l x r)) /\ - 0 <= height (Node l x r h) - height (fst (remove_min l x r)) <= 1. -Proof. - intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. - inv avl; simpl in *; split; auto. - avl_nns; omega_max. - (* l = Node *) - inversion_clear H. - rewrite e0 in IHp;simpl in IHp;destruct (IHp lh); auto. - split; simpl in *. - apply bal_avl; auto; omega_max. - omega_bal. -Qed. -Lemma remove_min_avl : forall l x r h, avl (Node l x r h) -> - avl (fst (remove_min l x r)). -Proof. - intros; generalize (remove_min_avl_1 l x r h H); intuition. -Qed. +(** * Extraction of minimum element *) -Lemma remove_min_in : forall l x r h y, avl (Node l x r h) -> - (In y (Node l x r h) <-> - X.eq y (snd (remove_min l x r)) \/ In y (fst (remove_min l x r))). +Lemma remove_min_in : forall l x r h y, + In y (Node l x r h) <-> + X.eq y (remove_min l x r)#2 \/ In y (remove_min l x r)#1. Proof. intros l x r; functional induction (remove_min l x r); simpl in *; intros. intuition_in. - (* l = Node *) - inversion_clear H. - generalize (remove_min_avl ll lx lr lh H0). - rewrite e0; simpl; intros. - rewrite bal_in; auto. - rewrite e0 in IHp;generalize (IHp lh y H0). - intuition. - inversion_clear H7; intuition. + rewrite bal_in, In_node_iff, IHp, e0; simpl; intuition. Qed. Lemma remove_min_bst : forall l x r h, - bst (Node l x r h) -> avl (Node l x r h) -> bst (fst (remove_min l x r)). + bst (Node l x r h) -> bst (remove_min l x r)#1. Proof. - intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. + intros l x r; functional induction (remove_min l x r); simpl; intros. inv bst; auto. - inversion_clear H; inversion_clear H0. - rewrite_all e0;simpl in *. + inversion_clear H. + specialize IHp with (1:=H0); rewrite e0 in IHp; auto. apply bal_bst; auto. - firstorder. - intro; intros. - generalize (remove_min_in ll lx lr lh y H). - rewrite e0; simpl. - destruct 1. - apply H3; intuition. + intro y; specialize (H2 y). + rewrite remove_min_in, e0 in H2; simpl in H2; intuition. Qed. Lemma remove_min_gt_tree : forall l x r h, - bst (Node l x r h) -> avl (Node l x r h) -> - gt_tree (snd (remove_min l x r)) (fst (remove_min l x r)). + bst (Node l x r h) -> + gt_tree (remove_min l x r)#2 (remove_min l x r)#1. Proof. - intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. + intros l x r; functional induction (remove_min l x r); simpl; intros. inv bst; auto. - inversion_clear H; inversion_clear H0. - intro; intro. - generalize (IHp lh H1 H); clear H6 H7 IHp. - generalize (remove_min_avl ll lx lr lh H). - generalize (remove_min_in ll lx lr lh m H). - rewrite e0; simpl; intros. - rewrite (bal_in l' x r y H7 H5) in H0. - destruct H6. - firstorder. - apply MX.lt_eq with x; auto. - apply X.lt_trans with x; auto. + inversion_clear H. + specialize IHp with (1:=H0); rewrite e0 in IHp; simpl in IHp. + intro y; rewrite bal_in; intuition; + specialize (H2 m); rewrite remove_min_in, e0 in H2; simpl in H2; + [ apply MX.lt_eq with x | ]; eauto. Qed. +Hint Resolve remove_min_bst remove_min_gt_tree. -(** * 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]. -*) -Function merge (s1 s2 :t) : t:= 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. -Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 -> - -(2) <= height s1 - height s2 <= 2 -> - avl (merge s1 s2) /\ - 0<= height (merge s1 s2) - max (height s1) (height s2) <=1. -Proof. - intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros. - split; auto; avl_nns; omega_max. - split; auto; avl_nns; simpl in *; omega_max. - destruct s1;try contradiction;clear y. - generalize (remove_min_avl_1 l2 x2 r2 h2 H0). - rewrite e1; simpl; destruct 1. - split. - apply bal_avl; auto. - simpl; omega_max. - omega_bal. -Qed. - -Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 -> - -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2). -Proof. - intros; generalize (merge_avl_1 s1 s2 H H0 H1); intuition. -Qed. +(** * Merging two trees *) -Lemma merge_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - (In y (merge s1 s2) <-> In y s1 \/ In y s2). -Proof. - intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros. +Lemma merge_in : forall s1 s2 y, + In y (merge s1 s2) <-> In y s1 \/ In y s2. +Proof. + intros s1 s2; functional induction (merge s1 s2); intros; + try factornode _x _x0 _x1 _x2 as s1. intuition_in. intuition_in. - destruct s1;try contradiction;clear y. - replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite e1; auto]. - rewrite bal_in; auto. - generalize (remove_min_avl l2 x2 r2 h2); rewrite e1; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y0); rewrite e1; simpl; intro. - rewrite H3 ; intuition. + rewrite bal_in, remove_min_in, e1; simpl; intuition. Qed. -Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> +Lemma merge_bst : forall s1 s2, bst s1 -> bst s2 -> (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> - bst (merge s1 s2). + bst (merge s1 s2). Proof. - intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto. - destruct s1;try contradiction;clear y. + intros s1 s2; functional induction (merge s1 s2); intros; auto; + try factornode _x _x0 _x1 _x2 as s1. apply bal_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2); rewrite e1; simpl in *; auto. - intro; intro. - apply H3; auto. - generalize (remove_min_in l2 x2 r2 h2 m); rewrite e1; simpl; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite e1; simpl; auto. -Qed. + change s2' with ((s2',m)#1); rewrite <-e1; eauto. + intros y Hy. + apply H1; auto. + rewrite remove_min_in, e1; simpl; auto. + change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto. +Qed. +Hint Resolve merge_bst. -(** * Deletion *) -Function remove (x:elt)(s:tree) { struct s } : t := 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. -Lemma remove_avl_1 : forall s x, avl s -> - avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1. -Proof. - intros s x; functional induction (remove x s); subst;simpl; intros. - intuition; omega_max. - (* LT *) - inv avl. - destruct (IHt H0). - split. - apply bal_avl; auto. - omega_max. - omega_bal. - (* EQ *) - inv avl. - generalize (merge_avl_1 l r H0 H1 H2). - intuition omega_max. - (* GT *) - inv avl. - destruct (IHt H1). - split. - apply bal_avl; auto. - omega_max. - omega_bal. -Qed. - -Lemma remove_avl : forall s x, avl s -> avl (remove x s). -Proof. - intros; generalize (remove_avl_1 s x H); intuition. -Qed. -Hint Resolve remove_avl. +(** * Deletion *) -Lemma remove_in : forall s x y, bst s -> avl s -> +Lemma remove_in : forall s x y, bst s -> (In y (remove x s) <-> ~ X.eq y x /\ In y s). Proof. - intros s x; functional induction (remove x s); subst;simpl; intros. + intros s x; functional induction (remove x s); intros; inv bst. intuition_in. - (* LT *) - inv avl; inv bst; clear e0. - rewrite bal_in; auto. - generalize (IHt y0 H0); intuition; [ order | order | intuition_in ]. - (* EQ *) - inv avl; inv bst; clear e0. - rewrite merge_in; intuition; [ order | order | intuition_in ]. - elim H9; eauto. - (* GT *) - inv avl; inv bst; clear e0. - rewrite bal_in; auto. - generalize (IHt y0 H5); intuition; [ order | order | intuition_in ]. + rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in]. + rewrite merge_in; clear e0; intuition; [order|order|intuition_in]. + elim H4; eauto. + rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in]. Qed. -Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s). +Lemma remove_bst : forall s x, bst s -> bst (remove x s). Proof. - intros s x; functional induction (remove x s); simpl; intros. + intros s x; functional induction (remove x s); intros; inv bst. auto. (* LT *) - inv avl; inv bst. apply bal_bst; auto. - intro; intro. - rewrite (remove_in l x y0) in H; auto. - destruct H; eauto. + intro z; rewrite remove_in; auto; destruct 1; eauto. (* EQ *) - inv avl; inv bst. - apply merge_bst; eauto. + eauto. (* GT *) - inv avl; inv bst. apply bal_bst; auto. - intro; intro. - rewrite (remove_in r x y0) in H; auto. - destruct H; eauto. + intro z; rewrite remove_in; auto; destruct 1; eauto. Qed. +Hint Resolve remove_bst. - (** * Minimum element *) -Function min_elt (s:t) : option elt := match s with - | Leaf => None - | Node Leaf y _ _ => Some y - | Node l _ _ _ => min_elt l -end. +(** * Minimum element *) Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s. Proof. - intro s; functional induction (min_elt s); subst; simpl. - inversion 1. - inversion 1; auto. - intros. - destruct l; auto. + intro s; functional induction (min_elt s); auto; inversion 1; auto. Qed. -Lemma min_elt_2 : forall s x y, bst s -> +Lemma min_elt_2 : forall s x y, bst s -> min_elt s = Some x -> In y s -> ~ X.lt y x. Proof. - intro s; functional induction (min_elt s); subst;simpl. + intro s; functional induction (min_elt s); + try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1. inversion_clear 2. inversion_clear 1. inversion 1; subst. inversion_clear 1; auto. inversion_clear H5. - destruct l;try contradiction. inversion_clear 1. simpl. destruct l1. inversion 1; subst. - assert (X.lt x _x) by (apply H2; auto). + assert (X.lt x y) by (apply H2; auto). inversion_clear 1; auto; order. - assert (X.lt t _x) by auto. + assert (X.lt x1 y) by auto. inversion_clear 2; auto; - (assert (~ X.lt t x) by auto); order. + (assert (~ X.lt x1 x) by auto); order. Qed. Lemma min_elt_3 : forall s, min_elt s = None -> Empty s. Proof. - intro s; functional induction (min_elt s); subst;simpl. - red; auto. + intro s; functional induction (min_elt s). + red; red; inversion 2. inversion 1. - destruct l;try contradiction. - clear y;intro H0. - destruct (IHo H0 t); auto. + intro H0. + destruct (IHo H0 _x2); auto. Qed. -(** * Maximum element *) -Function max_elt (s:t) : option elt := match s with - | Leaf => None - | Node _ y Leaf _ => Some y - | Node _ _ r _ => max_elt r -end. +(** * Maximum element *) Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s. Proof. - intro s; functional induction (max_elt s); subst;simpl. - inversion 1. - inversion 1; auto. - destruct r;try contradiction; auto. + intro s; functional induction (max_elt s); auto; inversion 1; auto. Qed. Lemma max_elt_2 : forall s x y, bst s -> max_elt s = Some x -> In y s -> ~ X.lt x y. Proof. - intro s; functional induction (max_elt s); subst;simpl. + intro s; functional induction (max_elt s); + try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1. inversion_clear 2. inversion_clear 1. inversion 1; subst. inversion_clear 1; auto. inversion_clear H5. - destruct r;try contradiction. inversion_clear 1. -(* inversion 1; subst. *) -(* assert (X.lt y x) by (apply H4; auto). *) -(* inversion_clear 1; auto; order. *) - assert (X.lt _x0 t) by auto. + assert (X.lt y x1) by auto. inversion_clear 2; auto; - (assert (~ X.lt x t) by auto); order. + (assert (~ X.lt x x1) by auto); order. Qed. Lemma max_elt_3 : forall s, max_elt s = None -> Empty s. Proof. - intro s; functional induction (max_elt s); subst;simpl. + intro s; functional induction (max_elt s). red; auto. inversion 1. - destruct r;try contradiction. - intros H0; destruct (IHo H0 t); auto. + intros H0; destruct (IHo H0 _x2); auto. Qed. -(** * Any element *) -Definition choose := min_elt. + +(** * Any element *) Lemma choose_1 : forall s x, choose s = Some x -> In x s. Proof. @@ -1021,353 +1023,215 @@ Proof. exact min_elt_3. Qed. -(** * Concatenation +Lemma choose_3 : forall s s', bst s -> bst s' -> + forall x x', choose s = Some x -> choose s' = Some x' -> + Equal s s' -> X.eq x x'. +Proof. + unfold choose, Equal; intros s s' Hb Hb' x x' Hx Hx' H. + assert (~X.lt x x'). + apply min_elt_2 with s'; auto. + rewrite <-H; auto using min_elt_1. + assert (~X.lt x' x). + apply min_elt_2 with s; auto. + rewrite H; auto using min_elt_1. + destruct (X.compare x x'); intuition. +Qed. - Same as [merge] but does not assume anything about heights. -*) -Function concat (s1 s2 : t) : t := - match s1, s2 with - | Leaf, _ => s2 - | _, Leaf => s1 - | _, Node l2 x2 r2 h2 => - let (s2',m) := remove_min l2 x2 r2 in - join s1 m s2' - end. +(** * Concatenation *) -Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2). +Lemma concat_in : forall s1 s2 y, + In y (concat s1 s2) <-> In y s1 \/ In y s2. Proof. - intros s1 s2; functional induction (concat s1 s2); subst;auto. - destruct s1;try contradiction;clear y. - intros; apply join_avl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite e1; simpl; auto. + intros s1 s2; functional induction (concat s1 s2); intros; + try factornode _x _x0 _x1 _x2 as s1. + intuition_in. + intuition_in. + rewrite join_in, remove_min_in, e1; simpl; intuition. Qed. -Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> +Lemma concat_bst : forall s1 s2, bst s1 -> bst s2 -> (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> bst (concat s1 s2). Proof. - intros s1 s2; functional induction (concat s1 s2); subst ;auto. - destruct s1;try contradiction;clear y. - intros; apply join_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2 H1 H2); rewrite e1; simpl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite e1; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 m H2); rewrite e1; simpl; auto. - destruct 1; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H2); rewrite e1; simpl; auto. -Qed. - -Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> - (In y (concat s1 s2) <-> In y s1 \/ In y s2). -Proof. - intros s1 s2; functional induction (concat s1 s2);subst;simpl. - intuition. - inversion_clear H5. - destruct s1;try contradiction;clear y;intuition. - inversion_clear H5. - destruct s1;try contradiction;clear y; intros. - rewrite (join_in (Node s1_1 t s1_2 i) m s2' y H0). - generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite e1; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y H2); rewrite e1; simpl. - intro EQ; rewrite EQ; intuition. + intros s1 s2; functional induction (concat s1 s2); intros; auto; + try factornode _x _x0 _x1 _x2 as s1. + apply join_bst; auto. + change (bst (s2',m)#1); rewrite <-e1; eauto. + intros y Hy. + apply H1; auto. + rewrite remove_min_in, e1; simpl; auto. + change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto. Qed. +Hint Resolve concat_bst. -(** * 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]. -*) +(** * Splitting *) -Function split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with - | Leaf => (Leaf, (false, Leaf)) - | Node l y r h => - match X.compare x y with - | LT _ => match split x l with - | (ll,(pres,rl)) => (ll, (pres, join rl y r)) - end - | EQ _ => (l, (true, r)) - | GT _ => match split x r with - | (rl,(pres,rr)) => (join l y rl, (pres, rr)) - end - end - end. - -Lemma split_avl : forall s x, avl s -> - avl (fst (split x s)) /\ avl (snd (snd (split x s))). -Proof. - intros s x; functional induction (split x s);subst;simpl in *. - auto. - rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition. - simpl; inversion_clear 1; auto. - rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition. -Qed. - -Lemma split_in_1 : forall s x y, bst s -> avl s -> - (In y (fst (split x s)) <-> In y s /\ X.lt y x). -Proof. - intros s x; functional induction (split x s);subst;simpl in *. - intuition; try inversion_clear H1. - (* LT *) - rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite (IHp y0 H0 H4); clear IHp e0. - intuition. - inversion_clear H6; auto; order. - (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. - intuition. - order. +Lemma split_in_1 : forall s x y, bst s -> + (In y (split x s)#l <-> In y s /\ X.lt y x). +Proof. + intros s x; functional induction (split x s); simpl; intros; + inv bst; try clear e0. + intuition_in. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. intuition_in; order. - (* GT *) - rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite join_in; auto. - generalize (split_avl r x H5); rewrite e1; simpl; intuition. - rewrite (IHp y0 H1 H5); clear e1. - intuition; [ eauto | eauto | intuition_in ]. + rewrite join_in. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma split_in_2 : forall s x y, bst s -> avl s -> - (In y (snd (snd (split x s))) <-> In y s /\ X.lt x y). +Lemma split_in_2 : forall s x y, bst s -> + (In y (split x s)#r <-> In y s /\ X.lt x y). Proof. - intros s x; functional induction (split x s);subst;simpl in *. - intuition; try inversion_clear H1. - (* LT *) - rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite join_in; auto. - generalize (split_avl l x H4); rewrite e1; simpl; intuition. - rewrite (IHp y0 H0 H4); clear IHp e0. - intuition; [ order | order | intuition_in ]. - (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. - intuition; [ order | intuition_in; order ]. - (* GT *) - rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite (IHp y0 H1 H5); clear IHp e0. - intuition; intuition_in; order. + intros s x; functional induction (split x s); subst; simpl; intros; + inv bst; try clear e0. + intuition_in. + rewrite join_in. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. + intuition_in; order. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma split_in_3 : forall s x, bst s -> avl s -> - (fst (snd (split x s)) = true <-> In x s). +Lemma split_in_3 : forall s x, bst s -> + ((split x s)#b = true <-> In x s). Proof. - intros s x; functional induction (split x s);subst;simpl in *. - intuition; try inversion_clear H1. - (* LT *) - rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite IHp; auto. - intuition_in; absurd (X.lt x y); eauto. - (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; intuition. - (* GT *) - rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite IHp; auto. - intuition_in; absurd (X.lt y x); eauto. + intros s x; functional induction (split x s); subst; simpl; intros; + inv bst; try clear e0. + intuition_in; try discriminate. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. + intuition. + rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed. -Lemma split_bst : forall s x, bst s -> avl s -> - bst (fst (split x s)) /\ bst (snd (snd (split x s))). +Lemma split_bst : forall s x, bst s -> + bst (split x s)#l /\ bst (split x s)#r. Proof. - intros s x; functional induction (split x s);subst;simpl in *. - intuition. - (* LT *) - rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. - intuition. - apply join_bst; auto. - generalize (split_avl l x H4); rewrite e1; simpl; intuition. - intro; intro. - generalize (split_in_2 l x y0 H0 H4); rewrite e1; simpl; intuition. - (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; intuition. - (* GT *) - rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. - intuition. - apply join_bst; auto. - generalize (split_avl r x H5); rewrite e1; simpl; intuition. - intro; intro. - generalize (split_in_1 r x y0 H1 H5); rewrite e1; simpl; intuition. + intros s x; functional induction (split x s); subst; simpl; intros; + inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition; + apply join_bst; auto. + intros y0. + generalize (split_in_2 x y0 H0); rewrite e1; simpl; intuition. + intros y0. + generalize (split_in_1 x y0 H1); rewrite e1; simpl; intuition. Qed. -(** * Intersection *) -Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with - | Leaf,_ => Leaf - | _,Leaf => Leaf - | Node l1 x1 r1 h1, _ => - match split x1 s2 with - | (l2',(true,r2')) => join (inter l1 l2') x1 (inter r1 r2') - | (l2',(false,r2')) => concat (inter l1 l2') (inter r1 r2') - end - end. -Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2). -Proof. - (* intros s1 s2; functional induction inter s1 s2; auto. BOF BOF *) - induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. - destruct s2 as [ | l2 x2 r2 h2]; intros; auto. - generalize H0; inv avl. - set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. - destruct (split_avl r x1 H8). - destruct (split x1 r) as [l2' (b,r2')]; simpl in *. - destruct b; [ apply join_avl | apply concat_avl ]; auto. -Qed. +(** * Intersection *) -Lemma inter_bst_in : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> +Lemma inter_bst_in : forall s1 s2, bst s1 -> bst s2 -> bst (inter s1 s2) /\ (forall y, In y (inter s1 s2) <-> In y s1 /\ In y s2). -Proof. - induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. - intuition; inversion_clear H3. - destruct s2 as [ | l2 x2 r2 h2]; intros. - simpl; intuition; inversion_clear H3. - generalize H1 H2; inv avl; inv bst. - set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. - destruct (split_avl r x1 H17). - destruct (split_bst r x1 H16 H17). - split. - (* bst *) - destruct (split x1 r) as [l2' (b,r2')]; simpl in *. - destruct (Hl1 l2'); auto. - destruct (Hr1 r2'); auto. - destruct b. +Proof. + intros s1 s2; functional induction inter s1 s2; intros B1 B2; + [intuition_in|intuition_in | | ]; + factornode _x0 _x1 _x2 _x3 as s2; + generalize (split_bst x1 B2); + rewrite e1; simpl; destruct 1; inv bst; + destruct IHt as (IHb1,IHi1); auto; + destruct IHt0 as (IHb2,IHi2); auto; + generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1) + (split_in_3 x1 B2)(split_bst x1 B2); + rewrite e1; simpl; split; intros. (* bst join *) - apply join_bst; try apply inter_avl; firstorder. - (* bst concat *) - apply concat_bst; try apply inter_avl; auto. - intros; generalize (H22 y1) (H24 y2); intuition eauto. - (* in *) - intros. - destruct (split_in_1 r x1 y H16 H17). - destruct (split_in_2 r x1 y H16 H17). - destruct (split_in_3 r x1 H16 H17). - destruct (split x1 r) as [l2' (b,r2')]; simpl in *. - destruct (Hl1 l2'); auto. - destruct (Hr1 r2'); auto. - destruct b. - (* in join *) - rewrite join_in; try apply inter_avl; auto. - rewrite H30. - rewrite H28. - intuition_in. + apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) + rewrite join_in, IHi1, IHi2, H5, H6; intuition_in. apply In_1 with x1; auto. - (* in concat *) - rewrite concat_in; try apply inter_avl; auto. - intros. - intros; generalize (H28 y1) (H30 y2); intuition eauto. - rewrite H30. - rewrite H28. + (* bst concat *) + apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. + (* In concat *) + rewrite concat_in, IHi1, IHi2, H5, H6; auto. + assert (~In x1 s2) by (rewrite <- H7; auto). intuition_in. - generalize (H26 (In_1 _ _ _ H22 H35)); intro; discriminate. + elim H9. + apply In_1 with y; auto. Qed. -Lemma inter_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - bst (inter s1 s2). +Lemma inter_in : forall s1 s2 y, bst s1 -> bst s2 -> + (In y (inter s1 s2) <-> In y s1 /\ In y s2). Proof. - intros; generalize (inter_bst_in s1 s2); intuition. + intros s1 s2 y B1 B2; destruct (inter_bst_in B1 B2); auto. Qed. -Lemma inter_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - (In y (inter s1 s2) <-> In y s1 /\ In y s2). +Lemma inter_bst : forall s1 s2, bst s1 -> bst s2 -> bst (inter s1 s2). Proof. - intros; generalize (inter_bst_in s1 s2); firstorder. + intros s1 s2 B1 B2; destruct (inter_bst_in B1 B2); auto. Qed. -(** * Difference *) - -Fixpoint diff (s1 s2 : t) { struct s1 } : t := match s1, s2 with - | Leaf, _ => Leaf - | _, Leaf => s1 - | Node l1 x1 r1 h1, _ => - match split x1 s2 with - | (l2',(true,r2')) => concat (diff l1 l2') (diff r1 r2') - | (l2',(false,r2')) => join (diff l1 l2') x1 (diff r1 r2') - end -end. -Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2). -Proof. - (* intros s1 s2; functional induction diff s1 s2; auto. BOF BOF *) - induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. - destruct s2 as [ | l2 x2 r2 h2]; intros; auto. - generalize H0; inv avl. - set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. - destruct (split_avl r x1 H8). - destruct (split x1 r) as [l2' (b,r2')]; simpl in *. - destruct b; [ apply concat_avl | apply join_avl ]; auto. -Qed. +(** * Difference *) -Lemma diff_bst_in : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> +Lemma diff_bst_in : forall s1 s2, bst s1 -> bst s2 -> bst (diff s1 s2) /\ (forall y, In y (diff s1 s2) <-> In y s1 /\ ~In y s2). -Proof. - induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. - intuition; inversion_clear H3. - destruct s2 as [ | l2 x2 r2 h2]; intros; auto. - intuition; inversion_clear H4. - generalize H1 H2; inv avl; inv bst. - set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. - destruct (split_avl r x1 H17). - destruct (split_bst r x1 H16 H17). - split. - (* bst *) - destruct (split x1 r) as [l2' (b,r2')]; simpl in *. - destruct (Hl1 l2'); auto. - destruct (Hr1 r2'); auto. - destruct b. +Proof. + intros s1 s2; functional induction diff s1 s2; intros B1 B2; + [intuition_in|intuition_in | | ]; + factornode _x0 _x1 _x2 _x3 as s2; + generalize (split_bst x1 B2); + rewrite e1; simpl; destruct 1; + inv avl; inv bst; + destruct IHt as (IHb1,IHi1); auto; + destruct IHt0 as (IHb2,IHi2); auto; + generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1) + (split_in_3 x1 B2)(split_bst x1 B2); + rewrite e1; simpl; split; intros. (* bst concat *) - apply concat_bst; try apply diff_avl; auto. - intros; generalize (H22 y1) (H24 y2); intuition eauto. + apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. + (* In concat *) + rewrite concat_in, IHi1, IHi2, H5, H6; intuition_in. + elim H13. + apply In_1 with x1; auto. (* bst join *) - apply join_bst; try apply diff_avl; firstorder. - (* in *) - intros. - destruct (split_in_1 r x1 y H16 H17). - destruct (split_in_2 r x1 y H16 H17). - destruct (split_in_3 r x1 H16 H17). - destruct (split x1 r) as [l2' (b,r2')]; simpl in *. - destruct (Hl1 l2'); auto. - destruct (Hr1 r2'); auto. - destruct b. - (* in concat *) - rewrite concat_in; try apply diff_avl; auto. - intros. - intros; generalize (H28 y1) (H30 y2); intuition eauto. - rewrite H30. - rewrite H28. + apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) + rewrite join_in, IHi1, IHi2, H5, H6; auto. + assert (~In x1 s2) by (rewrite <- H7; auto). intuition_in. - elim H35; apply In_1 with x1; auto. - (* in join *) - rewrite join_in; try apply diff_avl; auto. - rewrite H30. - rewrite H28. - intuition_in. - generalize (H26 (In_1 _ _ _ H34 H24)); intro; discriminate. + elim H9. + apply In_1 with y; auto. Qed. -Lemma diff_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - bst (diff s1 s2). +Lemma diff_in : forall s1 s2 y, bst s1 -> bst s2 -> + (In y (diff s1 s2) <-> In y s1 /\ ~In y s2). Proof. - intros; generalize (diff_bst_in s1 s2); intuition. + intros s1 s2 y B1 B2; destruct (diff_bst_in B1 B2); auto. Qed. -Lemma diff_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - (In y (diff s1 s2) <-> In y s1 /\ ~In y s2). +Lemma diff_bst : forall s1 s2, bst s1 -> bst s2 -> bst (diff s1 s2). Proof. - intros; generalize (diff_bst_in s1 s2); firstorder. + intros s1 s2 B1 B2; destruct (diff_bst_in B1 B2); auto. Qed. -(** * Elements *) -(** [elements_tree_aux acc t] catenates the elements of [t] in infix - order to the list [acc] *) +(** * Union *) -Fixpoint elements_aux (acc : list X.t) (t : tree) {struct t} : list X.t := - match t with - | Leaf => acc - | Node l x r _ => elements_aux (x :: elements_aux acc r) l - end. +Lemma union_in : forall s1 s2 y, bst s1 -> bst s2 -> + (In y (union s1 s2) <-> In y s1 \/ In y s2). +Proof. + intros s1 s2; functional induction union s1 s2; intros y B1 B2. + intuition_in. + intuition_in. + factornode _x0 _x1 _x2 _x3 as s2. + generalize (split_in_1 x1 y B2)(split_in_2 x1 y B2)(split_bst x1 B2). + rewrite e1; simpl. + destruct 3; inv bst. + rewrite join_in, IHt, IHt0, H, H0; auto. + case (X.compare y x1); intuition_in. +Qed. -(** then [elements] is an instanciation with an empty [acc] *) +Lemma union_bst : forall s1 s2, bst s1 -> bst s2 -> + bst (union s1 s2). +Proof. + intros s1 s2; functional induction union s1 s2; intros B1 B2; auto. + factornode _x0 _x1 _x2 _x3 as s2. + generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)(split_bst x1 B2). + rewrite e1; simpl; destruct 3. + inv bst. + apply join_bst; auto. + intro y; rewrite union_in, H; intuition_in. + intro y; rewrite union_in, H0; intuition_in. +Qed. -Definition elements := elements_aux nil. + +(** * Elements *) Lemma elements_aux_in : forall s acc x, InA X.eq x (elements_aux acc s) <-> In x s \/ InA X.eq x acc. @@ -1411,246 +1275,190 @@ Proof. Qed. Hint Resolve elements_sort. -(** * Filter *) - -Section F. -Variable f : elt -> bool. +Lemma elements_nodup : forall s : tree, bst s -> NoDupA X.eq (elements s). +Proof. + auto. +Qed. -Fixpoint filter_acc (acc:t)(s:t) { struct s } : t := match s with - | Leaf => acc - | Node l x r h => - filter_acc (filter_acc (if f x then add x acc else acc) l) r - end. +Lemma elements_aux_cardinal : + forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s). +Proof. + simple induction s; simpl in |- *; intuition. + rewrite <- H. + simpl in |- *. + rewrite <- H0; omega. +Qed. -Definition filter := filter_acc Leaf. +Lemma elements_cardinal : forall s : tree, cardinal s = length (elements s). +Proof. + exact (fun s => elements_aux_cardinal s nil). +Qed. -Lemma filter_acc_avl : forall s acc, avl s -> avl acc -> - avl (filter_acc acc s). +Lemma elements_app : + forall s acc, elements_aux acc s = elements s ++ acc. Proof. - induction s; simpl; auto. - intros. - inv avl. - apply IHs2; auto. - apply IHs1; auto. - destruct (f t); auto. -Qed. -Hint Resolve filter_acc_avl. + induction s; simpl; intros; auto. + rewrite IHs1, IHs2. + unfold elements; simpl. + rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto. +Qed. -Lemma filter_acc_bst : forall s acc, bst s -> avl s -> bst acc -> avl acc -> - bst (filter_acc acc s). +Lemma elements_node : + forall l x r h acc, + elements l ++ x :: elements r ++ acc = + elements (Node l x r h) ++ acc. Proof. - induction s; simpl; auto. - intros. - inv avl; inv bst. - destruct (f t); auto. - apply IHs2; auto. - apply IHs1; auto. - apply add_bst; auto. -Qed. + unfold elements; simpl; intros; auto. + rewrite !elements_app, <- !app_nil_end, !app_ass; auto. +Qed. + -Lemma filter_acc_in : forall s acc, avl s -> avl acc -> +(** * Filter *) + +Section F. +Variable f : elt -> bool. + +Lemma filter_acc_in : forall s acc, compat_bool X.eq f -> forall x : elt, - In x (filter_acc acc s) <-> In x acc \/ In x s /\ f x = true. + In x (filter_acc f acc s) <-> In x acc \/ In x s /\ f x = true. Proof. induction s; simpl; intros. intuition_in. - inv bst; inv avl. - rewrite IHs2; auto. - destruct (f t); auto. - rewrite IHs1; auto. - destruct (f t); auto. + rewrite IHs2, IHs1 by (destruct (f t); auto). case_eq (f t); intros. rewrite (add_in); auto. intuition_in. - rewrite (H1 _ _ H8). + rewrite (H _ _ H2). intuition. intuition_in. - rewrite (H1 _ _ H8) in H9. - rewrite H in H9; discriminate. -Qed. - -Lemma filter_avl : forall s, avl s -> avl (filter s). -Proof. - unfold filter; intros; apply filter_acc_avl; auto. + rewrite (H _ _ H2) in H3. + rewrite H0 in H3; discriminate. Qed. -Lemma filter_bst : forall s, bst s -> avl s -> bst (filter s). +Lemma filter_acc_bst : forall s acc, bst s -> bst acc -> + bst (filter_acc f acc s). Proof. - unfold filter; intros; apply filter_acc_bst; auto. + induction s; simpl; auto. + intros. + inv bst. + destruct (f t); auto. Qed. -Lemma filter_in : forall s, avl s -> +Lemma filter_in : forall s, compat_bool X.eq f -> forall x : elt, - In x (filter s) <-> In x s /\ f x = true. + In x (filter f s) <-> In x s /\ f x = true. Proof. unfold filter; intros; rewrite filter_acc_in; intuition_in. -Qed. - -(** * Partition *) - -Fixpoint partition_acc (acc : t*t)(s : t) { struct s } : t*t := - match s with - | Leaf => acc - | Node l x r _ => - let (acct,accf) := acc in - partition_acc - (partition_acc - (if f x then (add x acct, accf) else (acct, add x accf)) l) r - end. - -Definition partition := partition_acc (Leaf,Leaf). +Qed. -Lemma partition_acc_avl_1 : forall s acc, avl s -> - avl (fst acc) -> avl (fst (partition_acc acc s)). +Lemma filter_bst : forall s, bst s -> bst (filter f s). Proof. - induction s; simpl; auto. - destruct acc as [acct accf]; simpl in *. - intros. - inv avl. - apply IHs2; auto. - apply IHs1; auto. - destruct (f t); simpl; auto. -Qed. + unfold filter; intros; apply filter_acc_bst; auto. +Qed. -Lemma partition_acc_avl_2 : forall s acc, avl s -> - avl (snd acc) -> avl (snd (partition_acc acc s)). -Proof. - induction s; simpl; auto. - destruct acc as [acct accf]; simpl in *. - intros. - inv avl. - apply IHs2; auto. - apply IHs1; auto. - destruct (f t); simpl; auto. -Qed. -Hint Resolve partition_acc_avl_1 partition_acc_avl_2. -Lemma partition_acc_bst_1 : forall s acc, bst s -> avl s -> - bst (fst acc) -> avl (fst acc) -> - bst (fst (partition_acc acc s)). -Proof. - induction s; simpl; auto. - destruct acc as [acct accf]; simpl in *. - intros. - inv avl; inv bst. - destruct (f t); auto. - apply IHs2; simpl; auto. - apply IHs1; simpl; auto. - apply add_bst; auto. - apply partition_acc_avl_1; simpl; auto. -Qed. -Lemma partition_acc_bst_2 : forall s acc, bst s -> avl s -> - bst (snd acc) -> avl (snd acc) -> - bst (snd (partition_acc acc s)). -Proof. - induction s; simpl; auto. - destruct acc as [acct accf]; simpl in *. - intros. - inv avl; inv bst. - destruct (f t); auto. - apply IHs2; simpl; auto. - apply IHs1; simpl; auto. - apply add_bst; auto. - apply partition_acc_avl_2; simpl; auto. -Qed. +(** * Partition *) -Lemma partition_acc_in_1 : forall s acc, avl s -> avl (fst acc) -> +Lemma partition_acc_in_1 : forall s acc, compat_bool X.eq f -> forall x : elt, - In x (fst (partition_acc acc s)) <-> - In x (fst acc) \/ In x s /\ f x = true. + In x (partition_acc f acc s)#1 <-> + In x acc#1 \/ In x s /\ f x = true. Proof. induction s; simpl; intros. intuition_in. destruct acc as [acct accf]; simpl in *. - inv bst; inv avl. - rewrite IHs2; auto. - destruct (f t); auto. - apply partition_acc_avl_1; simpl; auto. - rewrite IHs1; auto. - destruct (f t); simpl; auto. + rewrite IHs2 by + (destruct (f t); auto; apply partition_acc_avl_1; simpl; auto). + rewrite IHs1 by (destruct (f t); simpl; auto). case_eq (f t); simpl; intros. rewrite (add_in); auto. intuition_in. - rewrite (H1 _ _ H8). + rewrite (H _ _ H2). intuition. intuition_in. - rewrite (H1 _ _ H8) in H9. - rewrite H in H9; discriminate. -Qed. + rewrite (H _ _ H2) in H3. + rewrite H0 in H3; discriminate. +Qed. -Lemma partition_acc_in_2 : forall s acc, avl s -> avl (snd acc) -> +Lemma partition_acc_in_2 : forall s acc, compat_bool X.eq f -> forall x : elt, - In x (snd (partition_acc acc s)) <-> - In x (snd acc) \/ In x s /\ f x = false. + In x (partition_acc f acc s)#2 <-> + In x acc#2 \/ In x s /\ f x = false. Proof. induction s; simpl; intros. intuition_in. destruct acc as [acct accf]; simpl in *. - inv bst; inv avl. - rewrite IHs2; auto. - destruct (f t); auto. - apply partition_acc_avl_2; simpl; auto. - rewrite IHs1; auto. - destruct (f t); simpl; auto. + rewrite IHs2 by + (destruct (f t); auto; apply partition_acc_avl_2; simpl; auto). + rewrite IHs1 by (destruct (f t); simpl; auto). case_eq (f t); simpl; intros. intuition. intuition_in. - rewrite (H1 _ _ H8) in H9. - rewrite H in H9; discriminate. + rewrite (H _ _ H2) in H3. + rewrite H0 in H3; discriminate. rewrite (add_in); auto. intuition_in. - rewrite (H1 _ _ H8). + rewrite (H _ _ H2). intuition. +Qed. + +Lemma partition_in_1 : forall s, + compat_bool X.eq f -> forall x : elt, + In x (partition f s)#1 <-> In x s /\ f x = true. +Proof. + unfold partition; intros; rewrite partition_acc_in_1; + simpl in *; intuition_in. Qed. -Lemma partition_avl_1 : forall s, avl s -> avl (fst (partition s)). +Lemma partition_in_2 : forall s, + compat_bool X.eq f -> forall x : elt, + In x (partition f s)#2 <-> In x s /\ f x = false. Proof. - unfold partition; intros; apply partition_acc_avl_1; auto. + unfold partition; intros; rewrite partition_acc_in_2; + simpl in *; intuition_in. +Qed. + +Lemma partition_acc_bst_1 : forall s acc, bst s -> bst acc#1 -> + bst (partition_acc f acc s)#1. +Proof. + induction s; simpl; auto. + destruct acc as [acct accf]; simpl in *. + intros. + inv bst. + destruct (f t); auto. + apply IHs2; simpl; auto. + apply IHs1; simpl; auto. Qed. -Lemma partition_avl_2 : forall s, avl s -> avl (snd (partition s)). +Lemma partition_acc_bst_2 : forall s acc, bst s -> bst acc#2 -> + bst (partition_acc f acc s)#2. Proof. - unfold partition; intros; apply partition_acc_avl_2; auto. + induction s; simpl; auto. + destruct acc as [acct accf]; simpl in *. + intros. + inv bst. + destruct (f t); auto. + apply IHs2; simpl; auto. + apply IHs1; simpl; auto. Qed. -Lemma partition_bst_1 : forall s, bst s -> avl s -> - bst (fst (partition s)). +Lemma partition_bst_1 : forall s, bst s -> bst (partition f s)#1. Proof. unfold partition; intros; apply partition_acc_bst_1; auto. Qed. -Lemma partition_bst_2 : forall s, bst s -> avl s -> - bst (snd (partition s)). +Lemma partition_bst_2 : forall s, bst s -> bst (partition f s)#2. Proof. unfold partition; intros; apply partition_acc_bst_2; auto. Qed. -Lemma partition_in_1 : forall s, avl s -> - compat_bool X.eq f -> forall x : elt, - In x (fst (partition s)) <-> In x s /\ f x = true. -Proof. - unfold partition; intros; rewrite partition_acc_in_1; - simpl in *; intuition_in. -Qed. - -Lemma partition_in_2 : forall s, avl s -> - compat_bool X.eq f -> forall x : elt, - In x (snd (partition s)) <-> In x s /\ f x = false. -Proof. - unfold partition; intros; rewrite partition_acc_in_2; - simpl in *; intuition_in. -Qed. -(** [for_all] and [exists] *) -Fixpoint for_all (s:t) : bool := match s with - | Leaf => true - | Node l x r _ => f x && for_all l && for_all r -end. +(** * [for_all] and [exists] *) -Lemma for_all_1 : forall s, compat_bool E.eq f -> - For_all (fun x => f x = true) s -> for_all s = true. +Lemma for_all_1 : forall s, compat_bool X.eq f -> + For_all (fun x => f x = true) s -> for_all f s = true. Proof. induction s; simpl; auto. intros. @@ -1660,8 +1468,8 @@ Proof. destruct (f t); simpl; auto. Qed. -Lemma for_all_2 : forall s, compat_bool E.eq f -> - for_all s = true -> For_all (fun x => f x = true) s. +Lemma for_all_2 : forall s, compat_bool X.eq f -> + for_all f s = true -> For_all (fun x => f x = true) s. Proof. induction s; simpl; auto; intros; red; intros; inv In. destruct (andb_prop _ _ H0); auto. @@ -1673,52 +1481,40 @@ Proof. destruct (andb_prop _ _ H0); auto. Qed. -Fixpoint exists_ (s:t) : bool := match s with - | Leaf => false - | Node l x r _ => f x || exists_ l || exists_ r -end. - -Lemma exists_1 : forall s, compat_bool E.eq f -> - Exists (fun x => f x = true) s -> exists_ s = true. +Lemma exists_1 : forall s, compat_bool X.eq f -> + Exists (fun x => f x = true) s -> exists_ f s = true. Proof. - induction s; simpl; destruct 2 as (x,(U,V)); inv In. + induction s; simpl; destruct 2 as (x,(U,V)); inv In; rewrite <- ?orb_lazy_alt. rewrite (H _ _ (X.eq_sym H0)); rewrite V; auto. apply orb_true_intro; left. - apply orb_true_intro; right; apply IHs1; firstorder. - apply orb_true_intro; right; apply IHs2; firstorder. + apply orb_true_intro; right; apply IHs1; auto; exists x; auto. + apply orb_true_intro; right; apply IHs2; auto; exists x; auto. Qed. -Lemma exists_2 : forall s, compat_bool E.eq f -> - exists_ s = true -> Exists (fun x => f x = true) s. +Lemma exists_2 : forall s, compat_bool X.eq f -> + exists_ f s = true -> Exists (fun x => f x = true) s. Proof. - induction s; simpl; intros. + induction s; simpl; intros; rewrite <- ?orb_lazy_alt in *. discriminate. destruct (orb_true_elim _ _ H0) as [H1|H1]. destruct (orb_true_elim _ _ H1) as [H2|H2]. exists t; auto. - destruct (IHs1 H H2); firstorder. - destruct (IHs2 H H1); firstorder. -Qed. + destruct (IHs1 H H2); auto; exists x; intuition. + destruct (IHs2 H H1); auto; exists x; intuition. +Qed. End F. -(** * Fold *) -Module L := FSetList.Raw X. -Fixpoint fold (A : Set) (f : elt -> A -> A)(s : tree) {struct s} : A -> A := - fun a => match s with - | Leaf => a - | Node l x r _ => fold A f r (f x (fold A f l a)) - end. -Implicit Arguments fold [A]. +(** * Fold *) -Definition fold' (A : Set) (f : elt -> A -> A)(s : tree) := +Definition fold' (A : Type) (f : elt -> A -> A)(s : tree) := L.fold f (elements s). Implicit Arguments fold' [A]. Lemma fold_equiv_aux : - forall (A : Set) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt), + forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt), L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a). Proof. simple induction s. @@ -1730,7 +1526,7 @@ Proof. Qed. Lemma fold_equiv : - forall (A : Set) (s : tree) (f : elt -> A -> A) (a : A), + forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A), fold f s a = fold' f s a. Proof. unfold fold', elements in |- *. @@ -1741,7 +1537,7 @@ Proof. Qed. Lemma fold_1 : - forall (s:t)(Hs:bst s)(A : Set)(f : elt -> A -> A)(i : A), + forall (s:t)(Hs:bst s)(A : Type)(f : elt -> A -> A)(i : A), fold f s i = fold_left (fun a e => f e a) (elements s) i. Proof. intros. @@ -1752,416 +1548,168 @@ Proof. apply elements_sort; auto. Qed. -(** * Cardinal *) - -Fixpoint cardinal (s : tree) : nat := - match s with - | Leaf => 0%nat - | Node l _ r _ => S (cardinal l + cardinal r) - end. +(** * Subset *) -Lemma cardinal_elements_aux_1 : - forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s). +Lemma subsetl_12 : forall subset_l1 l1 x1 h1 s2, + bst (Node l1 x1 Leaf h1) -> bst s2 -> + (forall s, bst s -> (subset_l1 s = true <-> Subset l1 s)) -> + (subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ). Proof. - simple induction s; simpl in |- *; intuition. - rewrite <- H. - simpl in |- *. - rewrite <- H0; omega. -Qed. + induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros. + unfold Subset; intuition; try discriminate. + assert (H': In x1 Leaf) by auto; inversion H'. + inversion_clear H0. + specialize (IHl2 H H2 H1). + specialize (IHr2 H H3 H1). + inv bst. clear H8. + destruct X.compare. + + rewrite IHl2; clear H1 IHl2 IHr2. + unfold Subset. intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. -Lemma cardinal_elements_1 : forall s : tree, cardinal s = length (elements s). -Proof. - exact (fun s => cardinal_elements_aux_1 s nil). -Qed. + rewrite H1 by auto; clear H1 IHl2 IHr2. + unfold Subset. intuition_in. + assert (X.eq a x2) by order; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. -(** NB: the remaining functions (union, subset, compare) are still defined - in a dependent style, due to the use of well-founded induction. *) + rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2. + unfold Subset. intuition_in. + assert (H':=mem_2 H6); apply In_1 with x1; auto. + apply mem_1; auto. + assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order. +Qed. -(** Induction over cardinals *) -Lemma sorted_subset_cardinal : forall l' l : list X.t, - sort X.lt l -> sort X.lt l' -> - (forall x : elt, InA X.eq x l -> InA X.eq x l') -> (length l <= length l')%nat. +Lemma subsetr_12 : 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). Proof. - simple induction l'; simpl in |- *; intuition. - destruct l; trivial; intros. - absurd (InA X.eq t nil); intuition. - inversion_clear H2. - inversion_clear H1. - destruct l0; simpl in |- *; intuition. + induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros. + unfold Subset; intuition; try discriminate. + assert (H': In x1 Leaf) by auto; inversion H'. inversion_clear H0. - apply le_n_S. - case (X.compare t a); intro. - absurd (InA X.eq t (a :: l)). - intro. - inversion_clear H0. - order. - assert (X.lt a t). - apply MX.Sort_Inf_In with l; auto. - order. - firstorder. - apply H; auto. - intros. - assert (InA X.eq x (a :: l)). - apply H2; auto. - inversion_clear H6; auto. - assert (X.lt t x). - apply MX.Sort_Inf_In with l0; auto. - order. - apply le_trans with (length (t :: l0)). - simpl in |- *; omega. - apply (H (t :: l0)); auto. - intros. - assert (InA X.eq x (a :: l)); firstorder. - inversion_clear H6; auto. - assert (X.lt a x). - apply MX.Sort_Inf_In with (t :: l0); auto. - elim (X.lt_not_eq (x:=a) (y:=x)); auto. -Qed. - -Lemma cardinal_subset : forall a b : tree, bst a -> bst b -> - (forall y : elt, In y a -> In y b) -> - (cardinal a <= cardinal b)%nat. -Proof. - intros. - do 2 rewrite cardinal_elements_1. - apply sorted_subset_cardinal; auto. - intros. - generalize (elements_in a x) (elements_in b x). - intuition. + specialize (IHl2 H H2 H1). + specialize (IHr2 H H3 H1). + inv bst. clear H7. + destruct X.compare. + + rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2. + unfold Subset. intuition_in. + assert (H':=mem_2 H1); apply In_1 with x1; auto. + apply mem_1; auto. + assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order. + + rewrite H1 by auto; clear H1 IHl2 IHr2. + unfold Subset. intuition_in. + assert (X.eq a x2) by order; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + + rewrite IHr2; clear H1 IHl2 IHr2. + unfold Subset. intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. Qed. -Lemma cardinal_left : forall (l r : tree) (x : elt) (h : int), - (cardinal l < cardinal (Node l x r h))%nat. -Proof. - simpl in |- *; intuition. -Qed. -Lemma cardinal_right : - forall (l r : tree) (x : elt) (h : int), - (cardinal r < cardinal (Node l x r h))%nat. +Lemma subset_12 : forall s1 s2, bst s1 -> bst s2 -> + (subset s1 s2 = true <-> Subset s1 s2). Proof. - simpl in |- *; intuition. -Qed. + induction s1 as [|l1 IHl1 x1 r1 IHr1 h1]; simpl; intros. + unfold Subset; intuition_in. + destruct s2 as [|l2 x2 r2 h2]; simpl; intros. + unfold Subset; intuition_in; try discriminate. + assert (H': In x1 Leaf) by auto; inversion H'. + inv bst. + destruct X.compare. + + rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto. + rewrite (@subsetl_12 (subset l1) l1 x1 h1) by auto. + clear IHl1 IHr1. + unfold Subset; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + + rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto. + clear IHl1 IHr1. + unfold Subset; intuition_in. + assert (X.eq a x2) by order; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + + rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto. + rewrite (@subsetr_12 (subset r1) r1 x1 h1) by auto. + clear IHl1 IHr1. + unfold Subset; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. +Qed. -Lemma cardinal_rec2 : forall P : tree -> tree -> Set, - (forall s1 s2 : tree, - (forall t1 t2 : tree, - (cardinal t1 + cardinal t2 < cardinal s1 + cardinal s2)%nat -> P t1 t2) - -> P s1 s2) -> - forall s1 s2 : tree, P s1 s2. -Proof. - intros P H s1 s2. - apply well_founded_induction_type_2 - with (R := fun yy' xx' : tree * tree => - (cardinal (fst yy') + cardinal (snd yy') < - cardinal (fst xx') + cardinal (snd xx'))%nat); auto. - apply (Wf_nat.well_founded_ltof _ - (fun xx' : tree * tree => (cardinal (fst xx') + cardinal (snd xx'))%nat)). -Qed. - -Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf. -Proof. - destruct 1; intuition; simpl in *. - avl_nns; simpl in *; false_omega_max. -Qed. - -(** * Union - - [union s1 s2] does an induction over the sum of the cardinals of - [s1] and [s2]. Code is -<< - let rec union s1 s2 = - match (s1, s2) with - (Empty, t2) -> t2 - | (t1, Empty) -> t1 - | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> - if h1 >= h2 then - if h2 = 1 then add v2 s1 else begin - let (l2', _, r2') = split v1 s2 in - join (union l1 l2') v1 (union r1 r2') - end - else - if h1 = 1 then add v1 s2 else begin - let (l1', _, r1') = split v2 s1 in - join (union l1' l2) v2 (union r1' r2) - end ->> -*) -Definition union : - forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> - {s' : t | bst s' /\ avl s' /\ forall x : elt, In x s' <-> In x s1 \/ In x s2}. -Proof. - intros s1 s2; pattern s1, s2; apply cardinal_rec2; clear s1 s2. - destruct s1 as [| l1 x1 r1 h1]; intros. - (* s = Leaf *) - clear H. - exists s2; intuition_in. - (* s1 = Node l1 x1 r1 *) - destruct s2 as [| l2 x2 r2 h2]; simpl in |- *. - (* s2 = Leaf *) - clear H. - exists (Node l1 x1 r1 h1); simpl; intuition_in. - (* x' = Node l2 x2 r2 *) - case (ge_lt_dec h1 h2); intro. - (* h1 >= h2 *) - case (eq_dec h2 1); intro. - (* h2 = 1 *) - clear H. - exists (add x2 (Node l1 x1 r1 h1)); auto. - inv avl; inv bst. - avl_nn l2; avl_nn r2. - rewrite (height_0 _ H); [ | omega_max]. - rewrite (height_0 _ H4); [ | omega_max]. - split; [apply add_bst; auto|]. - split; [apply add_avl; auto|]. - intros. - rewrite (add_in (Node l1 x1 r1 h1) x2 x); intuition_in. - (* h2 <> 1 *) - (* split x1 s2 = l2',_,r2' *) - case_eq (split x1 (Node l2 x2 r2 h2)); intros l2' (b,r2') EqSplit. - set (s2 := Node l2 x2 r2 h2) in *; clearbody s2. - generalize (split_avl s2 x1 H3); rewrite EqSplit; simpl in *; intros (A,B). - generalize (split_bst s2 x1 H2 H3); rewrite EqSplit; simpl in *; intros (C,D). - generalize (split_in_1 s2 x1); rewrite EqSplit; simpl in *; intros. - generalize (split_in_2 s2 x1); rewrite EqSplit; simpl in *; intros. - (* union l1 l2' = l0 *) - destruct (H l1 l2') as [l0 (H7,(H8,H9))]; inv avl; inv bst; auto. - assert (cardinal l2' <= cardinal s2)%nat. - apply cardinal_subset; trivial. - intros y; rewrite (H4 y); intuition. - omega. - (* union r1 r2' = r0 *) - destruct (H r1 r2') as [r0 (H10,(H11,H12))]; inv avl; inv bst; auto. - assert (cardinal r2' <= cardinal s2)%nat. - apply cardinal_subset; trivial. - intros y; rewrite (H5 y); intuition. - omega. - exists (join l0 x1 r0). - inv avl; inv bst; clear H. - split. - apply join_bst; auto. - red; intros. - rewrite (H9 y) in H. - destruct H; auto. - rewrite (H4 y) in H; intuition. - red; intros. - rewrite (H12 y) in H. - destruct H; auto. - rewrite (H5 y) in H; intuition. - split. - apply join_avl; auto. - intros. - rewrite join_in; auto. - rewrite H9. - rewrite H12. - rewrite H4; auto. - rewrite H5; auto. - intuition_in. - case (X.compare x x1); intuition. - (* h1 < h2 *) - case (eq_dec h1 1); intro. - (* h1 = 1 *) - exists (add x1 (Node l2 x2 r2 h2)); auto. - inv avl; inv bst. - avl_nn l1; avl_nn r1. - rewrite (height_0 _ H3); [ | omega_max]. - rewrite (height_0 _ H8); [ | omega_max]. - split; [apply add_bst; auto|]. - split; [apply add_avl; auto|]. - intros. - rewrite (add_in (Node l2 x2 r2 h2) x1 x); intuition_in. - (* h1 <> 1 *) - (* split x2 s1 = l1',_,r1' *) - case_eq (split x2 (Node l1 x1 r1 h1)); intros l1' (b,r1') EqSplit. - set (s1 := Node l1 x1 r1 h1) in *; clearbody s1. - generalize (split_avl s1 x2 H1); rewrite EqSplit; simpl in *; intros (A,B). - generalize (split_bst s1 x2 H0 H1); rewrite EqSplit; simpl in *; intros (C,D). - generalize (split_in_1 s1 x2); rewrite EqSplit; simpl in *; intros. - generalize (split_in_2 s1 x2); rewrite EqSplit; simpl in *; intros. - (* union l1' l2 = l0 *) - destruct (H l1' l2) as [l0 (H7,(H8,H9))]; inv avl; inv bst; auto. - assert (cardinal l1' <= cardinal s1)%nat. - apply cardinal_subset; trivial. - intros y; rewrite (H4 y); intuition. - omega. - (* union r1' r2 = r0 *) - destruct (H r1' r2) as [r0 (H10,(H11,H12))]; inv avl; inv bst; auto. - assert (cardinal r1' <= cardinal s1)%nat. - apply cardinal_subset; trivial. - intros y; rewrite (H5 y); intuition. - omega. - exists (join l0 x2 r0). - inv avl; inv bst; clear H. - split. - apply join_bst; auto. - red; intros. - rewrite (H9 y) in H. - destruct H; auto. - rewrite (H4 y) in H; intuition. - red; intros. - rewrite (H12 y) in H. - destruct H; auto. - rewrite (H5 y) in H; intuition. - split. - apply join_avl; auto. - intros. - rewrite join_in; auto. - rewrite H9. - rewrite H12. - rewrite H4; auto. - rewrite H5; auto. - intuition_in. - case (X.compare x x2); intuition. -Qed. - - -(** * Subset -<< - let rec subset s1 s2 = - match (s1, s2) with - Empty, _ -> true - | _, Empty -> false - | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> - let c = Ord.compare v1 v2 in - if c = 0 then - subset l1 l2 && subset r1 r2 - else if c < 0 then - subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 - else - subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2 ->> -*) - -Definition subset : forall s1 s2 : t, bst s1 -> bst s2 -> - {Subset s1 s2} + {~ Subset s1 s2}. -Proof. - intros s1 s2; pattern s1, s2; apply cardinal_rec2; clear s1 s2. - destruct s1 as [| l1 x1 r1 h1]; intros. - (* s1 = Leaf *) - left; red; intros; inv In. - (* s1 = Node l1 x1 r1 h1 *) - destruct s2 as [| l2 x2 r2 h2]. - (* s2 = Leaf *) - right; intros; intro. - assert (In x1 Leaf); auto. - inversion_clear H3. - (* s2 = Node l2 x2 r2 h2 *) - case (X.compare x1 x2); intro. - (* x1 < x2 *) - case (H (Node l1 x1 Leaf 0) l2); inv bst; auto; intros. - simpl in |- *; omega. - case (H r1 (Node l2 x2 r2 h2)); inv bst; auto; intros. - simpl in |- *; omega. - clear H; left; red; intuition. - generalize (s a) (s0 a); clear s s0; intuition_in. - clear H; right; red; firstorder. - clear H; right; red; inv bst; intuition. - apply n; red; intros. - assert (In a (Node l2 x2 r2 h2)) by (inv In; auto). - intuition_in; order. - (* x1 = x2 *) - case (H l1 l2); inv bst; auto; intros. - simpl in |- *; omega. - case (H r1 r2); inv bst; auto; intros. - simpl in |- *; omega. - clear H; left; red; intuition_in; eauto. - clear H; right; red; inv bst; intuition. - apply n; red; intros. - assert (In a (Node l2 x2 r2 h2)) by auto. - intuition_in; order. - clear H; right; red; inv bst; intuition. - apply n; red; intros. - assert (In a (Node l2 x2 r2 h2)) by auto. - intuition_in; order. - (* x1 > x2 *) - case (H (Node Leaf x1 r1 0) r2); inv bst; auto; intros. - simpl in |- *; omega. - intros; case (H l1 (Node l2 x2 r2 h2)); inv bst; auto; intros. - simpl in |- *; omega. - clear H; left; red; intuition. - generalize (s a) (s0 a); clear s s0; intuition_in. - clear H; right; red; firstorder. - clear H; right; red; inv bst; intuition. - apply n; red; intros. - assert (In a (Node l2 x2 r2 h2)) by (inv In; auto). - intuition_in; order. -Qed. (** * Comparison *) (** ** Relations [eq] and [lt] over trees *) -Definition eq : t -> t -> Prop := Equal. +Definition eq := Equal. +Definition lt (s1 s2 : t) : Prop := L.lt (elements s1) (elements s2). -Lemma eq_refl : forall s : t, eq s s. +Lemma eq_refl : forall s : t, Equal s s. Proof. - unfold eq, Equal in |- *; intuition. + unfold Equal; intuition. Qed. -Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s. +Lemma eq_sym : forall s s' : t, Equal s s' -> Equal s' s. Proof. - unfold eq, Equal in |- *; firstorder. + unfold Equal; intros s s' H x; destruct (H x); split; auto. Qed. -Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''. +Lemma eq_trans : forall s s' s'' : t, + Equal s s' -> Equal s' s'' -> Equal s s''. Proof. - unfold eq, Equal in |- *; firstorder. + unfold Equal; intros s s' s'' H1 H2 x; + destruct (H1 x); destruct (H2 x); split; auto. Qed. Lemma eq_L_eq : - forall s s' : t, eq s s' -> L.eq (elements s) (elements s'). + forall s s' : t, Equal s s' -> L.eq (elements s) (elements s'). Proof. - unfold eq, Equal, L.eq, L.Equal in |- *; intros. - generalize (elements_in s a) (elements_in s' a). - firstorder. + unfold Equal, L.eq, L.Equal; intros; do 2 rewrite elements_in; auto. Qed. Lemma L_eq_eq : - forall s s' : t, L.eq (elements s) (elements s') -> eq s s'. + forall s s' : t, L.eq (elements s) (elements s') -> Equal s s'. Proof. - unfold eq, Equal, L.eq, L.Equal in |- *; intros. - generalize (elements_in s a) (elements_in s' a). - firstorder. + unfold Equal, L.eq, L.Equal; intros; do 2 rewrite <-elements_in; auto. Qed. Hint Resolve eq_L_eq L_eq_eq. -Definition lt (s1 s2 : t) : Prop := L.lt (elements s1) (elements s2). - Definition lt_trans (s s' s'' : t) (h : lt s s') (h' : lt s' s'') : lt s s'' := L.lt_trans h h'. -Lemma lt_not_eq : forall s s' : t, bst s -> bst s' -> lt s s' -> ~ eq s s'. +Lemma lt_not_eq : forall s s' : t, + bst s -> bst s' -> lt s s' -> ~ Equal s s'. Proof. unfold lt in |- *; intros; intro. apply L.lt_not_eq with (s := elements s) (s' := elements s'); auto. Qed. -(** A new comparison algorithm suggested by Xavier Leroy: - -type enumeration = End | More of elt * t * enumeration - -let rec cons s e = match s with - | Empty -> e - | Node(l, v, r, _) -> cons l (More(v, r, e)) - -let rec compare_aux e1 e2 = match (e1, e2) with - | (End, End) -> 0 - | (End, More _) -> -1 - | (More _, End) -> 1 - | (More(v1, r1, k1), More(v2, r2, k2)) -> - let c = Ord.compare v1 v2 in - if c <> 0 then c else compare_aux (cons r1 k1) (cons r2 k2) - -let compare s1 s2 = compare_aux (cons s1 End) (cons s2 End) -*) +Lemma L_eq_cons : + forall (l1 l2 : list elt) (x y : elt), + X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2). +Proof. + unfold L.eq, L.Equal in |- *; intuition. + inversion_clear H1; generalize (H0 a); clear H0; intuition. + apply InA_eqA with x; eauto. + inversion_clear H1; generalize (H0 a); clear H0; intuition. + apply InA_eqA with y; eauto. +Qed. +Hint Resolve L_eq_cons. -(** ** Enumeration of the elements of a tree *) -Inductive enumeration : Set := - | End : enumeration - | More : elt -> tree -> enumeration -> enumeration. +(** * A new comparison algorithm suggested by Xavier Leroy *) (** [flatten_e e] returns the list of elements of [e] i.e. the list of elements actually compared *) @@ -2171,462 +1719,166 @@ Fixpoint flatten_e (e : enumeration) : list elt := match e with | More x t r => x :: elements t ++ flatten_e r end. -(** [sorted_e e] expresses that elements in the enumeration [e] are - sorted, and that all trees in [e] are binary search trees. *) - -Inductive In_e (x:elt) : enumeration -> Prop := - | InEHd1 : - forall (y : elt) (s : tree) (e : enumeration), - X.eq x y -> In_e x (More y s e) - | InEHd2 : - forall (y : elt) (s : tree) (e : enumeration), - In x s -> In_e x (More y s e) - | InETl : - forall (y : elt) (s : tree) (e : enumeration), - In_e x e -> In_e x (More y s e). - -Hint Constructors In_e. - -Inductive sorted_e : enumeration -> Prop := - | SortedEEnd : sorted_e End - | SortedEMore : - forall (x : elt) (s : tree) (e : enumeration), - bst s -> - (gt_tree x s) -> - sorted_e e -> - (forall y : elt, In_e y e -> X.lt x y) -> - (forall y : elt, - In y s -> forall z : elt, In_e z e -> X.lt y z) -> - sorted_e (More x s e). - -Hint Constructors sorted_e. - -Lemma in_app : - forall (x : elt) (l1 l2 : list elt), - InA X.eq x (l1 ++ l2) -> InA X.eq x l1 \/ InA X.eq x l2. -Proof. - simple induction l1; simpl in |- *; intuition. - inversion_clear H0; auto. - elim (H l2 H1); auto. -Qed. - -Lemma in_flatten_e : - forall (x : elt) (e : enumeration), InA X.eq x (flatten_e e) -> In_e x e. -Proof. - simple induction e; simpl in |- *; intuition. - inversion_clear H. - inversion_clear H0; auto. - elim (in_app x _ _ H1); auto. - destruct (elements_in t x); auto. -Qed. - -Lemma sort_app : - forall l1 l2 : list elt, sort X.lt l1 -> sort X.lt l2 -> - (forall x y : elt, InA X.eq x l1 -> InA X.eq y l2 -> X.lt x y) -> - sort X.lt (l1 ++ l2). -Proof. - simple induction l1; simpl in |- *; intuition. - apply cons_sort; auto. - apply H; auto. - inversion_clear H0; trivial. - induction l as [| a0 l Hrecl]; simpl in |- *; intuition. - induction l2 as [| a0 l2 Hrecl2]; simpl in |- *; intuition. - inversion_clear H0; inversion_clear H4; auto. -Qed. - -Lemma sorted_flatten_e : - forall e : enumeration, sorted_e e -> sort X.lt (flatten_e e). -Proof. - simple induction e; simpl in |- *; intuition. - apply cons_sort. - apply sort_app; inversion H0; auto. - intros; apply H8; auto. - destruct (elements_in t x0); auto. - apply in_flatten_e; auto. - apply L.MX.ListIn_Inf. - inversion_clear H0. - intros; elim (in_app_or _ _ _ H0); intuition. - destruct (elements_in t y); auto. - apply H4; apply in_flatten_e; auto. -Qed. - -Lemma elements_app : - forall (s : tree) (acc : list elt), elements_aux acc s = elements s ++ acc. -Proof. - simple induction s; simpl in |- *; intuition. - rewrite H0. - rewrite H. - unfold elements; simpl. - do 2 rewrite H. - rewrite H0. - repeat rewrite <- app_nil_end. - repeat rewrite app_ass; auto. -Qed. - -Lemma compare_flatten_1 : - forall (t0 t2 : tree) (t1 : elt) (z : int) (l : list elt), - elements t0 ++ t1 :: elements t2 ++ l = - elements (Node t0 t1 t2 z) ++ l. +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. Proof. - simpl in |- *; unfold elements in |- *; simpl in |- *; intuition. - repeat rewrite elements_app. - repeat rewrite <- app_nil_end. - repeat rewrite app_ass; auto. + intros; simpl; apply elements_node. Qed. -(** key lemma for correctness *) - -Lemma flatten_e_elements : - forall (x : elt) (l r : tree) (z : int) (e : enumeration), - elements l ++ flatten_e (More x r e) = elements (Node l x r z) ++ flatten_e e. +Lemma cons_1 : forall s e, + flatten_e (cons s e) = elements s ++ flatten_e e. Proof. - intros; simpl. - apply compare_flatten_1. + induction s; simpl; auto; intros. + rewrite IHs1; apply flatten_e_elements. Qed. -(** termination of [compare_aux] *) +(** Correctness of this comparison *) -Open Local Scope Z_scope. - -Fixpoint measure_e_t (s : tree) : Z := match s with - | Leaf => 0 - | Node l _ r _ => 1 + measure_e_t l + measure_e_t r - end. - -Fixpoint measure_e (e : enumeration) : Z := match e with - | End => 0 - | More _ s r => 1 + measure_e_t s + measure_e r +Definition Cmp c := + match c with + | Eq => L.eq + | Lt => L.lt + | Gt => (fun l1 l2 => L.lt l2 l1) end. -Ltac Measure_e_t := unfold measure_e_t in |- *; fold measure_e_t in |- *. -Ltac Measure_e := unfold measure_e in |- *; fold measure_e in |- *. - -Lemma measure_e_t_0 : forall s : tree, measure_e_t s >= 0. +Lemma cons_Cmp : forall c x1 x2 l1 l2, X.eq x1 x2 -> + Cmp c l1 l2 -> Cmp c (x1::l1) (x2::l2). Proof. - simple induction s. - simpl in |- *; omega. - intros. - Measure_e_t; omega. (* BUG Simpl! *) + destruct c; simpl; auto. Qed. +Hint Resolve cons_Cmp. -Ltac Measure_e_t_0 s := generalize (measure_e_t_0 s); intro. - -Lemma measure_e_0 : forall e : enumeration, measure_e e >= 0. +Lemma compare_end_Cmp : + forall e2, Cmp (compare_end e2) nil (flatten_e e2). Proof. - simple induction e. - simpl in |- *; omega. - intros. - Measure_e; Measure_e_t_0 t; omega. + destruct e2; simpl; auto. + apply L.eq_refl. Qed. -Ltac Measure_e_0 e := generalize (measure_e_0 e); intro. - -(** Induction principle over the sum of the measures for two lists *) - -Definition compare_rec2 : - forall P : enumeration -> enumeration -> Set, - (forall x x' : enumeration, - (forall y y' : enumeration, - measure_e y + measure_e y' < measure_e x + measure_e x' -> P y y') -> - P x x') -> - forall x x' : enumeration, P x x'. +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)). Proof. - intros P H x x'. - apply well_founded_induction_type_2 - with (R := fun yy' xx' : enumeration * enumeration => - measure_e (fst yy') + measure_e (snd yy') < - measure_e (fst xx') + measure_e (snd xx')); auto. - apply Wf_nat.well_founded_lt_compat - with (f := fun xx' : enumeration * enumeration => - Zabs_nat (measure_e (fst xx') + measure_e (snd xx'))). - intros; apply Zabs.Zabs_nat_lt. - Measure_e_0 (fst x0); Measure_e_0 (snd x0); Measure_e_0 (fst y); - Measure_e_0 (snd y); intros; omega. -Qed. - -(** [cons t e] adds the elements of tree [t] on the head of - enumeration [e]. Code: - -let rec cons s e = match s with - | Empty -> e - | Node(l, v, r, _) -> cons l (More(v, r, e)) -*) - -Definition cons : forall (s : tree) (e : enumeration), bst s -> sorted_e e -> - (forall (x y : elt), In x s -> In_e y e -> X.lt x y) -> - { r : enumeration - | sorted_e r /\ - measure_e r = measure_e_t s + measure_e e /\ - flatten_e r = elements s ++ flatten_e e - }. -Proof. - simple induction s; intuition. - (* s = Leaf *) - exists e; intuition. - (* s = Node t t0 t1 z *) - clear H0. - case (H (More t0 t1 e)); clear H; intuition. - inv bst; auto. - constructor; inversion_clear H1; auto. - inversion_clear H0; inv bst; intuition; order. - exists x; intuition. - generalize H4; Measure_e; intros; Measure_e_t; omega. - rewrite H5. - apply flatten_e_elements. + simpl; intros; destruct X.compare; simpl; auto. Qed. -Lemma l_eq_cons : - forall (l1 l2 : list elt) (x y : elt), - X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2). +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). Proof. - unfold L.eq, L.Equal in |- *; intuition. - inversion_clear H1; generalize (H0 a); clear H0; intuition. - apply InA_eqA with x; eauto. - inversion_clear H1; generalize (H0 a); clear H0; intuition. - apply InA_eqA with y; eauto. + induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto. + rewrite <- elements_node; simpl. + apply Hl1; auto. clear e2. intros [|x2 r2 e2]. + simpl; auto. + apply compare_more_Cmp. + rewrite <- cons_1; auto. Qed. -Definition compare_aux : - forall e1 e2 : enumeration, sorted_e e1 -> sorted_e e2 -> - Compare L.lt L.eq (flatten_e e1) (flatten_e e2). -Proof. - intros e1 e2; pattern e1, e2 in |- *; apply compare_rec2. - simple destruct x; simple destruct x'; intuition. - (* x = x' = End *) - constructor 2; unfold L.eq, L.Equal in |- *; intuition. - (* x = End x' = More *) - constructor 1; simpl in |- *; auto. - (* x = More x' = End *) - constructor 3; simpl in |- *; auto. - (* x = More e t e0, x' = More e3 t0 e4 *) - case (X.compare e e3); intro. - (* e < e3 *) - constructor 1; simpl; auto. - (* e = e3 *) - destruct (cons t e0) as [c1 (H2,(H3,H4))]; try inversion_clear H0; auto. - destruct (cons t0 e4) as [c2 (H5,(H6,H7))]; try inversion_clear H1; auto. - destruct (H c1 c2); clear H; intuition. - Measure_e; omega. - constructor 1; simpl. - apply L.lt_cons_eq; auto. - rewrite H4 in l; rewrite H7 in l; auto. - constructor 2; simpl. - apply l_eq_cons; auto. - rewrite H4 in e6; rewrite H7 in e6; auto. - constructor 3; simpl. - apply L.lt_cons_eq; auto. - rewrite H4 in l; rewrite H7 in l; auto. - (* e > e3 *) - constructor 3; simpl; auto. -Qed. - -Definition compare : forall s1 s2, bst s1 -> bst s2 -> Compare lt eq s1 s2. -Proof. - intros s1 s2 s1_bst s2_bst; unfold lt, eq; simpl. - destruct (cons s1 End); intuition. - inversion_clear H0. - destruct (cons s2 End); intuition. - inversion_clear H3. - simpl in H2; rewrite <- app_nil_end in H2. - simpl in H5; rewrite <- app_nil_end in H5. - destruct (compare_aux x x0); intuition. - constructor 1; simpl in |- *. - rewrite H2 in l; rewrite H5 in l; auto. - constructor 2; apply L_eq_eq; simpl in |- *. - rewrite H2 in e; rewrite H5 in e; auto. - constructor 3; simpl in |- *. - rewrite H2 in l; rewrite H5 in l; auto. +Lemma compare_Cmp : forall s1 s2, + Cmp (compare s1 s2) (elements s1) (elements s2). +Proof. + intros; unfold compare. + rewrite (app_nil_end (elements s1)). + replace (elements s2) with (flatten_e (cons s2 End)) by + (rewrite cons_1; simpl; rewrite <- app_nil_end; auto). + apply compare_cont_Cmp; auto. + intros. + apply compare_end_Cmp; auto. Qed. (** * Equality test *) -Definition equal : forall s s' : t, bst s -> bst s' -> {Equal s s'} + {~ Equal s s'}. +Lemma equal_1 : forall s1 s2, bst s1 -> bst s2 -> + Equal s1 s2 -> equal s1 s2 = true. Proof. - intros s s' Hs Hs'; case (compare s s'); auto; intros. - right; apply lt_not_eq; auto. - right; intro; apply (lt_not_eq s' s); auto; apply eq_sym; auto. -Qed. - -(** We provide additionally a different implementation for union, subset and - equal, which is less efficient, but uses structural induction, hence computes - within Coq. *) - -(** Alternative union based on fold. - Complexity : [min(|s|,|s'|)*log(max(|s|,|s'|))] *) - -Definition union' s s' := - if ge_lt_dec (height s) (height s') then fold add s' s else fold add s s'. - -Lemma fold_add_avl : forall s s', avl s -> avl s' -> avl (fold add s s'). -Proof. - induction s; simpl; intros; inv avl; auto. -Qed. -Hint Resolve fold_add_avl. - -Lemma union'_avl : forall s s', avl s -> avl s' -> avl (union' s s'). -Proof. - unfold union'; intros; destruct (ge_lt_dec (height s) (height s')); auto. -Qed. - -Lemma fold_add_bst : forall s s', bst s -> avl s -> bst s' -> avl s' -> - bst (fold add s s'). -Proof. - induction s; simpl; intros; inv avl; inv bst; auto. - apply IHs2; auto. - apply add_bst; auto. -Qed. - -Lemma union'_bst : forall s s', bst s -> avl s -> bst s' -> avl s' -> - bst (union' s s'). -Proof. - unfold union'; intros; destruct (ge_lt_dec (height s) (height s')); - apply fold_add_bst; auto. +unfold equal; intros s1 s2 B1 B2 E. +generalize (compare_Cmp s1 s2). +destruct (compare s1 s2); simpl in *; auto; intros. +elim (lt_not_eq B1 B2 H E); auto. +elim (lt_not_eq B2 B1 H (eq_sym E)); auto. Qed. -Lemma fold_add_in : forall s s' y, bst s -> avl s -> bst s' -> avl s' -> - (In y (fold add s s') <-> In y s \/ In y s'). -Proof. - induction s; simpl; intros; inv avl; inv bst; auto. - intuition_in. - rewrite IHs2; auto. - apply add_bst; auto. - apply fold_add_bst; auto. - rewrite add_in; auto. - rewrite IHs1; auto. - intuition_in. -Qed. - -Lemma union'_in : forall s s' y, bst s -> avl s -> bst s' -> avl s' -> - (In y (union' s s') <-> In y s \/ In y s'). +Lemma equal_2 : forall s1 s2, + equal s1 s2 = true -> Equal s1 s2. Proof. - unfold union'; intros; destruct (ge_lt_dec (height s) (height s')). - rewrite fold_add_in; intuition. - apply fold_add_in; auto. -Qed. - -(** Alternative subset based on diff. *) - -Definition subset' s s' := is_empty (diff s s'). - -Lemma subset'_1 : forall s s', bst s -> avl s -> bst s' -> avl s' -> - Subset s s' -> subset' s s' = true. -Proof. - unfold subset', Subset; intros; apply is_empty_1; red; intros. - rewrite (diff_in); intuition. +unfold equal; intros s1 s2 E. +generalize (compare_Cmp s1 s2); + destruct compare; auto; discriminate. Qed. -Lemma subset'_2 : forall s s', bst s -> avl s -> bst s' -> avl s' -> - subset' s s' = true -> Subset s s'. -Proof. - unfold subset', Subset; intros; generalize (is_empty_2 _ H3 a); unfold Empty. - rewrite (diff_in); intuition. - generalize (mem_2 s' a) (mem_1 s' a); destruct (mem a s'); intuition. -Qed. +End Proofs. -(** Alternative equal based on subset *) +End Raw. -Definition equal' s s' := subset' s s' && subset' s' s. -Lemma equal'_1 : forall s s', bst s -> avl s -> bst s' -> avl s' -> - Equal s s' -> equal' s s' = true. -Proof. - unfold equal', Equal; intros. - rewrite subset'_1; firstorder; simpl. - apply subset'_1; firstorder. -Qed. - -Lemma equal'_2 : forall s s', bst s -> avl s -> bst s' -> avl s' -> - equal' s s' = true -> Equal s s'. -Proof. - unfold equal', Equal; intros; destruct (andb_prop _ _ H3); split; - apply subset'_2; auto. -Qed. - -End Raw. (** * Encapsulation Now, in order to really provide a functor implementing [S], we - need to encapsulate everything into a type of balanced binary search trees. *) + 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 [FSetFullAVL] if you need more than just the FSet interface. +*) Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Module E := X. - Module Raw := Raw I X. + Module Raw := Raw I X. + Import Raw.Proofs. - Record bbst : Set := Bbst {this :> Raw.t; is_bst : Raw.bst this; is_avl: Raw.avl this}. - Definition t := bbst. + Record bst := Bst {this :> Raw.t; is_bst : Raw.bst this}. + Definition t := bst. Definition elt := E.t. - Definition In (x : elt) (s : t) : Prop := Raw.In x s. - Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'. - Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'. - Definition Empty (s:t) : Prop := forall a : elt, ~ In a s. - Definition For_all (P : elt -> Prop) (s:t) : Prop := forall x, In x s -> P x. - Definition Exists (P : elt -> Prop) (s:t) : Prop := exists x, In x s /\ P x. - + Definition In (x : elt) (s : t) := Raw.In x s. + Definition Equal (s s':t) := forall a : elt, In a s <-> In a s'. + Definition Subset (s s':t) := forall a : elt, In a s -> In a s'. + Definition Empty (s:t) := forall a : elt, ~ In a s. + Definition For_all (P : elt -> Prop) (s:t) := forall x, In x s -> P x. + Definition Exists (P : elt -> Prop) (s:t) := exists x, In x s /\ P x. + Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s. - Proof. intro s; exact (Raw.In_1 s). Qed. + Proof. intro s; exact (@In_1 s). Qed. Definition mem (x:elt)(s:t) : bool := Raw.mem x s. - Definition empty : t := Bbst _ Raw.empty_bst Raw.empty_avl. + Definition empty : t := Bst empty_bst. Definition is_empty (s:t) : bool := Raw.is_empty s. - Definition singleton (x:elt) : t := Bbst _ (Raw.singleton_bst x) (Raw.singleton_avl x). - Definition add (x:elt)(s:t) : t := - Bbst _ (Raw.add_bst s x (is_bst s) (is_avl s)) - (Raw.add_avl s x (is_avl s)). - Definition remove (x:elt)(s:t) : t := - Bbst _ (Raw.remove_bst s x (is_bst s) (is_avl s)) - (Raw.remove_avl s x (is_avl s)). - Definition inter (s s':t) : t := - Bbst _ (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.inter_avl _ _ (is_avl s) (is_avl s')). - Definition diff (s s':t) : t := - Bbst _ (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.diff_avl _ _ (is_avl s) (is_avl s')). + Definition singleton (x:elt) : t := Bst (singleton_bst x). + Definition add (x:elt)(s:t) : t := Bst (add_bst x (is_bst s)). + Definition remove (x:elt)(s:t) : t := Bst (remove_bst x (is_bst s)). + Definition inter (s s':t) : t := Bst (inter_bst (is_bst s) (is_bst s')). + Definition union (s s':t) : t := Bst (union_bst (is_bst s) (is_bst s')). + Definition diff (s s':t) : t := Bst (diff_bst (is_bst s) (is_bst s')). Definition elements (s:t) : list elt := Raw.elements s. Definition min_elt (s:t) : option elt := Raw.min_elt s. Definition max_elt (s:t) : option elt := Raw.max_elt s. Definition choose (s:t) : option elt := Raw.choose s. - Definition fold (B : Set) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. + Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. Definition cardinal (s:t) : nat := Raw.cardinal s. Definition filter (f : elt -> bool) (s:t) : t := - Bbst _ (Raw.filter_bst f _ (is_bst s) (is_avl s)) - (Raw.filter_avl f _ (is_avl s)). + Bst (filter_bst f (is_bst s)). Definition for_all (f : elt -> bool) (s:t) : bool := Raw.for_all f s. Definition exists_ (f : elt -> bool) (s:t) : bool := Raw.exists_ f s. Definition partition (f : elt -> bool) (s:t) : t * t := let p := Raw.partition f s in - (Bbst (fst p) (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) - (Raw.partition_avl_1 f _ (is_avl s)), - Bbst (snd p) (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) - (Raw.partition_avl_2 f _ (is_avl s))). - - Definition union (s s':t) : t := - let (u,p) := Raw.union _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') in - let (b,p) := p in - let (a,_) := p in - Bbst u b a. - - Definition union' (s s' : t) : t := - Bbst _ (Raw.union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.union'_avl _ _ (is_avl s) (is_avl s')). - - Definition equal (s s': t) : bool := if Raw.equal _ _ (is_bst s) (is_bst s') then true else false. - Definition equal' (s s':t) : bool := Raw.equal' s s'. + (@Bst (fst p) (partition_bst_1 f (is_bst s)), + @Bst (snd p) (partition_bst_2 f (is_bst s))). - Definition subset (s s':t) : bool := if Raw.subset _ _ (is_bst s) (is_bst s') then true else false. - Definition subset' (s s':t) : bool := Raw.subset' s s'. + Definition equal (s s':t) : bool := Raw.equal s s'. + Definition subset (s s':t) : bool := Raw.subset s s'. - Definition eq (s s':t) : Prop := Raw.eq s s'. - Definition lt (s s':t) : Prop := Raw.lt s s'. + Definition eq (s s':t) : Prop := Raw.Equal s s'. + Definition lt (s s':t) : Prop := Raw.Proofs.lt s s'. - Definition compare (s s':t) : Compare lt eq s s'. + Definition compare (s s':t) : Compare lt eq s s'. Proof. - intros; elim (Raw.compare _ _ (is_bst s) (is_bst s')); - [ constructor 1 | constructor 2 | constructor 3 ]; - auto. + intros (s,b) (s',b'). + generalize (compare_Cmp s s'). + destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. (* specs *) @@ -2634,260 +1886,164 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Variable s s' s'': t. Variable x y : elt. - Hint Resolve is_bst is_avl. + Hint Resolve is_bst. Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (Raw.mem_1 s x (is_bst s)). Qed. + Proof. exact (mem_1 (is_bst s)). Qed. Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (Raw.mem_2 s x). Qed. + Proof. exact (@mem_2 s x). Qed. Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. - unfold equal; destruct (Raw.equal s s'); simpl; auto. - Qed. - + Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed. Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. - unfold equal; destruct (Raw.equal s s'); simpl; intuition; discriminate. - Qed. + Proof. exact (@equal_2 s s'). Qed. - Lemma equal'_1 : Equal s s' -> equal' s s' = true. - Proof. exact (Raw.equal'_1 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. - Lemma equal'_2 : equal' s s' = true -> Equal s s'. - Proof. exact (Raw.equal'_2 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. + Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition. Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. - unfold subset; destruct (Raw.subset s s'); simpl; intuition. - Qed. - + Proof. wrap subset subset_12. Qed. Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. - unfold subset; destruct (Raw.subset s s'); simpl; intuition discriminate. - Qed. - - Lemma subset'_1 : Subset s s' -> subset' s s' = true. - Proof. exact (Raw.subset'_1 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. - Lemma subset'_2 : subset' s s' = true -> Subset s s'. - Proof. exact (Raw.subset'_2 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. + Proof. wrap subset subset_12. Qed. Lemma empty_1 : Empty empty. - Proof. exact Raw.empty_1. Qed. + Proof. exact empty_1. Qed. Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (Raw.is_empty_1 s). Qed. + Proof. exact (@is_empty_1 s). Qed. Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (Raw.is_empty_2 s). Qed. + Proof. exact (@is_empty_2 s). Qed. Lemma add_1 : E.eq x y -> In y (add x s). - Proof. - unfold add, In; simpl; rewrite Raw.add_in; auto. - Qed. - + Proof. wrap add add_in. Qed. Lemma add_2 : In y s -> In y (add x s). - Proof. - unfold add, In; simpl; rewrite Raw.add_in; auto. - Qed. - + Proof. wrap add add_in. Qed. Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. - Proof. - unfold add, In; simpl; rewrite Raw.add_in; intuition. - elim H; auto. - Qed. + Proof. wrap add add_in. elim H; auto. Qed. Lemma remove_1 : E.eq x y -> ~ In y (remove x s). - Proof. - unfold remove, In; simpl; rewrite Raw.remove_in; intuition. - Qed. - + Proof. wrap remove remove_in. Qed. Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). - Proof. - unfold remove, In; simpl; rewrite Raw.remove_in; intuition. - Qed. - + Proof. wrap remove remove_in. Qed. Lemma remove_3 : In y (remove x s) -> In y s. - Proof. - unfold remove, In; simpl; rewrite Raw.remove_in; intuition. - Qed. + Proof. wrap remove remove_in. Qed. Lemma singleton_1 : In y (singleton x) -> E.eq x y. - Proof. exact (Raw.singleton_1 x y). Qed. + Proof. exact (@singleton_1 x y). Qed. Lemma singleton_2 : E.eq x y -> In y (singleton x). - Proof. exact (Raw.singleton_2 x y). Qed. + Proof. exact (@singleton_2 x y). Qed. Lemma union_1 : In x (union s s') -> In x s \/ In x s'. - Proof. - unfold union, In; simpl. - destruct (Raw.union s s' (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - as (u,(b,(a,i))). - simpl in *; rewrite i; auto. - Qed. - + Proof. wrap union union_in. Qed. Lemma union_2 : In x s -> In x (union s s'). - Proof. - unfold union, In; simpl. - destruct (Raw.union s s' (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - as (u,(b,(a,i))). - simpl in *; rewrite i; auto. - Qed. - + Proof. wrap union union_in. Qed. Lemma union_3 : In x s' -> In x (union s s'). - Proof. - unfold union, In; simpl. - destruct (Raw.union s s' (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - as (u,(b,(a,i))). - simpl in *; rewrite i; auto. - Qed. - - Lemma union'_1 : In x (union' s s') -> In x s \/ In x s'. - Proof. - unfold union', In; simpl; rewrite Raw.union'_in; intuition. - Qed. - - Lemma union'_2 : In x s -> In x (union' s s'). - Proof. - unfold union', In; simpl; rewrite Raw.union'_in; intuition. - Qed. - - Lemma union'_3 : In x s' -> In x (union' s s'). - Proof. - unfold union', In; simpl; rewrite Raw.union'_in; intuition. - Qed. + Proof. wrap union union_in. Qed. Lemma inter_1 : In x (inter s s') -> In x s. - Proof. - unfold inter, In; simpl; rewrite Raw.inter_in; intuition. - Qed. - + Proof. wrap inter inter_in. Qed. Lemma inter_2 : In x (inter s s') -> In x s'. - Proof. - unfold inter, In; simpl; rewrite Raw.inter_in; intuition. - Qed. - + Proof. wrap inter inter_in. Qed. Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). - Proof. - unfold inter, In; simpl; rewrite Raw.inter_in; intuition. - Qed. + Proof. wrap inter inter_in. Qed. Lemma diff_1 : In x (diff s s') -> In x s. - Proof. - unfold diff, In; simpl; rewrite Raw.diff_in; intuition. - Qed. - + Proof. wrap diff diff_in. Qed. Lemma diff_2 : In x (diff s s') -> ~ In x s'. - Proof. - unfold diff, In; simpl; rewrite Raw.diff_in; intuition. - Qed. - + Proof. wrap diff diff_in. Qed. Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). - Proof. - unfold diff, In; simpl; rewrite Raw.diff_in; intuition. - Qed. + Proof. wrap diff diff_in. Qed. - Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A), - fold A f s i = fold_left (fun a e => f e a) (elements s) i. - Proof. - unfold fold, elements; intros; apply Raw.fold_1; auto. - Qed. + Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A), + fold f s i = fold_left (fun a e => f e a) (elements s) i. + Proof. unfold fold, elements; intros; apply fold_1; auto. Qed. Lemma cardinal_1 : cardinal s = length (elements s). Proof. - unfold cardinal, elements; intros; apply Raw.cardinal_elements_1; auto. + unfold cardinal, elements; intros; apply elements_cardinal; auto. Qed. Section Filter. Variable f : elt -> bool. Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. - Proof. - intro; unfold filter, In; simpl; rewrite Raw.filter_in; intuition. - Qed. - + Proof. intro. wrap filter filter_in. Qed. Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. - Proof. - intro; unfold filter, In; simpl; rewrite Raw.filter_in; intuition. - Qed. - + Proof. intro. wrap filter filter_in. Qed. Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. - intro; unfold filter, In; simpl; rewrite Raw.filter_in; intuition. - Qed. + Proof. intro. wrap filter filter_in. Qed. Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (Raw.for_all_1 f s). Qed. + Proof. exact (@for_all_1 f s). Qed. Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (Raw.for_all_2 f s). Qed. + Proof. exact (@for_all_2 f s). Qed. Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (Raw.exists_1 f s). Qed. + Proof. exact (@exists_1 f s). Qed. Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (Raw.exists_2 f s). Qed. + Proof. exact (@exists_2 f s). Qed. Lemma partition_1 : compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). Proof. unfold partition, filter, Equal, In; simpl ;intros H a. - rewrite Raw.partition_in_1; auto. - rewrite Raw.filter_in; intuition. + rewrite partition_in_1, filter_in; intuition. Qed. Lemma partition_2 : compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). Proof. unfold partition, filter, Equal, In; simpl ;intros H a. - rewrite Raw.partition_in_2; auto. - rewrite Raw.filter_in; intuition. - red; intros. - f_equal; auto. - destruct (f a); auto. + rewrite partition_in_2, filter_in; intuition. + rewrite H2; auto. destruct (f a); auto. + red; intros; f_equal. + rewrite (H _ _ H0); auto. Qed. End Filter. Lemma elements_1 : In x s -> InA E.eq x (elements s). - Proof. - unfold elements, In; rewrite Raw.elements_in; auto. - Qed. - + Proof. wrap elements elements_in. Qed. Lemma elements_2 : InA E.eq x (elements s) -> In x s. - Proof. - unfold elements, In; rewrite Raw.elements_in; auto. - Qed. - + Proof. wrap elements elements_in. Qed. Lemma elements_3 : sort E.lt (elements s). - Proof. exact (Raw.elements_sort _ (is_bst s)). Qed. + Proof. exact (elements_sort (is_bst s)). Qed. + Lemma elements_3w : NoDupA E.eq (elements s). + Proof. exact (elements_nodup (is_bst s)). Qed. Lemma min_elt_1 : min_elt s = Some x -> In x s. - Proof. exact (Raw.min_elt_1 s x). Qed. + Proof. exact (@min_elt_1 s x). Qed. Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. - Proof. exact (Raw.min_elt_2 s x y (is_bst s)). Qed. + Proof. exact (@min_elt_2 s x y (is_bst s)). Qed. Lemma min_elt_3 : min_elt s = None -> Empty s. - Proof. exact (Raw.min_elt_3 s). Qed. + Proof. exact (@min_elt_3 s). Qed. Lemma max_elt_1 : max_elt s = Some x -> In x s. - Proof. exact (Raw.max_elt_1 s x). Qed. + Proof. exact (@max_elt_1 s x). Qed. Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. - Proof. exact (Raw.max_elt_2 s x y (is_bst s)). Qed. + Proof. exact (@max_elt_2 s x y (is_bst s)). Qed. Lemma max_elt_3 : max_elt s = None -> Empty s. - Proof. exact (Raw.max_elt_3 s). Qed. + Proof. exact (@max_elt_3 s). Qed. Lemma choose_1 : choose s = Some x -> In x s. - Proof. exact (Raw.choose_1 s x). Qed. + Proof. exact (@choose_1 s x). Qed. Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (Raw.choose_2 s). Qed. + Proof. exact (@choose_2 s). Qed. + Lemma choose_3 : choose s = Some x -> choose s' = Some y -> + Equal s s' -> E.eq x y. + Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed. Lemma eq_refl : eq s s. - Proof. exact (Raw.eq_refl s). Qed. + Proof. exact (eq_refl s). Qed. Lemma eq_sym : eq s s' -> eq s' s. - Proof. exact (Raw.eq_sym s s'). Qed. + Proof. exact (@eq_sym s s'). Qed. Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''. - Proof. exact (Raw.eq_trans s s' s''). Qed. + Proof. exact (@eq_trans s s' s''). Qed. Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''. - Proof. exact (Raw.lt_trans s s' s''). Qed. + Proof. exact (@lt_trans s s' s''). Qed. Lemma lt_not_eq : lt s s' -> ~eq s s'. - Proof. exact (Raw.lt_not_eq _ _ (is_bst s) (is_bst s')). Qed. + Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed. End Specs. End IntMake. @@ -2897,4 +2053,3 @@ End IntMake. Module Make (X: OrderedType) <: S with Module E := X :=IntMake(Z_as_Int)(X). - |