From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- theories/FSets/FMapFacts.v | 55 +++++++++++++++++++++++++++------------------- 1 file changed, 32 insertions(+), 23 deletions(-) (limited to 'theories/FSets/FMapFacts.v') diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 8944f7ce..0c1448c9 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapFacts.v 12459 2009-11-02 18:51:43Z letouzey $ *) - (** * Finite maps library *) (** This functor derives additional facts from [FMapInterface.S]. These @@ -259,7 +257,7 @@ Qed. Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), MapsTo x b (mapi f m) -> - exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m. + exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m. Proof. intros; case_eq (find x m); intros. exists e. @@ -654,7 +652,7 @@ Add Relation key E.eq transitivity proved by E.eq_trans as KeySetoid. -Implicit Arguments Equal [[elt]]. +Arguments Equal {elt} m m'. Add Parametric Relation (elt : Type) : (t elt) Equal reflexivity proved by (@Equal_refl elt) @@ -740,7 +738,7 @@ End WFacts_fun. (** * Same facts for self-contained weak sets and for full maps *) -Module WFacts (M:S) := WFacts_fun M.E M. +Module WFacts (M:WS) := WFacts_fun M.E M. Module Facts := WFacts. (** * Additional Properties for weak maps @@ -761,8 +759,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Notation eqk := (@eq_key elt). Instance eqk_equiv : Equivalence eqk. - Proof. split; repeat red; eauto. Qed. - + Proof. unfold eq_key; split; eauto. Qed. + Instance eqke_equiv : Equivalence eqke. Proof. unfold eq_key_elt; split; repeat red; firstorder. @@ -834,8 +832,11 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). (** * Conversions between maps and association lists. *) + 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 (fun p => add (fst p) (snd p)) (empty _) l. + List.fold_right (uncurry (@add _)) (empty _) l. Definition to_list := elements. @@ -845,6 +846,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Proof. induction l as [|(k',e') l IH]; simpl; intros k e Hnodup. rewrite empty_mapsto_iff, InA_nil; intuition. + unfold uncurry; simpl. inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k e Hnodup'); clear Hnodup'. rewrite add_mapsto_iff, InA_cons, <- IH. @@ -861,6 +863,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Proof. induction l as [|(k',e') l IH]; simpl; intros k Hnodup. apply empty_o. + unfold uncurry; simpl. inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k Hnodup'); clear Hnodup'. rewrite add_o, IH. @@ -883,6 +886,14 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). (** * Fold *) + (** Alternative specification via [fold_right] *) + + Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) : + fold f m i = List.fold_right (uncurry f) i (rev (elements m)). + Proof. + rewrite fold_1. symmetry. apply fold_left_rev_right. + Qed. + (** ** Induction principles about fold contributed by S. Lescuyer *) (** In the following lemma, the step hypothesis is deliberately restricted @@ -897,8 +908,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). P m (fold f m i). Proof. intros A P f i m Hempty Hstep. - rewrite fold_1, <- fold_left_rev_right. - set (F:=fun (y : key * elt) (x : A) => f (fst y) (snd y) x). + rewrite fold_spec_right. + set (F:=uncurry f). set (l:=rev (elements m)). assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' -> Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)). @@ -983,8 +994,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). R (fold f m i) (fold g m j). Proof. intros A B R f g i j m Rempty Rstep. - do 2 rewrite fold_1, <- fold_left_rev_right. - set (l:=rev (elements m)). + rewrite 2 fold_spec_right. set (l:=rev (elements m)). assert (Rstep' : forall k e a b, InA eqke (k,e) l -> R a b -> R (f k e a) (g k e b)) by (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto with *). @@ -1099,14 +1109,15 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 -> eqA (fold f m1 i) (fold f m2 i). Proof. - intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. + 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_restr 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'); unfold eq_key; simpl; auto. + intros (k,e) (k',e'); unfold eq_key, uncurry; simpl; auto. rewrite <- NoDupA_altdef; auto. intros (k,e). rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H; @@ -1116,8 +1127,9 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). 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. - intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. - set (f':=fun y x0 => f (fst y) (snd y) x0) in *. + intros. + rewrite 2 fold_spec_right. + set (f':=uncurry f). change (f k e (fold_right f' i (rev (elements m1)))) with (f' (k,e) (fold_right f' i (rev (elements m1)))). assert (NoDupA eqk (rev (elements m1))) by (auto with *). @@ -1126,7 +1138,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). (R:=complement eqk)(eqA:=eqke)(eqB:=eqA); auto with *. intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto. unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto. - unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto. + unfold f'; intros (k1,e1) (k2,e2); unfold eq_key, uncurry; simpl; auto. rewrite <- NoDupA_altdef; auto. rewrite InA_rev, <- elements_mapsto_iff by (auto with *). firstorder. intros (a,b). @@ -2130,8 +2142,7 @@ Module OrdProperties (M:S). eqA (fold f m1 i) (fold f m2 i). Proof. intros m1 m2 A eqA st f i Hf Heq. - do 2 rewrite fold_1. - do 2 rewrite <- fold_left_rev_right. + rewrite 2 fold_spec_right. apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto. apply eqlistA_rev. apply elements_Equal_eqlistA. auto. @@ -2142,8 +2153,7 @@ Module OrdProperties (M:S). Above x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (f x e (fold f m1 i)). Proof. - intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. - set (f':=fun y x0 => f (fst y) (snd y) x0) in *. + intros. rewrite 2 fold_spec_right. set (f':=uncurry f). transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))). apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto. @@ -2158,8 +2168,7 @@ Module OrdProperties (M:S). Below x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (fold f m1 (f x e i)). Proof. - intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. - set (f':=fun y x0 => f (fst y) (snd y) x0) in *. + intros. rewrite 2 fold_spec_right. set (f':=uncurry f). transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))). apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto. -- cgit v1.2.3