diff options
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 49f595d7..c68216e6 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -8,8 +8,6 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 13768 2011-01-06 13:55:35Z glondu $ *) - (** * FMapAVL *) (** This module implements maps using AVL trees. @@ -34,11 +32,13 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. preservation *) Module Raw (Import I:Int)(X: OrderedType). -Open Local Scope pair_scope. -Open Local Scope lazy_bool_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. +Local Notation int := I.t. Definition key := X.t. +Hint Transparent key. (** * Trees *) @@ -542,12 +542,12 @@ Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo). Ltac join_tac := intros l; induction l as [| ll _ lx ld lr Hlr lh]; [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)); + [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE]; [ match goal with |- context [ bal ?u ?v ?w ?z ] => replace (bal u v w z) with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] end - | destruct (gt_le_dec rh (lh+2)); + | destruct (gt_le_dec rh (lh+2)) as [GT'|LE']; [ match goal with |- context [ bal ?u ?v ?w ?z ] => replace (bal u v w z) with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] @@ -604,12 +604,12 @@ Qed. Lemma lt_leaf : forall x, lt_tree x (Leaf elt). Proof. - unfold lt_tree in |- *; intros; intuition_in. + unfold lt_tree; intros; intuition_in. Qed. Lemma gt_leaf : forall x, gt_tree x (Leaf elt). Proof. - unfold gt_tree in |- *; intros; intuition_in. + unfold gt_tree; intros; intuition_in. Qed. Lemma lt_tree_node : forall x y l r e h, @@ -823,7 +823,7 @@ Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv bst; repeat apply create_bst; auto; unfold create; try constructor; (apply lt_tree_node || apply gt_tree_node); auto; - (eapply lt_tree_trans || eapply gt_tree_trans); eauto. + (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. Hint Resolve bal_bst. @@ -1113,7 +1113,7 @@ Lemma join_bst : forall l x d r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (join l x d r). Proof. join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; - clear Hrl Hlr z; intro; intros; rewrite join_in in *. + clear Hrl Hlr; intro; intros; rewrite join_in in *. intuition; [ apply MX.lt_eq with x | ]; eauto. intuition; [ apply MX.eq_lt with x | ]; eauto. Qed. @@ -1333,7 +1333,7 @@ Proof. inversion_clear H. destruct H7; simpl in *. order. - destruct (elements_aux_mapsto r acc x e0); intuition eauto. + destruct (elements_aux_mapsto r acc x e0); intuition eauto. Qed. Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s). @@ -1389,8 +1389,8 @@ Lemma fold_equiv_aux : L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a). Proof. simple induction s. - simpl in |- *; intuition. - simpl in |- *; intros. + simpl; intuition. + simpl; intros. rewrite H. simpl. apply H0. @@ -1400,11 +1400,11 @@ Lemma fold_equiv : forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A), fold f s a = fold' f s a. Proof. - unfold fold', elements in |- *. - simple induction s; simpl in |- *; auto; intros. + unfold fold', elements. + simple induction s; simpl; auto; intros. rewrite fold_equiv_aux. rewrite H0. - simpl in |- *; auto. + simpl; auto. Qed. Lemma fold_1 : |