diff options
Diffstat (limited to 'theories7/Sets/Infinite_sets.v')
| -rwxr-xr-x | theories7/Sets/Infinite_sets.v | 232 |
1 files changed, 0 insertions, 232 deletions
diff --git a/theories7/Sets/Infinite_sets.v b/theories7/Sets/Infinite_sets.v deleted file mode 100755 index bf423753..00000000 --- a/theories7/Sets/Infinite_sets.v +++ /dev/null @@ -1,232 +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: Infinite_sets.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) - -Require Export Finite_sets. -Require Export Constructive_sets. -Require Export Classical_Type. -Require Export Classical_sets. -Require Export Powerset. -Require Export Powerset_facts. -Require Export Powerset_Classical_facts. -Require Export Gt. -Require Export Lt. -Require Export Le. -Require Export Finite_sets_facts. -Require Export Image. - -Section Approx. -Variable U: Type. - -Inductive Approximant [A, X:(Ensemble U)] : Prop := - Defn_of_Approximant: (Finite U X) -> (Included U X A) -> (Approximant A X). -End Approx. - -Hints Resolve Defn_of_Approximant. - -Section Infinite_sets. -Variable U: Type. - -Lemma make_new_approximant: - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> (Approximant U A X) -> - (Inhabited U (Setminus U A X)). -Proof. -Intros A X H' H'0. -Elim H'0; Intros H'1 H'2. -Apply Strict_super_set_contains_new_element; Auto with sets. -Red; Intro H'3; Apply H'. -Rewrite <- H'3; Auto with sets. -Qed. - -Lemma approximants_grow: - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> - (n: nat) (cardinal U X n) -> (Included U X A) -> - (EXT Y | (cardinal U Y (S n)) /\ (Included U Y A)). -Proof. -Intros A X H' n H'0; Elim H'0; Auto with sets. -Intro H'1. -Cut (Inhabited U (Setminus U A (Empty_set U))). -Intro H'2; Elim H'2. -Intros x H'3. -Exists (Add U (Empty_set U) x); Auto with sets. -Split. -Apply card_add; Auto with sets. -Cut (In U A x). -Intro H'4; Red; Auto with sets. -Intros x0 H'5; Elim H'5; Auto with sets. -Intros x1 H'6; Elim H'6; Auto with sets. -Elim H'3; Auto with sets. -Apply make_new_approximant; Auto with sets. -Intros A0 n0 H'1 H'2 x H'3 H'5. -LApply H'2; [Intro H'6; Elim H'6; Clear H'2 | Clear H'2]; Auto with sets. -Intros x0 H'2; Try Assumption. -Elim H'2; Intros H'7 H'8; Try Exact H'8; Clear H'2. -Elim (make_new_approximant A x0); Auto with sets. -Intros x1 H'2; Try Assumption. -Exists (Add U x0 x1); Auto with sets. -Split. -Apply card_add; Auto with sets. -Elim H'2; Auto with sets. -Red. -Intros x2 H'9; Elim H'9; Auto with sets. -Intros x3 H'10; Elim H'10; Auto with sets. -Elim H'2; Auto with sets. -Auto with sets. -Apply Defn_of_Approximant; Auto with sets. -Apply cardinal_finite with n := (S n0); Auto with sets. -Qed. - -Lemma approximants_grow': - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> - (n: nat) (cardinal U X n) -> (Approximant U A X) -> - (EXT Y | (cardinal U Y (S n)) /\ (Approximant U A Y)). -Proof. -Intros A X H' n H'0 H'1; Try Assumption. -Elim H'1. -Intros H'2 H'3. -ElimType (EXT Y | (cardinal U Y (S n)) /\ (Included U Y A)). -Intros x H'4; Elim H'4; Intros H'5 H'6; Try Exact H'5; Clear H'4. -Exists x; Auto with sets. -Split; [Auto with sets | Idtac]. -Apply Defn_of_Approximant; Auto with sets. -Apply cardinal_finite with n := (S n); Auto with sets. -Apply approximants_grow with X := X; Auto with sets. -Qed. - -Lemma approximant_can_be_any_size: - (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> - (n: nat) (EXT Y | (cardinal U Y n) /\ (Approximant U A Y)). -Proof. -Intros A H' H'0 n; Elim n. -Exists (Empty_set U); Auto with sets. -Intros n0 H'1; Elim H'1. -Intros x H'2. -Apply approximants_grow' with X := x; Tauto. -Qed. - -Variable V: Type. - -Theorem Image_set_continuous: - (A: (Ensemble U)) - (f: U -> V) (X: (Ensemble V)) (Finite V X) -> (Included V X (Im U V A f)) -> - (EX n | - (EXT Y | ((cardinal U Y n) /\ (Included U Y A)) /\ (Im U V Y f) == X)). -Proof. -Intros A f X H'; Elim H'. -Intro H'0; Exists O. -Exists (Empty_set U); Auto with sets. -Intros A0 H'0 H'1 x H'2 H'3; Try Assumption. -LApply H'1; - [Intro H'4; Elim H'4; Intros n E; Elim E; Clear H'4 H'1 | Clear H'1]; Auto with sets. -Intros x0 H'1; Try Assumption. -Exists (S n); Try Assumption. -Elim H'1; Intros H'4 H'5; Elim H'4; Intros H'6 H'7; Try Exact H'6; Clear H'4 H'1. -Clear E. -Generalize H'2. -Rewrite <- H'5. -Intro H'1; Try Assumption. -Red in H'3. -Generalize (H'3 x). -Intro H'4; LApply H'4; [Intro H'8; Try Exact H'8; Clear H'4 | Clear H'4]; Auto with sets. -Specialize 5 Im_inv with U := U V:=V X := A f := f y := x; Intro H'11; - LApply H'11; [Intro H'13; Elim H'11; Clear H'11 | Clear H'11]; Auto with sets. -Intros x1 H'4; Try Assumption. -Apply exT_intro with x := (Add U x0 x1). -Split; [Split; [Try Assumption | Idtac] | Idtac]. -Apply card_add; Auto with sets. -Red; Intro H'9; Try Exact H'9. -Apply H'1. -Elim H'4; Intros H'10 H'11; Rewrite <- H'11; Clear H'4; Auto with sets. -Elim H'4; Intros H'9 H'10; Try Exact H'9; Clear H'4; Auto with sets. -Red; Auto with sets. -Intros x2 H'4; Elim H'4; Auto with sets. -Intros x3 H'11; Elim H'11; Auto with sets. -Elim H'4; Intros H'9 H'10; Rewrite <- H'10; Clear H'4; Auto with sets. -Apply Im_add; Auto with sets. -Qed. - -Theorem Image_set_continuous': - (A: (Ensemble U)) - (f: U -> V) (X: (Ensemble V)) (Approximant V (Im U V A f) X) -> - (EXT Y | (Approximant U A Y) /\ (Im U V Y f) == X). -Proof. -Intros A f X H'; Try Assumption. -Cut (EX n | (EXT Y | - ((cardinal U Y n) /\ (Included U Y A)) /\ (Im U V Y f) == X)). -Intro H'0; Elim H'0; Intros n E; Elim E; Clear H'0. -Intros x H'0; Try Assumption. -Elim H'0; Intros H'1 H'2; Elim H'1; Intros H'3 H'4; Try Exact H'3; - Clear H'1 H'0; Auto with sets. -Exists x. -Split; [Idtac | Try Assumption]. -Apply Defn_of_Approximant; Auto with sets. -Apply cardinal_finite with n := n; Auto with sets. -Apply Image_set_continuous; Auto with sets. -Elim H'; Auto with sets. -Elim H'; Auto with sets. -Qed. - -Theorem Pigeonhole_bis: - (A: (Ensemble U)) (f: U -> V) ~ (Finite U A) -> (Finite V (Im U V A f)) -> - ~ (injective U V f). -Proof. -Intros A f H'0 H'1; Try Assumption. -Elim (Image_set_continuous' A f (Im U V A f)); Auto with sets. -Intros x H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2. -Elim (make_new_approximant A x); Auto with sets. -Intros x0 H'2; Elim H'2. -Intros H'5 H'6. -Elim (finite_cardinal V (Im U V A f)); Auto with sets. -Intros n E. -Elim (finite_cardinal U x); Auto with sets. -Intros n0 E0. -Apply Pigeonhole with A := (Add U x x0) n := (S n0) n' := n. -Apply card_add; Auto with sets. -Rewrite (Im_add U V x x0 f); Auto with sets. -Cut (In V (Im U V x f) (f x0)). -Intro H'8. -Rewrite (Non_disjoint_union V (Im U V x f) (f x0)); Auto with sets. -Rewrite H'4; Auto with sets. -Elim (Extension V (Im U V x f) (Im U V A f)); Auto with sets. -Apply le_lt_n_Sm. -Apply cardinal_decreases with U := U V := V A := x f := f; Auto with sets. -Rewrite H'4; Auto with sets. -Elim H'3; Auto with sets. -Qed. - -Theorem Pigeonhole_ter: - (A: (Ensemble U)) - (f: U -> V) (n: nat) (injective U V f) -> (Finite V (Im U V A f)) -> - (Finite U A). -Proof. -Intros A f H' H'0 H'1. -Apply NNPP. -Red; Intro H'2. -Elim (Pigeonhole_bis A f); Auto with sets. -Qed. - -End Infinite_sets. |