diff options
Diffstat (limited to 'theories/Sets/Image.v')
| -rwxr-xr-x | theories/Sets/Image.v | 205 |
1 files changed, 205 insertions, 0 deletions
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v new file mode 100755 index 00000000..f58f2f81 --- /dev/null +++ b/theories/Sets/Image.v @@ -0,0 +1,205 @@ +(************************************************************************) +(* 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: Image.v,v 1.6.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. + +Section Image. +Variables U V : Type. + +Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V := + Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y. + +Lemma Im_def : + forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x). +Proof. +intros X f x H'; try assumption. +apply Im_intro with (x := x); auto with sets. +Qed. +Hint Resolve Im_def. + +Lemma Im_add : + forall (X:Ensemble U) (x:U) (f:U -> V), + Im (Add _ X x) f = Add _ (Im X f) (f x). +Proof. +intros X x f. +apply Extensionality_Ensembles. +split; red in |- *; intros x0 H'. +elim H'; intros. +rewrite H0. +elim Add_inv with U X x x1; auto with sets. +destruct 1; auto with sets. +elim Add_inv with V (Im X f) (f x) x0; auto with sets. +destruct 1 as [x0 H y H0]. +rewrite H0; auto with sets. +destruct 1; auto with sets. +Qed. + +Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V. +Proof. +intro f; try assumption. +apply Extensionality_Ensembles. +split; auto with sets. +red in |- *. +intros x H'; elim H'. +intros x0 H'0; elim H'0; auto with sets. +Qed. +Hint Resolve image_empty. + +Lemma finite_image : + forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f). +Proof. +intros X f H'; elim H'. +rewrite (image_empty f); auto with sets. +intros A H'0 H'1 x H'2; clear H' X. +rewrite (Im_add A x f); auto with sets. +apply Add_preserves_Finite; auto with sets. +Qed. +Hint Resolve finite_image. + +Lemma Im_inv : + forall (X:Ensemble U) (f:U -> V) (y:V), + In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y. +Proof. +intros X f y H'; elim H'. +intros x H'0 y0 H'1; rewrite H'1. +exists x; auto with sets. +Qed. + +Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. + +Lemma not_injective_elim : + forall f:U -> V, + ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). +Proof. +unfold injective in |- *; intros f H. +cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). +2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); + trivial with sets. +destruct 1 as [x C]; exists x. +cut (exists y : _, ~ (f x = f y -> x = y)). +2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); + trivial with sets. +destruct 1 as [y D]; exists y. +apply imply_to_and; trivial with sets. +Qed. + +Lemma cardinal_Im_intro : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p. +Proof. +intros. +apply finite_cardinal; apply finite_image. +apply cardinal_finite with n; trivial with sets. +Qed. + +Lemma In_Image_elim : + forall (A:Ensemble U) (f:U -> V), + injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x. +Proof. +intros. +elim Im_inv with A f (f x); trivial with sets. +intros z C; elim C; intros InAz E. +elim (H z x E); trivial with sets. +Qed. + +Lemma injective_preserves_cardinal : + forall (A:Ensemble U) (f:U -> V) (n:nat), + injective f -> + cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n. +Proof. +induction 2 as [| A n H'0 H'1 x H'2]; auto with sets. +rewrite (image_empty f). +intros n' CE. +apply cardinal_unicity with V (Empty_set V); auto with sets. +intro n'. +rewrite (Im_add A x f). +intro H'3. +elim cardinal_Im_intro with A f n; trivial with sets. +intros i CI. +lapply (H'1 i); trivial with sets. +cut (~ In _ (Im A f) (f x)). +intros H0 H1. +apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets. +apply card_add; auto with sets. +rewrite <- H1; trivial with sets. +red in |- *; intro; apply H'2. +apply In_Image_elim with f; trivial with sets. +Qed. + +Lemma cardinal_decreases : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n. +Proof. +induction 1 as [| A n H'0 H'1 x H'2]; auto with sets. +rewrite (image_empty f); intros. +cut (n' = 0). +intro E; rewrite E; trivial with sets. +apply cardinal_unicity with V (Empty_set V); auto with sets. +intro n'. +rewrite (Im_add A x f). +elim cardinal_Im_intro with A f n; trivial with sets. +intros p C H'3. +apply le_trans with (S p). +apply card_Add_gen with V (Im A f) (f x); trivial with sets. +apply le_n_S; auto with sets. +Qed. + +Theorem Pigeonhole : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal U A n -> + forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f. +Proof. +unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I. +cut (n' = n). +intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n). +apply injective_preserves_cardinal with (A := A) (f := f) (n := n); + trivial with sets. +Qed. + +Lemma Pigeonhole_principle : + forall (A:Ensemble U) (f:U -> V) (n:nat), + cardinal _ A n -> + forall n':nat, + cardinal _ (Im A f) n' -> + n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y). +Proof. +intros; apply not_injective_elim. +apply Pigeonhole with A n n'; trivial with sets. +Qed. +End Image. +Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file |