petits ajouts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 44 insertions, 0 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 6217a7037..6b1ef79c3 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -326,6 +326,22 @@ rewrite <- H0; rewrite H2; rewrite H1; auto.
 auto.
 Qed.
 
+Lemma empty_o : forall x, find x (empty elt) = None.
+Proof.
+intros.
+case_eq (find x (empty elt)); intros; auto.
+generalize (find_2 H).
+rewrite empty_mapsto_iff; intuition.
+Qed.
+
+Lemma empty_a : forall x, mem x (empty elt) = false.
+Proof.
+intros.
+case_eq (mem x (empty elt)); intros; auto.
+generalize (mem_2 H).
+rewrite empty_in_iff; intuition.
+Qed.
+
 Lemma add_eq_o : forall m x y e, 
  E.eq x y -> find y (add x e m) = Some e.
 Proof.
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index f53e1d2b5..af8dccf53 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -326,6 +326,22 @@ rewrite <- H0; rewrite H2; rewrite H1; auto.
 auto.
 Qed.
 
+Lemma empty_o : forall x, find x (empty elt) = None.
+Proof.
+intros.
+case_eq (find x (empty elt)); intros; auto.
+generalize (find_2 H).
+rewrite empty_mapsto_iff; intuition.
+Qed.
+
+Lemma empty_a : forall x, mem x (empty elt) = false.
+Proof.
+intros.
+case_eq (mem x (empty elt)); intros; auto.
+generalize (mem_2 H).
+rewrite empty_in_iff; intuition.
+Qed.
+
 Lemma add_eq_o : forall m x y e, 
  E.eq x y -> find y (add x e m) = Some e.
 Proof.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 2b9548fe4..6874ceb33 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -159,6 +159,12 @@ generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H).
 destruct (mem x s); destruct (mem y s); intuition.
 Qed.
 
+Lemma empty_b : mem y empty = false.
+Proof.
+generalize (empty_iff y)(mem_iff empty y).
+destruct (mem y empty); intuition.
+Qed.
+
 Lemma add_b : mem y (add x s) = eqb x y || mem y s.
 Proof.
 generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb.
diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v
index c5e82e09c..798a3f855 100644
--- a/theories/FSets/FSetWeakFacts.v
+++ b/theories/FSets/FSetWeakFacts.v
@@ -159,6 +159,12 @@ generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H).
 destruct (mem x s); destruct (mem y s); intuition.
 Qed.
 
+Lemma empty_b : mem y empty = false.
+Proof.
+generalize (empty_iff y)(mem_iff empty y).
+destruct (mem y empty); intuition.
+Qed.
+
 Lemma add_b : mem y (add x s) = eqb x y || mem y s.
 Proof.
 generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb.