summaryrefslogtreecommitdiff
path: root/theories/FSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapAVL.v13
-rw-r--r--theories/FSets/FMapFacts.v55
-rw-r--r--theories/FSets/FMapFullAVL.v2
-rw-r--r--theories/FSets/FMapInterface.v3
-rw-r--r--theories/FSets/FMapList.v2
-rw-r--r--theories/FSets/FMapPositive.v12
-rw-r--r--theories/FSets/FMapWeakList.v2
-rw-r--r--theories/FSets/FMaps.v2
-rw-r--r--theories/FSets/FSetAVL.v2
-rw-r--r--theories/FSets/FSetBridge.v2
-rw-r--r--theories/FSets/FSetCompat.v2
-rw-r--r--theories/FSets/FSetDecide.v2
-rw-r--r--theories/FSets/FSetEqProperties.v2
-rw-r--r--theories/FSets/FSetFacts.v2
-rw-r--r--theories/FSets/FSetInterface.v3
-rw-r--r--theories/FSets/FSetList.v2
-rw-r--r--theories/FSets/FSetProperties.v29
-rw-r--r--theories/FSets/FSetToFiniteSet.v2
-rw-r--r--theories/FSets/FSetWeakList.v2
-rw-r--r--theories/FSets/FSets.v2
20 files changed, 61 insertions, 82 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 49f595d7..c761e2a7 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -8,8 +8,6 @@
(* Finite map library. *)
-(* $Id: FMapAVL.v 13768 2011-01-06 13:55:35Z glondu $ *)
-
(** * FMapAVL *)
(** This module implements maps using AVL trees.
@@ -39,6 +37,7 @@ Open Local Scope lazy_bool_scope.
Open Local Scope Int_scope.
Definition key := X.t.
+Hint Transparent key.
(** * Trees *)
@@ -542,12 +541,12 @@ Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo).
Ltac join_tac :=
intros l; induction l as [| ll _ lx ld lr Hlr lh];
[ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
- [ | destruct (gt_le_dec lh (rh+2));
+ [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
[ match goal with |- context [ bal ?u ?v ?w ?z ] =>
replace (bal u v w z)
with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
end
- | destruct (gt_le_dec rh (lh+2));
+ | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
[ match goal with |- context [ bal ?u ?v ?w ?z ] =>
replace (bal u v w z)
with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto]
@@ -823,7 +822,7 @@ Proof.
intros l x e r; functional induction (bal l x e r); intros; clearf;
inv bst; repeat apply create_bst; auto; unfold create; try constructor;
(apply lt_tree_node || apply gt_tree_node); auto;
- (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
+ (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
Qed.
Hint Resolve bal_bst.
@@ -1113,7 +1112,7 @@ Lemma join_bst : forall l x d r, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (join l x d r).
Proof.
join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto;
- clear Hrl Hlr z; intro; intros; rewrite join_in in *.
+ clear Hrl Hlr; intro; intros; rewrite join_in in *.
intuition; [ apply MX.lt_eq with x | ]; eauto.
intuition; [ apply MX.eq_lt with x | ]; eauto.
Qed.
@@ -1333,7 +1332,7 @@ Proof.
inversion_clear H.
destruct H7; simpl in *.
order.
- destruct (elements_aux_mapsto r acc x e0); intuition eauto.
+ destruct (elements_aux_mapsto r acc x e0); intuition eauto.
Qed.
Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
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.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 2b9e7077..774bcd9b 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -8,8 +8,6 @@
(* Finite map library. *)
-(* $Id: FMapFullAVL.v 13090 2010-06-08 13:56:14Z herbelin $ *)
-
(** * FMapFullAVL
This file contains some complements to [FMapAVL].
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index bbfecfb1..4d89b562 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapInterface.v 12640 2010-01-07 15:32:49Z letouzey $ *)
-
(** * Finite map library *)
(** This file proposes interfaces for finite maps *)
@@ -58,6 +56,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
Module Type WSfun (E : DecidableType).
Definition key := E.t.
+ Hint Transparent key.
Parameter t : Type -> Type.
(** the abstract type of maps *)
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 4b7f183c..f15ab222 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapList.v 12458 2009-11-02 18:50:33Z letouzey $ *)
-
(** * Finite map library *)
(** This file proposes an implementation of the non-dependant interface
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 30bce2db..2e2eb166 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapPositive.v 13297 2010-07-19 23:32:42Z letouzey $ *)
-
(** * FMapPositive : an implementation of FMapInterface for [positive] keys. *)
Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
@@ -86,7 +84,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Section A.
Variable A:Type.
- Implicit Arguments Leaf [A].
+ Arguments Leaf [A].
Definition empty : t A := Leaf.
@@ -496,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
- Global Instance eqk_equiv : Equivalence eq_key.
- Global Instance eqke_equiv : Equivalence eq_key_elt.
- Global Instance ltk_strorder : StrictOrder lt_key.
+ Global Program Instance eqk_equiv : Equivalence eq_key.
+ Global Program Instance eqke_equiv : Equivalence eq_key_elt.
+ Global Program Instance ltk_strorder : StrictOrder lt_key.
Lemma mem_find :
forall m x, mem x m = match find x m with None => false | _ => true end.
@@ -816,7 +814,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Variable A B C : Type.
Variable f : option A -> option B -> option C.
- Implicit Arguments Leaf [A].
+ Arguments Leaf [A].
Fixpoint xmap2_l (m : t A) : t C :=
match m with
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index db479ea8..6c1e8ca8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapWeakList.v 12458 2009-11-02 18:50:33Z letouzey $ *)
-
(** * Finite map library *)
(** This file proposes an implementation of the non-dependant interface
diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v
index 75904202..19b25d95 100644
--- a/theories/FSets/FMaps.v
+++ b/theories/FSets/FMaps.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMaps.v 10699 2008-03-19 20:56:43Z letouzey $ *)
-
Require Export OrderedType OrderedTypeEx OrderedTypeAlt.
Require Export DecidableType DecidableTypeEx.
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 2cbba723..df627a14 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -7,8 +7,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetAVL.v 12641 2010-01-07 15:32:52Z letouzey $ *)
-
(** * FSetAVL : Implementation of FSetInterface via AVL trees *)
(** This module implements finite sets using AVL trees.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index c2d921be..25ce5577 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetBridge.v 13253 2010-07-07 08:39:30Z letouzey $ *)
-
(** * Finite sets library *)
(** This module implements bridges (as functors) from dependent
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index c3d614ee..6b3d86d3 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -264,7 +264,7 @@ Module Update_WSets
Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In.
Proof. intros x x' Hx s s' Hs. subst. apply MF.In_eq_iff; auto. Qed.
- Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
Section Spec.
Variable s s': t.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 7c321779..f64df9fe 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetDecide.v 14527 2011-10-07 14:33:38Z letouzey $ *)
-
(**************************************************************)
(* FSetDecide.v *)
(* *)
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index ac55aef5..755bc7dd 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetEqProperties.v 12400 2009-10-19 13:14:18Z letouzey $ *)
-
(** * Finite sets library *)
(** This module proves many properties of finite sets that
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 45b43d83..f473b334 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetFacts.v 12461 2009-11-03 08:24:06Z letouzey $ *)
-
(** * Finite sets library *)
(** This functor derives additional facts from [FSetInterface.S]. These
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index f366ed3e..a0361119 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetInterface.v 12640 2010-01-07 15:32:49Z letouzey $ *)
-
(** * Finite set library *)
(** Set interfaces, inspired by the one of Ocaml. When compared with
@@ -253,6 +251,7 @@ Module Type WSfun (E : DecidableType).
End Spec.
+ Hint Transparent elt.
Hint Resolve mem_1 equal_1 subset_1 empty_1
is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
remove_2 singleton_2 union_1 union_2 union_3
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 9408ba05..1f36306c 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetList.v 12641 2010-01-07 15:32:52Z letouzey $ *)
-
(** * Finite sets library *)
(** This file proposes an implementation of the non-dependant
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.
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index 2aa1b433..3ac5d9e4 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetToFiniteSet.v 12363 2009-09-28 15:04:07Z letouzey $ *)
-
(** * Finite sets library : conversion to old [Finite_sets] *)
Require Import Ensembles Finite_sets.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index b55db37a..2ea32e97 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetWeakList.v 12641 2010-01-07 15:32:52Z letouzey $ *)
-
(** * Finite sets library *)
(** This file proposes an implementation of the non-dependant
diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v
index a725c1eb..572f2865 100644
--- a/theories/FSets/FSets.v
+++ b/theories/FSets/FSets.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSets.v 13297 2010-07-19 23:32:42Z letouzey $ *)
-
Require Export OrderedType.
Require Export OrderedTypeEx.
Require Export OrderedTypeAlt.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:36:22 +0000