diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /theories/FSets/FSetEqProperties.v | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'theories/FSets/FSetEqProperties.v')
-rw-r--r-- | theories/FSets/FSetEqProperties.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 006d78c7..d7062d5a 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetEqProperties.v 8639 2006-03-16 19:21:55Z letouzey $ *) +(* $Id: FSetEqProperties.v 8853 2006-05-23 18:17:38Z herbelin $ *) (** * Finite sets library *) @@ -276,7 +276,7 @@ Lemma is_empty_cardinal: is_empty s = zerob (cardinal s). Proof. intros; apply bool_1; split; intros. rewrite cardinal_1; simpl; auto. -assert (cardinal s = 0) by apply zerob_true_elim; auto. +assert (cardinal s = 0) by (apply zerob_true_elim; auto). auto. Qed. @@ -672,7 +672,7 @@ unfold Add, MP.Add; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. assert (E.eq x y -> f y = true) by - intro H0; rewrite <- (Comp _ _ H0); auto. + (intro H0; rewrite <- (Comp _ _ H0); auto). tauto. Qed. @@ -704,6 +704,11 @@ assert (f a || g a = true <-> f a = true \/ g a = true). tauto. Qed. +Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s'). +Proof. +unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto. +Qed. + (** Properties of [for_all] *) Lemma for_all_mem_1: forall s, |