diff options
Diffstat (limited to 'theories/FSets/FMapFacts.v')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 72 |
1 files changed, 41 insertions, 31 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 0c1448c9..8c6f4b64 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -437,12 +437,6 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. -Definition option_map (A B:Type)(f:A->B)(o:option A) : option B := - match o with - | Some a => Some (f a) - | None => None - end. - Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = option_map f (find x m). Proof. @@ -519,7 +513,7 @@ Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, elements_mapsto_iff. unfold eqb. -rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto. +rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto. Qed. Lemma elements_b : forall m x, @@ -678,9 +672,9 @@ Qed. Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. -unfold Empty; intros m m' Hm; intuition. -rewrite <-Hm in H0; eauto. -rewrite Hm in H0; eauto. +unfold Empty; intros m m' Hm. split; intros; intro. +rewrite <-Hm in H0; eapply H, H0. +rewrite Hm in H0; eapply H, H0. Qed. Add Parametric Morphism elt : (@is_empty elt) @@ -708,18 +702,18 @@ Add Parametric Morphism elt : (@add elt) with signature E.eq ==> eq ==> Equal ==> Equal as add_m. Proof. intros k k' Hk e m m' Hm y. -rewrite add_o, add_o; do 2 destruct eq_dec; auto. -elim n; rewrite <-Hk; auto. -elim n; rewrite Hk; auto. +rewrite add_o, add_o; do 2 destruct eq_dec as [|?Hnot]; auto. +elim Hnot; rewrite <-Hk; auto. +elim Hnot; rewrite Hk; auto. Qed. Add Parametric Morphism elt : (@remove elt) with signature E.eq ==> Equal ==> Equal as remove_m. Proof. intros k k' Hk m m' Hm y. -rewrite remove_o, remove_o; do 2 destruct eq_dec; auto. -elim n; rewrite <-Hk; auto. -elim n; rewrite Hk; auto. +rewrite remove_o, remove_o; do 2 destruct eq_dec as [|?Hnot]; auto. +elim Hnot; rewrite <-Hk; auto. +elim Hnot; rewrite Hk; auto. Qed. Add Parametric Morphism elt elt' : (@map elt elt') @@ -835,8 +829,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W := fun p => f (fst p) (snd p). - Definition of_list (l : list (key*elt)) := - List.fold_right (uncurry (@add _)) (empty _) l. + Definition of_list := + List.fold_right (uncurry (@add _)) (empty elt). Definition to_list := elements. @@ -867,7 +861,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k Hnodup'); clear Hnodup'. rewrite add_o, IH. - unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto. + unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. Qed. Lemma of_list_2 : forall l, NoDupA eqk l -> @@ -934,7 +928,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). apply InA_eqke_eqk with k e'; auto. rewrite <- of_list_1; auto. intro k'. rewrite Hsame, add_o, of_list_1b. simpl. - unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto. + unfold eqb. do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. inversion_clear Hdup; auto. apply IHl. intros; eapply Hstep'; eauto. @@ -1124,6 +1118,27 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). auto with *. Qed. + Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j -> + eqA (fold f m1 i) (fold f m2 j). + Proof. + intros. + rewrite 2 fold_spec_right. + assert (NoDupA eqk (rev (elements m1))) by (auto with * ). + assert (NoDupA eqk (rev (elements m2))) by (auto with * ). + apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke) + ; auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto. + - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto. + - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. + rewrite h'. + auto. + - rewrite <- NoDupA_altdef; auto. + - intros (k,e). + rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H; + auto with *. + Qed. + + Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 -> eqA (fold f m2 i) (f k e (fold f m1 i)). Proof. @@ -1871,14 +1886,9 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke, O.ltk; simpl. - destruct (E.compare t0 x); intuition. - right; split; auto; ME.order. - ME.order. - elim H. - exists e0; apply MapsTo_1 with t0; auto. - right; right; split; auto; ME.order. - ME.order. - right; split; auto; ME.order. + destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto. + - elim H; exists e0; apply MapsTo_1 with t0; auto. + - fold (~E.lt t0 x); auto. Qed. Lemma elements_Add_Above : forall m m' x e, @@ -1901,7 +1911,7 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke; simpl. intuition. - destruct (E.eq_dec x t0); auto. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m). exists e0; auto. @@ -1930,7 +1940,7 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke; simpl. intuition. - destruct (E.eq_dec x t0); auto. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m). exists e0; auto. @@ -1986,7 +1996,7 @@ Module OrdProperties (M:S). inversion_clear H1; [ | inversion_clear H2; eauto ]. red in H3; simpl in H3; destruct H3. destruct p as (p1,p2). - destruct (E.eq_dec p1 x). + destruct (E.eq_dec p1 x) as [Heq|Hneq]. apply ME.lt_eq with p1; auto. inversion_clear H2. inversion_clear H5. |