diff options
| -rw-r--r-- | theories/FSets/FMapFacts.v | 43 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 27 | ||||
| -rw-r--r-- | theories/MSets/MSetProperties.v | 25 |
3 files changed, 56 insertions, 39 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 9f9eca3c6..7665ac05b 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -832,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. @@ -843,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. @@ -859,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. @@ -881,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 @@ -895,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)). @@ -981,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 *). @@ -1097,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; @@ -1114,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 *). @@ -1124,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). @@ -2128,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. @@ -2140,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. @@ -2156,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. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 80da1c5d8..1bad80615 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -335,6 +335,14 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Section Fold. + (** Alternative specification via [fold_right] *) + + Lemma fold_spec_right (s:t)(A:Type)(i:A)(f : elt -> A -> A) : + fold f s i = List.fold_right f i (rev (elements s)). + Proof. + rewrite fold_1. symmetry. apply fold_left_rev_right. + Qed. + Notation NoDup := (NoDupA E.eq). Notation InA := (InA E.eq). @@ -351,8 +359,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). P s (fold f s i). Proof. intros A P f i s Pempty Pstep. - rewrite fold_1, <- fold_left_rev_right. - set (l:=rev (elements s)). + rewrite fold_spec_right. set (l:=rev (elements s)). assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)). intros; eapply Pstep; eauto. @@ -424,8 +431,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). R (fold f s i) (fold g s j). Proof. intros A B R f g i j s Rempty Rstep. - do 2 rewrite fold_1, <- fold_left_rev_right. - set (l:=rev (elements s)). + rewrite 2 fold_spec_right. set (l:=rev (elements s)). assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *). clearbody l; clear Rstep s. @@ -483,8 +489,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). split; intros. rewrite elements_iff; do 2 rewrite InA_alt. split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. - rewrite fold_left_rev_right. - apply fold_1. + apply fold_spec_right. Qed. (** An alternate (and previous) specification for [fold] was based on @@ -1086,8 +1091,7 @@ Module OrdProperties (M:S). Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)). Proof. intros. - do 2 rewrite M.fold_1. - do 2 rewrite <- fold_left_rev_right. + rewrite 2 fold_spec_right. change (f x (fold_right f i (rev (elements s)))) with (fold_right f i (rev (x::nil)++rev (elements s))). apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. @@ -1103,11 +1107,11 @@ Module OrdProperties (M:S). Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)). Proof. intros. - do 2 rewrite M.fold_1. + rewrite 2 M.fold_1. set (g:=fun (a : A) (e : elt) => f e a). change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)). unfold g. - do 2 rewrite <- fold_left_rev_right. + rewrite <- 2 fold_left_rev_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply elements_Add_Below; auto. @@ -1124,8 +1128,7 @@ Module OrdProperties (M:S). Lemma fold_equal : forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i). Proof. - intros; do 2 rewrite M.fold_1. - do 2 rewrite <- fold_left_rev_right. + intros. rewrite 2 fold_spec_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply sort_equivlistA_eqlistA; auto with set. diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 9cd28e171..0f24d76a9 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -337,6 +337,14 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). Notation NoDup := (NoDupA E.eq). Notation InA := (InA E.eq). + (** Alternative specification via [fold_right] *) + + Lemma fold_spec_right (s:t)(A:Type)(i:A)(f : elt -> A -> A) : + fold f s i = List.fold_right f i (rev (elements s)). + Proof. + rewrite fold_spec. symmetry. apply fold_left_rev_right. + Qed. + (** ** Induction principles for fold (contributed by S. Lescuyer) *) (** In the following lemma, the step hypothesis is deliberately restricted @@ -350,8 +358,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). P s (fold f s i). Proof. intros A P f i s Pempty Pstep. - rewrite fold_1; unfold flip; rewrite <- fold_left_rev_right. - set (l:=rev (elements s)). + rewrite fold_spec_right. set (l:=rev (elements s)). assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)). intros; eapply Pstep; eauto. @@ -423,8 +430,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). R (fold f s i) (fold g s j). Proof. intros A B R f g i j s Rempty Rstep. - do 2 (rewrite fold_1; unfold flip; rewrite <- fold_left_rev_right). - set (l:=rev (elements s)). + rewrite 2 fold_spec_right. set (l:=rev (elements s)). assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *). clearbody l; clear Rstep s. @@ -482,8 +488,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). split; intros. rewrite elements_iff; do 2 rewrite InA_alt. split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. - rewrite fold_left_rev_right. - apply fold_1. + apply fold_spec_right. Qed. (** An alternate (and previous) specification for [fold] was based on @@ -1093,8 +1098,7 @@ Module OrdProperties (M:Sets). Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)). Proof. intros. - rewrite !FM.fold_1. - unfold flip; rewrite <-!fold_left_rev_right. + rewrite 2 fold_spec_right. change (f x (fold_right f i (rev (elements s)))) with (fold_right f i (rev (x::nil)++rev (elements s))). apply (@fold_right_eqlistA E.t E.eq A eqA st); auto with *. @@ -1110,7 +1114,7 @@ Module OrdProperties (M:Sets). Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)). Proof. intros. - rewrite !FM.fold_1. + rewrite !fold_spec. change (eqA (fold_left (flip f) (elements s') i) (fold_left (flip f) (x::elements s) i)). unfold flip; rewrite <-!fold_left_rev_right. @@ -1131,8 +1135,7 @@ Module OrdProperties (M:Sets). forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i). Proof. intros. - rewrite !FM.fold_1. - unfold flip; rewrite <- !fold_left_rev_right. + rewrite 2 fold_spec_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply sort_equivlistA_eqlistA; auto with set. |