diff options
Diffstat (limited to 'theories/Sets/Classical_sets.v')
| -rwxr-xr-x | theories/Sets/Classical_sets.v | 132 |
1 files changed, 132 insertions, 0 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v new file mode 100755 index 00000000..98cb14e4 --- /dev/null +++ b/theories/Sets/Classical_sets.v @@ -0,0 +1,132 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(****************************************************************************) +(* *) +(* Naive Set Theory in Coq *) +(* *) +(* INRIA INRIA *) +(* Rocquencourt Sophia-Antipolis *) +(* *) +(* Coq V6.1 *) +(* *) +(* Gilles Kahn *) +(* Gerard Huet *) +(* *) +(* *) +(* *) +(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) +(* to the Newton Institute for providing an exceptional work environment *) +(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) +(****************************************************************************) + +(*i $Id: Classical_sets.v,v 1.4.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +Require Export Ensembles. +Require Export Constructive_sets. +Require Export Classical_Type. + +(* Hints Unfold not . *) + +Section Ensembles_classical. +Variable U : Type. + +Lemma not_included_empty_Inhabited : + forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A. +Proof. +intros A NI. +elim (not_all_ex_not U (fun x:U => ~ In U A x)). +intros x H; apply Inhabited_intro with x. +apply NNPP; auto with sets. +red in |- *; intro. +apply NI; red in |- *. +intros x H'; elim (H x); trivial with sets. +Qed. +Hint Resolve not_included_empty_Inhabited. + +Lemma not_empty_Inhabited : + forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. +Proof. +intros; apply not_included_empty_Inhabited. +red in |- *; auto with sets. +Qed. + +Lemma Inhabited_Setminus : + forall X Y:Ensemble U, + Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X). +Proof. +intros X Y I NI. +elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI). +intros x YX. +apply Inhabited_intro with x. +apply Setminus_intro. +apply not_imply_elim with (In U X x); trivial with sets. +auto with sets. +Qed. +Hint Resolve Inhabited_Setminus. + +Lemma Strict_super_set_contains_new_element : + forall X Y:Ensemble U, + Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X). +Proof. +auto 7 with sets. +Qed. +Hint Resolve Strict_super_set_contains_new_element. + +Lemma Subtract_intro : + forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. +Proof. +unfold Subtract at 1 in |- *; auto with sets. +Qed. +Hint Resolve Subtract_intro. + +Lemma Subtract_inv : + forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y. +Proof. +intros A x y H'; elim H'; auto with sets. +Qed. + +Lemma Included_Strict_Included : + forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y. +Proof. +intros X Y H'; try assumption. +elim (classic (X = Y)); auto with sets. +Qed. + +Lemma Strict_Included_inv : + forall X Y:Ensemble U, + Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X). +Proof. +intros X Y H'; red in H'. +split; [ tauto | idtac ]. +elim H'; intros H'0 H'1; try exact H'1; clear H'. +apply Strict_super_set_contains_new_element; auto with sets. +Qed. + +Lemma not_SIncl_empty : + forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). +Proof. +intro X; red in |- *; intro H'; try exact H'. +lapply (Strict_Included_inv X (Empty_set U)); auto with sets. +intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. +intros x H'0; elim H'0. +intro H'3; elim H'3. +Qed. + +Lemma Complement_Complement : + forall A:Ensemble U, Complement U (Complement U A) = A. +Proof. +unfold Complement in |- *; intros; apply Extensionality_Ensembles; + auto with sets. +red in |- *; split; auto with sets. +red in |- *; intros; apply NNPP; auto with sets. +Qed. + +End Ensembles_classical. + +Hint Resolve Strict_super_set_contains_new_element Subtract_intro + not_SIncl_empty: sets v62.
\ No newline at end of file |