diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 108 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 42 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 28 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 156 |
4 files changed, 166 insertions, 168 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 425528ee..786ade0e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -9,7 +9,7 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FMapAVL.v 8985 2006-06-23 16:12:45Z jforest $ *) (** This module implements map using AVL trees. It follows the implementation from Ocaml's standard library. *) @@ -512,7 +512,7 @@ Proof. (* LT *) inv avl. rewrite bal_in; auto. - rewrite (IHt H1); intuition_in. + rewrite (IHt H0); intuition_in. (* EQ *) inv avl. firstorder_in. @@ -520,7 +520,7 @@ Proof. (* GT *) inv avl. rewrite bal_in; auto. - rewrite (IHt H2); intuition_in. + rewrite (IHt H1); intuition_in. Qed. Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m). @@ -530,13 +530,13 @@ Proof. (* lt_tree -> lt_tree (add ...) *) red; red in H4. intros. - rewrite (add_in x y0 e H) in H1. + rewrite (add_in x y0 e H) in H0. intuition. eauto. (* gt_tree -> gt_tree (add ...) *) - red; red in H5. + red; red in H4. intros. - rewrite (add_in x y0 e H6) in H1. + rewrite (add_in x y0 e H5) in H0. intuition. apply lt_eq with x; auto. Qed. @@ -591,9 +591,9 @@ Proof. inversion_clear H. destruct (IHp lh); auto. split; simpl in *. - rewrite_all H0. simpl in *. + rewrite_all e1. simpl in *. apply bal_avl; subst;auto; omega_max. - rewrite_all H0;simpl in *;omega_bal. + rewrite_all e1;simpl in *;omega_bal. Qed. Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> @@ -610,13 +610,13 @@ Proof. intuition_in. (* l = Node *) inversion_clear H. - generalize (remove_min_avl H1). + generalize (remove_min_avl H0). - rewrite_all H0; simpl; intros. + rewrite_all e1; simpl; intros. rewrite bal_in; auto. - generalize (IHp lh y H1). + generalize (IHp lh y H0). intuition. - inversion_clear H8; intuition. + inversion_clear H7; intuition. Qed. Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> @@ -628,14 +628,14 @@ Proof. intuition_in; subst; auto. (* l = Node *) inversion_clear H. - generalize (remove_min_avl H1). - rewrite_all H0; simpl; intros. + generalize (remove_min_avl H0). + rewrite_all e1; simpl; intros. rewrite bal_mapsto; auto; unfold create. simpl in *;destruct (IHp lh y e'). auto. intuition. - inversion_clear H3; intuition. - inversion_clear H10; intuition. + inversion_clear H2; intuition. + inversion_clear H9; intuition. Qed. Lemma remove_min_bst : forall elt (l:t elt) x e r h, @@ -643,14 +643,14 @@ Lemma remove_min_bst : forall elt (l:t elt) x e r h, Proof. intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. + inversion_clear H; inversion_clear H0. apply bal_bst; auto. - rewrite_all H0;simpl in *;firstorder. + rewrite_all e1;simpl in *;firstorder. intro; intros. generalize (remove_min_in y H). - rewrite_all H0; simpl in *. + rewrite_all e1; simpl in *. destruct 1. - apply H4; intuition. + apply H3; intuition. Qed. Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, @@ -659,15 +659,15 @@ Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, Proof. intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. + inversion_clear H; inversion_clear H0. intro; intro. - rewrite_all H0;simpl in *. - generalize (IHp lh H2 H); clear H7 H8 IHp. + rewrite_all e1;simpl in *. + generalize (IHp lh H1 H); clear H7 H6 IHp. generalize (remove_min_avl H). generalize (remove_min_in (fst m) H). - rewrite H0; simpl; intros. - rewrite (bal_in x e y H8 H6) in H1. - destruct H7. + rewrite e1; simpl; intros. + rewrite (bal_in x e y H7 H5) in H0. + destruct H6. firstorder. apply lt_eq with x; auto. apply X.lt_trans with x; auto. @@ -696,11 +696,11 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> Proof. intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros. split; auto; avl_nns; omega_max. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. 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 H0). - rewrite H2; simpl;destruct 1. + rewrite e3; simpl;destruct 1. split. apply bal_avl; auto. simpl; omega_max. @@ -719,13 +719,13 @@ Proof. intros elt s1 s2; functional induction (merge s1 s2);intros. intuition_in. intuition_in. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. (* rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *) - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto]. rewrite bal_in; auto. - generalize (remove_min_avl H4); rewrite H2; simpl; auto. - generalize (remove_min_in y H4); rewrite H2; simpl; intro. - rewrite H1; intuition. + generalize (remove_min_avl H2); rewrite e3; simpl; auto. + generalize (remove_min_in y0 H2); rewrite e3; simpl; intro. + rewrite H3; intuition. Qed. Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -734,13 +734,13 @@ Proof. intros elt s1 s2; functional induction (@merge elt s1 s2); intros. intuition_in. intuition_in. - destruct s1;try contradiction;clear H1. - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. + destruct s1;try contradiction;clear y. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto]. rewrite bal_mapsto; auto; unfold create. - generalize (remove_min_avl H4); rewrite H2; simpl; auto. - generalize (remove_min_mapsto y e0 H4); rewrite H2; simpl; intro. - rewrite H1; intuition (try subst; auto). - inversion_clear H1; intuition. + generalize (remove_min_avl H2); rewrite e3; simpl; auto. + generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro. + rewrite H3; intuition (try subst; auto). + inversion_clear H3; intuition. Qed. Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -751,13 +751,13 @@ Proof. apply bal_bst; auto. destruct s1;try contradiction. - generalize (remove_min_bst H3); rewrite H2; simpl in *; auto. + generalize (remove_min_bst H1); rewrite e3; simpl in *; auto. destruct s1;try contradiction. intro; intro. - apply H5; auto. - generalize (remove_min_in x H4); rewrite H2; simpl; intuition. + apply H3; auto. + generalize (remove_min_in x H2); rewrite e3; simpl; intuition. destruct s1;try contradiction. - generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto. + generalize (remove_min_gt_tree H1); rewrite e3; simpl; auto. Qed. (** * Deletion *) @@ -779,18 +779,18 @@ Proof. split; auto; 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 H1 H2 H3). + generalize (merge_avl_1 H0 H1 H2). intuition omega_max. (* GT *) inv avl. - destruct (IHt H2). + destruct (IHt H1). split. apply bal_avl; auto. omega_max. @@ -809,17 +809,17 @@ Proof. intros elt s x; functional induction (@remove elt x s); simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e1. 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 e1. rewrite merge_in; intuition; [ order | order | intuition_in ]. elim H9; eauto. (* GT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e1. 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 elt (s:t elt) x, bst s -> avl s -> bst (remove x s). @@ -830,7 +830,7 @@ Proof. inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H1) in H; auto. + rewrite (remove_in x y0 H0) in H; auto. destruct H; eauto. (* EQ *) inv avl; inv bst. @@ -839,7 +839,7 @@ Proof. inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H6) in H; auto. + rewrite (remove_in x y0 H5) in H; auto. destruct H; eauto. Qed. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index c671ba82..067f5a3e 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapList.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FMapList.v 9035 2006-07-09 15:42:09Z herbelin $ *) (** * Finite map library *) @@ -20,8 +20,6 @@ Require Import FMapInterface. Set Implicit Arguments. Unset Strict Implicit. -Arguments Scope list [type_scope]. - Module Raw (X:OrderedType). Module E := X. @@ -161,14 +159,14 @@ Proof. inversion 2. inversion_clear 2. - clear H0;compute in H1; destruct H1;order. - clear H0;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H1)); compute; order. + clear e1;compute in H0; destruct H0;order. + clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order. - clear H0;inversion_clear 2. + clear e1;inversion_clear 2. compute in H0; destruct H0; intuition congruence. generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order. - clear H0; do 2 inversion_clear 1; auto. + clear e1; do 2 inversion_clear 1; auto. compute in H2; destruct H2; order. Qed. @@ -197,7 +195,7 @@ Lemma add_2 : forall m x y e e', Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. - functional induction (add x e' m) ;simpl;auto; clear H0. + functional induction (add x e' m) ;simpl;auto; clear e0. subst;auto. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. @@ -214,9 +212,9 @@ Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl; intros. apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H1); compute; auto. - constructor 2; apply (In_inv_3 H1); compute; auto. - inversion_clear H1; auto. + apply (In_inv_3 H0); compute; auto. + constructor 2; apply (In_inv_3 H0); compute; auto. + inversion_clear H0; auto. Qed. @@ -265,13 +263,13 @@ Proof. red; inversion 1; inversion H1. apply Sort_Inf_NotIn with x0; auto. - clear H0;constructor; compute; order. + clear e0;constructor; compute; order. - clear H0;inversion_clear Hm. + clear e0;inversion_clear Hm. apply Sort_Inf_NotIn with x0; auto. apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto. - clear H0;inversion_clear Hm. + clear e0;inversion_clear Hm. assert (notin:~ In y (remove x l)) by auto. intros (x1,abs). inversion_clear abs. @@ -393,7 +391,7 @@ Proof. assert (cmp_e_e':cmp e e' = true). - apply H2 with x; auto. + apply H1 with x; auto. rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. @@ -402,7 +400,7 @@ Proof. destruct (H0 k). assert (In k ((x,e) ::l)). destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H1 H4)); auto. + destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. @@ -415,10 +413,10 @@ Proof. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. - apply H2 with k; destruct (eq_dec x k); auto. + apply H1 with k; destruct (eq_dec x k); auto. - destruct (X.compare x x'); try contradiction;clear H2. + destruct (X.compare x x'); try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. @@ -492,16 +490,16 @@ Proof. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. - destruct (IHb H1 H4 H7). + destruct (IHb H2 H4 H7). inversion_clear H0. destruct H9; simpl in *; subst. - inversion_clear H2. + inversion_clear H1. destruct H9; simpl in *; subst; auto. elim (Sort_Inf_NotIn H4 H5). exists e'0; apply MapsTo_eq with k; auto; order. - inversion_clear H2. + inversion_clear H1. destruct H0; simpl in *; subst; auto. - elim (Sort_Inf_NotIn H1 H3). + elim (Sort_Inf_NotIn H2 H3). exists e0; apply MapsTo_eq with k; auto; order. apply H8 with k; auto. Qed. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 3a91b868..890485a8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapWeakList.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FMapWeakList.v 8985 2006-06-23 16:12:45Z jforest $ *) (** * Finite map library *) @@ -104,8 +104,8 @@ Proof. inversion belong1. inversion H. inversion_clear NoDup. inversion_clear belong1. - inversion_clear H2. - compute in H3; destruct H3. + inversion_clear H1. + compute in H2; destruct H2. contradiction. apply IHb; auto. exists x0; auto. @@ -144,11 +144,11 @@ Proof. inversion 2. do 2 inversion_clear 1. - compute in H3; destruct H3; subst; trivial. + compute in H2; destruct H2; subst; trivial. elim H; apply InA_eqk with (x,e); auto. do 2 inversion_clear 1; auto. - compute in H3; destruct H3; elim _x; auto. + compute in H2; destruct H2; elim _x; auto. Qed. (* Not part of the exported specifications, used later for [combine]. *) @@ -184,7 +184,7 @@ Proof. intros m x y e e'; generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl;auto. intros y' e'' eqky'; inversion_clear 1. - destruct H1; simpl in *. + destruct H0; simpl in *. elim eqky'; apply X.eq_trans with k'; auto. auto. intros y' e'' eqky'; inversion_clear 1; intuition. @@ -196,7 +196,7 @@ Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl;auto. intros; apply (In_inv_3 H0); auto. - constructor 2; apply (In_inv_3 H1); auto. + constructor 2; apply (In_inv_3 H0); auto. inversion_clear 2; auto. Qed. @@ -208,8 +208,8 @@ Proof. inversion_clear 2. compute in H1; elim H; auto. inversion H1. - constructor 2; inversion_clear H1; auto. - compute in H2; elim H; auto. + constructor 2; inversion_clear H0; auto. + compute in H1; elim H; auto. inversion_clear 2; auto. Qed. @@ -272,17 +272,17 @@ Proof. inversion_clear Hm. subst. - swap H1. - destruct H3 as (e,H3); unfold PX.MapsTo in H3. + swap H0. + destruct H2 as (e,H2); unfold PX.MapsTo in H2. apply InA_eqk with (y,e); auto. compute; apply X.eq_trans with x; auto. intro H2. destruct H2 as (e,H2); inversion_clear H2. - compute in H1; destruct H1. + compute in H0; destruct H0. elim _x; apply X.eq_trans with y; auto. inversion_clear Hm. - elim (IHt0 H3 H). + elim (IHt0 H2 H). exists e; auto. Qed. @@ -292,7 +292,7 @@ Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. functional induction (remove x m);auto. inversion_clear 3; auto. - compute in H2; destruct H2. + compute in H1; destruct H1. elim H; apply X.eq_trans with k'; auto. inversion_clear 1; inversion_clear 2; auto. 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 *) |