diff options
Diffstat (limited to 'theories7/Sets/Classical_sets.v')
-rwxr-xr-x | theories7/Sets/Classical_sets.v | 133 |
1 files changed, 0 insertions, 133 deletions
diff --git a/theories7/Sets/Classical_sets.v b/theories7/Sets/Classical_sets.v deleted file mode 100755 index a6928ffd..00000000 --- a/theories7/Sets/Classical_sets.v +++ /dev/null @@ -1,133 +0,0 @@ -(************************************************************************) -(* 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.1.2.1 2004/07/16 19:31:38 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: - (A: (Ensemble U)) ~ (Included U A (Empty_set U)) -> (Inhabited U A). -Proof. -Intros A NI. -Elim (not_all_ex_not U [x:U]~(In U A x)). -Intros x H; Apply Inhabited_intro with x. -Apply NNPP; Auto with sets. -Red; Intro. -Apply NI; Red. -Intros x H'; Elim (H x); Trivial with sets. -Qed. -Hints Resolve not_included_empty_Inhabited. - -Lemma not_empty_Inhabited: - (A: (Ensemble U)) ~ A == (Empty_set U) -> (Inhabited U A). -Proof. -Intros; Apply not_included_empty_Inhabited. -Red; Auto with sets. -Qed. - -Lemma Inhabited_Setminus : -(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 [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. -Hints Resolve Inhabited_Setminus. - -Lemma Strict_super_set_contains_new_element: - (X, Y: (Ensemble U)) (Included U X Y) -> ~ X == Y -> - (Inhabited U (Setminus U Y X)). -Proof. -Auto 7 with sets. -Qed. -Hints Resolve Strict_super_set_contains_new_element. - -Lemma Subtract_intro: - (A: (Ensemble U)) (x, y: U) (In U A y) -> ~ x == y -> - (In U (Subtract U A x) y). -Proof. -Unfold 1 Subtract; Auto with sets. -Qed. -Hints Resolve Subtract_intro. - -Lemma Subtract_inv: - (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: - (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: - (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: - (X: (Ensemble U)) ~ (Strict_Included U X (Empty_set U)). -Proof. -Intro X; Red; 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 : - (A: (Ensemble U)) (Complement U (Complement U A)) == A. -Proof. -Unfold Complement; Intros; Apply Extensionality_Ensembles; Auto with sets. -Red; Split; Auto with sets. -Red; Intros; Apply NNPP; Auto with sets. -Qed. - -End Ensembles_classical. - -Hints Resolve Strict_super_set_contains_new_element Subtract_intro - not_SIncl_empty : sets v62. |