diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-09 16:10:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-09 16:10:59 +0000 |
| commit | 8907c227f5c456f14617890946aa808ef522d7da (patch) | |
| tree | f8b9abbfb9f1713642fe5bf48d5ead64e4a5510c /theories/FSets/FSetEqProperties.v | |
| parent | e1723b1094719c1a60fddaa2668151b4f8ebc9ea (diff) | |
Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements
Mostly results about Zgcd (commutativity, associativity, ...).
Slight improvement of ZMicromega.
Beware: some lemmas of Zdiv/ Znumtheory were asking for
too strict or useless hypothesis. Some minor glitches may occur.
By the way, some iff lemmas about negb in Bool.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetEqProperties.v')
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index ae2f0a298..7ec360a66 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -734,7 +734,7 @@ generalize (equal_mem_2 _ _ H x). rewrite filter_b; auto. rewrite empty_mem. rewrite H0; simpl;intros. -replace true with (negb false);auto;apply negb_sym;auto. +rewrite <- negb_false_iff; auto. Qed. Lemma for_all_mem_3: @@ -762,7 +762,7 @@ exists x. rewrite filter_b in H1; auto. elim (andb_prop _ _ H1). split;auto. -replace false with (negb true);auto;apply negb_sym;auto. +rewrite <- negb_true_iff; auto. Qed. (** Properties of [exists] *) @@ -794,8 +794,8 @@ Proof. intros. rewrite for_all_exists; auto. rewrite for_all_mem_1;auto with bool. -intros;generalize (H x H0);intros. -symmetry;apply negb_sym;simpl;auto. +intros;generalize (H x H0);intros. +rewrite negb_true_iff; auto. Qed. Lemma exists_mem_2: @@ -803,9 +803,9 @@ Lemma exists_mem_2: Proof. intros. rewrite for_all_exists in H; auto. -replace false with (negb true);auto;apply negb_sym;symmetry. -rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto. -replace true with (negb false);auto;apply negb_sym;auto. +rewrite negb_false_iff in H. +rewrite <- negb_true_iff. +apply for_all_mem_2 with (2:=H); auto. Qed. Lemma exists_mem_3: @@ -813,9 +813,9 @@ Lemma exists_mem_3: Proof. intros. rewrite for_all_exists; auto. -symmetry;apply negb_sym;simpl. +rewrite negb_true_iff. apply for_all_mem_3 with x;auto. -rewrite H0;auto. +rewrite negb_false_iff; auto. Qed. Lemma exists_mem_4: @@ -823,11 +823,11 @@ Lemma exists_mem_4: Proof. intros. rewrite for_all_exists in H; auto. -elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros. +rewrite negb_true_iff in H. +elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto. elim p;intros. exists x;split;auto. -replace true with (negb false);auto;apply negb_sym;auto. -replace false with (negb true);auto;apply negb_sym;auto. +rewrite <-negb_false_iff; auto. Qed. End Bool'. |