diff options
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 108 |
1 files changed, 54 insertions, 54 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. |