|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(****************************************************************************)
(* *)
(* 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. *)
(****************************************************************************)
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
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.
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; intros x0 H'.
elim H'; intros.
rewrite H0.
elim Add_inv with U X x x1; auto using Im_def with sets.
destruct 1; auto using Im_def with sets.
elim Add_inv with V (Im X f) (f x) x0.
destruct 1 as [x0 H y H0].
rewrite H0; auto using Im_def with sets.
destruct 1; auto using Im_def with sets.
trivial.
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.
intros x H'; elim H'.
intros x0 H'0; elim H'0; auto with sets.
Qed.
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.
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; 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; 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; 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.
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
