diff options
Diffstat (limited to 'theories/FSets')
-rw-r--r-- | theories/FSets/FMapAVL.v | 34 | ||||
-rw-r--r-- | theories/FSets/FMapFacts.v | 55 | ||||
-rw-r--r-- | theories/FSets/FMapFullAVL.v | 6 | ||||
-rw-r--r-- | theories/FSets/FMapInterface.v | 3 | ||||
-rw-r--r-- | theories/FSets/FMapList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FMapPositive.v | 14 | ||||
-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 | 150 | ||||
-rw-r--r-- | theories/FSets/FSetCompat.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetDecide.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetEqProperties.v | 10 | ||||
-rw-r--r-- | theories/FSets/FSetFacts.v | 8 | ||||
-rw-r--r-- | theories/FSets/FSetInterface.v | 3 | ||||
-rw-r--r-- | theories/FSets/FSetList.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetProperties.v | 31 | ||||
-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, 156 insertions, 178 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 49f595d7..c68216e6 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. @@ -34,11 +32,13 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. preservation *) Module Raw (Import I:Int)(X: OrderedType). -Open Local Scope pair_scope. -Open Local Scope lazy_bool_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. +Local Notation int := I.t. Definition key := X.t. +Hint Transparent key. (** * Trees *) @@ -542,12 +542,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] @@ -604,12 +604,12 @@ Qed. Lemma lt_leaf : forall x, lt_tree x (Leaf elt). Proof. - unfold lt_tree in |- *; intros; intuition_in. + unfold lt_tree; intros; intuition_in. Qed. Lemma gt_leaf : forall x, gt_tree x (Leaf elt). Proof. - unfold gt_tree in |- *; intros; intuition_in. + unfold gt_tree; intros; intuition_in. Qed. Lemma lt_tree_node : forall x y l r e h, @@ -823,7 +823,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 +1113,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 +1333,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). @@ -1389,8 +1389,8 @@ Lemma fold_equiv_aux : L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a). Proof. simple induction s. - simpl in |- *; intuition. - simpl in |- *; intros. + simpl; intuition. + simpl; intros. rewrite H. simpl. apply H0. @@ -1400,11 +1400,11 @@ Lemma fold_equiv : forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A), fold f s a = fold' f s a. Proof. - unfold fold', elements in |- *. - simple induction s; simpl in |- *; auto; intros. + unfold fold', elements. + simple induction s; simpl; auto; intros. rewrite fold_equiv_aux. rewrite H0. - simpl in |- *; auto. + simpl; auto. Qed. Lemma fold_1 : 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..e1c60351 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]. @@ -36,8 +34,8 @@ Module AvlProofs (Import I:Int)(X: OrderedType). Module Import Raw := Raw I X. Module Import II:=MoreInt(I). Import Raw.Proofs. -Open Local Scope pair_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope Int_scope. Ltac omega_max := i2z_refl; romega with Z. 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..c59f7c22 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -6,14 +6,12 @@ (* * 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. Set Implicit Arguments. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. @@ -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..1ac544e1 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 @@ -46,7 +44,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. Definition add : forall (x : elt) (s : t), {s' : t | Add x s s'}. Proof. intros; exists (add x s); auto. - unfold Add in |- *; intuition. + unfold Add; intuition. elim (E.eq_dec x y); auto. intros; right. eapply add_3; eauto. @@ -133,7 +131,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}), compat_P E.eq P -> compat_bool E.eq (fdec Pdec). Proof. - unfold compat_P, compat_bool, Proper, respectful, fdec in |- *; intros. + unfold compat_P, compat_bool, Proper, respectful, fdec; intros. generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder. Qed. @@ -149,11 +147,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intuition. eauto with set. generalize (filter_2 H0 H1). - unfold fdec in |- *. + unfold fdec. case (Pdec x); intuition. inversion H2. apply filter_3; auto. - unfold fdec in |- *; simpl in |- *. + unfold fdec; simpl. case (Pdec x); intuition. Qed. @@ -164,17 +162,17 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intros. generalize (for_all_1 (s:=s) (f:=fdec Pdec)) (for_all_2 (s:=s) (f:=fdec Pdec)). - case (for_all (fdec Pdec) s); unfold For_all in |- *; [ left | right ]; + case (for_all (fdec Pdec) s); unfold For_all; [ left | right ]; intros. assert (compat_bool E.eq (fdec Pdec)); auto. - generalize (H0 H3 (refl_equal _) _ H2). - unfold fdec in |- *. + generalize (H0 H3 Logic.eq_refl _ H2). + unfold fdec. case (Pdec x); intuition. inversion H4. intuition. absurd (false = true); [ auto with bool | apply H; auto ]. intro. - unfold fdec in |- *. + unfold fdec. case (Pdec x); intuition. Qed. @@ -185,19 +183,19 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intros. generalize (exists_1 (s:=s) (f:=fdec Pdec)) (exists_2 (s:=s) (f:=fdec Pdec)). - case (exists_ (fdec Pdec) s); unfold Exists in |- *; [ left | right ]; + case (exists_ (fdec Pdec) s); unfold Exists; [ left | right ]; intros. elim H0; auto; intros. exists x; intuition. generalize H4. - unfold fdec in |- *. + unfold fdec. case (Pdec x); intuition. inversion H2. intuition. elim H2; intros. absurd (false = true); [ auto with bool | apply H; auto ]. exists x; intuition. - unfold fdec in |- *. + unfold fdec. case (Pdec x); intuition. Qed. @@ -214,26 +212,26 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. exists (partition (fdec Pdec) s). generalize (partition_1 s (f:=fdec Pdec)) (partition_2 s (f:=fdec Pdec)). case (partition (fdec Pdec) s). - intros s1 s2; simpl in |- *. + intros s1 s2; simpl. intros; assert (compat_bool E.eq (fdec Pdec)); auto. intros; assert (compat_bool E.eq (fun x => negb (fdec Pdec x))). - generalize H2; unfold compat_bool, Proper, respectful in |- *; intuition; + generalize H2; unfold compat_bool, Proper, respectful; intuition; apply (f_equal negb); auto. intuition. - generalize H4; unfold For_all, Equal in |- *; intuition. + generalize H4; unfold For_all, Equal; intuition. elim (H0 x); intros. assert (fdec Pdec x = true). eapply filter_2; eauto with set. - generalize H8; unfold fdec in |- *; case (Pdec x); intuition. + generalize H8; unfold fdec; case (Pdec x); intuition. inversion H9. - generalize H; unfold For_all, Equal in |- *; intuition. + generalize H; unfold For_all, Equal; intuition. elim (H0 x); intros. cut ((fun x => negb (fdec Pdec x)) x = true). - unfold fdec in |- *; case (Pdec x); intuition. - change ((fun x => negb (fdec Pdec x)) x = true) in |- *. + unfold fdec; case (Pdec x); intuition. + change ((fun x => negb (fdec Pdec x)) x = true). apply (filter_2 (s:=s) (x:=x)); auto. - set (b := fdec Pdec x) in *; generalize (refl_equal b); - pattern b at -1 in |- *; case b; unfold b in |- *; + set (b := fdec Pdec x) in *; generalize (Logic.eq_refl b); + pattern b at -1; case b; unfold b; [ left | right ]. elim (H4 x); intros _ B; apply B; auto with set. elim (H x); intros _ B; apply B; auto with set. @@ -310,7 +308,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intros; generalize (min_elt_1 (s:=s)) (min_elt_2 (s:=s)) (min_elt_3 (s:=s)). case (min_elt s); [ left | right ]; auto. - exists e; unfold For_all in |- *; eauto. + exists e; unfold For_all; eauto. Qed. Definition max_elt : @@ -320,7 +318,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intros; generalize (max_elt_1 (s:=s)) (max_elt_2 (s:=s)) (max_elt_3 (s:=s)). case (max_elt s); [ left | right ]; auto. - exists e; unfold For_all in |- *; eauto. + exists e; unfold For_all; eauto. Qed. Definition elt := elt. @@ -362,7 +360,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma empty_1 : Empty empty. Proof. - unfold empty in |- *; case M.empty; auto. + unfold empty; case M.empty; auto. Qed. Definition is_empty (s : t) : bool := @@ -370,12 +368,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true. Proof. - intros; unfold is_empty in |- *; case (M.is_empty s); auto. + intros; unfold is_empty; case (M.is_empty s); auto. Qed. Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s. Proof. - intro s; unfold is_empty in |- *; case (M.is_empty s); auto. + intro s; unfold is_empty; case (M.is_empty s); auto. intros; discriminate H. Qed. @@ -384,12 +382,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma mem_1 : forall (s : t) (x : elt), In x s -> mem x s = true. Proof. - intros; unfold mem in |- *; case (M.mem x s); auto. + intros; unfold mem; case (M.mem x s); auto. Qed. Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s. Proof. - intros s x; unfold mem in |- *; case (M.mem x s); auto. + intros s x; unfold mem; case (M.mem x s); auto. intros; discriminate H. Qed. @@ -400,12 +398,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma equal_1 : forall s s' : t, Equal s s' -> equal s s' = true. Proof. - intros; unfold equal in |- *; case M.equal; intuition. + intros; unfold equal; case M.equal; intuition. Qed. Lemma equal_2 : forall s s' : t, equal s s' = true -> Equal s s'. Proof. - intros s s'; unfold equal in |- *; case (M.equal s s'); intuition; + intros s s'; unfold equal; case (M.equal s s'); intuition; inversion H. Qed. @@ -414,12 +412,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma subset_1 : forall s s' : t, Subset s s' -> subset s s' = true. Proof. - intros; unfold subset in |- *; case M.subset; intuition. + intros; unfold subset; case M.subset; intuition. Qed. Lemma subset_2 : forall s s' : t, subset s s' = true -> Subset s s'. Proof. - intros s s'; unfold subset in |- *; case (M.subset s s'); intuition; + intros s s'; unfold subset; case (M.subset s s'); intuition; inversion H. Qed. @@ -431,14 +429,14 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma choose_1 : forall (s : t) (x : elt), choose s = Some x -> In x s. Proof. - intros s x; unfold choose in |- *; case (M.choose s). + intros s x; unfold choose; case (M.choose s). simple destruct s0; intros; injection H; intros; subst; auto. intros; discriminate H. Qed. Lemma choose_2 : forall s : t, choose s = None -> Empty s. Proof. - intro s; unfold choose in |- *; case (M.choose s); auto. + intro s; unfold choose; case (M.choose s); auto. simple destruct s0; intros; discriminate H. Qed. @@ -455,17 +453,17 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma elements_1 : forall (s : t) (x : elt), In x s -> InA E.eq x (elements s). Proof. - intros; unfold elements in |- *; case (M.elements s); firstorder. + intros; unfold elements; case (M.elements s); firstorder. Qed. Lemma elements_2 : forall (s : t) (x : elt), InA E.eq x (elements s) -> In x s. Proof. - intros s x; unfold elements in |- *; case (M.elements s); firstorder. + intros s x; unfold elements; case (M.elements s); firstorder. Qed. Lemma elements_3 : forall s : t, sort E.lt (elements s). Proof. - intros; unfold elements in |- *; case (M.elements s); firstorder. + intros; unfold elements; case (M.elements s); firstorder. Qed. Hint Resolve elements_3. @@ -480,7 +478,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s. Proof. - intros s x; unfold min_elt in |- *; case (M.min_elt s). + intros s x; unfold min_elt; case (M.min_elt s). simple destruct s0; intros; injection H; intros; subst; intuition. intros; discriminate H. Qed. @@ -488,15 +486,15 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma min_elt_2 : forall (s : t) (x y : elt), min_elt s = Some x -> In y s -> ~ E.lt y x. Proof. - intros s x y; unfold min_elt in |- *; case (M.min_elt s). - unfold For_all in |- *; simple destruct s0; intros; injection H; intros; + intros s x y; unfold min_elt; case (M.min_elt s). + unfold For_all; simple destruct s0; intros; injection H; intros; subst; firstorder. intros; discriminate H. Qed. Lemma min_elt_3 : forall s : t, min_elt s = None -> Empty s. Proof. - intros s; unfold min_elt in |- *; case (M.min_elt s); auto. + intros s; unfold min_elt; case (M.min_elt s); auto. simple destruct s0; intros; discriminate H. Qed. @@ -508,7 +506,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma max_elt_1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s. Proof. - intros s x; unfold max_elt in |- *; case (M.max_elt s). + intros s x; unfold max_elt; case (M.max_elt s). simple destruct s0; intros; injection H; intros; subst; intuition. intros; discriminate H. Qed. @@ -516,15 +514,15 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma max_elt_2 : forall (s : t) (x y : elt), max_elt s = Some x -> In y s -> ~ E.lt x y. Proof. - intros s x y; unfold max_elt in |- *; case (M.max_elt s). - unfold For_all in |- *; simple destruct s0; intros; injection H; intros; + intros s x y; unfold max_elt; case (M.max_elt s). + unfold For_all; simple destruct s0; intros; injection H; intros; subst; firstorder. intros; discriminate H. Qed. Lemma max_elt_3 : forall s : t, max_elt s = None -> Empty s. Proof. - intros s; unfold max_elt in |- *; case (M.max_elt s); auto. + intros s; unfold max_elt; case (M.max_elt s); auto. simple destruct s0; intros; discriminate H. Qed. @@ -532,20 +530,20 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma add_1 : forall (s : t) (x y : elt), E.eq x y -> In y (add x s). Proof. - intros; unfold add in |- *; case (M.add x s); unfold Add in |- *; + intros; unfold add; case (M.add x s); unfold Add; firstorder. Qed. Lemma add_2 : forall (s : t) (x y : elt), In y s -> In y (add x s). Proof. - intros; unfold add in |- *; case (M.add x s); unfold Add in |- *; + intros; unfold add; case (M.add x s); unfold Add; firstorder. Qed. Lemma add_3 : forall (s : t) (x y : elt), ~ E.eq x y -> In y (add x s) -> In y s. Proof. - intros s x y; unfold add in |- *; case (M.add x s); unfold Add in |- *; + intros s x y; unfold add; case (M.add x s); unfold Add; firstorder. Qed. @@ -553,30 +551,30 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma remove_1 : forall (s : t) (x y : elt), E.eq x y -> ~ In y (remove x s). Proof. - intros; unfold remove in |- *; case (M.remove x s); firstorder. + intros; unfold remove; case (M.remove x s); firstorder. Qed. Lemma remove_2 : forall (s : t) (x y : elt), ~ E.eq x y -> In y s -> In y (remove x s). Proof. - intros; unfold remove in |- *; case (M.remove x s); firstorder. + intros; unfold remove; case (M.remove x s); firstorder. Qed. Lemma remove_3 : forall (s : t) (x y : elt), In y (remove x s) -> In y s. Proof. - intros s x y; unfold remove in |- *; case (M.remove x s); firstorder. + intros s x y; unfold remove; case (M.remove x s); firstorder. Qed. Definition singleton (x : elt) : t := let (s, _) := singleton x in s. Lemma singleton_1 : forall x y : elt, In y (singleton x) -> E.eq x y. Proof. - intros x y; unfold singleton in |- *; case (M.singleton x); firstorder. + intros x y; unfold singleton; case (M.singleton x); firstorder. Qed. Lemma singleton_2 : forall x y : elt, E.eq x y -> In y (singleton x). Proof. - intros x y; unfold singleton in |- *; case (M.singleton x); firstorder. + intros x y; unfold singleton; case (M.singleton x); firstorder. Qed. Definition union (s s' : t) : t := let (s'', _) := union s s' in s''. @@ -584,60 +582,60 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Lemma union_1 : forall (s s' : t) (x : elt), In x (union s s') -> In x s \/ In x s'. Proof. - intros s s' x; unfold union in |- *; case (M.union s s'); firstorder. + intros s s' x; unfold union; case (M.union s s'); firstorder. Qed. Lemma union_2 : forall (s s' : t) (x : elt), In x s -> In x (union s s'). Proof. - intros s s' x; unfold union in |- *; case (M.union s s'); firstorder. + intros s s' x; unfold union; case (M.union s s'); firstorder. Qed. Lemma union_3 : forall (s s' : t) (x : elt), In x s' -> In x (union s s'). Proof. - intros s s' x; unfold union in |- *; case (M.union s s'); firstorder. + intros s s' x; unfold union; case (M.union s s'); firstorder. Qed. Definition inter (s s' : t) : t := let (s'', _) := inter s s' in s''. Lemma inter_1 : forall (s s' : t) (x : elt), In x (inter s s') -> In x s. Proof. - intros s s' x; unfold inter in |- *; case (M.inter s s'); firstorder. + intros s s' x; unfold inter; case (M.inter s s'); firstorder. Qed. Lemma inter_2 : forall (s s' : t) (x : elt), In x (inter s s') -> In x s'. Proof. - intros s s' x; unfold inter in |- *; case (M.inter s s'); firstorder. + intros s s' x; unfold inter; case (M.inter s s'); firstorder. Qed. Lemma inter_3 : forall (s s' : t) (x : elt), In x s -> In x s' -> In x (inter s s'). Proof. - intros s s' x; unfold inter in |- *; case (M.inter s s'); firstorder. + intros s s' x; unfold inter; case (M.inter s s'); firstorder. Qed. Definition diff (s s' : t) : t := let (s'', _) := diff s s' in s''. Lemma diff_1 : forall (s s' : t) (x : elt), In x (diff s s') -> In x s. Proof. - intros s s' x; unfold diff in |- *; case (M.diff s s'); firstorder. + intros s s' x; unfold diff; case (M.diff s s'); firstorder. Qed. Lemma diff_2 : forall (s s' : t) (x : elt), In x (diff s s') -> ~ In x s'. Proof. - intros s s' x; unfold diff in |- *; case (M.diff s s'); firstorder. + intros s s' x; unfold diff; case (M.diff s s'); firstorder. Qed. Lemma diff_3 : forall (s s' : t) (x : elt), In x s -> ~ In x s' -> In x (diff s s'). Proof. - intros s s' x; unfold diff in |- *; case (M.diff s s'); firstorder. + intros s s' x; unfold diff; case (M.diff s s'); firstorder. Qed. Definition cardinal (s : t) : nat := let (f, _) := cardinal s in f. Lemma cardinal_1 : forall s, cardinal s = length (elements s). Proof. - intros; unfold cardinal in |- *; case (M.cardinal s); unfold elements in *; + intros; unfold cardinal; case (M.cardinal s); unfold elements in *; destruct (M.elements s); auto. Qed. @@ -648,7 +646,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i. Proof. - intros; unfold fold in |- *; case (M.fold f s i); unfold elements in *; + intros; unfold fold; case (M.fold f s i); unfold elements in *; destruct (M.elements s); auto. Qed. @@ -675,7 +673,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> In x s. Proof. - intros s x f; unfold filter in |- *; case M.filter; intuition. + intros s x f; unfold filter; case M.filter; intuition. generalize (i (compat_P_aux H)); firstorder. Qed. @@ -683,7 +681,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> f x = true. Proof. - intros s x f; unfold filter in |- *; case M.filter; intuition. + intros s x f; unfold filter; case M.filter; intuition. generalize (i (compat_P_aux H)); firstorder. Qed. @@ -691,7 +689,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). Proof. - intros s x f; unfold filter in |- *; case M.filter; intuition. + intros s x f; unfold filter; case M.filter; intuition. generalize (i (compat_P_aux H)); firstorder. Qed. @@ -705,7 +703,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. Proof. - intros s f; unfold for_all in |- *; case M.for_all; intuition; elim n; + intros s f; unfold for_all; case M.for_all; intuition; elim n; auto. Qed. @@ -714,7 +712,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. Proof. - intros s f; unfold for_all in |- *; case M.for_all; intuition; + intros s f; unfold for_all; case M.for_all; intuition; inversion H0. Qed. @@ -727,7 +725,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (f : elt -> bool), compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. Proof. - intros s f; unfold exists_ in |- *; case M.exists_; intuition; elim n; + intros s f; unfold exists_; case M.exists_; intuition; elim n; auto. Qed. @@ -735,7 +733,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (f : elt -> bool), compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. Proof. - intros s f; unfold exists_ in |- *; case M.exists_; intuition; + intros s f; unfold exists_; case M.exists_; intuition; inversion H0. Qed. @@ -747,10 +745,10 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (f : elt -> bool), compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). Proof. - intros s f; unfold partition in |- *; case M.partition. + intros s f; unfold partition; case M.partition. intro p; case p; clear p; intros s1 s2 H C. generalize (H (compat_P_aux C)); clear H; intro H. - simpl in |- *; unfold Equal in |- *; intuition. + simpl; unfold Equal; intuition. apply filter_3; firstorder. elim (H2 a); intros. assert (In a s). @@ -765,13 +763,13 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (f : elt -> bool), compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). Proof. - intros s f; unfold partition in |- *; case M.partition. + intros s f; unfold partition; case M.partition. intro p; case p; clear p; intros s1 s2 H C. generalize (H (compat_P_aux C)); clear H; intro H. assert (D : compat_bool E.eq (fun x => negb (f x))). generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb); auto. - simpl in |- *; unfold Equal in |- *; intuition. + simpl; unfold Equal; intuition. apply filter_3; firstorder. elim (H2 a); intros. assert (In a s). 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..ac495c04 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 @@ -208,7 +206,7 @@ intros. generalize (@choose_1 s) (@choose_2 s). destruct (choose s);intros. exists e;auto with set. -generalize (H1 (refl_equal None)); clear H1. +generalize (H1 Logic.eq_refl); clear H1. intros; rewrite (is_empty_1 H1) in H; discriminate. Qed. @@ -633,7 +631,7 @@ destruct (choose (filter f s)). intros H0 _; apply exists_1; auto. exists e; generalize (H0 e); rewrite filter_iff; auto. intros _ H0. -rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate. +rewrite (is_empty_1 (H0 Logic.eq_refl)) in H; auto; discriminate. Qed. Lemma partition_filter_1: @@ -883,8 +881,8 @@ generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0 assert (~ In x (filter f s0)). intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. case (f x); simpl; intros. -rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto. -rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto. +rewrite (MP.cardinal_2 H1 (H2 Logic.eq_refl (MP.Add_add s0 x))); auto. +rewrite <- (MP.Equal_cardinal (H3 Logic.eq_refl (MP.Add_add s0 x))); auto. intros; rewrite fold_empty;auto. rewrite MP.cardinal_1; auto. unfold Empty; intros. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 45b43d83..b240ede4 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 @@ -317,11 +315,11 @@ symmetry. rewrite <- H1; intros a Ha. rewrite <- (H a) in Ha. destruct H0 as (_,H0). -exact (H0 (refl_equal true) _ Ha). +exact (H0 Logic.eq_refl _ Ha). rewrite <- H0; intros a Ha. rewrite (H a) in Ha. destruct H1 as (_,H1). -exact (H1 (refl_equal true) _ Ha). +exact (H1 Logic.eq_refl _ Ha). Qed. Instance Empty_m : Proper (Equal ==> iff) Empty. @@ -491,5 +489,3 @@ End WFacts_fun. Module WFacts (M:WS) := WFacts_fun M.E M. Module Facts := WFacts. - - 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..d53ce0c8 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 @@ -820,7 +823,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). rewrite (inter_subset_equal H). generalize (@cardinal_inv_1 (diff s' s)). destruct (cardinal (diff s' s)). - intro H2; destruct (H2 (refl_equal _) x). + intro H2; destruct (H2 Logic.eq_refl x). set_iff; auto. intros _. change (0 + cardinal s < S n + cardinal s). @@ -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. |