summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetProperties.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /theories/FSets/FSetProperties.v
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'theories/FSets/FSetProperties.v')
-rw-r--r--theories/FSets/FSetProperties.v29
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.