diff options
Diffstat (limited to 'theories/Sets/Infinite_sets.v')
| -rwxr-xr-x | theories/Sets/Infinite_sets.v | 244 |
1 files changed, 244 insertions, 0 deletions
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v new file mode 100755 index 00000000..c357e26c --- /dev/null +++ b/theories/Sets/Infinite_sets.v @@ -0,0 +1,244 @@ +(************************************************************************) +(* 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.5.2.1 2004/07/16 19:31:17 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. + +Hint Resolve Defn_of_Approximant. + +Section Infinite_sets. +Variable U : Type. + +Lemma make_new_approximant : + forall A 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 in |- *; intro H'3; apply H'. +rewrite <- H'3; auto with sets. +Qed. + +Lemma approximants_grow : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, + cardinal U X n -> + Included U X A -> exists 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 in |- *; 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 in |- *. +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' : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, + cardinal U X n -> + Approximant U A X -> + exists 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 (exists 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 : + forall A X:Ensemble U, + ~ Finite U A -> + forall n:nat, exists 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 : + forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), + Finite V X -> + Included V X (Im U V A f) -> + exists n : _, + (exists 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 0. +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 5Im_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 ex_intro with (x := Add U x0 x1). +split; [ split; [ try assumption | idtac ] | idtac ]. +apply card_add; auto with sets. +red in |- *; 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 in |- *; 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' : + forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), + Approximant V (Im U V A f) X -> + exists Y : _, Approximant U A Y /\ Im U V Y f = X. +Proof. +intros A f X H'; try assumption. +cut + (exists n : _, + (exists 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 : + forall (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 : + forall (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 in |- *; intro H'2. +elim (Pigeonhole_bis A f); auto with sets. +Qed. + +End Infinite_sets. |