diff options
Diffstat (limited to 'theories/FSets/FSetAVL.v')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 156 |
1 files changed, 78 insertions, 78 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index b385f50e..5b09945b 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -12,7 +12,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FSetAVL.v 8985 2006-06-23 16:12:45Z jforest $ *) (** This module implements sets using AVL trees. It follows the implementation from Ocaml's standard library. *) @@ -515,7 +515,7 @@ Proof. (* LT *) inv avl. rewrite bal_in; auto. - rewrite (IHt y0 H1); intuition_in. + rewrite (IHt y0 H0); intuition_in. (* EQ *) inv avl. intuition. @@ -523,7 +523,7 @@ Proof. (* GT *) inv avl. rewrite bal_in; auto. - rewrite (IHt y0 H2); intuition_in. + rewrite (IHt y0 H1); intuition_in. Qed. Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s). @@ -531,16 +531,16 @@ Proof. intros s x; functional induction (add x s); auto; intros. inv bst; inv avl; apply bal_bst; auto. (* lt_tree -> lt_tree (add ...) *) - red; red in H5. + red; red in H4. intros. - rewrite (add_in l x y0 H) in H1. + rewrite (add_in l x y0 H) in H0. intuition. eauto. inv bst; inv avl; apply bal_bst; auto. (* gt_tree -> gt_tree (add ...) *) - red; red in H5. + red; red in H4. intros. - rewrite (add_in r x y0 H6) in H1. + rewrite (add_in r x y0 H5) in H0. intuition. apply MX.lt_eq with x; auto. Qed. @@ -703,7 +703,7 @@ Proof. avl_nns; omega_max. (* l = Node *) inversion_clear H. - rewrite H0 in IHp;simpl in IHp;destruct (IHp lh); auto. + rewrite e0 in IHp;simpl in IHp;destruct (IHp lh); auto. split; simpl in *. apply bal_avl; auto; omega_max. omega_bal. @@ -723,12 +723,12 @@ Proof. intuition_in. (* l = Node *) inversion_clear H. - generalize (remove_min_avl ll lx lr lh H1). - rewrite H0; simpl; intros. + generalize (remove_min_avl ll lx lr lh H0). + rewrite e0; simpl; intros. rewrite bal_in; auto. - rewrite H0 in IHp;generalize (IHp lh y H1). + rewrite e0 in IHp;generalize (IHp lh y H0). intuition. - inversion_clear H8; intuition. + inversion_clear H7; intuition. Qed. Lemma remove_min_bst : forall l x r h, @@ -736,15 +736,15 @@ Lemma remove_min_bst : forall l x r h, Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. - rewrite_all H0;simpl in *. + inversion_clear H; inversion_clear H0. + rewrite_all e0;simpl in *. apply bal_bst; auto. firstorder. intro; intros. generalize (remove_min_in ll lx lr lh y H). - rewrite H0; simpl. + rewrite e0; simpl. destruct 1. - apply H4; intuition. + apply H3; intuition. Qed. Lemma remove_min_gt_tree : forall l x r h, @@ -753,14 +753,14 @@ Lemma remove_min_gt_tree : forall l x r h, Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. + inversion_clear H; inversion_clear H0. intro; intro. - generalize (IHp lh H2 H); clear H8 H7 IHp. + 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 H0; simpl; intros. - rewrite (bal_in l' x r y H8 H6) in H1. - destruct H7. + 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. @@ -788,9 +788,9 @@ 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 H1. + destruct s1;try contradiction;clear y. generalize (remove_min_avl_1 l2 x2 r2 h2 H0). - rewrite H2; simpl; destruct 1. + rewrite e1; simpl; destruct 1. split. apply bal_avl; auto. simpl; omega_max. @@ -809,12 +809,12 @@ Proof. intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros. intuition_in. intuition_in. - destruct s1;try contradiction;clear H1. - replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto]. + 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 H2; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y); rewrite H2; simpl; intro. - rewrite H1; intuition. + 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. Qed. Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -822,13 +822,13 @@ Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> bst (merge s1 s2). Proof. intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. apply bal_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto. + generalize (remove_min_bst l2 x2 r2 h2); rewrite e1; simpl in *; auto. intro; intro. - apply H5; auto. - generalize (remove_min_in l2 x2 r2 h2 m); rewrite H2; simpl; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H2; simpl; auto. + 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. (** * Deletion *) @@ -850,18 +850,18 @@ Proof. intuition; omega_max. (* LT *) inv avl. - destruct (IHt H1). + destruct (IHt H0). split. apply bal_avl; auto. omega_max. omega_bal. (* EQ *) inv avl. - generalize (merge_avl_1 l r H1 H2 H3). + generalize (merge_avl_1 l r H0 H1 H2). intuition omega_max. (* GT *) inv avl. - destruct (IHt H2). + destruct (IHt H1). split. apply bal_avl; auto. omega_max. @@ -880,17 +880,17 @@ Proof. intros s x; functional induction (remove x s); subst;simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e0. rewrite bal_in; auto. - generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H0); intuition; [ order | order | intuition_in ]. (* EQ *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. elim H9; eauto. (* GT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e0. rewrite bal_in; auto. - generalize (IHt y0 H6); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H5); intuition; [ order | order | intuition_in ]. Qed. Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s). @@ -945,7 +945,7 @@ Proof. simpl. destruct l1. inversion 1; subst. - assert (X.lt x _x) by (apply H3; auto). + assert (X.lt x _x) by (apply H2; auto). inversion_clear 1; auto; order. assert (X.lt t _x) by auto. inversion_clear 2; auto; @@ -958,7 +958,7 @@ Proof. red; auto. inversion 1. destruct l;try contradiction. - clear H0;intro H0. + clear y;intro H0. destruct (IHo H0 t); auto. Qed. @@ -1004,7 +1004,7 @@ Proof. red; auto. inversion 1. destruct r;try contradiction. - clear H0;intros H0; destruct (IHo H0 t); auto. + intros H0; destruct (IHo H0 t); auto. Qed. (** * Any element *) @@ -1038,9 +1038,9 @@ Function concat (s1 s2 : t) : t := Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2). Proof. intros s1 s2; functional induction (concat s1 s2); subst;auto. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. intros; apply join_avl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite e1; simpl; auto. Qed. Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1048,13 +1048,13 @@ Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> bst (concat s1 s2). Proof. intros s1 s2; functional induction (concat s1 s2); subst ;auto. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. intros; apply join_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 m H3); rewrite H2; simpl; 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 H3); rewrite H2; simpl; auto. + 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 -> @@ -1064,12 +1064,12 @@ Proof. intros s1 s2; functional induction (concat s1 s2);subst;simpl. intuition. inversion_clear H5. - destruct s1;try contradiction;clear H1;intuition. + destruct s1;try contradiction;clear y;intuition. inversion_clear H5. - destruct s1;try contradiction;clear H1; intros. + 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 H3); rewrite H2; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl. + 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. Qed. @@ -1100,9 +1100,9 @@ Lemma split_avl : forall s x, avl s -> Proof. intros s x; functional induction (split x s);subst;simpl in *. auto. - rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition. + rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition. simpl; inversion_clear 1; auto. - rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition. + rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition. Qed. Lemma split_in_1 : forall s x y, bst s -> avl s -> @@ -1111,20 +1111,20 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H9. - rewrite (IHp y0 H2 H6); clear IHp H0. + 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 H0; auto; order. + inversion_clear H6; auto; order. (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0. + simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. intuition. order. intuition_in; order. (* GT *) - rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite join_in; auto. - generalize (split_avl r x H7); rewrite H1; simpl; intuition. - rewrite (IHp y0 H3 H7); clear H1. + generalize (split_avl r x H5); rewrite e1; simpl; intuition. + rewrite (IHp y0 H1 H5); clear e1. intuition; [ eauto | eauto | intuition_in ]. Qed. @@ -1134,17 +1134,17 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite join_in; auto. - generalize (split_avl l x H6); rewrite H1; simpl; intuition. - rewrite (IHp y0 H2 H6); clear IHp H0. + 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 H8 H7 H0. + simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. intuition; [ order | intuition_in; order ]. (* GT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. - rewrite (IHp y0 H3 H7); clear IHp H0. + 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. Qed. @@ -1154,13 +1154,13 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + 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 H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + 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. Qed. @@ -1171,21 +1171,21 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition. (* LT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. intuition. apply join_bst; auto. - generalize (split_avl l x H6); rewrite H1; simpl; intuition. + generalize (split_avl l x H4); rewrite e1; simpl; intuition. intro; intro. - generalize (split_in_2 l x y0 H2 H6); rewrite H1; simpl; intuition. + 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 H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. intuition. apply join_bst; auto. - generalize (split_avl r x H7); rewrite H1; simpl; intuition. + generalize (split_avl r x H5); rewrite e1; simpl; intuition. intro; intro. - generalize (split_in_1 r x y0 H3 H7); rewrite H1; simpl; intuition. + generalize (split_in_1 r x y0 H1 H5); rewrite e1; simpl; intuition. Qed. (** * Intersection *) |