diff options
Diffstat (limited to 'theories7/Sets/Image.v')
| -rwxr-xr-x | theories7/Sets/Image.v | 199 |
1 files changed, 0 insertions, 199 deletions
diff --git a/theories7/Sets/Image.v b/theories7/Sets/Image.v deleted file mode 100755 index 0794a3bb..00000000 --- a/theories7/Sets/Image.v +++ /dev/null @@ -1,199 +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: 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. |