diff options
Diffstat (limited to 'theories7/Sets/Image.v')
| -rwxr-xr-x | theories7/Sets/Image.v | 199 |
1 files changed, 199 insertions, 0 deletions
diff --git a/theories7/Sets/Image.v b/theories7/Sets/Image.v new file mode 100755 index 00000000..0794a3bb --- /dev/null +++ b/theories7/Sets/Image.v @@ -0,0 +1,199 @@ +(************************************************************************) +(* 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.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. + +Section Image. +Variables U, V: Type. + +Inductive Im [X:(Ensemble U); f:U -> V]: (Ensemble V) := + Im_intro: (x: U) (In ? X x) -> (y: V) y == (f x) -> (In ? (Im X f) y). + +Lemma Im_def: + (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. +Hints Resolve Im_def. + +Lemma Im_add: + (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; Intros x0 H'. +Elim H'; Intros. +Rewrite H0. +Elim Add_inv with U X x x1; Auto with sets. +NewDestruct 1; Auto with sets. +Elim Add_inv with V (Im X f) (f x) x0; Auto with sets. +NewDestruct 1 as [x0 H y H0]. +Rewrite H0; Auto with sets. +NewDestruct 1; Auto with sets. +Qed. + +Lemma image_empty: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V). +Proof. +Intro f; Try Assumption. +Apply Extensionality_Ensembles. +Split; Auto with sets. +Red. +Intros x H'; Elim H'. +Intros x0 H'0; Elim H'0; Auto with sets. +Qed. +Hints Resolve image_empty. + +Lemma finite_image: + (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. +Hints Resolve finite_image. + +Lemma Im_inv: + (X: (Ensemble U)) (f: U -> V) (y: V) (In ? (Im X f) y) -> + (exT ? [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] (x, y: U) (f x) == (f y) -> x == y. + +Lemma not_injective_elim: + (f: U -> V) ~ (injective f) -> + (EXT x | (EXT y | (f x) == (f y) /\ ~ x == y)). +Proof. +Unfold injective; Intros f H. +Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)). +2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; + Trivial with sets. +NewDestruct 1 as [x C]; Exists x. +Cut (EXT y | ~((f x)==(f y)->x==y)). +2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets. +NewDestruct 1 as [y D]; Exists y. +Apply imply_to_and; Trivial with sets. +Qed. + +Lemma cardinal_Im_intro: + (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> + (EX 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: + (A: (Ensemble U)) (f: U -> V) (injective f) -> + (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: + (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) -> + (n': nat) (cardinal ? (Im A f) n') -> n' = n. +Proof. +NewInduction 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; Intro; Apply H'2. +Apply In_Image_elim with f; Trivial with sets. +Qed. + +Lemma cardinal_decreases: + (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> + (n': nat) (cardinal V (Im A f) n') -> (le n' n). +Proof. +NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets. +Rewrite (image_empty f); Intros. +Cut n' = O. +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: + (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) -> + (n': nat) (cardinal V (Im A f) n') -> (lt n' n) -> ~ (injective f). +Proof. +Unfold not; Intros A f n CAn n' CIfn' ltn'n I. +Cut n' = n. +Intro E; Generalize ltn'n; Rewrite E; Exact (lt_n_n n). +Apply injective_preserves_cardinal with A := A f := f n := n; Trivial with sets. +Qed. + +Lemma Pigeonhole_principle: + (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) -> + (n': nat) (cardinal ? (Im A f) n') -> (lt n' n) -> + (EXT x | (EXT 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. +Hints Resolve Im_def image_empty finite_image : sets v62. |