diff options
Diffstat (limited to 'theories/FSets')
-rw-r--r-- | theories/FSets/FMapAVL.v | 13 | ||||
-rw-r--r-- | theories/FSets/FMapFacts.v | 55 | ||||
-rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 | ||||
-rw-r--r-- | theories/FSets/FMapInterface.v | 3 | ||||
-rw-r--r-- | theories/FSets/FMapList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FMapPositive.v | 12 | ||||
-rw-r--r-- | theories/FSets/FMapWeakList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FMaps.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetAVL.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetBridge.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetCompat.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetDecide.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetEqProperties.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetFacts.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetInterface.v | 3 | ||||
-rw-r--r-- | theories/FSets/FSetList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetProperties.v | 29 | ||||
-rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetWeakList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSets.v | 2 |
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. |