diff options
Diffstat (limited to 'theories/FSets/FSetProperties.v')
| -rw-r--r-- | theories/FSets/FSetProperties.v | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 59e19cd3..1bad8061 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetProperties.v 12400 2009-10-19 13:14:18Z letouzey $ *) - (** * Finite sets library *) (** This functor derives additional properties from [FSetInterface.S]. @@ -337,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). @@ -353,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. @@ -426,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. @@ -485,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 @@ -1088,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. @@ -1105,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. @@ -1126,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. |