aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FSetEqProperties.v10
-rw-r--r--theories/FSets/FSetProperties.v38
2 files changed, 24 insertions, 24 deletions
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 59b2f789ab..3f8840529e 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -170,7 +170,7 @@ Qed.
Lemma equal_cardinal:
equal s s'=true -> cardinal s=cardinal s'.
Proof.
-auto with set.
+auto with set fset.
Qed.
(* Properties of [subset] *)
@@ -268,7 +268,7 @@ Proof.
intros; apply bool_1; split; intros.
rewrite MP.cardinal_1; simpl; auto with set.
assert (cardinal s = 0) by (apply zerob_true_elim; auto).
-auto with set.
+auto with set fset.
Qed.
(** Properties of [singleton] *)
@@ -551,7 +551,7 @@ End Fold.
Lemma add_cardinal_1:
forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
Proof.
-auto with set.
+auto with set fset.
Qed.
Lemma add_cardinal_2:
@@ -846,9 +846,9 @@ Lemma sum_plus :
Proof.
unfold sum.
intros f g Hf Hg.
-assert (fc : compat_opL (fun x:elt =>plus (f x))). red; auto.
+assert (fc : compat_opL (fun x:elt =>plus (f x))). red; auto with fset.
assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto.
+assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset.
assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 17f0e25e7a..6b6546f82d 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,8 +21,8 @@ Require Import DecidableTypeEx FSetFacts FSetDecide.
Set Implicit Arguments.
Unset Strict Implicit.
-Hint Unfold transpose compat_op Proper respectful : core.
-Hint Extern 1 (Equivalence _) => constructor; congruence : core.
+Hint Unfold transpose compat_op Proper respectful : fset.
+Hint Extern 1 (Equivalence _) => constructor; congruence : fset.
(** First, a functor for Weak Sets in functorial version. *)
@@ -708,7 +708,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
Proof.
- intros; rewrite cardinal_fold; apply fold_1; auto.
+ intros; rewrite cardinal_fold; apply fold_1; auto with fset.
Qed.
Lemma cardinal_2 :
@@ -716,7 +716,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Proof.
intros; do 2 rewrite cardinal_fold.
change S with ((fun _ => S) x).
- apply fold_2; auto.
+ apply fold_2; auto with fset.
Qed.
(** ** Cardinal and (non-)emptiness *)
@@ -732,7 +732,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Proof.
intros; rewrite cardinal_Empty; auto.
Qed.
- Hint Resolve cardinal_inv_1 : core.
+ Hint Resolve cardinal_inv_1 : fset.
Lemma cardinal_inv_2 :
forall s n, cardinal s = S n -> { x : elt | In x s }.
@@ -757,7 +757,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
symmetry.
remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
induction n; intros.
- apply cardinal_1; rewrite <- H; auto.
+ apply cardinal_1; rewrite <- H; auto with fset.
destruct (cardinal_inv_2 Heqn) as (x,H2).
revert Heqn.
rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
@@ -769,13 +769,13 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
exact Equal_cardinal.
Qed.
- Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core.
+ Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : fset.
(** ** Cardinal and set operators *)
Lemma empty_cardinal : cardinal empty = 0.
Proof.
- rewrite cardinal_fold; apply fold_1; auto with set.
+ rewrite cardinal_fold; apply fold_1; auto with set fset.
Qed.
Hint Immediate empty_cardinal cardinal_1 : set.
@@ -795,7 +795,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Proof.
intros; do 3 rewrite cardinal_fold.
rewrite <- fold_plus.
- apply fold_diff_inter with (eqA:=@Logic.eq nat); auto.
+ apply fold_diff_inter with (eqA:=@Logic.eq nat); auto with fset.
Qed.
Lemma union_cardinal:
@@ -804,7 +804,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Proof.
intros; do 3 rewrite cardinal_fold.
rewrite <- fold_plus.
- apply fold_union; auto.
+ apply fold_union; auto with fset.
Qed.
Lemma subset_cardinal :
@@ -838,7 +838,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
intros.
do 4 rewrite cardinal_fold.
do 2 rewrite <- fold_plus.
- apply fold_union_inter with (eqA:=@Logic.eq nat); auto.
+ apply fold_union_inter with (eqA:=@Logic.eq nat); auto with fset.
Qed.
Lemma union_cardinal_inter :
@@ -860,7 +860,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Lemma add_cardinal_1 :
forall s x, In x s -> cardinal (add x s) = cardinal s.
Proof.
- auto with set.
+ auto with set fset.
Qed.
Lemma add_cardinal_2 :
@@ -869,7 +869,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
intros.
do 2 rewrite cardinal_fold.
change S with ((fun _ => S) x);
- apply fold_add with (eqA:=@Logic.eq nat); auto.
+ apply fold_add with (eqA:=@Logic.eq nat); auto with fset.
Qed.
Lemma remove_cardinal_1 :
@@ -878,16 +878,16 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
intros.
do 2 rewrite cardinal_fold.
change S with ((fun _ =>S) x).
- apply remove_fold_1 with (eqA:=@Logic.eq nat); auto.
+ apply remove_fold_1 with (eqA:=@Logic.eq nat); auto with fset.
Qed.
Lemma remove_cardinal_2 :
forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
Proof.
- auto with set.
+ auto with set fset.
Qed.
- Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core.
+ Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : fset.
End WProperties_fun.
@@ -952,7 +952,7 @@ Module OrdProperties (M:S).
red; intros x a b H; unfold leb.
f_equal; apply gtb_compat; auto.
Qed.
- Hint Resolve gtb_compat leb_compat : core.
+ Hint Resolve gtb_compat leb_compat : fset.
Lemma elements_split : forall x s,
elements s = elements_lt x s ++ elements_ge x s.
@@ -1047,7 +1047,7 @@ Module OrdProperties (M:S).
(forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
forall s : t, P s.
Proof.
- intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+ intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto with fset.
case_eq (max_elt s); intros.
apply X0 with (remove e s) e; auto with set.
apply IHn.
@@ -1068,7 +1068,7 @@ Module OrdProperties (M:S).
(forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
forall s : t, P s.
Proof.
- intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+ intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto with fset.
case_eq (min_elt s); intros.
apply X0 with (remove e s) e; auto with set.
apply IHn.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 08:58:19 +0000