diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 23:43:05 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 23:43:05 +0000 |
| commit | 189770d9cf98db9ba08da66707002c52f092d73f (patch) | |
| tree | 45e49e7e80b44e60a27e698b962e826be33196e2 /theories/FSets/FSetAVL.v | |
| parent | ab8c213b7a4873265e325d0f8da0744bf31d96be (diff) | |
Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)
* FSetAVL is greatly lightened : modulo a minor change in bal, formal
proofs of avl invariant is not needed for building a functor
implementing FSetInterface.S (even if this invariant is still true)
* Non-structural functions (union, subset, compare, equal) are
transformed into efficient structural versions
* Both proofs of avl preservation and non-structural functions are
moved to a new file FSetFullAVL, that can be ignored by the average
user.
Same for FMapAVL (still work in progress...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetAVL.v')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 1840 |
1 files changed, 603 insertions, 1237 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 83dc3f1c4..5973b21ec 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 *) @@ -14,8 +13,29 @@ (* $Id$ *) +(** * 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 Recdef FSetInterface FSetList ZArith Int. @@ -23,8 +43,7 @@ Set Implicit Arguments. Unset Strict Implicit. Module Raw (Import I:Int)(X:OrderedType). -Module Import II:=MoreInt(I). -Open Scope Int_scope. +Open Local Scope Int_scope. Module MX := OrderedTypeFacts X. Definition elt := X.t. @@ -87,35 +106,11 @@ Inductive bst : tree -> Prop := | BSNode : forall x l r h, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (Node l x r h). -(** * 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 *) - -Inductive avl : tree -> Prop := - | RBLeaf : avl Leaf - | RBNode : forall x l r h, avl l -> avl r -> - -(2) <= height l - height r <= 2 -> - h = max (height l) (height r) + 1 -> - avl (Node l x r h). - - - (** * Automation and dedicated tactics *) -Hint Constructors In bst avl. +Hint Constructors In bst. Hint Unfold lt_tree gt_tree. -(** A tactic for cleaning hypothesis after use of functional induction. *) - -Ltac clearf := - match goal with - | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf - | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf - | _ => idtac - end. - (** A tactic to repeat [inversion_clear] on all hyps of the form [(f (Node _ _ _ _))] *) @@ -128,14 +123,6 @@ Ltac inv f := | _ => idtac end. -(** Same, but with a backup of the original hypothesis. *) - -Ltac safe_inv f := match goal with - | H:f (Node _ _ _ _) |- _ => - generalize H; inversion_clear H; safe_inv f - | _ => intros - end. - Ltac intuition_in := repeat progress (intuition; inv In). (** Helper tactic concerning order of elements. *) @@ -146,39 +133,8 @@ Ltac order := match goal with | _ => MX.order end. -(** Tactics about [avl] *) - -Lemma height_non_negative : forall s : tree, avl s -> height s >= 0. -Proof. - induction s; simpl; intros; auto with zarith. - inv avl; intuition; omega_max. -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. - - - -(** * Basic results about [In], [lt_tree], [gt_tree], [avl], [height] *) +(** * Basic results about [In], [lt_tree], [gt_tree], [height] *) (** [In] is compatible with [X.eq] *) @@ -189,6 +145,13 @@ Proof. Qed. Hint Immediate In_1. +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. @@ -243,26 +206,6 @@ Qed. Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. -(** Results about [avl] *) - -Lemma avl_node : - forall x l r, 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. - -(** Results about [height] *) - -Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf. -Proof. - destruct 1; intuition; simpl in *. - avl_nns; simpl in *; elimtype False; omega_max. -Qed. - - (** * Some shortcuts. *) @@ -273,35 +216,21 @@ 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. - -(** trick for emulating [assert false] in Coq. *) - -Definition assert_false := Leaf. -Lemma assert_false_cardinal : cardinal assert_false = 0%nat. -Proof. simpl; auto. Qed. -Opaque assert_false. - - - (** * Empty set *) Definition empty := Leaf. -Lemma empty_bst : bst empty. +Lemma empty_1 : Empty empty. Proof. - auto. + intro; intro. + inversion H. Qed. -Lemma empty_avl : avl empty. -Proof. +Lemma empty_bst : bst empty. +Proof. auto. Qed. -Lemma empty_1 : Empty empty. -Proof. - intro; intro. - inversion H. -Qed. (** * Emptyness test *) @@ -337,7 +266,7 @@ Function mem (x:elt)(s:t) { struct s } : bool := Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. Proof. - intros s x; functional induction mem x s; auto; intros; clearf; + intros s x; functional induction mem x s; auto; intros; try clear e0; inv bst; intuition_in; order. Qed. @@ -352,17 +281,6 @@ Qed. 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. - Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y. Proof. unfold singleton; intros; inv In; order. @@ -373,6 +291,11 @@ Proof. unfold singleton; auto. Qed. +Lemma singleton_bst : forall x : elt, bst (singleton x). +Proof. + unfold singleton; auto. +Qed. + (** * Helper functions *) @@ -383,6 +306,12 @@ Qed. Definition create l x r := Node l x r (max (height l) (height r) + 1). +Lemma create_in : + forall l x r y, In y (create l x r) <-> X.eq y x \/ In y l \/ In y r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + Lemma create_bst : forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (create l x r). @@ -391,42 +320,24 @@ Proof. 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. - -Lemma create_in : - forall l x r y, In y (create l x r) <-> X.eq y x \/ In y l \/ In y r. -Proof. - unfold create; split; [ inversion_clear 1 | ]; intuition. -Qed. - (** [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. + Function bal (l:t)(x:elt)(r:t) : t := let hl := height l in let hr := height r in if gt_le_dec hl (hr+2) then match l with - | Leaf => assert_false + | 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 + | Leaf => assert_false l x r | Node lrl lrx lrr _ => create (create ll lx lrl) lrx (create lrr x r) end @@ -434,13 +345,13 @@ Function bal (l:t)(x:elt)(r:t) : t := else if gt_le_dec hr (hl+2) then match r with - | Leaf => assert_false + | 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 + | Leaf => assert_false l x r | Node rll rlx rlr _ => create (create l x rll) rlx (create rlr rx rr) end @@ -448,6 +359,13 @@ Function bal (l:t)(x:elt)(r:t) : t := else create l x r. +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. + intros l x r; functional induction bal l x r; intros; try clear e0; + rewrite !create_in; intuition_in. +Qed. + 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. @@ -456,51 +374,7 @@ Proof. (apply lt_tree_node || apply gt_tree_node); auto; (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. - -Lemma bal_avl : forall l x r, avl l -> avl r -> - -(3) <= height l - height r <= 3 -> avl (bal l x r). -Proof. - intros l x r; functional induction bal l x r; intros; clearf; - inv avl; repeat apply create_avl; simpl in *; auto; omega_max. -Qed. - -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. -Proof. - intros l x r; functional induction bal l x r; intros; clearf; - inv avl; avl_nns; simpl in *; omega_max. -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. -Proof. - intros l x r; functional induction bal l x r; intros; clearf; - inv avl; simpl in *; omega_max. -Qed. - -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. - intros l x r; functional induction bal l x r; intros; clearf; - solve [repeat rewrite create_in; intuition_in - |inv avl; avl_nns; simpl in *; omega_max ]. -Qed. - -Lemma bal_cardinal : forall l x r, - (cardinal (bal l x r) <= S (cardinal l + cardinal r))%nat. -Proof. - intros l x r; functional induction bal l x r; intros; clearf; - simpl; auto with arith; romega with *. -Qed. - -Ltac omega_bal := match goal with - | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] => - generalize (bal_height_1 x H H') (bal_height_2 x H H'); - omega_max - end. - +Hint Resolve bal_bst. (** * Insertion *) @@ -515,76 +389,33 @@ Function add (x:elt)(s:t) { struct s } : t := match s with 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; destruct (@add_avl_1 s x H); auto. -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 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 x y0 H5) in H0. + rewrite add_in in H. intuition. apply MX.lt_eq with x; auto. Qed. - -Lemma add_cardinal : forall x s, - (cardinal (add x s) <= S (cardinal s))%nat. -Proof. - intros; functional induction add x s; simpl; auto with arith. - generalize (bal_cardinal (add x l) y r); romega with *. - generalize (bal_cardinal l y (add x r)); romega with *. -Qed. +Hint Resolve add_bst. @@ -607,7 +438,7 @@ Fixpoint join (l:t) : elt -> t -> t := end end. -(* XXX: Comment utiliser Function pour definit join et eviter join_tac ? *) +(* Function 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]; @@ -624,128 +455,33 @@ 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. - join_tac. - - split; simpl; auto. - destruct (add_avl_1 x H0). - avl_nns; omega_max. - split; auto. - set (l:=Node ll lx lr lh) in *. - destruct (add_avl_1 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; destruct (@join_avl_1 l x r H H0); auto. -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. -Qed. - -Lemma join_cardinal : forall l x r, - (cardinal (join l x r) <= S (cardinal l + cardinal r))%nat. -Proof. - join_tac; simpl; auto with arith. - apply add_cardinal. - destruct X.compare; simpl; auto with arith. - generalize (bal_cardinal (add x ll) lx lr) (add_cardinal x ll); - romega with *. - generalize (bal_cardinal ll lx (add x lr)) (add_cardinal x lr); - romega with *. - generalize (bal_cardinal ll lx (join lr x (Node rl rx rr rh))) - (Hlr x (Node rl rx rr rh)); simpl; romega with *. - generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr). - simpl in *; romega with *. + 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 + 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]). *) @@ -757,75 +493,40 @@ Function remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := let (l',m) := remove_min ll lx lr in (bal l' x r, m) end. -Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> - avl (remove_min l x r)#1 /\ - 0 <= height (Node l x r h) - height (remove_min l x r)#1 <= 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 (remove_min l x r)#1. -Proof. - intros; destruct (@remove_min_avl_1 l x r h H); auto. -Qed. - -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 (remove_min l x r)#2 \/ In y (remove_min l x r)#1). +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 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 (remove_min l x r)#1. + 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. 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. - apply (IHp lh); auto. - intro; intros. - generalize (remove_min_in 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) -> + 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. inv bst; auto. - inversion_clear H; inversion_clear H0. - intro; intro. - generalize (IHp lh H1 H); clear H6 H7 IHp. - generalize (remove_min_in m H)(remove_min_avl H). - rewrite e0; simpl; intros. - rewrite (bal_in x y H7 H5) in H0. - assert (In m (Node ll lx lr lh)) by (rewrite H6; auto); clear H6. - assert (X.lt m x) by order. - decompose [or] H0; order. + 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. @@ -843,56 +544,28 @@ Function merge (s1 s2 :t) : t:= match s1,s2 with 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. +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); 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 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; destruct (@merge_avl_1 s1 s2 H H0 H1); auto. -Qed. - -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. intuition_in. intuition_in. - destruct s1;try contradiction;clear y. - replace s2' with ((remove_min l2 x2 r2)#1); [|rewrite e1; auto]. - rewrite bal_in; auto. - generalize (remove_min_in y0 H2); rewrite e1; simpl; intro. - rewrite H3 ; intuition. - generalize (remove_min_avl H2); rewrite e1; simpl; auto. + 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); subst; simpl in *; intros; auto; clear y. apply bal_bst; auto. - generalize (remove_min_bst H1 H2); rewrite e1; simpl in *; auto. - intro; intro. - apply H3; auto. - generalize (remove_min_in m H2); rewrite e1; simpl; intuition. - generalize (remove_min_gt_tree H1 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. @@ -908,76 +581,33 @@ Function remove (x:elt)(s:t) { struct s } : t := match s with 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 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; destruct (@remove_avl_1 s x H); auto. -Qed. -Hint Resolve remove_avl. - -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); subst; simpl; + 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); simpl; + intros; inv bst. auto. (* LT *) - inv avl; inv bst. apply bal_bst; auto. - intro; intro. - rewrite (remove_in x y0 H0) 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 x y0 H5) in H; auto. - destruct H; eauto. + intro z; rewrite remove_in; auto; destruct 1; eauto. Qed. +Hint Resolve remove_bst. @@ -998,7 +628,7 @@ Proof. destruct l; 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. @@ -1088,11 +718,11 @@ Proof. exact min_elt_3. Qed. -Lemma choose_3 : forall s s', bst s -> avl s -> bst s' -> avl s' -> +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 Ha Hb' Ha' x x' Hx Hx' H. + 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. @@ -1118,45 +748,28 @@ Function concat (s1 s2 : t) : t := join s1 m s2' end. -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 H0); rewrite e1; simpl; auto. + intros s1 s2; functional induction (concat s1 s2);subst;simpl;intros. + 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 H1 H2); rewrite e1; simpl; auto. - generalize (remove_min_avl H2); rewrite e1; simpl; auto. - generalize (remove_min_in m H2); rewrite e1; simpl; auto. - destruct 1; intuition. - generalize (remove_min_gt_tree H1 H2); rewrite e1; simpl; auto. + intros s1 s2; functional induction (concat s1 s2); subst; auto; clear y. + intros; 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. - -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 _ m s2' y H0). - generalize (remove_min_in y H2); rewrite e1; simpl. - intro EQ; rewrite EQ; intuition. - generalize (remove_min_avl H2); rewrite e1; simpl; auto. -Qed. - -Hint Resolve concat_avl concat_bst. +Hint Resolve concat_bst. @@ -1182,118 +795,51 @@ Function split (x:elt)(s:t) { struct s } : t * (bool * t) := match s with end end. -Lemma split_avl : forall s x, avl s -> - avl (split x s)#1 /\ avl (split x s)#2#2. -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 -> +Lemma split_in_1 : forall s x y, bst s -> (In y (split x s)#1 <-> 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. +Proof. + intros s x; functional induction (split x s); subst; simpl; intros; + inv bst; try clear e0. + intuition_in. + rewrite e1 in IHp; simpl in IHp; rewrite IHp; 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. - rewrite (IHp y0 H1 H5); clear e1. - intuition; [ eauto | eauto | intuition_in ]. - generalize (split_avl x H5); rewrite e1; simpl; intuition. + rewrite join_in. + rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order. Qed. -Lemma split_in_2 : forall s x y, bst s -> avl s -> +Lemma split_in_2 : forall s x y, bst s -> (In y (split x s)#2#2 <-> 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. - rewrite (IHp y0 H0 H4); clear IHp e0. - intuition; [ order | order | intuition_in ]. - generalize (split_avl x H4); rewrite e1; simpl; intuition. - (* 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 IHp; simpl in IHp; rewrite IHp; intuition_in; order. + intuition_in; order. + rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order. Qed. -Lemma split_in_3 : forall s x, bst s -> avl s -> +Lemma split_in_3 : forall s x, bst s -> ((split x s)#2#1 = 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 IHp; simpl in IHp; rewrite IHp; intuition_in; order. + intuition. + rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order. Qed. -Lemma split_bst : forall s x, bst s -> avl s -> +Lemma split_bst : forall s x, bst s -> bst (split x s)#1 /\ bst (split x s)#2#2. 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 x H4); rewrite e1; simpl; intuition. - intro; intro. - generalize (split_in_2 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 x H5); rewrite e1; simpl; intuition. - intro; intro. - generalize (split_in_1 x y0 H1 H5); rewrite e1; simpl; intuition. -Qed. - -Lemma split_cardinal_1 : forall x s, - (cardinal (split x s)#1 <= cardinal s)%nat. -Proof. - intros x s; functional induction split x s; simpl; auto. - rewrite e1 in IHp; simpl in *. - romega with *. - romega with *. - rewrite e1 in IHp; simpl in *. - generalize (@join_cardinal l y rl); romega with *. -Qed. - -Lemma split_cardinal_2 : forall x s, - (cardinal (split x s)#2#2 <= cardinal s)%nat. -Proof. - intros x s; functional induction split x s; simpl; auto. - rewrite e1 in IHp; simpl in *. - generalize (@join_cardinal rl y r); romega with *. - romega with *. - rewrite e1 in IHp; simpl in *; romega with *. + 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. @@ -1310,57 +856,45 @@ Function inter (s1 s2 : t) { struct s1 } : t := match s1, s2 with 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; intros A1 A2; - generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1; - inv avl; auto. -Qed. -Hint Resolve inter_avl. - -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. - intros s1 s2; functional induction inter s1 s2; intros B1 A1 B2 A2; + intros s1 s2; functional induction inter s1 s2; intros B1 B2; [intuition_in|intuition_in | | ]; set (r:=Node l2 x2 r2 h2) in *; - generalize (split_avl x1 A2)(split_bst x1 B2 A2); - rewrite e1; simpl; destruct 1; destruct 1; - inv avl; inv bst; + generalize (split_bst x1 B2); + rewrite e1; simpl; destruct 1; inv bst; destruct IHt as (IHb1,IHi1); auto; destruct IHt0 as (IHb2,IHi2); auto; - destruct (distr_pair e1); clear e1; - destruct (distr_pair H12); clear H12; split. + destruct (distr_pair e1); clear e1; + destruct (distr_pair H6); clear H6; split. (* bst join *) apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) - intros; rewrite join_in; auto; rewrite IHi1; rewrite IHi2. - rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. - rewrite split_in_3 in H13; intuition_in. + intros. + rewrite join_in, IHi1, IHi2, <- H5, <- H8, split_in_1, split_in_2; auto. + rewrite split_in_3 in H7; intuition_in. apply In_1 with x1; auto. (* bst concat *) apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. (* In concat *) - intros; rewrite concat_in; auto. - rewrite IHi1; rewrite IHi2. - rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. - assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto). + intros. + rewrite concat_in, IHi1, IHi2, <- H5, <- H8, split_in_1, split_in_2; auto. + assert (~In x1 r) by (rewrite <- split_in_3, H7; auto). intuition_in. - elim H12. + elim H6. apply In_1 with y; auto. - intros y1 y2; rewrite IHi1, IHi2; intuition; order. 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 s1 s2 B1 A1 B2 A2; destruct (inter_bst_in B1 A1 B2 A2); auto. + 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 s1 s2 y B1 A1 B2 A2; destruct (inter_bst_in B1 A1 B2 A2); auto. + intros s1 s2 B1 B2; destruct (inter_bst_in B1 B2); auto. Qed. @@ -1377,173 +911,95 @@ Function diff (s1 s2 : t) { struct s1 } : t := match s1, s2 with 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; intros A1 A2; - generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1; - inv avl; auto. -Qed. -Hint Resolve diff_avl. - -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. - intros s1 s2; functional induction diff s1 s2; intros B1 A1 B2 A2; + intros s1 s2; functional induction diff s1 s2; intros B1 B2; [intuition_in|intuition_in | | ]; set (r:=Node l2 x2 r2 h2) in *; - generalize (split_avl x1 A2)(split_bst x1 B2 A2); - rewrite e1; simpl; destruct 1; destruct 1; + 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; destruct (distr_pair e1); clear e1; - destruct (distr_pair H12); clear H12; split. + destruct (distr_pair H6); clear H6; split. (* bst concat *) apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. (* In concat *) - intros; rewrite concat_in; auto. - rewrite IHi1; rewrite IHi2. - rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. - rewrite split_in_3 in H13; intuition_in. - elim H17. + intros. + rewrite concat_in, IHi1, IHi2, <-H5, <- H8, split_in_1, split_in_2; auto. + rewrite split_in_3 in H7; intuition_in. + elim H10. apply In_1 with x1; auto. - intros y1 y2; rewrite IHi1, IHi2; intuition; order. (* bst join *) apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) - intros; rewrite join_in; auto; rewrite IHi1; rewrite IHi2. - rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. - assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto). + intros. + rewrite join_in, IHi1, IHi2, <-H5, <-H8, split_in_1, split_in_2; auto. + assert (~In x1 r) by (rewrite <- split_in_3, H7; auto). intuition_in. - elim H12. + elim H6. 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 s1 s2 B1 A1 B2 A2; destruct (diff_bst_in B1 A1 B2 A2); auto. + 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 s1 s2 y B1 A1 B2 A2; destruct (diff_bst_in B1 A1 B2 A2); auto. + intros s1 s2 B1 B2; destruct (diff_bst_in B1 B2); auto. Qed. (** * Union *) -Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat. - -Ltac union_tac := - intros; unfold cardinal2; simpl fst in *; simpl snd in *; - match goal with H: split ?x ?s = _ |- _ => - generalize (split_cardinal_1 x s) (split_cardinal_2 x s); - rewrite H; simpl; romega with * - end. +(** 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]. +*) -Function union (s : t * t) { measure cardinal2 s } : t := - match s with - | (Leaf, Leaf) => s#2 - | (Leaf, Node _ _ _ _) => s#2 - | (Node _ _ _ _, Leaf) => s#1 - | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => - if ge_lt_dec h1 h2 then - if eq_dec h2 1 then add x2 s#1 else - let (l2',r2') := split x1 s#2 in - join (union (l1,l2')) x1 (union (r1,r2'#2)) - else - if eq_dec h1 1 then add x1 s#2 else - let (l1',r1') := split x2 s#1 in - join (union (l1',l2)) x2 (union (r1'#2,r2)) +Function union (s1 s2 : t) { struct s1 } : t := + match s1, s2 with + | Leaf, _ => s2 + | Node _ _ _ _, Leaf => s1 + | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => + let (l2',r2') := split x1 s2 in + join (union l1 l2') x1 (union r1 r2'#2) end. -Proof. -abstract union_tac. -abstract union_tac. -abstract union_tac. -abstract union_tac. -Defined. - -Lemma union_avl : forall s, - avl s#1 -> avl s#2 -> avl (union s). -Proof. - intros s; functional induction union s; - simpl fst in *; simpl snd in *; auto. - intros A1 A2; generalize (split_avl x1 A2); rewrite e2; simpl. - inv avl; destruct 1; auto. - intros A1 A2; generalize (split_avl x2 A1); rewrite e2; simpl. - inv avl; destruct 1; auto. -Qed. -Hint Resolve union_avl. -Lemma union_in : forall s y, - bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> - (In y (union s) <-> In y s#1 \/ In y s#2). +Lemma union_in : forall s1 s2 y, bst s1 -> bst s2 -> + (In y (union s1 s2) <-> In y s1 \/ In y s2). Proof. - intros s; functional induction union s; intros y B1 A1 B2 A2; - simpl fst in *; simpl snd in *; try clear e0 e1. + intros s1 s2; functional induction union s1 s2; intros y B1 B2. intuition_in. intuition_in. - intuition_in. - (* add x2 s#1 *) - inv avl. - rewrite (height_0 H); [ | avl_nn l2; omega_max]. - rewrite (height_0 H0); [ | avl_nn r2; omega_max]. - rewrite add_in; auto; intuition_in. - (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *) - generalize - (split_avl x1 A2) (split_bst x1 B2 A2) - (split_in_1 x1 y B2 A2) (split_in_2 x1 y B2 A2). - rewrite e2; simpl. - destruct 1; destruct 1; inv avl; inv bst. - rewrite join_in; auto. - rewrite IHt; auto. - rewrite IHt0; auto. + generalize (split_bst x1 B2) (split_in_1 x1 y B2) (split_in_2 x1 y B2). + rewrite e1; simpl. + destruct 1; inv bst. + rewrite join_in, IHt, IHt0; auto. do 2 (intro Eq; rewrite Eq; clear Eq). case (X.compare y x1); intuition_in. - (* add x1 s#2 *) - inv avl. - rewrite (height_0 H3); [ | avl_nn l1; omega_max]. - rewrite (height_0 H4); [ | avl_nn r1; omega_max]. - rewrite add_in; auto; intuition_in. - (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *) - generalize - (split_avl x2 A1) (split_bst x2 B1 A1) - (split_in_1 x2 y B1 A1) (split_in_2 x2 y B1 A1). - rewrite e2; simpl. - destruct 1; destruct 1; inv avl; inv bst. - rewrite join_in; auto. - rewrite IHt; auto. - rewrite IHt0; auto. - do 2 (intro Eq; rewrite Eq; clear Eq). - case (X.compare y x2); intuition_in. Qed. -Lemma union_bst : forall s, - bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (union s). +Lemma union_bst : forall s1 s2, bst s1 -> bst s2 -> + bst (union s1 s2). Proof. - intros s; functional induction union s; intros B1 A1 B2 A2; - simpl fst in *; simpl snd in *; try clear e0 e1; - try apply add_bst; auto. - (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *) - generalize (split_avl x1 A2) (split_bst x1 B2 A2). - rewrite e2; simpl. - destruct 1; destruct 1. - destruct (distr_pair e2) as (L,R); clear e2. - inv bst; inv avl. - apply join_bst; auto. - intro y; rewrite union_in; auto; simpl. - rewrite <- L, split_in_1; auto; intuition_in. - intro y; rewrite union_in; auto; simpl. - rewrite <- R, split_in_2; auto; intuition_in. - (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *) - generalize (split_avl x2 A1) (split_bst x2 B1 A1). - rewrite e2; simpl. - destruct 1; destruct 1. - destruct (distr_pair e2) as (L,R); clear e2. - inv bst; inv avl. + intros s1 s2; functional induction union s1 s2; intros B1 B2; auto. + generalize (split_bst x1 B2) . + inv bst. + rewrite e1; simpl; destruct 1. + destruct (distr_pair e1) as (L,R); clear e1. apply join_bst; auto. intro y; rewrite union_in; auto; simpl. rewrite <- L, split_in_1; auto; intuition_in. @@ -1644,65 +1100,43 @@ Fixpoint filter_acc (acc:t)(s:t) { struct s } : t := match s with Definition filter := filter_acc Leaf. -Lemma filter_acc_avl : forall s acc, avl s -> avl acc -> - avl (filter_acc acc s). -Proof. - induction s; simpl; auto. - intros. - inv avl. - apply IHs2; auto. - apply IHs1; auto. - destruct (f t); auto. -Qed. -Hint Resolve filter_acc_avl. - -Lemma filter_acc_bst : forall s acc, bst s -> avl s -> bst acc -> avl acc -> - bst (filter_acc acc s). -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. - -Lemma filter_acc_in : forall s acc, avl s -> avl acc -> +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. Proof. induction s; simpl; intros. intuition_in. - inv bst; inv avl. - rewrite IHs2 by (destruct (f t); auto). - rewrite IHs1 by (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 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. Proof. unfold filter; intros; rewrite filter_acc_in; intuition_in. -Qed. +Qed. + +Lemma filter_bst : forall s, bst s -> bst (filter s). +Proof. + unfold filter; intros; apply filter_acc_bst; auto. +Qed. @@ -1720,62 +1154,7 @@ Fixpoint partition_acc (acc : t*t)(s : t) { struct s } : t*t := Definition partition := partition_acc (Leaf,Leaf). -Lemma partition_acc_avl_1 : forall s acc, avl s -> - avl acc#1 -> avl (partition_acc acc s)#1. -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. - -Lemma partition_acc_avl_2 : forall s acc, avl s -> - avl acc#2 -> avl (partition_acc acc s)#2. -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 acc#1 -> avl acc#1 -> - bst (partition_acc acc s)#1. -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 acc#2 -> avl acc#2 -> - bst (partition_acc acc s)#2. -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. - -Lemma partition_acc_in_1 : forall s acc, avl s -> avl acc#1 -> +Lemma partition_acc_in_1 : forall s acc, compat_bool X.eq f -> forall x : elt, In x (partition_acc acc s)#1 <-> In x acc#1 \/ In x s /\ f x = true. @@ -1783,21 +1162,20 @@ Proof. induction s; simpl; intros. intuition_in. destruct acc as [acct accf]; simpl in *. - inv bst; inv avl. 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. + rewrite (H _ _ H2) in H3. + rewrite H0 in H3; discriminate. Qed. -Lemma partition_acc_in_2 : forall s acc, avl s -> avl acc#2 -> +Lemma partition_acc_in_2 : forall s acc, compat_bool X.eq f -> forall x : elt, In x (partition_acc acc s)#2 <-> In x acc#2 \/ In x s /\ f x = false. @@ -1805,44 +1183,21 @@ Proof. induction s; simpl; intros. intuition_in. destruct acc as [acct accf]; simpl in *. - inv bst; inv avl. 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_avl_1 : forall s, avl s -> avl (partition s)#1. -Proof. - unfold partition; intros; apply partition_acc_avl_1; auto. -Qed. - -Lemma partition_avl_2 : forall s, avl s -> avl (partition s)#2. -Proof. - unfold partition; intros; apply partition_acc_avl_2; auto. -Qed. - -Lemma partition_bst_1 : forall s, bst s -> avl s -> - bst (partition s)#1. -Proof. - unfold partition; intros; apply partition_acc_bst_1; auto. Qed. -Lemma partition_bst_2 : forall s, bst s -> avl s -> - bst (partition s)#2. -Proof. - unfold partition; intros; apply partition_acc_bst_2; auto. -Qed. - -Lemma partition_in_1 : forall s, avl s -> +Lemma partition_in_1 : forall s, compat_bool X.eq f -> forall x : elt, In x (partition s)#1 <-> In x s /\ f x = true. Proof. @@ -1850,7 +1205,7 @@ Proof. simpl in *; intuition_in. Qed. -Lemma partition_in_2 : forall s, avl s -> +Lemma partition_in_2 : forall s, compat_bool X.eq f -> forall x : elt, In x (partition s)#2 <-> In x s /\ f x = false. Proof. @@ -1858,6 +1213,40 @@ Proof. simpl in *; intuition_in. Qed. +Lemma partition_acc_bst_1 : forall s acc, bst s -> bst acc#1 -> + bst (partition_acc 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_acc_bst_2 : forall s acc, bst s -> bst acc#2 -> + bst (partition_acc acc s)#2. +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_bst_1 : forall s, bst s -> bst (partition s)#1. +Proof. + unfold partition; intros; apply partition_acc_bst_1; auto. +Qed. + +Lemma partition_bst_2 : forall s, bst s -> bst (partition s)#2. +Proof. + unfold partition; intros; apply partition_acc_bst_2; auto. +Qed. + (** * [for_all] and [exists] *) @@ -1976,56 +1365,141 @@ Qed. (** * Subset *) -Function subset (s:t*t) { measure cardinal2 s } : bool := - match s with - | (Leaf, _) => true - | (Node _ _ _ _, Leaf) => false - | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => +(** 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 _ => subset (Node l1 x1 Leaf 0, l2) && subset (r1,s#2) - | GT _ => subset (Node Leaf x1 r1 0, r2) && subset (l1,s#2) + | 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. +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. - intros; unfold cardinal2; simpl; abstract romega with *. - intros; unfold cardinal2; simpl; abstract romega with *. - intros; unfold cardinal2; simpl; abstract romega with *. - intros; unfold cardinal2; simpl; abstract romega with *. - intros; unfold cardinal2; simpl; abstract romega with *. - intros; unfold cardinal2; simpl; abstract romega with *. -Defined. + 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 subset_12 : forall s, - bst s#1 -> bst s#2 -> - (Subset s#1 s#2 <-> subset s = true). + 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 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. + + +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. - intros s; functional induction subset s; simpl; - intros B1 B2; try clear e0. - intuition. - red; auto; inversion 1. - split; intros; try discriminate. - assert (H': In _x0 Leaf) by auto; inversion H'. - (**) - simpl in *; inv bst. - rewrite andb_true_iff. - rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0. + 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 H7. + destruct X.compare. + + rewrite 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 subset_12 : forall s1 s2, bst s1 -> bst s2 -> + (subset s1 s2 = true <-> Subset s1 s2). +Proof. + 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_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. - assert (X.eq a x2) by order; intuition_in. - (**) - simpl in *; inv bst. - rewrite andb_true_iff. - rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0. + + rewrite 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. - (**) - simpl in *; inv bst. - rewrite andb_true_iff. - rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0. + + rewrite 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. @@ -2037,8 +1511,6 @@ Qed. (** ** Relations [eq] and [lt] over trees *) -(* NB: Don't use name eq yet otherwise Function won't work *) - Lemma eq_refl : forall s : t, Equal s s. Proof. unfold Equal; intuition. @@ -2081,8 +1553,28 @@ Proof. apply L.lt_not_eq with (s := elements s) (s' := elements s'); 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). +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. + -(** * A new comparison algorithm suggested by Xavier Leroy *) +(** * 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 *) @@ -2116,80 +1608,49 @@ 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) -> + bst s -> gt_tree x s -> sorted_e e -> + (forall y, In_e y e -> X.lt x y) -> + (forall y, In y s -> forall z, In_e z e -> X.lt y z) -> sorted_e (More x s e). Hint Constructors In_e sorted_e. Lemma elements_app : - forall (s : tree) (acc : list elt), elements_aux acc s = elements s ++ acc. + forall s acc, elements_aux acc s = elements s ++ acc. Proof. - simple induction s; simpl in |- *; intuition. - rewrite H0. - rewrite H. + induction s; simpl; intuition. + rewrite IHs1, IHs2. unfold elements; simpl. - do 2 rewrite H. - rewrite H0. - repeat rewrite <- app_nil_end. - repeat rewrite app_ass; auto. + rewrite 2 IHs1, IHs2, <- !app_nil_end, !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. + forall l x r h acc, + elements l ++ x :: elements r ++ acc = + elements (Node l x r h) ++ acc. Proof. - simpl in |- *; unfold elements in |- *; simpl in |- *; intuition. - repeat rewrite elements_app. - repeat rewrite <- app_nil_end. - repeat rewrite app_ass; auto. + unfold elements; simpl; intuition. + rewrite !elements_app, <- !app_nil_end, !app_ass; auto. 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. + forall l x r h e, + elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ flatten_e e. Proof. - intros; simpl. - apply compare_flatten_1. + intros; simpl; apply compare_flatten_1. Qed. -(** termination of [compare_aux] *) - -Open Scope nat_scope. - -Fixpoint measure_e_t (s : tree) : nat := match s with - | Leaf => 0 - | Node l _ r _ => 1 + measure_e_t l + measure_e_t r - end. - -Fixpoint measure_e (e : enumeration) : nat := match e with - | End => 0 - | More _ s r => 1 + measure_e_t s + measure_e r - end. - (** [cons t e] adds the elements of tree [t] on the head of enumeration [e]. *) -Fixpoint cons s e {struct s} : enumeration := +Fixpoint cons s e : enumeration := match s with | Leaf => e | Node l x r h => cons l (More x r e) end. -Lemma cons_measure_e : forall s e, - measure_e (cons s e) = measure_e_t s + measure_e e. -Proof. - induction s; simpl; intros; auto. - rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith. -Qed. - Lemma cons_1 : forall s e, bst s -> sorted_e e -> (forall (x y : elt), In x s -> In_e y e -> X.lt x y) -> @@ -2205,115 +1666,97 @@ Proof. apply flatten_e_elements. 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). -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. +(** One step of comparison of elements *) -Definition measure2 e := measure_e e#1 + measure_e e#2. - -Function compare_aux - (e:enumeration*enumeration) { measure measure2 e } : comparison := - match e with - | (End,End) => Eq - | (End,More _ _ _) => Lt - | (More _ _ _, End) => Gt - | (More x1 r1 e1, More x2 r2 e2) => - match X.compare x1 x2 with - | EQ _ => compare_aux (cons r1 e1, cons r2 e2) - | LT _ => Lt - | GT _ => Gt - end +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. -Proof. -intros; unfold measure2; simpl; -abstract (do 2 rewrite cons_measure_e; romega with *). -Defined. +(** Comparison of left tree, middle element, then right tree *) -Definition compare s1 s2 := compare_aux (cons s1 End, cons s2 End). +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. -Lemma compare_aux_Eq : forall e, - sorted_e e#1 -> sorted_e e#2 -> - compare_aux e = Eq -> L.eq (flatten_e e#1) (flatten_e e#2). -Proof. - intros e; functional induction compare_aux e; simpl; intros; auto; - try discriminate. - apply L.eq_refl. - apply l_eq_cons; auto. - inversion H; subst; clear H. - inversion H0; subst; clear H0. - destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto. - rewrite <- H0; rewrite <- H3; auto. -Qed. +(** Initial continuation *) -Lemma compare_aux_Lt : forall e, - sorted_e e#1 -> sorted_e e#2 -> - compare_aux e = Lt -> L.lt (flatten_e e#1) (flatten_e e#2). -Proof. - intros e; functional induction compare_aux e; simpl; intros; auto; - try discriminate. - apply L.lt_cons_eq; auto. - inversion H; subst; clear H. - inversion H0; subst; clear H0. - destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto. - rewrite <- H0; rewrite <- H3; auto. -Qed. +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). -Lemma compare_aux_Gt : forall e, - sorted_e e#1 -> sorted_e e#2 -> - compare_aux e = Gt -> L.lt (flatten_e e#2) (flatten_e e#1). +(** Correctness of this comparison *) + +Definition Cmp c := + match c with + | Eq => L.eq + | Lt => L.lt + | Gt => (fun l1 l2 => L.lt l2 l1) + end. + +Lemma cons_Cmp : forall c x1 x2 l1 l2, X.eq x1 x2 -> + Cmp c l1 l2 -> Cmp c (x1::l1) (x2::l2). Proof. - intros e; functional induction compare_aux e; simpl; intros; auto; - try discriminate. - apply L.lt_cons_eq; auto. - inversion H; subst; clear H. - inversion H0; subst; clear H0. - destruct (@cons_1 r1 e1); destruct (@cons_1 r2 e2); auto. - rewrite <- H0; rewrite <- H3; auto. + destruct c; simpl; auto. Qed. +Hint Resolve cons_Cmp. -Lemma compare_Eq : forall s1 s2, bst s1 -> bst s2 -> - compare s1 s2 = Eq -> Equal s1 s2. +Lemma compare_end_Cmp : + forall e2, Cmp (compare_end e2) nil (flatten_e e2). Proof. - unfold compare; intros. - destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2. - destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2. - simpl in *; rewrite <- app_nil_end in *. - apply L_eq_eq; rewrite <-E1, <-E2. - apply (@compare_aux_Eq (cons s1 End, cons s2 End)); simpl; auto. + destruct e2; simpl; auto. + apply L.eq_refl. Qed. -Lemma compare_Lt : forall s1 s2, bst s1 -> bst s2 -> - compare s1 s2 = Lt -> lt s1 s2. +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. - unfold compare; intros. - destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2. - destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2. - simpl in *; rewrite <- app_nil_end in *. - red; rewrite <- E1, <- E2. - apply (@compare_aux_Lt (cons s1 End, cons s2 End)); simpl; auto. + simpl; intros; destruct X.compare; simpl; auto. Qed. -Lemma compare_Gt : forall s1 s2, bst s1 -> bst s2 -> - compare s1 s2 = Gt -> lt s2 s1. +Lemma compare_cont_Cmp : forall s1 cont e2 l, + bst s1 -> sorted_e e2 -> + (forall e, sorted_e e -> Cmp (cont e) l (flatten_e e)) -> + Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2). Proof. - unfold compare; intros. - destruct (@cons_1 s1 End) as (S1,E1); auto; try inversion 2. - destruct (@cons_1 s2 End) as (S2,E2); auto; try inversion 2. - simpl in *; rewrite <- app_nil_end in *. - red; rewrite <- E1, <- E2. - apply (@compare_aux_Gt (cons s1 End, cons s2 End)); simpl; auto. + induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto. + inv bst. + rewrite <- compare_flatten_1; simpl. + apply Hl1; auto. clear e2 H0. intros [|x2 r2 e2] He2. + simpl; auto. + apply compare_more_Cmp. + inversion_clear He2. + destruct (cons_1 H H6); auto. + rewrite <- H10; auto. +Qed. + +Lemma compare_Cmp : forall s1 s2, bst s1 -> bst s2 -> + Cmp (compare s1 s2) (elements s1) (elements s2). +Proof. + intros; unfold compare. + rewrite (app_nil_end (elements s1)), (app_nil_end (elements s2)). + destruct (@cons_1 s2 End); auto. + inversion 2. + simpl in H2. unfold elt in *; rewrite <- H2. + apply compare_cont_Cmp; auto. + intros. + apply compare_end_Cmp; auto. Qed. -Close Scope nat_scope. - (** * Equality test *) Definition equal s1 s2 : bool := @@ -2326,17 +1769,17 @@ Lemma equal_1 : forall s1 s2, bst s1 -> bst s2 -> Equal s1 s2 -> equal s1 s2 = true. Proof. unfold equal; intros s1 s2 B1 B2 E. -generalize (compare_Lt B1 B2)(compare_Gt B1 B2). -destruct (compare s1 s2); auto; intros. -elim (lt_not_eq B1 B2 (H (refl_equal Lt)) E); auto. -elim (lt_not_eq B2 B1 (H0 (refl_equal Gt)) (eq_sym E)); auto. +generalize (compare_Cmp B1 B2). +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 equal_2 : forall s1 s2, bst s1 -> bst s2 -> equal s1 s2 = true -> Equal s1 s2. Proof. unfold equal; intros s1 s2 B1 B2 E. -generalize (compare_Eq B1 B2); +generalize (compare_Cmp B1 B2); destruct compare; auto; discriminate. Qed. @@ -2347,76 +1790,66 @@ 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. - Record bbst := 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. 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 Raw.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 x (is_bst s) (is_avl s)) - (Raw.add_avl x (is_avl s)). - Definition remove (x:elt)(s:t) : t := - Bbst (Raw.remove_bst x (is_bst s) (is_avl s)) - (Raw.remove_avl 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 union (s s':t) : t := - let (s,b,a) := s in let (s',b',a') := s' in - Bbst (@Raw.union_bst (s,s') b a b' a') - (@Raw.union_avl (s,s') a a'). - 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 (Raw.singleton_bst x). + Definition add (x:elt)(s:t) : t := Bst (Raw.add_bst x (is_bst s)). + Definition remove (x:elt)(s:t) : t := Bst (Raw.remove_bst x (is_bst s)). + Definition inter (s s':t) : t := Bst (Raw.inter_bst (is_bst s) (is_bst s')). + Definition union (s s':t) : t := Bst (Raw.union_bst (is_bst s) (is_bst s')). + Definition diff (s s':t) : t := Bst (Raw.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 : Type) (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 (Raw.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))). + (@Bst (fst p) (Raw.partition_bst_1 f (is_bst s)), + @Bst (snd p) (Raw.partition_bst_2 f (is_bst s))). Definition equal (s s':t) : bool := Raw.equal s s'. - Definition subset (s s':t) : bool := Raw.subset (s.(this),s'.(this)). + Definition subset (s s':t) : bool := Raw.subset s s'. Definition eq (s s':t) : Prop := Raw.Equal s s'. Definition lt (s s':t) : Prop := Raw.lt s s'. Definition compare (s s':t) : Compare lt eq s s'. - Proof. - intros (s,b,a) (s',b',a'). - generalize (Raw.compare_Eq b b') (Raw.compare_Lt b b') (Raw.compare_Gt b b'). + Proof. + intros (s,b) (s',b'). + generalize (Raw.compare_Cmp b b'). destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. @@ -2425,7 +1858,7 @@ 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 (is_bst s)). Qed. @@ -2437,15 +1870,12 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma equal_2 : equal s s' = true -> Equal s s'. Proof. exact (Raw.equal_2 (is_bst s) (is_bst s')). Qed. - Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. - unfold subset; rewrite <- Raw.subset_12; simpl; auto. - Qed. + Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition. + Lemma subset_1 : Subset s s' -> subset s s' = true. + Proof. wrap subset Raw.subset_12. Qed. Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. - unfold subset; rewrite <- Raw.subset_12; simpl; auto. - Qed. + Proof. wrap subset Raw.subset_12. Qed. Lemma empty_1 : Empty empty. Proof. exact Raw.empty_1. Qed. @@ -2456,35 +1886,18 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. exact (@Raw.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 Raw.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 Raw.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 Raw.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 Raw.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 Raw.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 Raw.remove_in. Qed. Lemma singleton_1 : In y (singleton x) -> E.eq x y. Proof. exact (@Raw.singleton_1 x y). Qed. @@ -2492,52 +1905,25 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. exact (@Raw.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 s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto. - Qed. - + Proof. wrap union Raw.union_in. Qed. Lemma union_2 : In x s -> In x (union s s'). - Proof. - unfold union, In; simpl. - destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto. - Qed. - + Proof. wrap union Raw.union_in. Qed. Lemma union_3 : In x s' -> In x (union s s'). - Proof. - unfold union, In; simpl. - destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto. - Qed. + Proof. wrap union Raw.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 Raw.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 Raw.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 Raw.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 Raw.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 Raw.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 Raw.diff_in. 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. @@ -2554,19 +1940,11 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. 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 Raw.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 Raw.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 Raw.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. @@ -2582,16 +1960,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. 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 Raw.partition_in_1, Raw.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. + rewrite Raw.partition_in_2, Raw.filter_in; intuition. rewrite H2; auto. destruct (f a); auto. red; intros; f_equal. @@ -2601,18 +1977,11 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. 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 Raw.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 Raw.elements_in. Qed. Lemma elements_3 : sort E.lt (elements s). Proof. exact (Raw.elements_sort (is_bst s)). Qed. - Lemma elements_3w : NoDupA E.eq (elements s). Proof. exact (Raw.elements_nodup (is_bst s)). Qed. @@ -2636,9 +2005,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. exact (@Raw.choose_2 s). Qed. Lemma choose_3 : choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y. - Proof. - exact (@Raw.choose_3 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') x y). - Qed. + Proof. exact (@Raw.choose_3 _ _ (is_bst s) (is_bst s') x y). Qed. Lemma eq_refl : eq s s. Proof. exact (Raw.eq_refl s). Qed. @@ -2660,4 +2027,3 @@ End IntMake. Module Make (X: OrderedType) <: S with Module E := X :=IntMake(Z_as_Int)(X). - |