diff options
Diffstat (limited to 'theories')
-rw-r--r-- | theories/FSets/FMapFacts.v | 106 | ||||
-rw-r--r-- | theories/FSets/FMapInterface.v | 19 | ||||
-rw-r--r-- | theories/FSets/FMapWeakFacts.v | 70 | ||||
-rw-r--r-- | theories/FSets/FMapWeakInterface.v | 17 | ||||
-rw-r--r-- | theories/FSets/FSetBridge.v | 22 | ||||
-rw-r--r-- | theories/FSets/FSetEqProperties.v | 56 | ||||
-rw-r--r-- | theories/FSets/FSetFacts.v | 7 | ||||
-rw-r--r-- | theories/FSets/FSetInterface.v | 32 | ||||
-rw-r--r-- | theories/FSets/FSetProperties.v | 32 | ||||
-rw-r--r-- | theories/FSets/FSetWeakInterface.v | 27 | ||||
-rw-r--r-- | theories/FSets/FSetWeakProperties.v | 14 |
11 files changed, 208 insertions, 194 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index b119f27ce..0906099de 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -114,9 +114,9 @@ intros. intuition. destruct (eq_dec x y); [left|right]. split; auto. -symmetry; apply (MapsTo_fun (e':=e) H); auto. +symmetry; apply (MapsTo_fun (e':=e) H); auto with map. split; auto; apply add_3 with x e; auto. -subst; auto. +subst; auto with map. Qed. Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m. @@ -204,27 +204,27 @@ split. case_eq (find x m); intros. exists e. split. -apply (MapsTo_fun (m:=map f m) (x:=x)); auto. -apply find_2; auto. +apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map. +apply find_2; auto with map. assert (In x (map f m)) by (exists b; auto). destruct (map_2 H1) as (a,H2). rewrite (find_1 H2) in H; discriminate. intros (a,(H,H0)). -subst b; auto. +subst b; auto with map. Qed. Lemma map_in_iff : forall m x (f : elt -> elt'), In x (map f m) <-> In x m. Proof. -split; intros; eauto. +split; intros; eauto with map. destruct H as (a,H). -exists (f a); auto. +exists (f a); auto with map. Qed. Lemma mapi_in_iff : forall m x (f:key->elt->elt'), In x (mapi f m) <-> In x m. Proof. -split; intros; eauto. +split; intros; eauto with map. destruct H as (a,H). destruct (mapi_1 f H) as (y,(H0,H1)). exists (f y a); auto. @@ -240,9 +240,9 @@ Proof. intros; case_eq (find x m); intros. exists e. destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)). -apply find_2; auto. -exists y; repeat split; auto. -apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto. +apply find_2; auto with map. +exists y; repeat split; auto with map. +apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map. assert (In x (mapi f m)) by (exists b; auto). destruct (mapi_2 H1) as (a,H2). rewrite (find_1 H2) in H0; discriminate. @@ -345,24 +345,24 @@ Qed. Lemma add_eq_o : forall m x y e, E.eq x y -> find y (add x e m) = Some e. Proof. -auto. +auto with map. Qed. Lemma add_neq_o : forall m x y e, ~ E.eq x y -> find y (add x e m) = find y m. Proof. intros. -case_eq (find y m); intros; auto. -case_eq (find y (add x e m)); intros; auto. +case_eq (find y m); intros; auto with map. +case_eq (find y (add x e m)); intros; auto with map. rewrite <- H0; symmetry. -apply find_1; apply add_3 with x e; auto. +apply find_1; apply add_3 with x e; auto with map. Qed. -Hint Resolve add_neq_o. +Hint Resolve add_neq_o : map. Lemma add_o : forall m x y e, find y (add x e m) = if eq_dec x y then Some e else find y m. Proof. -intros; destruct (eq_dec x y); auto. +intros; destruct (eq_dec x y); auto with map. Qed. Lemma add_eq_b : forall m x y e, @@ -394,23 +394,23 @@ destruct (find y (remove x m)); auto. destruct 2. exists e; rewrite H0; auto. Qed. -Hint Resolve remove_eq_o. +Hint Resolve remove_eq_o : map. Lemma remove_neq_o : forall m x y, ~ E.eq x y -> find y (remove x m) = find y m. Proof. intros. -case_eq (find y m); intros; auto. -case_eq (find y (remove x m)); intros; auto. +case_eq (find y m); intros; auto with map. +case_eq (find y (remove x m)); intros; auto with map. rewrite <- H0; symmetry. -apply find_1; apply remove_3 with x; auto. +apply find_1; apply remove_3 with x; auto with map. Qed. -Hint Resolve remove_neq_o. +Hint Resolve remove_neq_o : map. Lemma remove_o : forall m x y, find y (remove x m) = if eq_dec x y then None else find y m. Proof. -intros; destruct (eq_dec x y); auto. +intros; destruct (eq_dec x y); auto with map. Qed. Lemma remove_eq_b : forall m x y, @@ -495,14 +495,14 @@ intros. case_eq (find x m); intros. rewrite <- H0. apply map2_1; auto. -left; exists e; auto. +left; exists e; auto with map. case_eq (find x m'); intros. rewrite <- H0; rewrite <- H1. apply map2_1; auto. -right; exists e; auto. +right; exists e; auto with map. rewrite H. -case_eq (find x (map2 f m m')); intros; auto. -assert (In x (map2 f m m')) by (exists e; auto). +case_eq (find x (map2 f m m')); intros; auto with map. +assert (In x (map2 f m m')) by (exists e; auto with map). destruct (map2_2 H3) as [(e0,H4)|(e0,H4)]. rewrite (find_1 H4) in H0; discriminate. rewrite (find_1 H4) in H1; discriminate. @@ -647,13 +647,13 @@ Module Properties (M: S). unfold leb; f_equal; apply gtb_compat; auto. Qed. - Hint Resolve gtb_compat leb_compat elements_3. + Hint Resolve gtb_compat leb_compat elements_3 : map. Lemma elements_split : forall p m, elements m = elements_lt p m ++ elements_ge p m. Proof. unfold elements_lt, elements_ge, leb; intros. - apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto. + apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with map. intros; destruct x; destruct y; destruct p. rewrite gtb_1 in H; unfold O.ltk in H; simpl in *. assert (~ltk (t1,e0) (k,e1)). @@ -667,15 +667,15 @@ Module Properties (M: S). (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m). Proof. intros; unfold elements_lt, elements_ge. - apply sort_equivlistA_eqlistA; auto. - apply (@SortA_app _ eqke); auto. - apply (@filter_sort _ eqke); auto; clean_eauto. - constructor; auto. - apply (@filter_sort _ eqke); auto; clean_eauto. - rewrite (@InfA_alt _ eqke); auto; try (clean_eauto; fail). - apply (@filter_sort _ eqke); auto; clean_eauto. + apply sort_equivlistA_eqlistA; auto with map. + apply (@SortA_app _ eqke); auto with map. + apply (@filter_sort _ eqke); auto with map; clean_eauto. + constructor; auto with map. + apply (@filter_sort _ eqke); auto with map; clean_eauto. + rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail). + apply (@filter_sort _ eqke); auto with map; clean_eauto. intros. - rewrite filter_InA in H1; auto; destruct H1. + rewrite filter_InA in H1; auto with map; destruct H1. rewrite leb_1 in H2. destruct y; unfold O.ltk in *; simpl in *. rewrite <- elements_mapsto_iff in H1. @@ -684,18 +684,18 @@ Module Properties (M: S). exists e0; apply MapsTo_1 with t0; auto. ME.order. intros. - rewrite filter_InA in H1; auto; destruct H1. + rewrite filter_InA in H1; auto with map; destruct H1. rewrite gtb_1 in H3. destruct y; destruct x0; unfold O.ltk in *; simpl in *. inversion_clear H2. red in H4; simpl in *; destruct H4. ME.order. - rewrite filter_InA in H4; auto; destruct H4. + rewrite filter_InA in H4; auto with map; destruct H4. rewrite leb_1 in H4. unfold O.ltk in *; simpl in *; ME.order. red; intros a; destruct a. rewrite InA_app_iff; rewrite InA_cons. - do 2 (rewrite filter_InA; auto). + do 2 (rewrite filter_InA; auto with map). do 2 rewrite <- elements_mapsto_iff. rewrite leb_1; rewrite gtb_1. rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff. @@ -716,8 +716,8 @@ Module Properties (M: S). eqlistA eqke (elements m') (elements m ++ (x,e)::nil). Proof. intros. - apply sort_equivlistA_eqlistA; auto. - apply (@SortA_app _ eqke); auto. + apply sort_equivlistA_eqlistA; auto with map. + apply (@SortA_app _ eqke); auto with map. intros. inversion_clear H2. destruct x0; destruct y. @@ -745,9 +745,9 @@ Module Properties (M: S). eqlistA eqke (elements m') ((x,e)::elements m). Proof. intros. - apply sort_equivlistA_eqlistA; auto. + apply sort_equivlistA_eqlistA; auto with map. change (sort ltk (((x,e)::nil) ++ elements m)). - apply (@SortA_app _ eqke); auto. + apply (@SortA_app _ eqke); auto with map. intros. inversion_clear H1. destruct y; destruct x0. @@ -774,7 +774,7 @@ Module Properties (M: S). Equal m m' -> eqlistA eqke (elements m) (elements m'). Proof. intros. - apply sort_equivlistA_eqlistA; auto. + apply sort_equivlistA_eqlistA; auto with map. red; intros. destruct x; do 2 rewrite <- elements_mapsto_iff. do 2 rewrite find_mapsto_iff; rewrite H; split; auto. @@ -978,12 +978,12 @@ Module Properties (M: S). destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *. assert (Add x e (remove x m) m). red; intros. - rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto. - apply X0 with (remove x m) x e; auto. - apply IHn; auto. + rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto with map. + apply X0 with (remove x m) x e; auto with map. + apply IHn; auto with map. assert (S n = S (cardinal (remove x m))). - rewrite Heqn; eapply cardinal_2; eauto. - inversion H1; auto. + rewrite Heqn; eapply cardinal_2; eauto with map. + inversion H1; auto with map. Qed. Lemma map_induction_max : @@ -1002,11 +1002,11 @@ Module Properties (M: S). rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto. apply find_1; apply MapsTo_1 with k; auto. apply max_elt_MapsTo; auto. - apply X0 with (remove k m) k e; auto. + apply X0 with (remove k m) k e; auto with map. apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto. + eapply cardinal_2; eauto with map. inversion H1; auto. eapply max_elt_Above; eauto. @@ -1033,7 +1033,7 @@ Module Properties (M: S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto. + eapply cardinal_2; eauto with map. inversion H1; auto. eapply min_elt_Below; eauto. diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 0bd2c4525..d4e07461c 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -12,12 +12,9 @@ (** This file proposes an interface for finite maps *) -(* begin hide *) -Require Export Bool. -Require Export OrderedType. +Require Export Bool OrderedType. Set Implicit Arguments. Unset Strict Implicit. -(* end hide *) (** When compared with Ocaml Map, this signature has been split in two: - The first part [S] contains the usual operators (add, find, ...) @@ -206,12 +203,14 @@ Module Type S. (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. - (* begin hide *) - Hint Immediate MapsTo_1 mem_2 is_empty_2. - - Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 add_3 remove_1 - remove_2 remove_3 find_1 find_2 fold_1 map_1 map_2 mapi_1 mapi_2. - (* end hide *) + Hint Immediate MapsTo_1 mem_2 is_empty_2 + map_2 mapi_2 add_3 remove_3 find_2 + : map. + Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 + remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 + : map. + (** for compatibility with earlier hints *) + Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap. End S. diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v index 180df008e..e0f5e1c93 100644 --- a/theories/FSets/FMapWeakFacts.v +++ b/theories/FSets/FMapWeakFacts.v @@ -112,9 +112,9 @@ intros. intuition. destruct (E.eq_dec x y); [left|right]. split; auto. -symmetry; apply (MapsTo_fun (e':=e) H); auto. +symmetry; apply (MapsTo_fun (e':=e) H); auto with map. split; auto; apply add_3 with x e; auto. -subst; auto. +subst; auto with map. Qed. Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m. @@ -202,27 +202,27 @@ split. case_eq (find x m); intros. exists e. split. -apply (MapsTo_fun (m:=map f m) (x:=x)); auto. -apply find_2; auto. +apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map. +apply find_2; auto with map. assert (In x (map f m)) by (exists b; auto). destruct (map_2 H1) as (a,H2). rewrite (find_1 H2) in H; discriminate. intros (a,(H,H0)). -subst b; auto. +subst b; auto with map. Qed. Lemma map_in_iff : forall m x (f : elt -> elt'), In x (map f m) <-> In x m. Proof. -split; intros; eauto. +split; intros; eauto with map. destruct H as (a,H). -exists (f a); auto. +exists (f a); auto with map. Qed. Lemma mapi_in_iff : forall m x (f:key->elt->elt'), In x (mapi f m) <-> In x m. Proof. -split; intros; eauto. +split; intros; eauto with map. destruct H as (a,H). destruct (mapi_1 f H) as (y,(H0,H1)). exists (f y a); auto. @@ -238,9 +238,9 @@ Proof. intros; case_eq (find x m); intros. exists e. destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)). -apply find_2; auto. -exists y; repeat split; auto. -apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto. +apply find_2; auto with map. +exists y; repeat split; auto with map. +apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map. assert (In x (mapi f m)) by (exists b; auto). destruct (mapi_2 H1) as (a,H2). rewrite (find_1 H2) in H0; discriminate. @@ -345,24 +345,24 @@ Qed. Lemma add_eq_o : forall m x y e, E.eq x y -> find y (add x e m) = Some e. Proof. -auto. +auto with map. Qed. Lemma add_neq_o : forall m x y e, ~ E.eq x y -> find y (add x e m) = find y m. Proof. intros. -case_eq (find y m); intros; auto. -case_eq (find y (add x e m)); intros; auto. +case_eq (find y m); intros; auto with map. +case_eq (find y (add x e m)); intros; auto with map. rewrite <- H0; symmetry. -apply find_1; apply add_3 with x e; auto. +apply find_1; apply add_3 with x e; auto with map. Qed. -Hint Resolve add_neq_o. +Hint Resolve add_neq_o : map. Lemma add_o : forall m x y e, find y (add x e m) = if E.eq_dec x y then Some e else find y m. Proof. -intros; destruct (E.eq_dec x y); auto. +intros; destruct (E.eq_dec x y); auto with map. Qed. Lemma add_eq_b : forall m x y e, @@ -394,23 +394,23 @@ destruct (find y (remove x m)); auto. destruct 2. exists e; rewrite H0; auto. Qed. -Hint Resolve remove_eq_o. +Hint Resolve remove_eq_o : map. Lemma remove_neq_o : forall m x y, ~ E.eq x y -> find y (remove x m) = find y m. Proof. intros. -case_eq (find y m); intros; auto. -case_eq (find y (remove x m)); intros; auto. +case_eq (find y m); intros; auto with map. +case_eq (find y (remove x m)); intros; auto with map. rewrite <- H0; symmetry. -apply find_1; apply remove_3 with x; auto. +apply find_1; apply remove_3 with x; auto with map. Qed. -Hint Resolve remove_neq_o. +Hint Resolve remove_neq_o : map. Lemma remove_o : forall m x y, find y (remove x m) = if E.eq_dec x y then None else find y m. Proof. -intros; destruct (E.eq_dec x y); auto. +intros; destruct (E.eq_dec x y); auto with map. Qed. Lemma remove_eq_b : forall m x y, @@ -494,15 +494,15 @@ Proof. intros. case_eq (find x m); intros. rewrite <- H0. -apply map2_1; auto. -left; exists e; auto. +apply map2_1; auto with map. +left; exists e; auto with map. case_eq (find x m'); intros. rewrite <- H0; rewrite <- H1. apply map2_1; auto. -right; exists e; auto. +right; exists e; auto with map. rewrite H. -case_eq (find x (map2 f m m')); intros; auto. -assert (In x (map2 f m m')) by (exists e; auto). +case_eq (find x (map2 f m m')); intros; auto with map. +assert (In x (map2 f m m')) by (exists e; auto with map). destruct (map2_2 H3) as [(e0,H4)|(e0,H4)]. rewrite (find_1 H4) in H0; discriminate. rewrite (find_1 H4) in H1; discriminate. @@ -667,7 +667,7 @@ Module Properties (M: S). inversion H3; auto. f_equal; auto. elim H1. - exists b; apply MapsTo_1 with a; auto. + exists b; apply MapsTo_1 with a; auto with map. elim n; auto. Qed. @@ -710,7 +710,7 @@ Module Properties (M: S). red; inversion 1. inversion H. Qed. - Hint Resolve cardinal_inv_1. + Hint Resolve cardinal_inv_1 : map. Lemma cardinal_inv_2 : forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. @@ -735,12 +735,12 @@ Module Properties (M: S). destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *. assert (Add x e (remove x m) m). red; intros. - rewrite add_o; rewrite remove_o; destruct (E.eq_dec x y); eauto. - apply X0 with (remove x m) x e; auto. - apply IHn; auto. + rewrite add_o; rewrite remove_o; destruct (E.eq_dec x y); eauto with map. + apply X0 with (remove x m) x e; auto with map. + apply IHn; auto with map. assert (S n = S (cardinal (remove x m))). - rewrite Heqn; eapply cardinal_2; eauto. - inversion H1; auto. + rewrite Heqn; eapply cardinal_2; eauto with map. + inversion H1; auto with map. Qed. End Elt. diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v index 5a9d3cca6..c4bfad59a 100644 --- a/theories/FSets/FMapWeakInterface.v +++ b/theories/FSets/FMapWeakInterface.v @@ -13,12 +13,9 @@ (** This file proposes an interface for finite maps over keys with decidable equality, but no decidable order. *) -(* begin hide *) -Require Export Bool. -Require Export DecidableType. +Require Export Bool DecidableType. Set Implicit Arguments. Unset Strict Implicit. -(* end hide *) Module Type S. @@ -195,9 +192,13 @@ Module Type S. (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. - Hint Immediate MapsTo_1 mem_2 is_empty_2. - - Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 add_3 remove_1 - remove_2 remove_3 find_1 find_2 fold_1 map_1 map_2 mapi_1 mapi_2. + Hint Immediate MapsTo_1 mem_2 is_empty_2 + map_2 mapi_2 add_3 remove_3 find_2 + : map. + Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 + remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 + : map. + (** for compatibility with earlier hints *) + Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap. End S. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 55b00f063..c5656402f 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -27,7 +27,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Definition empty : {s : t | Empty s}. Proof. - exists empty; auto. + exists empty; auto with set. Qed. Definition is_empty : forall s : t, {Empty s} + {~ Empty s}. @@ -66,12 +66,12 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. Proof. intros; exists (remove x s); intuition. - absurd (In x (remove x s)); auto. + absurd (In x (remove x s)); auto with set. apply In_1 with y; auto. elim (ME.eq_dec x y); intros; auto. - absurd (In x (remove x s)); auto. + absurd (In x (remove x s)); auto with set. apply In_1 with y; auto. - eauto. + eauto with set. Qed. Definition union : @@ -83,14 +83,14 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Definition inter : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}. Proof. - intros; exists (inter s s'); intuition; eauto. + intros; exists (inter s s'); intuition; eauto with set. Qed. Definition diff : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}. Proof. - intros; exists (diff s s'); intuition; eauto. - absurd (In x s'); eauto. + intros; exists (diff s s'); intuition; eauto with set. + absurd (In x s'); eauto with set. Qed. Definition equal : forall s s' : t, {Equal s s'} + {~ Equal s s'}. @@ -150,7 +150,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. exists (filter (fdec Pdec) s). intro H; assert (compat_bool E.eq (fdec Pdec)); auto. intuition. - eauto. + eauto with set. generalize (filter_2 H0 H1). unfold fdec in |- *. case (Pdec x); intuition. @@ -226,7 +226,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. generalize H4; unfold For_all, Equal in |- *; intuition. elim (H0 x); intros. assert (fdec Pdec x = true). - eauto. + eapply filter_2; eauto with set. generalize H8; unfold fdec in |- *; case (Pdec x); intuition. inversion H9. generalize H; unfold For_all, Equal in |- *; intuition. @@ -238,8 +238,8 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. set (b := fdec Pdec x) in *; generalize (refl_equal b); pattern b at -1 in |- *; case b; unfold b in |- *; [ left | right ]. - elim (H4 x); intros _ B; apply B; auto. - elim (H x); intros _ B; apply B; auto. + elim (H4 x); intros _ B; apply B; auto with set. + elim (H x); intros _ B; apply B; auto with set. apply filter_3; auto. rewrite H5; auto. eapply (filter_1 (s:=s) (x:=x) H2); elim (H4 x); intros B _; apply B; diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 9e1ca4058..4a99a44a3 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -76,7 +76,7 @@ Qed. Lemma empty_mem: mem x empty=false. Proof. -rewrite <- not_mem_iff; auto. +rewrite <- not_mem_iff; auto with set. Qed. Lemma is_empty_equal_empty: is_empty s = equal s empty. @@ -88,17 +88,17 @@ Qed. Lemma choose_mem_1: choose s=Some x -> mem x s=true. Proof. -auto. +auto with set. Qed. Lemma choose_mem_2: choose s=None -> is_empty s=true. Proof. -auto. +auto with set. Qed. Lemma add_mem_1: mem x (add x s)=true. Proof. -auto. +auto with set. Qed. Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s. @@ -108,7 +108,7 @@ Qed. Lemma remove_mem_1: mem x (remove x s)=false. Proof. -rewrite <- not_mem_iff; auto. +rewrite <- not_mem_iff; auto with set. Qed. Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s. @@ -216,7 +216,7 @@ Proof. intros. generalize (@choose_1 s) (@choose_2 s). destruct (choose s);intros. -exists e;auto. +exists e;auto with set. generalize (H1 (refl_equal None)); clear H1. intros; rewrite (is_empty_1 H1) in H; discriminate. Qed. @@ -233,7 +233,7 @@ Qed. Lemma add_mem_3: mem y s=true -> mem y (add x s)=true. Proof. -auto. +auto with set. Qed. Lemma add_equal: @@ -260,7 +260,7 @@ Qed. Lemma add_remove: mem x s=true -> equal (add x (remove x s)) s=true. Proof. -intros; apply equal_1; apply add_remove; auto. +intros; apply equal_1; apply add_remove; auto with set. Qed. Lemma remove_add: @@ -275,9 +275,9 @@ Qed. Lemma is_empty_cardinal: is_empty s = zerob (cardinal s). Proof. intros; apply bool_1; split; intros. -rewrite cardinal_1; simpl; auto. +rewrite cardinal_1; simpl; auto with set. assert (cardinal s = 0) by (apply zerob_true_elim; auto). -auto. +auto with set. Qed. (** Properties of [singleton] *) @@ -295,7 +295,7 @@ Qed. Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y. Proof. -auto. +intros; apply singleton_1; auto with set. Qed. (** Properties of [union] *) @@ -358,7 +358,7 @@ Lemma union_subset_3: subset s s''=true -> subset s' s''=true -> subset (union s s') s''=true. Proof. -intros; apply subset_1; apply union_subset_3; auto. +intros; apply subset_1; apply union_subset_3; auto with set. Qed. (** Properties of [inter] *) @@ -433,7 +433,7 @@ Lemma inter_subset_3: subset s'' s=true -> subset s'' s'=true -> subset s'' (inter s s')=true. Proof. -intros; apply subset_1; apply inter_subset_3; auto. +intros; apply subset_1; apply inter_subset_3; auto with set. Qed. (** Properties of [diff] *) @@ -516,7 +516,7 @@ Qed. Lemma fold_equal: equal s s'=true -> eqA (fold f s i) (fold f s' i). Proof. -intros; apply fold_equal with (eqA:=eqA); auto. +intros; apply fold_equal with (eqA:=eqA); auto with set. Qed. Lemma fold_add: @@ -529,13 +529,13 @@ Qed. Lemma add_fold: mem x s=true -> eqA (fold f (add x s) i) (fold f s i). Proof. -intros; apply add_fold with (eqA:=eqA); auto. +intros; apply add_fold with (eqA:=eqA); auto with set. Qed. Lemma remove_fold_1: mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i). Proof. -intros; apply remove_fold_1 with (eqA:=eqA); auto. +intros; apply remove_fold_1 with (eqA:=eqA); auto with set. Qed. Lemma remove_fold_2: @@ -573,13 +573,13 @@ Qed. Lemma remove_cardinal_1: forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s. Proof. -intros; apply remove_cardinal_1; auto. +intros; apply remove_cardinal_1; auto with set. Qed. Lemma remove_cardinal_2: forall s x, mem x s=false -> cardinal (remove x s)=cardinal s. Proof. -auto with set. +intros; apply Equal_cardinal; apply equal_2; auto with set. Qed. Lemma union_cardinal: @@ -593,7 +593,7 @@ Qed. Lemma subset_cardinal: forall s s', subset s s'=true -> cardinal s<=cardinal s'. Proof. -intros; apply subset_cardinal; auto. +intros; apply subset_cardinal; auto with set. Qed. Section Bool. @@ -636,7 +636,7 @@ Proof. intros; apply bool_1; split; intros. destruct (exists_2 Comp H) as (a,(Ha1,Ha2)). apply bool_6. -red; intros; apply (@is_empty_2 _ H0 a); auto. +red; intros; apply (@is_empty_2 _ H0 a); auto with set. generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)). destruct (choose (filter f s)). intros H0 _; apply exists_1; auto. @@ -648,13 +648,13 @@ Qed. Lemma partition_filter_1: forall s, equal (fst (partition f s)) (filter f s)=true. Proof. -auto. +auto with set. Qed. Lemma partition_filter_2: forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true. Proof. -auto. +auto with set. Qed. Lemma filter_add_1 : forall s x, f x = true -> @@ -912,13 +912,13 @@ trans_st (fold f s0 i). apply fold_equal with (eqA:=eqA); auto. rewrite equal_sym; auto. trans_st (fold g s0 i). -apply H0; intros; apply H1; auto. -elim (equal_2 H x); auto; intros. -apply fold_equal with (eqA:=eqA); auto. +apply H0; intros; apply H1; auto with set. +elim (equal_2 H x); auto with set; intros. +apply fold_equal with (eqA:=eqA); auto with set. trans_st (f x (fold f s0 i)). -apply fold_add with (eqA:=eqA); auto. -trans_st (g x (fold f s0 i)). -trans_st (g x (fold g s0 i)). +apply fold_add with (eqA:=eqA); auto with set. +trans_st (g x (fold f s0 i)); auto with set. +trans_st (g x (fold g s0 i)); auto with set. sym_st; apply fold_add with (eqA:=eqA); auto. trans_st i; [idtac | sym_st ]; apply fold_empty; auto. Qed. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index ac0227f5c..e83b861fb 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -258,7 +258,8 @@ apply H0; auto. symmetry. rewrite H0; intros. destruct H1 as (_,H1). -apply H1; auto. +apply H1; auto with set. +apply elements_2; auto with set. Qed. Lemma exists_b : compat_bool E.eq f -> @@ -271,7 +272,7 @@ destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. rewrite <- H1; intros. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); auto. -exists a; auto. +exists a; intuition; auto with set. symmetry. rewrite H0. destruct H1 as (_,H1). @@ -420,7 +421,7 @@ Add Relation t Subset Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. Proof. -unfold Subset, impl; intros; eauto. +unfold Subset, impl; intros; eauto with set. Qed. Add Morphism Empty with signature Subset --> impl as Empty_s_m. diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 012f95d87..ded81426d 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -12,12 +12,9 @@ (** Set interfaces *) -(* begin hide *) -Require Export Bool. -Require Export OrderedType. +Require Export Bool OrderedType. Set Implicit Arguments. Unset Strict Implicit. -(* end hide *) (** * Non-dependent signature @@ -273,16 +270,25 @@ Module Type S. End Spec. - (* begin hide *) - Hint Immediate In_1. + 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 + inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1 + partition_1 partition_2 elements_1 elements_3 + : set. + Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 + remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 + filter_1 filter_2 for_all_2 exists_2 elements_2 + min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 + : set. + (** for compatibility with earlier hints *) + Hint Resolve mem_2 equal_2 subset_2 is_empty_2 add_3 + remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 + filter_1 filter_2 for_all_2 exists_2 elements_2 + min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 + : oldset. - Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1 - is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1 - remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1 - inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1 - for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2 - elements_3 min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3. - (* end hide *) + End S. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 2070cf815..d6c978c05 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -239,7 +239,7 @@ Module Properties (M: S). Proof. unfold Equal; intros; set_iff. destruct (ME.eq_dec x a); intuition. - left; eauto. + left; eauto with set. Qed. Lemma union_subset_1 : s [<=] union s s'. @@ -525,7 +525,7 @@ Module Properties (M: S). elements s = elements_lt x s ++ elements_ge x s. Proof. unfold elements_lt, elements_ge, leb; intros. - eapply (@filter_split _ E.eq); eauto. ME.order. ME.order. ME.order. + eapply (@filter_split _ E.eq); eauto with set. ME.order. ME.order. ME.order. intros. rewrite gtb_1 in H. assert (~E.lt y x). @@ -537,13 +537,13 @@ Module Properties (M: S). eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s). Proof. intros; unfold elements_ge, elements_lt. - apply sort_equivlistA_eqlistA; auto. + apply sort_equivlistA_eqlistA; auto with set. apply (@SortA_app _ E.eq); auto. - apply (@filter_sort _ E.eq); auto; eauto. + apply (@filter_sort _ E.eq); auto with set; eauto with set. constructor; auto. - apply (@filter_sort _ E.eq); auto; eauto. + apply (@filter_sort _ E.eq); auto with set; eauto with set. rewrite Inf_alt; auto; intros. - apply (@filter_sort _ E.eq); auto; eauto. + apply (@filter_sort _ E.eq); auto with set; eauto with set. rewrite filter_InA in H1; auto; destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. @@ -574,8 +574,8 @@ Module Properties (M: S). eqlistA E.eq (elements s') (elements s ++ x::nil). Proof. intros. - apply sort_equivlistA_eqlistA; auto. - apply (@SortA_app _ E.eq); auto. + apply sort_equivlistA_eqlistA; auto with set. + apply (@SortA_app _ E.eq); auto with set. intros. inversion_clear H2. rewrite <- elements_iff in H1. @@ -591,9 +591,9 @@ Module Properties (M: S). eqlistA E.eq (elements s') (x::elements s). Proof. intros. - apply sort_equivlistA_eqlistA; auto. + apply sort_equivlistA_eqlistA; auto with set. change (sort E.lt ((x::nil) ++ elements s)). - apply (@SortA_app _ E.eq); auto. + apply (@SortA_app _ E.eq); auto with set. intros. inversion_clear H1. rewrite <- elements_iff in H2. @@ -615,7 +615,7 @@ Module Properties (M: S). intros. do 2 rewrite M.cardinal_1. apply (@eqlistA_length _ E.eq); auto. - apply sort_equivlistA_eqlistA; auto. + apply sort_equivlistA_eqlistA; auto with set. red; intro a. do 2 rewrite <- elements_iff; auto. Qed. @@ -755,7 +755,7 @@ Module Properties (M: S). fold f s i = fold_right f i l. Proof. intros; exists (rev (elements s)); split. - apply NoDupA_rev; auto. + apply NoDupA_rev; auto with set. exact E.eq_trans. split; intros. rewrite elements_iff; do 2 rewrite InA_alt. @@ -843,7 +843,7 @@ Module Properties (M: S). Lemma fold_empty : forall i, eqA (fold f empty i) i. Proof. - intros; apply fold_1; auto. + intros; apply fold_1; auto with set. Qed. Lemma fold_equal : @@ -853,7 +853,7 @@ Module Properties (M: S). do 2 rewrite <- fold_left_rev_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. - apply sort_equivlistA_eqlistA; auto. + apply sort_equivlistA_eqlistA; auto with set. red; intro a; do 2 rewrite <- elements_iff; auto. Qed. @@ -882,7 +882,7 @@ Module Properties (M: S). Proof. intros. sym_st. - apply fold_2 with (eqA:=eqA); auto. + apply fold_2 with (eqA:=eqA); auto with set. Qed. Lemma remove_fold_2: forall i s x, ~In x s -> @@ -983,7 +983,7 @@ Module Properties (M: S). Lemma empty_cardinal : cardinal empty = 0. Proof. - rewrite cardinal_fold; apply fold_1; auto. + rewrite cardinal_fold; apply fold_1; auto with set. Qed. Hint Immediate empty_cardinal cardinal_1 : set. diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v index 72084d034..3079ec871 100644 --- a/theories/FSets/FSetWeakInterface.v +++ b/theories/FSets/FSetWeakInterface.v @@ -12,8 +12,7 @@ (** Set interfaces for types with only a decidable equality, but no ordering *) -Require Export Bool. -Require Export DecidableType. +Require Export Bool DecidableType. Set Implicit Arguments. Unset Strict Implicit. @@ -229,13 +228,21 @@ Module Type S. End Spec. - Hint Immediate In_1. - - Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1 - is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1 - remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1 - inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1 - for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2 - elements_3. + 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 + inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1 + partition_1 partition_2 elements_1 elements_3 + : set. + Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 + remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 + filter_1 filter_2 for_all_2 exists_2 elements_2 + : set. + (* for compatibility with earlier hints *) + Hint Resolve In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 + remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 + filter_1 filter_2 for_all_2 exists_2 elements_2 + : oldset. + End S. diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v index 169543e32..07e087241 100644 --- a/theories/FSets/FSetWeakProperties.v +++ b/theories/FSets/FSetWeakProperties.v @@ -455,7 +455,7 @@ Module Properties (M: S). fold f s i = fold_right f i l. Proof. intros; exists (rev (elements s)); split. - apply NoDupA_rev; auto. + apply NoDupA_rev; auto with set. exact E.eq_trans. split; intros. rewrite elements_iff; do 2 rewrite InA_alt. @@ -583,9 +583,9 @@ Module Properties (M: S). Proof. simple induction n; intros; auto. destruct (cardinal_inv_2 H) as (x,H0). - apply X0 with (remove x s) x; auto. - apply X1; auto. - rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto. + apply X0 with (remove x s) x; auto with set. + apply X1; auto with set. + rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto with set. Qed. Lemma set_induction : @@ -608,7 +608,7 @@ Module Properties (M: S). Lemma fold_empty : eqA (fold f empty i) i. Proof. - apply fold_1; auto. + apply fold_1; auto with set. Qed. Lemma fold_equal : @@ -643,7 +643,7 @@ Module Properties (M: S). Proof. intros. sym_st. - apply fold_2 with (eqA:=eqA); auto. + apply fold_2 with (eqA:=eqA); auto with set. Qed. Lemma remove_fold_2: forall s x, ~In x s -> @@ -779,7 +779,7 @@ Module Properties (M: S). Lemma empty_cardinal : cardinal empty = 0. Proof. - rewrite cardinal_fold; apply fold_1; auto. + rewrite cardinal_fold; apply fold_1; auto with set. Qed. Hint Immediate empty_cardinal cardinal_1 : set. |