diff --git a/README.md b/README.md index 65b0c925..5eb37e05 100644 --- a/README.md +++ b/README.md @@ -74,9 +74,7 @@ make # or make -j ### Filters and nets -- `Filters.v` - `FilterLimits.v` -- `DirectedSets.v` - `Nets.v` - `FiltersAndNets.v` - various transformations between filters and nets @@ -123,8 +121,14 @@ topological spaces In alphabetical order, except where related files are grouped together: -- `Cardinals.v` - cardinalities of sets -- `Ordinals.v` - a construction of the ordinals without reference to well-orders +- `Cardinals.v` - collects the files in the folder `Cardinals` +- `Cardinals/Cardinals.v` defines cardinal comparisons for types +- `Cardinals/CardinalsEns.v` defines cardinal comparisons for ensembles +- `Cardinals/Combinatorics.v` defines some elementary bijections +- `Cardinals/Comparability.v` given choice, cardinals form a total order +- `Cardinals/CSB.v` prove Cantor-Schröder-Bernstein theorem +- `Cardinals/Diagonalization.v` Cantor's diagonalization and corollaries +- `Cardinals/LeastCardinalsEns.v` the cardinal orders are well-founded - `Classical_Wf.v` - proofs of the classical equivalence of wellfoundedness, the minimal element property, and the descending sequence property @@ -134,9 +138,16 @@ In alphabetical order, except where related files are grouped together: - `DependentTypeChoice.v` - choice on a relation (`forall a: A, B a -> Prop`) +- `DirectedSets.v` - basics of directed sets +- `Filters.v` - basics of filters + +- `EnsembleProduct.v` - products of ensembles, living in the type `A * B` + - `EnsemblesImplicit.v` - settings for appropriate implicit parameters for the standard library's Ensembles functions +- `FiniteImplicit.v` - same for the standard library's Sets/Finite_sets - `ImageImplicit.v` - same for the standard library's Sets/Image - `Relation_Definitions_Implicit.v` - same for the standard library's Relation_Definitions +- `EnsemblesExplicit.v` - clears the implicit parameters set in the above files - `EnsemblesSpec.v` - defines a notation for e.g. `[ n: nat | n > 5 /\ even n ] : Ensemble nat.` @@ -154,9 +165,13 @@ In alphabetical order, except where related files are grouped together: - `InfiniteTypes.v` - same for infinite types - `FunctionProperties.v` - injective, surjective, etc. +- `FunctionProperitesEns.v` - same but definitions restricted to ensembles +- `Image.v` - images of subsets under functions - `InverseImage.v` - inverse images of subsets under functions +- `Ordinals.v` - a construction of the ordinals without reference to well-orders + - `Powerset_facts.v` - some lemmas about the operations on subsets that the stdlib is missing - `Proj1SigInjective.v` - inclusion of `{ x: X | P x }` into `X` is injective @@ -168,3 +183,9 @@ In alphabetical order, except where related files are grouped together: - `WellOrders.v` - some basic properties of well-orders, including a proof that Zorn's Lemma implies the well-ordering principle - `ZornsLemma.v` - proof that choice implies Zorn's Lemma + +## Bibliography +- Cunningham, D. W. (2016). "Set theory : a first course". Cambridge University Press. ISBN: 9781107120327 +- Munkres, J. R. (2000). "Topology" (2nd ed.). Prentice-Hall. ISBN: 9780131816299 +- Pradic, C. and Brown, C. E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv: https://arxiv.org/abs/1904.09193 +- Preuss, G. (1975). "Allgemeine Topologie" (2., korr. Aufl.). Springer. ISBN: 3540074279 diff --git a/_CoqProject b/_CoqProject index 4cf60728..a5e29fd4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,8 +1,6 @@ -R theories/Topology Topology -R theories/ZornsLemma ZornsLemma -arg -set -arg "'Default Goal Selector=!'" --arg -w -arg -deprecated-hint-rewrite-without-locality --arg -w -arg -deprecated-instance-without-locality theories/Topology/AdjunctionSpace.v theories/Topology/Compactness.v @@ -40,10 +38,15 @@ theories/Topology/UrysohnsLemma.v theories/Topology/WeakTopology.v theories/Topology/Examples/S1.v theories/ZornsLemma/Cardinals.v -theories/ZornsLemma/CardinalsEns.v +theories/ZornsLemma/Cardinals/Cardinals.v +theories/ZornsLemma/Cardinals/CardinalsEns.v +theories/ZornsLemma/Cardinals/Combinatorics.v +theories/ZornsLemma/Cardinals/Comparability.v +theories/ZornsLemma/Cardinals/CSB.v +theories/ZornsLemma/Cardinals/Diagonalization.v +theories/ZornsLemma/Cardinals/LeastCardinalsEns.v theories/ZornsLemma/Classical_Wf.v theories/ZornsLemma/CountableTypes.v -theories/ZornsLemma/CSB.v theories/ZornsLemma/DecidableDec.v theories/ZornsLemma/DependentTypeChoice.v theories/ZornsLemma/DirectedSets.v @@ -64,7 +67,6 @@ theories/ZornsLemma/FunctionPropertiesEns.v theories/ZornsLemma/Image.v theories/ZornsLemma/ImageImplicit.v theories/ZornsLemma/IndexedFamilies.v -theories/ZornsLemma/InfiniteTypes.v theories/ZornsLemma/InverseImage.v theories/ZornsLemma/Ordinals.v theories/ZornsLemma/Powerset_facts.v diff --git a/meta.yml b/meta.yml index f163ae6c..f77d1e7b 100644 --- a/meta.yml +++ b/meta.yml @@ -99,9 +99,7 @@ documentation: |- ### Filters and nets - - `Filters.v` - `FilterLimits.v` - - `DirectedSets.v` - `Nets.v` - `FiltersAndNets.v` - various transformations between filters and nets @@ -148,8 +146,14 @@ documentation: |- In alphabetical order, except where related files are grouped together: - - `Cardinals.v` - cardinalities of sets - - `Ordinals.v` - a construction of the ordinals without reference to well-orders + - `Cardinals.v` - collects the files in the folder `Cardinals` + - `Cardinals/Cardinals.v` defines cardinal comparisons for types + - `Cardinals/CardinalsEns.v` defines cardinal comparisons for ensembles + - `Cardinals/Combinatorics.v` defines some elementary bijections + - `Cardinals/Comparability.v` given choice, cardinals form a total order + - `Cardinals/CSB.v` prove Cantor-Schröder-Bernstein theorem + - `Cardinals/Diagonalization.v` Cantor's diagonalization and corollaries + - `Cardinals/LeastCardinalsEns.v` the cardinal orders are well-founded - `Classical_Wf.v` - proofs of the classical equivalence of wellfoundedness, the minimal element property, and the descending sequence property @@ -159,9 +163,16 @@ documentation: |- - `DependentTypeChoice.v` - choice on a relation (`forall a: A, B a -> Prop`) + - `DirectedSets.v` - basics of directed sets + - `Filters.v` - basics of filters + + - `EnsembleProduct.v` - products of ensembles, living in the type `A * B` + - `EnsemblesImplicit.v` - settings for appropriate implicit parameters for the standard library's Ensembles functions + - `FiniteImplicit.v` - same for the standard library's Sets/Finite_sets - `ImageImplicit.v` - same for the standard library's Sets/Image - `Relation_Definitions_Implicit.v` - same for the standard library's Relation_Definitions + - `EnsemblesExplicit.v` - clears the implicit parameters set in the above files - `EnsemblesSpec.v` - defines a notation for e.g. `[ n: nat | n > 5 /\ even n ] : Ensemble nat.` @@ -179,9 +190,13 @@ documentation: |- - `InfiniteTypes.v` - same for infinite types - `FunctionProperties.v` - injective, surjective, etc. + - `FunctionProperitesEns.v` - same but definitions restricted to ensembles + - `Image.v` - images of subsets under functions - `InverseImage.v` - inverse images of subsets under functions + - `Ordinals.v` - a construction of the ordinals without reference to well-orders + - `Powerset_facts.v` - some lemmas about the operations on subsets that the stdlib is missing - `Proj1SigInjective.v` - inclusion of `{ x: X | P x }` into `X` is injective @@ -193,4 +208,10 @@ documentation: |- - `WellOrders.v` - some basic properties of well-orders, including a proof that Zorn's Lemma implies the well-ordering principle - `ZornsLemma.v` - proof that choice implies Zorn's Lemma + + ## Bibliography + - Cunningham, D. W. (2016). "Set theory : a first course". Cambridge University Press. ISBN: 9781107120327 + - Munkres, J. R. (2000). "Topology" (2nd ed.). Prentice-Hall. ISBN: 9780131816299 + - Pradic, C. and Brown, C. E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv: https://arxiv.org/abs/1904.09193 + - Preuss, G. (1975). "Allgemeine Topologie" (2., korr. Aufl.). Springer. ISBN: 3540074279 --- diff --git a/theories/Topology/Compactness.v b/theories/Topology/Compactness.v index f5164cea..e313abb6 100644 --- a/theories/Topology/Compactness.v +++ b/theories/Topology/Compactness.v @@ -616,27 +616,31 @@ Qed. Lemma topological_property_compact : topological_property compact. Proof. - intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hcomp F H eq. + apply Build_topological_property. + intros X Y f Hcont_f g Hcont_g Hfg Hcomp F H eq. destruct (Hcomp (inverse_image (inverse_image g) F)) as [F' [H1 [H2 H3]]]. - intros. - rewrite <- (inverse_image_id_comp Hgf). + rewrite <- (inverse_image_id_comp (proj1 Hfg)). apply Hcont_f, H. now destruct H0. - erewrite <- inverse_image_full, - <- (inverse_image_id_comp Hgf (FamilyUnion _)). + <- (inverse_image_id_comp (proj1 Hfg) (FamilyUnion _)). f_equal. - now rewrite <- (inverse_image_family_union F Hgf), - inverse_image_id_comp. + erewrite <- inverse_image_family_union. + 2, 3: apply Hfg. + rewrite inverse_image_id_comp; auto. + apply Hfg. - exists (inverse_image (inverse_image f) F'). split; [|split]. + apply injective_finite_inverse_image; auto. apply inverse_image_surjective_injective. apply invertible_impl_bijective. - exists g; assumption. + exists g; apply Hfg. + intros S [Hin]. destruct (H2 _ Hin) as [H0]. - now rewrite inverse_image_id_comp in H0. - + rewrite <- (inverse_image_family_union _ Hfg Hgf), H3. + rewrite inverse_image_id_comp in H0; auto. + apply Hfg. + + rewrite <- (inverse_image_family_union _ (proj2 Hfg) (proj1 Hfg)), H3. apply inverse_image_full. Qed. @@ -683,8 +687,9 @@ Lemma compact_hausdorff_homeo {X Y : TopologicalSpace} (f : X -> Y) : Proof. intros. apply bijective_impl_invertible in H1. - destruct H1 as [g Hgf Hfg]. - exists g; auto. + destruct H1 as [g [Hgf Hfg]]. + split; auto. + exists g. repeat split; auto. apply continuous_closed. intros. assert (compact (SubspaceTopology U)) as HU_compact. diff --git a/theories/Topology/Connectedness.v b/theories/Topology/Connectedness.v index be146154..07567814 100644 --- a/theories/Topology/Connectedness.v +++ b/theories/Topology/Connectedness.v @@ -117,18 +117,19 @@ Qed. Lemma topological_property_connected : topological_property connected. Proof. -intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hconn S HS. +apply Build_topological_property. +intros X Y f Hf g Hg Hfg Hconn S HS. destruct (Hconn (inverse_image f S)) as [HfS|HfS]; [ | left | right ]; try extensionality_ensembles. - apply continuous_clopen; auto. -- rewrite <- Hfg. +- rewrite <- (proj2 Hfg). apply in_inverse_image. rewrite inverse_image_empty, <- HfS. constructor. - now rewrite Hfg. + now rewrite (proj2 Hfg). - constructor. -- rewrite <- Hfg. +- rewrite <- (proj2 Hfg). apply in_inverse_image. rewrite HfS. constructor. diff --git a/theories/Topology/CountabilityAxioms.v b/theories/Topology/CountabilityAxioms.v index d59796b5..c5792681 100644 --- a/theories/Topology/CountabilityAxioms.v +++ b/theories/Topology/CountabilityAxioms.v @@ -7,13 +7,12 @@ From Topology Require Export Nets SubspaceTopology. From ZornsLemma Require Export - CardinalsEns + Cardinals CountableTypes. From ZornsLemma Require Import Classical_Wf DecidableDec - FiniteIntersections - InfiniteTypes. + FiniteIntersections. From Coq Require Import RelationClasses. diff --git a/theories/Topology/Homeomorphisms.v b/theories/Topology/Homeomorphisms.v index 1271e249..72d11d9d 100644 --- a/theories/Topology/Homeomorphisms.v +++ b/theories/Topology/Homeomorphisms.v @@ -1,30 +1,28 @@ -From Coq Require Export - Relation_Definitions. -From ZornsLemma Require Import - EnsemblesTactics - Relation_Definitions_Implicit. +From Coq Require Import + Morphisms. From Topology Require Export TopologicalSpaces Continuity. +From Coq Require Import + RelationClasses. -Inductive homeomorphism {X Y:TopologicalSpace} - (f:X -> Y) : Prop := -| intro_homeomorphism: forall g:Y -> point_set X, - continuous f -> continuous g -> - (forall x:point_set X, g (f x) = x) -> - (forall y:point_set Y, f (g y) = y) -> homeomorphism f. +Definition homeomorphism {X Y : TopologicalSpace} + (f : X -> Y) : Prop := + continuous f /\ + exists g : Y -> X, + continuous g /\ + inverse_map f g. Lemma homeomorphism_is_invertible: forall {X Y:TopologicalSpace} (f:X -> Y), homeomorphism f -> invertible f. Proof. intros. -destruct H as [g]. -exists g; trivial. +destruct H as [_ [g []]]. +exists g; assumption. Qed. -Definition open_map {X Y:TopologicalSpace} - (f:X -> Y) : Prop := +Definition open_map {X Y:TopologicalSpace} (f:X -> Y) : Prop := forall U:Ensemble X, open U -> open (Im U f). Lemma homeomorphism_is_open_map: forall {X Y:TopologicalSpace} @@ -32,61 +30,132 @@ Lemma homeomorphism_is_open_map: forall {X Y:TopologicalSpace} homeomorphism f -> open_map f. Proof. intros. -destruct H as [g]. +destruct H as [Hf [g [Hg]]]. red; intros. -assert (Im U f = inverse_image g U). -{ extensionality_ensembles. - - subst. - constructor. - now rewrite H1. - - exists (g x); auto. } -rewrite H4. -auto. +erewrite inverse_map_image_inverse_image; + eauto. +Qed. + +Lemma inverse_open_map_continuous + {X Y : TopologicalSpace} (f : X -> Y) (g : Y -> X) : + inverse_map f g -> + open_map f <-> continuous g. +Proof. + intros Hfg. + split. + - (* -> *) + intros Hf U HU. + erewrite <- inverse_map_image_inverse_image; + eauto. + - (* <- *) + intros Hg U HU. + erewrite inverse_map_image_inverse_image; + eauto. Qed. Lemma invertible_open_map_is_homeomorphism: forall {X Y:TopologicalSpace} (f:X -> Y), invertible f -> continuous f -> open_map f -> homeomorphism f. Proof. -intros. -destruct H as [g]. -exists g; trivial. -red. -intros. -assert (inverse_image g V = Im V f). -{ extensionality_ensembles. - - exists (g x); auto. - - constructor. - now rewrite H5, H. } -rewrite H4. -auto. +intros X Y f [g Hfg] Hfcont Hfopen. +split; auto. +exists g; split; auto. +eapply inverse_open_map_continuous; eassumption. +Qed. + +(** every continuous self-inverse map is a homeomorphism *) +Lemma homeomorphism_cont_involution (X : TopologicalSpace) + (f : X -> X) : + continuous f -> (forall x, f (f x) = x) -> homeomorphism f. +Proof. + intros Hf Hff. + split; auto. + exists f; split; auto. + split; auto. Qed. Lemma homeomorphism_id (X : TopologicalSpace) : homeomorphism (@id X). Proof. - exists id; auto using continuous_identity. + apply homeomorphism_cont_involution; auto. + apply continuous_identity. +Qed. + +Lemma homeomorphism_compose {X Y Z : TopologicalSpace} + (f : X -> Y) (g : Y -> Z) : + homeomorphism f -> homeomorphism g -> + homeomorphism (compose g f). +Proof. + intros [Hf [f0 [Hf0 Hff]]] [Hg [g0 [Hg0 Hgg]]]. + split. + { unfold compose. apply continuous_composition; auto. } + exists (compose f0 g0). split. + { unfold compose. apply continuous_composition; auto. } + apply inverse_map_compose; auto. Qed. -Inductive homeomorphic (X Y:TopologicalSpace) : Prop := -| intro_homeomorphic: forall f:X -> point_set Y, - homeomorphism f -> homeomorphic X Y. +Definition homeomorphic (X Y : TopologicalSpace) : Prop := + exists f : X -> Y, homeomorphism f. -Lemma homeomorphic_equiv: equivalence homeomorphic. +Instance homeomorphic_Equivalence : Equivalence homeomorphic. Proof. constructor. - eexists; eapply homeomorphism_id. -- intros X Y Z ? ?. - destruct H as [f [finv]]. - destruct H0 as [g [ginv]]. - exists (fun x => g (f x)), (fun z => finv (ginv z)); - congruence || now apply continuous_composition. -- intros X Y ?. - destruct H as [f [finv]]. - now exists finv, f. +- intros X Y [f Hf]. + destruct Hf as [Hf [g [Hg Hfg]]]. + exists g. split; auto. + exists f; split; auto. + apply inverse_map_sym; auto. +- intros X Y Z [f Hf] [g Hg]. + exists (compose g f). + apply homeomorphism_compose; assumption. Qed. +(** To prove `topological_property` it is helpful to use + `Coq.Classes.Morphisms.proper_sym_impl_iff` *) Definition topological_property (P : TopologicalSpace -> Prop) := - forall (X Y : TopologicalSpace) (f : X -> Y), - homeomorphism f -> P X -> P Y. + Proper (homeomorphic ==> iff) P. -Global Hint Unfold topological_property : homeo. +(** a lemma to prove [topological_property] more easily, with less + boilerplate *) +Lemma Build_topological_property (P : TopologicalSpace -> Prop) : + (forall (X Y : TopologicalSpace) + (f : X -> Y) (Hf : continuous f) + (g : Y -> X) (Hg : continuous g) + (Hfg : inverse_map f g) (HX : P X), P Y) -> + topological_property P. +Proof. + intros H. + apply proper_sym_impl_iff. + { typeclasses eauto. } + intros X Y [f [Hf [g [Hg Hfg]]]]. + exact (H X Y f Hf g Hg Hfg). +Qed. + +Lemma topological_property_Proper (P Q : TopologicalSpace -> Prop) : + (forall X : TopologicalSpace, P X <-> Q X) -> + topological_property P -> topological_property Q. +Proof. + intros HPQ HP X Y HXY. + rewrite <- !HPQ. + exact (HP X Y HXY). +Qed. + +Lemma topological_property_and (P Q : TopologicalSpace -> Prop) : + topological_property P -> topological_property Q -> + topological_property (fun X => P X /\ Q X). +Proof. + intros HP HQ X Y HXY. + specialize (HP X Y HXY). + specialize (HQ X Y HXY). + tauto. +Qed. + +Lemma topological_property_or (P Q : TopologicalSpace -> Prop) : + topological_property P -> topological_property Q -> + topological_property (fun X => P X \/ Q X). +Proof. + intros HP HQ X Y HXY. + specialize (HP X Y HXY). + specialize (HQ X Y HXY). + tauto. +Qed. diff --git a/theories/Topology/OpenBases.v b/theories/Topology/OpenBases.v index 6a4373ed..f70a89b2 100644 --- a/theories/Topology/OpenBases.v +++ b/theories/Topology/OpenBases.v @@ -1,7 +1,7 @@ From Coq Require Import ClassicalChoice. From ZornsLemma Require Import - CardinalsEns. + Cardinals. From Topology Require Export TopologicalSpaces. diff --git a/theories/Topology/RFuncContinuity.v b/theories/Topology/RFuncContinuity.v index 7cc4d229..ffc31507 100644 --- a/theories/Topology/RFuncContinuity.v +++ b/theories/Topology/RFuncContinuity.v @@ -322,8 +322,8 @@ assert (forall x:point_set RTop, In U (x / (1 + Rabs x))). { intros. now constructor. } exists (continuous_factorization _ _ H0). -exists (fun x => (subspace_inc U x) / (1 - Rabs (subspace_inc U x))). -- apply factorization_is_continuous. +split. +{ apply factorization_is_continuous. apply pointwise_continuity. intros. apply quotient_continuous. @@ -333,6 +333,9 @@ exists (fun x => (subspace_inc U x) / (1 - Rabs (subspace_inc U x))). * apply continuous_func_continuous_everywhere, Rabs_continuous. + pose proof (Rabs_pos x). lra. +} +exists (fun x => (subspace_inc U x) / (1 - Rabs (subspace_inc U x))). +split; [|split]. - apply pointwise_continuity. intros. apply quotient_continuous. diff --git a/theories/Topology/SeparatednessAxioms.v b/theories/Topology/SeparatednessAxioms.v index c637b8d1..d392877c 100644 --- a/theories/Topology/SeparatednessAxioms.v +++ b/theories/Topology/SeparatednessAxioms.v @@ -1,5 +1,7 @@ From Coq Require Import - Program.Subset. + Morphisms + Program.Subset + RelationClasses. From Topology Require Export Nets. From Topology Require Import @@ -7,13 +9,14 @@ From Topology Require Import SubspaceTopology. Definition T0_sep (X:TopologicalSpace) : Prop := - forall x y:point_set X, x <> y -> - (exists U:Ensemble (point_set X), open U /\ In U x /\ ~ In U y) \/ - (exists U:Ensemble (point_set X), open U /\ ~ In U x /\ In U y). + forall x y:X, x <> y -> + (exists U:Ensemble X, open U /\ In U x /\ ~ In U y) \/ + (exists U:Ensemble X, open U /\ ~ In U x /\ In U y). Lemma topological_property_T0_sep : topological_property T0_sep. Proof. - intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hsep x y neq. + apply Build_topological_property. + intros X Y f Hcont_f g Hcont_g Hfg Hsep x y neq. destruct (Hsep (g x) (g y)) as [[U [Hopen [Hin H']]] | [U [Hopen [H' Hin]]]]; [ shelve | left | right ]; exists (inverse_image g U); @@ -23,7 +26,7 @@ Proof. Unshelve. intro contra. eapply f_equal in contra. - rewrite Hfg, Hfg in contra. + rewrite (proj2 Hfg), (proj2 Hfg) in contra. contradiction. Qed. @@ -48,30 +51,20 @@ Proof. Qed. Definition T1_sep (X:TopologicalSpace) : Prop := - forall x:point_set X, closed (Singleton x). + forall x:X, closed (Singleton x). Lemma topological_property_T1_sep : topological_property T1_sep. Proof. - intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hsep x. - replace (Singleton x) with (inverse_image g (Singleton (g x))). - - red. - rewrite <- inverse_image_complement. - apply Hcont_g. - apply Hsep. - - apply Extensionality_Ensembles. - split; - red; - intros. - + destruct H. - inversion H. - eapply f_equal in H1. - rewrite Hfg, Hfg in H1. - subst. - constructor. - + inversion H. - subst. - constructor. - constructor. + apply Build_topological_property. + intros X Y f Hcont_f g Hcont_g Hfg Hsep x. + rewrite <- (proj1 (injective_inverse_image_Singleton g)). + 2: { + apply invertible_impl_bijective. + exists f. apply inverse_map_sym, Hfg. + } + apply continuous_closed. + { apply Hcont_g. } + apply Hsep. Qed. (** the [T1_sep] property is hereditary *) @@ -95,9 +88,9 @@ Proof. Qed. Definition Hausdorff (X:TopologicalSpace) : Prop := - forall x y:point_set X, x <> y -> - exists U:Ensemble (point_set X), - exists V:Ensemble (point_set X), + forall x y:X, x <> y -> + exists U:Ensemble X, + exists V:Ensemble X, open U /\ open V /\ In U x /\ In V y /\ Intersection U V = Empty_set. Definition T2_sep := Hausdorff. @@ -105,17 +98,19 @@ Definition T2_sep := Hausdorff. Definition topological_property_Hausdorff : topological_property Hausdorff. Proof. - intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hhaus x y neq. + apply Build_topological_property. + intros X Y f Hcont_f g Hcont_g Hfg Hhaus x y neq. destruct (Hhaus (g x) (g y)) as [U [V [HopenU [HopenV [HinU [HinV eq]]]]]]. - - intro contra. + { intro contra. eapply f_equal in contra. - now rewrite Hfg, Hfg in contra. - - exists (inverse_image g U), (inverse_image g V). - repeat split; - try apply Hcont_g; - trivial. - erewrite <- inverse_image_intersection, <- inverse_image_empty. - now f_equal. + now rewrite (proj2 Hfg), (proj2 Hfg) in contra. + } + exists (inverse_image g U), (inverse_image g V). + repeat split; + try apply Hcont_g; + trivial. + erewrite <- inverse_image_intersection, <- inverse_image_empty. + now f_equal. Qed. (** the [Hausdorff] property is hereditary *) @@ -144,36 +139,35 @@ Qed. Definition T3_sep (X:TopologicalSpace) : Prop := T1_sep X /\ - forall (x:point_set X) (F:Ensemble (point_set X)), - closed F -> ~ In F x -> exists U:Ensemble (point_set X), - exists V:Ensemble (point_set X), + forall (x:X) (F:Ensemble X), + closed F -> ~ In F x -> exists U:Ensemble X, + exists V:Ensemble X, open U /\ open V /\ In U x /\ Included F V /\ Intersection U V = Empty_set. Lemma topological_property_T3_sep : topological_property T3_sep. Proof. - intros X Y f Hf [HT1 H]. - split. - - eapply topological_property_T1_sep. - + exact Hf. - + assumption. - - destruct Hf as [g Hcont_f Hcont_g Hgf Hfg]. - intros y F Hcl Hn. - destruct (H (g y) (inverse_image f F)) as [U [V [HopenU [HopenV [HinU [Hincl eq]]]]]]. - + red. - rewrite <- inverse_image_complement. - now apply Hcont_f. - + intros [contra]. - now rewrite Hfg in contra. - + exists (inverse_image g U), (inverse_image g V). - repeat split; - try apply Hcont_g; - trivial. - * apply Hincl. - constructor. - now rewrite Hfg. - * erewrite <- inverse_image_intersection, <- inverse_image_empty. - now f_equal. + apply topological_property_and. + { apply topological_property_T1_sep. } + apply proper_sym_impl_iff. + { typeclasses eauto. } + intros X Y HXY H. + destruct HXY as [f [Hcont_f [g [Hcont_g Hfg]]]]. + intros y F Hcl Hn. + specialize (H (g y) (inverse_image f F)) as [U [V [HopenU [HopenV [HinU [Hincl eq]]]]]]. + { now apply continuous_closed. } + { intros [contra]. + now rewrite (proj2 Hfg) in contra. + } + exists (inverse_image g U), (inverse_image g V). + repeat split; + try apply Hcont_g; + trivial. + - apply Hincl. + constructor. + now rewrite (proj2 Hfg). + - erewrite <- inverse_image_intersection, <- inverse_image_empty. + now f_equal. Qed. (** the [T3_sep] property is hereditary *) @@ -207,13 +201,41 @@ Qed. Definition normal_sep (X:TopologicalSpace) : Prop := T1_sep X /\ - forall (F G:Ensemble (point_set X)), + forall (F G:Ensemble X), closed F -> closed G -> Intersection F G = Empty_set -> - exists U:Ensemble (point_set X), exists V:Ensemble (point_set X), + exists U:Ensemble X, exists V:Ensemble X, open U /\ open V /\ Included F U /\ Included G V /\ Intersection U V = Empty_set. Definition T4_sep := normal_sep. +Lemma topological_property_T4_sep : topological_property T4_sep. +Proof. + apply topological_property_and. + { apply topological_property_T1_sep. } + apply proper_sym_impl_iff. + { typeclasses eauto. } + intros X Y HXY H. + intros F G HF_closed HG_closed HFG. + destruct HXY as [f [Hcont_f [g [Hcont_g Hfg]]]]. + specialize (H (inverse_image f F) (inverse_image f G)) + as [U [V [HU_open [HV_open [HFU [HGV HUV]]]]]]. + { now apply continuous_closed. } + { now apply continuous_closed. } + { erewrite <- inverse_image_intersection, <- inverse_image_empty. + now f_equal. + } + exists (inverse_image g U), (inverse_image g V). + repeat split; + try apply Hcont_g; + trivial. + - apply HFU. constructor. + now rewrite (proj2 Hfg). + - apply HGV. constructor. + now rewrite (proj2 Hfg). + - erewrite <- inverse_image_intersection, <- inverse_image_empty. + now f_equal. +Qed. + Lemma T1_sep_impl_T0_sep: forall X:TopologicalSpace, T1_sep X -> T0_sep X. Proof. @@ -316,8 +338,8 @@ Qed. Lemma Hausdorff_impl_net_limit_is_unique_cluster_point: forall {X:TopologicalSpace} {I:DirectedSet} (x:Net I X) - (x0:point_set X), Hausdorff X -> net_limit x x0 -> - forall y:point_set X, net_cluster_point x y -> y = x0. + (x0:X), Hausdorff X -> net_limit x x0 -> + forall y:X, net_cluster_point x y -> y = x0. Proof. intros. destruct (net_cluster_point_impl_subnet_converges _ _ x y H1) as @@ -333,7 +355,7 @@ Qed. Lemma net_limit_is_unique_cluster_point_impl_Hausdorff: forall (X:TopologicalSpace), - (forall (I:DirectedSet) (x:Net I X) (x0 y:point_set X), + (forall (I:DirectedSet) (x:Net I X) (x0 y:X), net_limit x x0 -> net_cluster_point x y -> y = x0) -> Hausdorff X. Proof. diff --git a/theories/Topology/SubspaceTopology.v b/theories/Topology/SubspaceTopology.v index 2d35d1e5..fb3195da 100644 --- a/theories/Topology/SubspaceTopology.v +++ b/theories/Topology/SubspaceTopology.v @@ -1,5 +1,5 @@ From ZornsLemma Require Import - CardinalsEns + Cardinals DecidableDec FiniteIntersections Proj1SigInjective. diff --git a/theories/Topology/TietzeExtension.v b/theories/Topology/TietzeExtension.v index cf580681..a9e542ec 100644 --- a/theories/Topology/TietzeExtension.v +++ b/theories/Topology/TietzeExtension.v @@ -715,34 +715,37 @@ pose (U := characteristic_function_to_ensemble pose proof (open_interval_homeomorphic_to_real_line). fold U in H2. simpl in H2. -destruct H2 as [a [b]]. +destruct H2 as [a [Ha [b [Hb Hab]]]]. pose (f0 := fun x:SubspaceTopology F => subspace_inc U (a (f x))). destruct (open_bounded_Tietze_extension_theorem X F f0) as [g0 [? []]]; trivial. -- unfold f0. +{ unfold f0. apply continuous_composition. - + apply subspace_inc_continuous. - + now apply continuous_composition. -- intros. + - apply subspace_inc_continuous. + - now apply continuous_composition. +} +{ intros. unfold f0. destruct (a (f x)). now destruct i. -- assert (forall x:X, In U (g0 x)). - { intros. - constructor. - apply H8. } - pose (g0_U := continuous_factorization g0 U H9). - assert (continuous g0_U) by - now apply factorization_is_continuous. - exists (fun x:X => b (g0_U x)). - split. - { now apply continuous_composition. } - intros. - unfold g0_U, continuous_factorization. - generalize (H9 (subspace_inc F x)). - rewrite H7. - intros. - replace (exist _ (f0 x) i) with (a (f x)) by - now apply (proj1_sig_injective (In U)). +} +assert (forall x:X, In U (g0 x)) as HUg0. +{ intros. + constructor. apply H4. +} +pose (g0_U := continuous_factorization g0 U HUg0). +assert (continuous g0_U) by + now apply factorization_is_continuous. +exists (fun x:X => b (g0_U x)). +split. +{ now apply continuous_composition. } +intros. +unfold g0_U, continuous_factorization. +generalize (HUg0 (subspace_inc F x)). +rewrite H3. +intros. +replace (exist _ (f0 x) i) with (a (f x)) by + now apply (proj1_sig_injective (In U)). +apply Hab. Qed. diff --git a/theories/ZornsLemma/Cardinals.v b/theories/ZornsLemma/Cardinals.v index c780c5cf..9299e1c4 100644 --- a/theories/ZornsLemma/Cardinals.v +++ b/theories/ZornsLemma/Cardinals.v @@ -1,604 +1,8 @@ -From Coq Require Export Relation_Definitions. -From Coq Require Import ClassicalChoice. -From Coq Require Import ProofIrrelevance. -From Coq Require Import FunctionalExtensionality. -From Coq Require Import Description. -From ZornsLemma Require Export FunctionProperties. -From ZornsLemma Require Import FunctionPropertiesEns. -From ZornsLemma Require Import Relation_Definitions_Implicit. -From ZornsLemma Require Import CSB. -From ZornsLemma Require Import ZornsLemma. -From ZornsLemma Require Import EnsemblesImplicit. -From ZornsLemma Require Import CountableTypes. -From ZornsLemma Require Import FiniteTypes. -From ZornsLemma Require Import InfiniteTypes. -From Coq Require Import RelationClasses. - -Definition eq_cardinal (A B : Type) : Prop := - exists f : A -> B, bijective f. -Definition le_cardinal (A B : Type) : Prop := - exists f : A -> B, injective f. - -Definition lt_cardinal (kappa lambda:Type) : Prop := - le_cardinal kappa lambda /\ ~ eq_cardinal kappa lambda. -Definition ge_cardinal (kappa lambda:Type) : Prop := - le_cardinal lambda kappa. -Definition gt_cardinal (kappa lambda:Type) : Prop := - lt_cardinal lambda kappa. - -Global Instance eq_cardinal_equiv : Equivalence eq_cardinal. -Proof. -split. -- red; intro. exists id. apply id_bijective. -- red; intros ? ? [f Hf]. - apply bijective_impl_invertible in Hf. - destruct Hf as [g Hfg Hgf]. - exists g. - apply invertible_impl_bijective. - exists f; auto. -- intros ? ? ? [f Hf] [g Hg]. - exists (compose g f). - apply bijective_compose; auto. -Qed. - -Instance le_cardinal_preorder : PreOrder le_cardinal. -Proof. -split. -- red; intro; exists id; apply id_bijective. -- intros ? ? ? [f Hf] [g Hg]. - exists (compose g f). - apply injective_compose; auto. -Qed. - -Instance le_cardinal_PartialOrder : - PartialOrder eq_cardinal le_cardinal. -Proof. -split. -- intros [f Hf]; split. - + exists f; apply Hf. - + apply bijective_impl_invertible in Hf. - destruct Hf as [g Hgf Hfg]. - exists g. apply invertible_impl_bijective. - exists f; auto. -- intros [[f Hf] [g Hg]]. - apply CSB with (f := f) (g := g); auto. -Qed. - -Lemma eq_cardinal_impl_le_cardinal: forall kappa lambda: Type, - eq_cardinal kappa lambda -> le_cardinal kappa lambda. -Proof. -intros ? ? [f Hf]. -exists f. apply Hf. -Qed. - -(** This lemma is helpful, if one wants - to avoid using an axiom of choice. *) -Lemma le_cardinal_img_inj_ens {X Y : Type} (Z : Type) (f : X -> Y) (U : Ensemble X) : - injective_ens f U -> - le_cardinal X Z -> - le_cardinal (sig (Im U f)) Z. -Proof. - intros Hf [g Hg]. - assert (forall p : { y : Y | In (Im U f) y }, - { x : X | In U x /\ (proj1_sig p) = f x}) as H. - { intros [y Hy]. - simpl. - apply constructive_definite_description. - inversion Hy; subst; clear Hy. - exists x; split; auto. - intros x' []; auto. - } - exists (compose g (fun p => proj1_sig (H p))). - apply injective_compose; auto. - clear g Hg. - intros p0 p1 Hp. - pose proof (proj2_sig (H p0)) as [Hp00 Hp01]. - pose proof (proj2_sig (H p1)) as [Hp10 Hp11]. - destruct p0 as [y0 Hy0], p1 as [y1 Hy1]. - simpl in *. rewrite <- Hp in Hp11. - cut (y0 = y1); try congruence. - intros. destruct H0. - destruct (proof_irrelevance _ Hy0 Hy1). - reflexivity. -Qed. - -Definition countable_img_inj {X Y : Type} (f : X -> Y) (U : Ensemble X) : - injective_ens f U -> - CountableT X -> - Countable (Im U f) := - @le_cardinal_img_inj_ens X Y nat f U. - -Lemma cantor_diag: forall (X:Type) (f:X->(X->bool)), - ~ surjective f. -Proof. -intros. -red; intro. -pose (g := fun x:X => negb (f x x)). -pose proof (H g). -destruct H0. -assert (f x x = g x). -{ rewrite H0. - reflexivity. -} -unfold g in H1. -destruct (f x x). -- discriminate H1. -- discriminate H1. -Qed. - -Lemma P_neq_not_P: forall (P:Prop), P <> ~P. -Proof. -unfold not; intros. -assert (~P). -{ unfold not; intro. - assert (P->False). - { rewrite <- H. - assumption. - } - tauto. -} -assert P. -{ rewrite H. - assumption. -} -contradiction. -Qed. - -Lemma cantor_diag2: forall (X:Type) (f:X->(X->Prop)), - ~ surjective f. -Proof. -unfold not; intros. -pose (g := fun x:X => ~ f x x). -pose proof (H g). -destruct H0. -assert (f x x = g x). -{ rewrite H0. - reflexivity. -} -unfold g in H1. -contradiction P_neq_not_P with (f x x). -Qed. - -Lemma cardinals_unbounded: forall kappa:Type, - gt_cardinal (Ensemble kappa) kappa. -Proof. -intros ?. -split. -- exists Singleton. - red; intros. - apply Powerset_facts.Singleton_injective. - assumption. -- intros [f Hf]. - apply (cantor_diag2 _ f). - apply Hf. -Qed. - -(* The results below require Axiom of Choice *) - -Lemma surj_le_cardinal: forall {X Y:Type} (f:X->Y), - surjective f -> le_cardinal Y X. -Proof. -intros. -pose proof (choice (fun (y:Y) (x:X) => f x = y) H). -simpl in H0. -destruct H0 as [g]. -exists g. -red; intros. -congruence. -Qed. - -Section le_cardinal_total. - -Variable X Y:Type. - -Record partial_injection : Type := { - pi_dom: Ensemble X; - pi_func: forall x:X, In pi_dom x -> Y; - pi_inj: forall (x1 x2:X) (i1:In pi_dom x1) (i2:In pi_dom x2), - pi_func x1 i1 = pi_func x2 i2 -> x1 = x2 -}. -Record partial_injection_ord (pi1 pi2:partial_injection) : Prop := { - pi_dom_inc: Included (pi_dom pi1) (pi_dom pi2); - pi_func_ext: forall (x:X) (i1:In (pi_dom pi1) x) - (i2:In (pi_dom pi2) x), - pi_func pi1 x i1 = pi_func pi2 x i2 -}. - -Lemma partial_injection_preord: preorder partial_injection_ord. -Proof. -constructor. -- red; intros. - destruct x. - constructor. - + auto with sets. - + intros. simpl in *. - assert (i1 = i2). - { apply proof_irrelevance. } - rewrite H. - reflexivity. -- red; intros. - destruct H. - destruct H0. - constructor. - + auto with sets. - + intros. - assert (In (pi_dom y) x0). - { auto with sets. } - transitivity (pi_func y x0 H); trivial. -Qed. - -Lemma partial_injection_chain_ub: forall S:Ensemble partial_injection, - chain partial_injection_ord S -> exists x:partial_injection, - forall y:partial_injection, In S y -> partial_injection_ord y x. -Proof. -intros. -pose (ub_dom := [x:X | exists y:partial_injection, - In S y /\ In (pi_dom y) x]). -assert (forall x:X, In ub_dom x -> { y:Y | exists z:partial_injection, - In S z /\ exists i:In (pi_dom z) x, pi_func z x i = y }). -{ intros. - apply constructive_definite_description. - destruct H0. - destruct H0. - destruct H0. - exists (pi_func x0 x H1). - red; split. - - exists x0. - split. - + assumption. - + exists H1. - reflexivity. - - intros. - destruct H2. - destruct H2. - destruct H3. - pose proof (H x0 x1 H0 H2). - case H4. - + intro. - rewrite <- H3. - apply pi_func_ext. - assumption. - + intro. - rewrite <- H3. - symmetry. - apply pi_func_ext. - assumption. -} -assert (forall (x1 x2:X) (i1:In ub_dom x1) (i2:In ub_dom x2), - proj1_sig (X0 x1 i1) = proj1_sig (X0 x2 i2) -> x1 = x2). -{ intros. - destruct X0 in H0. - destruct X0 in H0. - simpl in H0. - destruct H0. - destruct e. - destruct H0. - destruct H1. - destruct e0. - destruct H2. - destruct H3. - destruct H1. - case (H x0 x4 H0 H2). - - intro. - assert (In (pi_dom x4) x1). - { apply (pi_dom_inc _ _ H1). - assumption. - } - assert (pi_func x4 x1 H4 = pi_func x4 x2 x5). - { rewrite H3. - symmetry. - apply pi_func_ext. - assumption. - } - apply pi_inj in H5. - assumption. - - intro. - assert (In (pi_dom x0) x2). - { apply (pi_dom_inc _ _ H1). - assumption. - } - assert (pi_func x0 x1 x3 = pi_func x0 x2 H4). - { rewrite <- H3. - apply pi_func_ext. - assumption. - } - apply pi_inj in H5. - assumption. -} -exists (Build_partial_injection ub_dom - (fun (x:X) (i:In ub_dom x) => proj1_sig (X0 x i)) H0). -intros. -constructor. -- simpl. - red; intros. - constructor. - exists y. - tauto. -- simpl. - intros. - destruct (X0 x i2). - simpl. - destruct e. - destruct H2. - destruct H3. - destruct H3. - case (H y x1 H1 H2). - + intro. - apply pi_func_ext. - assumption. - + intro. - symmetry. - apply pi_func_ext. - assumption. -Qed. - -Lemma premaximal_partial_injection: - exists x:partial_injection, premaximal partial_injection_ord x. -Proof. -apply ZornsLemmaForPreorders. -- exact partial_injection_preord. -- exact partial_injection_chain_ub. -Qed. - -Lemma premaximal_pi_is_full_or_surj: - forall x:partial_injection, premaximal partial_injection_ord x -> - pi_dom x = Full_set \/ - forall y:Y, exists x0:X, exists i:(In (pi_dom x) x0), - pi_func x x0 i = y. -Proof. -intros. -case (classic (pi_dom x = Full_set)). -{ left. - trivial. -} -intro. -assert (exists x0:X, ~ In (pi_dom x) x0). -{ apply NNPP. - intuition. - apply H0. - apply Extensionality_Ensembles. - red; split. - - red; intros. - constructor. - - red; intros. - apply NNPP. - intuition. - apply H1. - exists x0. - assumption. -} -right. -destruct H1. -intros. -apply NNPP. -intuition. - -pose (pi_dom_ext := Add (pi_dom x) x0). -assert (forall (x':X), In pi_dom_ext x' -> - { y':Y | (exists i2:In (pi_dom x) x', y' = pi_func x x' i2) \/ - (x' = x0 /\ y' = y) }). -{ intros. - apply constructive_definite_description. - case H3. - - intros. - exists (pi_func x x1 H4). - red; split. - + left. - exists H4. - reflexivity. - + intros. - case H5. - * intro. - destruct H6. - subst. - replace H4 with x2. - -- reflexivity. - -- apply proof_irrelevance. - * intros. - destruct H6. - subst. - contradict H1. - assumption. - - intros. - destruct H4. - exists y. - red; split. - + right. - tauto. - + intros. - case H4. - * intro. - destruct H5. - subst. - contradiction H1. - * intros. - symmetry. - tauto. -} - -pose (pi_func_ext0 := fun (x:X) (i:In pi_dom_ext x) => - proj1_sig (X0 x i)). - -assert (forall (x1:X) (i:In (pi_dom x) x1) (i2:In pi_dom_ext x1), - pi_func_ext0 x1 i2 = pi_func x x1 i). -{ intros. - unfold pi_func_ext0. - destruct (X0 x1 i2). - simpl. - case o. - - intros. - destruct H3. - subst. - replace i with x3. - + reflexivity. - + apply proof_irrelevance. - - intros. - destruct H3. - contradiction H1. - rewrite <- H3. - assumption. -} - -assert (forall (i:In pi_dom_ext x0), pi_func_ext0 x0 i = y). -{ intros. - unfold pi_func_ext0. - destruct (X0 x0 i); simpl. - case o. - - intro. - destruct H4. - contradiction H1. - - tauto. -} - -assert (forall (x1 x2:X) (i1:In pi_dom_ext x1) (i2:In pi_dom_ext x2), - pi_func_ext0 x1 i1 = pi_func_ext0 x2 i2 -> x1 = x2). -{ intros. - inversion i1; subst. - - inversion i2; subst. - + rewrite (H3 x1 H6 i1) in H5. - rewrite (H3 x2 H7 i2) in H5. - apply pi_inj in H5. - assumption. - + destruct H7. - rewrite (H3 x1 H6 i1) in H5. - rewrite H4 in H5. - contradiction H2. - exists x1, H6. - assumption. - - destruct H6. - rewrite H4 in H5. - inversion i2. - + rewrite (H3 x2 H6 i2) in H5. - contradiction H2. - exists x2, H6. - symmetry; assumption. - + destruct H6. - reflexivity. -} - -pose (pi_ext := Build_partial_injection pi_dom_ext pi_func_ext0 H5). -assert (partial_injection_ord x pi_ext). -{ constructor. - - unfold pi_ext; simpl. - unfold pi_dom_ext. - red; intros. - left. - assumption. - - intros. - symmetry. - apply H3. -} - -apply H in H6. -contradiction H1. -apply (pi_dom_inc _ _ H6). -simpl. -right. -constructor. -Qed. - -Lemma types_comparable: (exists f:X->Y, injective f) \/ - (exists f:Y->X, injective f). -Proof. -pose proof premaximal_partial_injection. -destruct H. -apply premaximal_pi_is_full_or_surj in H. -case H. -- left. - assert (forall x0:X, In (pi_dom x) x0). - { rewrite H0. - constructor. - } - exists (fun x0:X => pi_func x x0 (H1 x0)). - red; intros. - apply pi_inj in H2. - assumption. -- right. - assert (forall y:Y, { x0:X | exists i:In (pi_dom x) x0, pi_func x x0 i = y }). - { intro. - apply constructive_definite_description. - pose proof (H0 y). - destruct H1. - exists x0. - red; split. - - assumption. - - intros. - destruct H1. - destruct H2. - destruct H2. - apply pi_inj in H1. - assumption. - } - exists (fun y:Y => proj1_sig (X0 y)). - red; intros. - destruct X0 in H1; destruct X0 in H1; simpl in H1. - destruct e; destruct e0. - subst. - replace x3 with x4. - + reflexivity. - + apply proof_irrelevance. -Qed. - -End le_cardinal_total. - -Corollary le_cardinal_total: forall kappa lambda:Type, - le_cardinal kappa lambda \/ le_cardinal lambda kappa. -Proof. -intros T0 T1. -destruct (types_comparable T0 T1) as [[f]|[f]]; - [left|right]; - exists f; assumption. -Qed. - -Lemma CountableT_cardinality {X : Type} : - CountableT X <-> le_cardinal X nat. -Proof. - reflexivity. -Qed. - -Lemma FiniteT_cardinality {X : Type} : - FiniteT X <-> lt_cardinal X nat. -Proof. -split; intros. -- constructor. - + destruct (FiniteT_nat_embeds H) as [f]. - exists f. assumption. - + intros [f []]. - apply nat_infinite. - apply surj_finite with (f := f); auto. - intros; apply classic. -- destruct H as [[f Hf] H]. - apply NNPP. intro. - destruct (infinite_nat_inj _ H0) as [g]. - contradict H. - apply CSB with (f := f) (g := g); - auto. -Qed. - -Lemma cardinal_no_inj_equiv_lt_cardinal (A B : Type) : - (forall f : A -> B, ~ injective f) <-> - lt_cardinal B A. -Proof. -split. -- intros. - split. - + (* |B| ≤ |A| *) - destruct (le_cardinal_total B A). - { assumption. } - destruct H0 as [f Hf]. - specialize (H f Hf). - contradiction. - + (* |B| ≠ |A| *) - intro. - destruct H0 as [f Hf]. - apply bijective_impl_invertible in Hf. - destruct Hf as [g Hgf Hfg]. - pose proof (invertible_impl_bijective g). - destruct H0 as [Hg0 Hg1]. - { exists f; assumption. } - apply (H g Hg0). -- intros [[f Hf]] g Hg. - contradict H. - apply CSB with (f := f) (g := g); - assumption. -Qed. +(** Export all files in the folder [Cardinals] *) +From ZornsLemma Require Export + Cardinals.Cardinals + Cardinals.CardinalsEns + Cardinals.Combinatorics + Cardinals.CSB + Cardinals.Diagonalization + Cardinals.LeastCardinalsEns. diff --git a/theories/ZornsLemma/CSB.v b/theories/ZornsLemma/Cardinals/CSB.v similarity index 58% rename from theories/ZornsLemma/CSB.v rename to theories/ZornsLemma/Cardinals/CSB.v index 0c875c64..9ca80e17 100644 --- a/theories/ZornsLemma/CSB.v +++ b/theories/ZornsLemma/Cardinals/CSB.v @@ -1,10 +1,14 @@ From Coq Require Import Classical - Description. -From ZornsLemma Require Export - FunctionProperties. + Description + RelationClasses. From ZornsLemma Require Import - DecidableDec. + Cardinals.Cardinals + Cardinals.CardinalsEns + DecidableDec + FunctionProperties + FunctionPropertiesEns + Proj1SigInjective. (* CSB = Cantor-Schroeder-Bernstein theorem *) @@ -203,13 +207,123 @@ unfold CSB_bijection2; case (classic_dec (Y_even y)). + trivial. Qed. -Theorem CSB: exists h:X->Y, bijective h. +Theorem CSB_inverse_map : + exists (h0 : X -> Y) (h1 : Y -> X), + inverse_map h0 h1. +Proof. + exists CSB_bijection, CSB_bijection2. + split. + - exact CSB_comp1. + - exact CSB_comp2. +Qed. + +Theorem CSB: eq_cardinal X Y. Proof. exists CSB_bijection. -apply invertible_impl_bijective. -exists CSB_bijection2. +exists CSB_bijection2. split. - exact CSB_comp1. - exact CSB_comp2. Qed. End CSB. + +#[export] +Instance le_cardinal_PartialOrder : + PartialOrder eq_cardinal le_cardinal. +Proof. +split. +- intros [f Hf]; split. + + exists f. apply invertible_impl_bijective; assumption. + + destruct Hf as [g Hfg]. + exists g. apply invertible_impl_bijective. + exists f. apply inverse_map_sym. + assumption. +- intros [[f Hf] [g Hg]]. + apply CSB_inverse_map with (f := f) (g := g); auto. +Qed. + +Theorem CSB_ens {X Y : Type} + (U : Ensemble X) (V : Ensemble Y) + (f : X -> Y) (g : Y -> X) : + range f U V -> + range g V U -> + injective_ens f U -> + injective_ens g V -> + exists h : X -> Y, + range h U V /\ + bijective_ens h U V. +Proof. + intros. + assert (exists h0 : sig U -> sig V, invertible h0) + as [h0 Hh]. + { apply CSB with (f := range_restr f U V H) + (g := range_restr g V U H0); + apply injective_ens_char; assumption. + } + destruct (classic (inhabited Y)). + 2: { + assert (X -> False) as HX. + { intros x. + apply H3. constructor. + apply (f x). + } + exists (fun x => False_rect Y (HX x)). + repeat split; intros ? ?; try contradiction. + contradict H3; constructor; auto. + } + clear f g H H0 H1 H2. + destruct H3 as [y0]. + exists (sig_fn_extend (compose (@proj1_sig Y V) h0) y0). + assert (range (compose (proj1_sig (P:=V)) h0) + Full_set V). + { apply (range_compose _ Full_set). + - apply range_full. + - intros ? _. apply proj2_sig. + } + split; [|split]. + - apply sig_fn_extend_range; assumption. + - apply sig_fn_extend_injective_ens. + apply injective_compose. + + apply invertible_impl_bijective, Hh. + + intros ? ?. apply proj1_sig_injective. + - apply sig_fn_extend_surjective_ens. + intros y Hy. + destruct Hh as [h' [Hh0 Hh1]]. + exists (h' (exist V y Hy)). + split; [constructor|]. + unfold compose. + rewrite Hh1. + reflexivity. +Qed. + +Corollary le_cardinal_ens_antisymmetry + {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : + le_cardinal_ens U V -> + le_cardinal_ens V U -> + eq_cardinal_ens U V. +Proof. + intros [H|[f [Hf0 Hf1]]]. + { left. assumption. } + intros [H|[g [Hg0 Hg1]]]. + { apply eq_cardinal_ens_sym. + left. assumption. + } + right. + apply (CSB_ens _ _ f g); assumption. +Qed. + +Lemma le_lt_cardinal_ens_transitive {X Y Z : Type} + (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : + le_cardinal_ens U V -> + lt_cardinal_ens V W -> + lt_cardinal_ens U W. +Proof. + intros HUV [HVW HVWn]. + split. + { eapply le_cardinal_ens_transitive; eauto. } + intros Heq. + contradict HVWn. + apply eq_cardinal_ens_sym in Heq. + apply le_cardinal_ens_antisymmetry; auto. + eapply le_cardinal_ens_Proper_l; eauto. +Qed. diff --git a/theories/ZornsLemma/Cardinals/Cardinals.v b/theories/ZornsLemma/Cardinals/Cardinals.v new file mode 100644 index 00000000..0d9663e9 --- /dev/null +++ b/theories/ZornsLemma/Cardinals/Cardinals.v @@ -0,0 +1,92 @@ +From Coq Require Import + ClassicalChoice + Description + FunctionalExtensionality + ProofIrrelevance. +From ZornsLemma Require Import + FunctionProperties + FunctionPropertiesEns + ZornsLemma. +From Coq Require Import RelationClasses. + +Definition le_cardinal (A B : Type) : Prop := + exists f : A -> B, injective f. +Definition eq_cardinal (X Y : Type) : Prop := + exists (f : X -> Y) (g : Y -> X), inverse_map f g. + +Definition lt_cardinal (kappa lambda:Type) : Prop := + le_cardinal kappa lambda /\ ~ eq_cardinal kappa lambda. + +#[export] +Instance le_cardinal_preorder : PreOrder le_cardinal. +Proof. +split. +- red; intro; exists id; apply id_bijective. +- intros ? ? ? [f Hf] [g Hg]. + exists (compose g f). + apply injective_compose; auto. +Qed. + +#[export] +Instance eq_cardinal_equiv : Equivalence eq_cardinal. +Proof. +split. +- red; intro. exists id, id. apply id_inverse_map. +- red; intros ? ? [f [g Hfg]]. + exists g, f. apply inverse_map_sym. assumption. +- intros ? ? ? [f Hf] [g Hg]. + exists (compose g f). + apply invertible_compose; assumption. +Qed. + +Lemma eq_cardinal_impl_le_cardinal: forall kappa lambda: Type, + eq_cardinal kappa lambda -> le_cardinal kappa lambda. +Proof. +intros ? ? [f Hf]. +exists f. apply invertible_impl_bijective; auto. +Qed. + +(** This lemma is helpful, if one wants + to avoid using an axiom of choice. *) +Lemma le_cardinal_img_inj_ens {X Y : Type} (Z : Type) (f : X -> Y) (U : Ensemble X) : + injective_ens f U -> + le_cardinal X Z -> + le_cardinal (sig (Im U f)) Z. +Proof. + intros Hf [g Hg]. + assert (forall p : { y : Y | In (Im U f) y }, + { x : X | In U x /\ (proj1_sig p) = f x}) as H. + { intros [y Hy]. + simpl. + apply constructive_definite_description. + inversion Hy; subst; clear Hy. + exists x; split; auto. + intros x' []; auto. + } + exists (compose g (fun p => proj1_sig (H p))). + apply injective_compose; auto. + clear g Hg. + intros p0 p1 Hp. + pose proof (proj2_sig (H p0)) as [Hp00 Hp01]. + pose proof (proj2_sig (H p1)) as [Hp10 Hp11]. + destruct p0 as [y0 Hy0], p1 as [y1 Hy1]. + simpl in *. rewrite <- Hp in Hp11. + cut (y0 = y1); try congruence. + intros. destruct H0. + destruct (proof_irrelevance _ Hy0 Hy1). + reflexivity. +Qed. + +(* The results below require Axiom of Choice *) + +Lemma surj_le_cardinal: forall {X Y:Type} (f:X->Y), + surjective f -> le_cardinal Y X. +Proof. +intros. +pose proof (choice (fun (y:Y) (x:X) => f x = y) H). +simpl in H0. +destruct H0 as [g]. +exists g. +red; intros. +congruence. +Qed. diff --git a/theories/ZornsLemma/Cardinals/CardinalsEns.v b/theories/ZornsLemma/Cardinals/CardinalsEns.v new file mode 100644 index 00000000..9a34a35d --- /dev/null +++ b/theories/ZornsLemma/Cardinals/CardinalsEns.v @@ -0,0 +1,393 @@ +(** Instead of comparing cardinalities of elements of [Type], + compare cardinalities of ensembles. + With this technique, we can avoid problems w.r.t. type universes + that occur with the approach of [ZornsLemma.Cardinals]. + + On the other hand, we need classical logic more often, because a + statement like [eq_cardinal_ens] decides whether the ensemble and + a type are inhabited or not. + + Similarly, we can not define [eq_cardinal_ens] via + [inverse_map_ens], because that leads to a notion incompatible + with [le_cardinal_ens]. Namely it would reqiure classical logic + to prove [eq_cardinal_ens -> le_cardinal_ens]. +*) +From Coq Require Import + ClassicalChoice + Description + Lia + PeanoNat + Program.Subset. +From ZornsLemma Require Import + Cardinals.Cardinals + DecidableDec + Families + FunctionProperties + FunctionPropertiesEns + InverseImage + Powerset_facts + Proj1SigInjective + ReverseMath.AddSubtract. +From Coq Require Import + RelationClasses. + +Definition eq_cardinal_ens {A B : Type} + (U : Ensemble A) (V : Ensemble B) : Prop := + ((B -> False) /\ forall a : A, ~ In U a) \/ + exists f : A -> B, + range f U V /\ bijective_ens f U V. +Definition le_cardinal_ens {A B : Type} + (U : Ensemble A) (V : Ensemble B) : Prop := + ((B -> False) /\ forall a : A, ~ In U a) \/ + exists f : A -> B, + range f U V /\ injective_ens f U. +Definition lt_cardinal_ens {A B : Type} + (U : Ensemble A) (V : Ensemble B) : Prop := + le_cardinal_ens U V /\ + ~ eq_cardinal_ens V U. +Definition ge_cardinal_ens {A B : Type} + (U : Ensemble A) (V : Ensemble B) : Prop := + (forall b : B, ~ In V b) \/ + exists f : A -> B, + range f U V /\ surjective_ens f U V. + +#[export] +Instance eq_cardinal_ens_Reflexive (A : Type) : + Reflexive (@eq_cardinal_ens A A). +Proof. + right. + exists id. split; auto. + - reflexivity. + - apply bijective_ens_id. +Qed. + +Lemma eq_cardinal_ens_sym_dec {A B : Type} + (HA : inhabited A \/ ~ inhabited A) + (U : Ensemble A) (V : Ensemble B) + (HVdec : forall b : B, In V b \/ ~ In V b) : + eq_cardinal_ens U V -> + eq_cardinal_ens V U. +Proof. + intros [[H0 H1]|[f [Hf0 Hf1]]]. + - right. + exists (fun b : B => + False_rect A (H0 b)). + split; [|split]; intros ? ?; try contradiction. + firstorder. + - destruct HA. + 2: { + left. split. + { intros a; apply H; constructor; auto. } + intros b Hb. + destruct Hf1 as [_ Hf1]. + specialize (Hf1 b Hb) as [a [Ha0 Ha1]]. + apply H. constructor; auto. + } + right. + destruct H as [a0]. + pose proof (bijective_impl_invertible_ens_dec + f U V a0 HVdec Hf0 Hf1) as [g Hfg]. + exists g. split. + + apply (inverse_map_ens_surjective_ens_range f); auto. + apply Hf1. + + apply (inverse_map_ens_range_bijective_ens f); auto. +Qed. + +Lemma eq_cardinal_ens_sym {A B : Type} + (U : Ensemble A) (V : Ensemble B) : + eq_cardinal_ens U V -> + eq_cardinal_ens V U. +Proof. + apply eq_cardinal_ens_sym_dec. + - apply classic. + - intros ?. apply classic. +Qed. + +Lemma eq_cardinal_ens_trans {A B C : Type} + (U : Ensemble A) (V : Ensemble B) (W : Ensemble C) : + eq_cardinal_ens U V -> eq_cardinal_ens V W -> + eq_cardinal_ens U W. +Proof. + intros [[H0 H1]|[f [Hf0 Hf1]]]. + { intros [[H2 H3]|[g [Hg0 Hg1]]]. + { left. split; auto. } + destruct (classic (inhabited C)). + 2: now left; split; auto. + right. + destruct H as [c]. + exists (fun _ => c); split; [|split]. + - intros x Hx. specialize (H1 x Hx); contradiction. + - intros ? ? Hx. specialize (H1 _ Hx); contradiction. + - intros z Hz. + destruct Hg1 as [Hg1 Hg2]. + specialize (Hg2 z Hz) as [b Hb]. + contradiction. + } + intros [[H0 H1]|[g [Hg0 Hg1]]]. + { left. split; auto. + intros a Ha. + apply (H1 (f a)). + apply Hf0. assumption. + } + right. exists (compose g f). + split. + - eapply range_compose; eauto. + - eapply bijective_ens_compose; eauto. +Qed. + +Lemma eq_cardinal_ens_le {A B : Type} + (U : Ensemble A) (V : Ensemble B) : + eq_cardinal_ens U V -> + le_cardinal_ens U V. +Proof. + intros [H|[f [Hf0 [Hf1 _]]]]. + { left; auto. } + right. exists f; split; auto. +Qed. + +Section compose. + Context {A B C : Type} + (U : Ensemble A) (V : Ensemble B) (W : Ensemble C). + + Lemma le_cardinal_ens_transitive : + le_cardinal_ens U V -> + le_cardinal_ens V W -> + le_cardinal_ens U W. + Proof. + intros HUV [[H0 H1]|[g [Hg0 Hg1]]]. + { left. split; auto. + destruct HUV as [[H2 H3]|[f [Hf0 Hf1]]]. + { assumption. } + intros a Ha. + apply (H1 (f a)). + apply (Hf0 a Ha). + } + destruct HUV as [[H0 H1]|[f [Hf0 Hf1]]]. + { destruct (classic (inhabited C)). + - right. + destruct H as [c0]. + exists (fun _ => c0). split. + + intros a Ha. firstorder. + + intros a0 a1 Ha0 Ha1; firstorder. + - left. split; auto. + } + right. exists (compose g f). + split. + - eapply range_compose; eauto. + - eapply injective_ens_compose; eauto. + Qed. +End compose. + +Lemma le_cardinal_ens_Proper_r {X Y Z : Type} + (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : + eq_cardinal_ens V W -> + le_cardinal_ens U V -> le_cardinal_ens U W. +Proof. + intros H0 H1. + apply eq_cardinal_ens_le in H0. + eapply le_cardinal_ens_transitive; eauto. +Qed. + +Lemma le_cardinal_ens_Proper_l {X Y Z : Type} + (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : + eq_cardinal_ens U V -> + le_cardinal_ens U W -> le_cardinal_ens V W. +Proof. + intros H0 H1. + apply eq_cardinal_ens_sym in H0. + apply eq_cardinal_ens_le in H0. + eapply le_cardinal_ens_transitive; eauto. +Qed. + +Lemma le_cardinal_ens_Empty_set (X : Type) {Y : Type} + (U : Ensemble Y) : + le_cardinal_ens (@Empty_set X) U. +Proof. + destruct (classic (inhabited Y)). + - destruct H as [y]. + right. exists (fun _ => y). + firstorder. + - left. firstorder. +Qed. + +Lemma eq_cardinal_ens_empty {X Y : Type} (U : Ensemble Y) : + eq_cardinal_ens (@Empty_set X) U <-> + (forall y : Y, ~ In U y). +Proof. + split. + - intros [|[f [Hf0 [Hf1 Hf2]]]] y Hy. + + tauto. + + specialize (Hf2 y Hy) as [x [Hx Hxy]]. + contradiction. + - intros HU. + destruct (classic (inhabited Y)). + 2: { + left; auto with sets. + } + right. + destruct H as [y0]. + exists (fun _ => y0). split; firstorder. +Qed. + +Lemma eq_cardinal_ens_Im_injective + {X Y : Type} (U : Ensemble X) (f : X -> Y) : + injective_ens f U -> + eq_cardinal_ens U (Im U f). +Proof. + intros Hf. + right. exists f. + split. + - apply range_char_Im. + reflexivity. + - split. + + assumption. + + apply surjective_ens_Im. +Qed. + +Lemma le_cardinal_ens_Im {X Y : Type} (f : X -> Y) + (U : Ensemble X) : + le_cardinal_ens (Im U f) U. +Proof. + destruct (classic (Inhabited U)). + 2: { + destruct (classic (inhabited X)). + - destruct H0 as [x0]. + right. exists (fun _ => x0). + split; intros ? **. + + contradict H. + inversion H0; subst; clear H0. + firstorder. + + contradict H. + inversion H0; subst; clear H0. + firstorder. + - left; split; [firstorder|]. + intros y Hy. + inversion Hy; subst; clear Hy. + apply H; exists x. assumption. + } + destruct H as [x0 Hx0]. + pose proof + (surjective_ens_right_inverse + U (Im U f) f x0 Hx0) as [g [Hg0 Hg1]]. + { apply range_char_Im. + reflexivity. + } + { apply surjective_ens_Im. } + right. exists g; split; auto. + intros y0 y1 Hy0 Hy1. + pose proof (Hg1 y0 Hy0). + pose proof (Hg1 y1 Hy1). + congruence. +Qed. + +Lemma eq_cardinal_ens_sig {X : Type} (P : X -> Prop) : + eq_cardinal_ens (@Full_set (sig P)) P. +Proof. + right. + exists (@proj1_sig X P). + split; [|split]. + - intros p _. apply proj2_sig. + - intros p0 p1 _ _. + destruct p0, p1. + apply subset_eq_compat. + - intros x Hx. + exists (exist P x Hx). + split; [constructor|reflexivity]. +Qed. + +Lemma le_cardinal_ens_Included {X : Type} + (U V : Ensemble X) : + Included U V -> + le_cardinal_ens U V. +Proof. + right. exists id. firstorder. +Qed. + +Lemma le_cardinal_ens_surj {X Y : Type} + (U : Ensemble X) (V : Ensemble Y) : + le_cardinal_ens U V <-> + ge_cardinal_ens V U. +Proof. + split. + - intros [[H0 H1]|[f [Hf0 Hf1]]]. + { right. exists (fun y : Y => False_rect X (H0 y)). + split; intros ? ?; firstorder; try contradiction. + } + destruct (classic (Inhabited U)). + 2: { + left. firstorder. + } + destruct H as [x0 Hx0]. + right. + pose proof (injective_ens_left_inverse U V f x0 + Hx0 Hf0 Hf1) as [g [Hg0 Hg1]]. + exists g; split; auto. + intros x Hx. + exists (f x). split; auto. + symmetry. apply Hg1. + assumption. + - intros [H|[f [Hf0 Hf1]]]. + { destruct (classic (inhabited Y)). + { destruct H0 as [y]. + right. exists (fun _ => y). + split; intros ? ?; firstorder. + } + left. split; auto. + } + destruct (classic (Inhabited V)). + 2: { + destruct (classic (inhabited Y)). + { destruct H0 as [y0]. + right. exists (fun _ => y0). + firstorder. + } + left. firstorder. + } + destruct H as [y Hy]. + pose proof (surjective_ens_right_inverse V U f y Hy Hf0 Hf1) + as [g [Hg0 Hg1]]. + right. exists g; split; auto. + intros x0 x1 Hx0 Hx1 Hx. + pose proof (Hg1 x0 Hx0). + pose proof (Hg1 x1 Hx1). + congruence. +Qed. + +Lemma le_cardinal_ens_sig_injective + {X Y : Type} (U : Ensemble X) (V : Ensemble Y) + (f : sig U -> sig V) : + injective f -> le_cardinal_ens U V. +Proof. + destruct (classic (inhabited Y)). + 2: { + left. split; auto. + intros x Hx. + contradict H. + constructor. + apply (proj1_sig (f (exist U x Hx))). + } + destruct H as [y0]. + right. + exists (sig_fn_extend (compose (@proj1_sig Y V) f) y0). + split. + - apply sig_fn_extend_range. + intros [x Hx] _. + apply (proj2_sig (f (exist U x Hx))). + - apply sig_fn_extend_injective_ens. + apply injective_compose; auto. + intros ? ?. apply proj1_sig_injective. +Qed. + +(** for each point in [U] at most one point lands in [inverse_image f U] *) +Lemma inverse_image_injective_cardinal_le + {X Y : Type} (f : X -> Y) (U : Ensemble Y) : + injective f -> + le_cardinal_ens (inverse_image f U) U. +Proof. + intros Hf. + right. exists f. + split. + - apply range_char_inverse_image. + reflexivity. + - apply injective_injective_ens, Hf. +Qed. diff --git a/theories/ZornsLemma/Cardinals/Combinatorics.v b/theories/ZornsLemma/Cardinals/Combinatorics.v new file mode 100644 index 00000000..f370e3a5 --- /dev/null +++ b/theories/ZornsLemma/Cardinals/Combinatorics.v @@ -0,0 +1,404 @@ +(** Collect many constructive [eq_cardinal] results. *) +From Coq Require Fin. +From Coq Require Import + Description + FunctionalExtensionality + Morphisms + Program.Basics. +From ZornsLemma Require Import + Cardinals.Cardinals + DecidableDec + EnsemblesImplicit + FunctionProperties. + +(* give precedence to [proof_irrelevance] *) +From Coq Require Import ProofIrrelevance. +Import ProofIrrelevanceFacts. + +Set Asymmetric Patterns. + +(** ** Basic types *) +Lemma eq_cardinal_empty_type (X : Type) : + (X -> False) -> + eq_cardinal False X. +Proof. + intros f. + exists (False_rect X), f. + split. + - intros []. + - intros x; destruct (f x). +Qed. + +Lemma eq_cardinal_option_False_True : + eq_cardinal (option False) True. +Proof. + exists (fun _ => I), (fun _ => None). + split. + - intros []; auto; contradiction. + - intros []; auto. +Qed. + +Lemma eq_cardinal_unit_option_False : + eq_cardinal (option False) unit. +Proof. + exists (fun _ => tt), (fun _ => None). + split. + - intros []; auto; contradiction. + - intros []; reflexivity. +Qed. + +(** ** Sigma types *) +Lemma eq_cardinal_False_sig_Empty_set (X : Type) : + eq_cardinal False { x : X | In Empty_set x }. +Proof. + exists (False_rect _), + (fun p : {x : X | In Empty_set x} => + Empty_set_rect X (fun _ => False) + (proj1_sig p) (proj2_sig p)). + split. + - intros; contradiction. + - intros []. + destruct i. +Qed. + +Lemma eq_cardinal_sig_Full_set (X : Type) : + eq_cardinal { x : X | In Full_set x } X. +Proof. + exists (@proj1_sig _ Full_set), + (fun x => exist Full_set x (Full_intro X x)). + split. + - intros [x Hx]. simpl. + destruct Hx. reflexivity. + - reflexivity. +Qed. + +(** interestingly, this does not require [proof_irrelevance]. *) +Lemma eq_cardinal_sig_Singleton {X : Type} (x0 : X) : + eq_cardinal (option False) { x : X | In (Singleton x0) x }. +Proof. + exists (fun _ => exist _ x0 (In_singleton X x0)), (fun _ => None). + split. + - intros []; auto. contradiction. + - intros [x Hx]. + destruct Hx. reflexivity. +Qed. + +(** disjoint union *) +Lemma eq_cardinal_sig_disjoint_Union_sum {X : Type} + (U V : Ensemble X) : + Intersection U V = Empty_set -> + eq_cardinal + ((sig U) + (sig V)) + (sig (Union U V)). +Proof. + intros HUV. + assert (forall x : X, In U x -> In V x -> False) as HUVdisj. + { intros x HUx HVx. + eapply Empty_set_rect. + rewrite <- HUV. split; eassumption. + } + clear HUV. + assert (forall x : X, In (Union U V) x -> {In U x} + {In V x}) + as Hdec. + { intros x Hx. + apply exclusive_dec. + 2: { destruct Hx; auto. } + intros [HUx HVx]. + firstorder. + } + exists (fun p : sig U + sig V => + match p with + | inl pU => exist _ (proj1_sig pU) + (Union_introl X U V (proj1_sig pU) (proj2_sig pU)) + | inr pV => exist _ (proj1_sig pV) + (Union_intror X U V (proj1_sig pV) (proj2_sig pV)) + end). + exists (fun p => + match Hdec (proj1_sig p) (proj2_sig p) with + | left HU => inl (exist _ (proj1_sig p) HU) + | right HV => inr (exist _ (proj1_sig p) HV) + end). + split. + - intros [[x Hx]|[x Hx]]. + + simpl. destruct (Hdec x _). + * f_equal. f_equal. apply proof_irrelevance. + * specialize (HUVdisj x Hx i). contradiction. + + simpl. destruct (Hdec x _). + * specialize (HUVdisj x i Hx). contradiction. + * f_equal. f_equal. apply proof_irrelevance. + - intros [x Hx]. simpl. + destruct (Hdec x Hx); + simpl; f_equal; apply proof_irrelevance. +Qed. + +(** If [U] is an ensemble of [option X] and does contain [None], + then [sig U] has the same cardinality as "the ensemble of [X] which + 'is' in [U]" plus one element. *) +Lemma eq_cardinal_sig_option_In {X : Type} (U : Ensemble (option X)) : + In U None -> + eq_cardinal (option (sig (fun x : X => U (Some x)))) (sig U). +Proof. + intros HN. + exists (fun (x:option {x:X | U (Some x)}) => + match x return {x:option X | U x} with + | Some (exist x0 i) => exist U (Some x0) i + | None => exist U None HN + end). + exists (fun (s:{x0:option X | U x0}) => + match s return option {x:X | U (Some x)} with + | exist (Some x0) i => Some (exist (fun y:X => U (Some y)) x0 i) + | exist None _ => None + end). + split. + - intros [[x Hx]|]; auto. + - intros [[x|] Hx]; auto. + f_equal. apply proof_irrelevance. +Qed. + +(** If [U] is an ensemble of [option X] and does *not* contain [None], + then [sig U] has the same cardinality as "the ensemble of [X] which + 'is' in [U]". *) +Lemma eq_cardinal_sig_option_nIn {X : Type} (U : Ensemble (option X)) : + ~ In U None -> + eq_cardinal (sig (compose U Some)) (sig U). +Proof. + intros HN. + exists (fun (x:{x:X | U (Some x)}) => + match x return {x:option X | U x} with + | exist x0 i => exist (fun x:option X => U x) (Some x0) i + end). + exists (fun s:{x0:option X | U x0} => + match s return {x:X | U (Some x)} with + | exist (Some x0) i => exist (fun x:X => U (Some x)) x0 i + | exist None i => False_rect _ (HN i) + end). + split. + - intros [x Hx]. reflexivity. + - intros [[x|] Hx]; auto. + contradiction. +Qed. + +(** actually [compose U f = inverse_image f U] *) +Lemma eq_cardinal_sig_comp_invertible + {X Y : Type} (f : X -> Y) (U : Ensemble Y) : + invertible f -> + eq_cardinal (sig (compose U f)) (sig U). +Proof. + intros [g Hfg]. + unfold compose. + assert (forall y : Y, U y -> U (f (g y))) as HU. + { intros y Hy. rewrite (proj2 Hfg). assumption. } + exists (fun p => exist U (f (proj1_sig p)) (proj2_sig p)). + exists (fun p => exist + (compose U f) + (g (proj1_sig p)) (HU (proj1_sig p) (proj2_sig p))). + split. + - intros [x Hx]. + simpl. apply subset_eq_compat. + apply Hfg. + - intros [y Hy]. + simpl. apply subset_eq_compat. + apply Hfg. +Qed. + +Lemma eq_cardinal_sig_injective_image + {X Y : Type} (f : X -> Y) (U : Ensemble X) : + injective f -> + eq_cardinal (sig (Im U f)) (sig U). +Proof. + intros Hf. + assert (forall p : { y : Y | Im U f y }, + { x : X | In U x /\ f x = proj1_sig p }) as finv. + { intros [y Hy]. simpl. + apply constructive_definite_description. + destruct Hy as [x Hx y Hy]. + subst. exists x. split; auto. + intros x0 []; auto. + } + exists (fun p => + exist + U + (proj1_sig (finv p)) + (proj1 (proj2_sig (finv p)))). + exists (fun p => + exist (Im U f) + (f (proj1_sig p)) + (Im_def U f (proj1_sig p) (proj2_sig p))). + split. + - intros [y Hy]. + simpl. + destruct (finv (exist _ y Hy)). + simpl. + destruct a. simpl in *. subst. + f_equal. apply proof_irrelevance. + - intros [x Hx]. + simpl. + apply subset_eq_compat. + apply Hf. + apply (proj2 (proj2_sig (finv (exist _ (f x) (Im_def U f x Hx))))). +Qed. + +(** ** Sum types *) +Lemma eq_cardinal_sum_False (X : Type) : + eq_cardinal X (X + False). +Proof. + exists inl, (fun (x : X + False) => + match x with + | inl x => x + | inr f => False_rect X f + end). + split. + - reflexivity. + - intros []; try contradiction; reflexivity. +Qed. + +Lemma eq_cardinal_sum_option_r (X Y : Type) : + eq_cardinal (option (X + Y)) (X + option Y). +Proof. + exists (fun (x:option (X+Y)) => + match x with + | Some (inl x) => inl _ x + | Some (inr y) => inr _ (Some y) + | None => inr _ None + end). + exists (fun (x:X + option Y) => + match x with + | inl x => Some (inl _ x) + | inr (Some y) => Some (inr _ y) + | inr None => None + end). + split. + - intros [[]|]; reflexivity. + - intros [|[]]; reflexivity. +Qed. + +Instance eq_cardinal_sum_Proper : + Proper (eq_cardinal ==> eq_cardinal ==> eq_cardinal) sum. +Proof. + intros X0 X1 [f0 [f1 []]]. + intros Y0 Y1 [g0 [g1 []]]. + exists (sum_rect + (fun _ => X1 + Y1)%type + (compose inl f0) + (compose inr g0)). + exists (sum_rect + (fun _ => X0 + Y0)%type + (compose inl f1) + (compose inr g1)). + split; intros [|]; simpl; + unfold compose; f_equal; auto. +Qed. + +(** ** Product types *) +Lemma eq_cardinal_prod_False (X : Type) : + eq_cardinal False (X * False)%type. +Proof. + exists (False_rect _), snd. + split. + - intros ?; contradiction. + - intros []; contradiction. +Qed. + +Lemma eq_cardinal_prod_option_r (X Y : Type) : + eq_cardinal (X * Y + X) (X * option Y). +Proof. + exists (fun (x:X*Y + X) => + match x with + | inl (pair x0 t) => pair x0 (Some t) + | inr x0 => pair x0 None + end). + exists (fun (x:X * option Y) => + match x with + | (x0, Some t) => inl _ (x0, t) + | (x0, None) => inr _ x0 + end). + split. + - intros [[x y]|x]; reflexivity. + - intros [x [y|]]; reflexivity. +Qed. + +Instance eq_cardinal_prod_Proper : + Proper (eq_cardinal ==> eq_cardinal ==> eq_cardinal) prod. +Proof. + intros X0 X1 [f0 [f1 []]]. + intros Y0 Y1 [g0 [g1 []]]. + exists (fun p => (f0 (fst p), g0 (snd p))). + exists (fun p => (f1 (fst p), g1 (snd p))). + split; intros []; simpl; f_equal; auto. +Qed. + +(** ** Function types *) +Lemma eq_cardinal_fun_from_False (X : Type) : + eq_cardinal (option False) (False -> X). +Proof. + exists (fun _ => False_rect X), (fun _ => None). + split. + - intros []; auto; contradiction. + - intros f; extensionality x; contradiction. +Qed. + +Lemma eq_cardinal_fun_option_l (X Y : Type) : + eq_cardinal ((X -> Y) * Y) (option X -> Y). +Proof. + exists (fun p o => + match o with + | None => snd p + | Some x => fst p x + end). + exists (fun f => (compose f Some, f None)). + split. + - intros [f y]. simpl. + split. + - intros f. + extensionality o. + destruct o as [x|]; reflexivity. +Qed. + +Lemma eq_cardinal_fun_l (X0 X1 Y : Type) : + eq_cardinal X0 X1 -> + eq_cardinal (X0 -> Y) (X1 -> Y). +Proof. + intros [f [g Hfg]]. + exists (fun p : X0 -> Y => compose p g). + exists (fun p : X1 -> Y => compose p f). + split; intros p; extensionality x; + unfold compose; f_equal; apply Hfg. +Qed. + +(** ** Booleans *) +Lemma eq_cardinal_bool_sum_unit : + eq_cardinal (unit + unit) bool. +Proof. + exists (fun p => + match p with + | inl _ => true + | inr _ => false + end), + (fun p : bool => if p then inl tt else inr tt). + split. + - intros [[]|[]]; reflexivity. + - intros []; reflexivity. +Qed. + +(** ** Coq stdlib [Fin.t] *) +Lemma eq_cardinal_Fin_S (n : nat) : + eq_cardinal (option (Fin.t n)) (Fin.t (S n)). +Proof. + exists (fun o => + match o with + | None => Fin.F1 + | Some p => Fin.FS p + end). + exists (fun p : Fin.t (S n) => + Fin.caseS' + p (fun _ => option (Fin.t n)) + None Some). + split. + - intros [|]; reflexivity. + - revert n. + apply Fin.rectS. + + intros n. simpl. + reflexivity. + + intros n p _. + simpl. reflexivity. +Qed. diff --git a/theories/ZornsLemma/Cardinals/Comparability.v b/theories/ZornsLemma/Cardinals/Comparability.v new file mode 100644 index 00000000..d29031b8 --- /dev/null +++ b/theories/ZornsLemma/Cardinals/Comparability.v @@ -0,0 +1,360 @@ +(** Proves the cardinal comparability theorem [types_comparable] using + Zorns Lemma for preorders. It states that between any two types [A] + and [B] there is an injection [A -> B] or an injection [B -> A]. + + Alternate proofs can be done using the well-ordering principle, + using the fact that well-orders are totally ordered. + *) + +From Coq Require Import + Description. +From ZornsLemma Require Import + Cardinals.Cardinals + Cardinals.CardinalsEns + Cardinals.CSB + Families + FunctionProperties + Image + ZornsLemma. + +Section le_cardinal_total. + +Variable X Y:Type. + +(** We define the type of "partial injections" from [X] to [Y] + consisting of injective maps [pi_func] which are only defined on + an Ensemble of [X]. + + We define a preorder on them, by defining [pi1 ≤ pi2] if + the same inequality holds for their domains and [pi2] agrees with + [pi1] wherever the latter is defined. + + We go on to show that this order satisfies Zorns Lemma + (see [partial_injection_chain_ub]) and thus contains a maximal + element (see [premaximal_partial_injection]). + + Next we show that such a maximal element is either surjective or + its domain is the whole of [X] (see + [premaximal_pi_is_full_or_surj]). + + In [types_comparable] we show that in one case, we can transform + the partial injection to an injection [X -> Y], while in the other + case we can construct an injection [Y -> X] because the maximal element + is surjective. + *) +Record partial_injection : Type := { + pi_dom: Ensemble X; + pi_func: forall x:X, In pi_dom x -> Y; + pi_inj: forall (x1 x2:X) (i1:In pi_dom x1) (i2:In pi_dom x2), + pi_func x1 i1 = pi_func x2 i2 -> x1 = x2 +}. +Record partial_injection_ord (pi1 pi2:partial_injection) : Prop := { + pi_dom_inc: Included (pi_dom pi1) (pi_dom pi2); + pi_func_ext: forall (x:X) (i1:In (pi_dom pi1) x) + (i2:In (pi_dom pi2) x), + pi_func pi1 x i1 = pi_func pi2 x i2 +}. + +Lemma partial_injection_preord: preorder partial_injection_ord. +Proof. +constructor. +- intros x. + destruct x. + constructor. + + auto with sets. + + intros. simpl in *. + f_equal. + apply proof_irrelevance. +- intros x y z ? ?. + destruct H. + destruct H0. + constructor. + + auto with sets. + + intros. + assert (In (pi_dom y) x0). + { auto with sets. } + transitivity (pi_func y x0 H); trivial. +Qed. + +Lemma partial_injection_chain_ub: forall S:Ensemble partial_injection, + chain partial_injection_ord S -> exists x:partial_injection, + forall y:partial_injection, In S y -> partial_injection_ord y x. +Proof. +intros S HS. +(* whenever two elements of [S] are applied to the same element, + they agree *) +assert (forall (pi1 pi2 : partial_injection) + (Hpi1 : In S pi1) (Hpi2 : In S pi2) + (x : X) (Hx1 : In (pi_dom pi1) x) + (Hx2 : In (pi_dom pi2) x), + pi_func pi1 x Hx1 = pi_func pi2 x Hx2) as HSeq. +{ intros pi1 pi2 Hpi1 Hpi2 x Hx1 Hx2. + specialize (HS pi1 pi2 Hpi1 Hpi2) as [Hpi|Hpi]. + - apply pi_func_ext, Hpi. + - symmetry. apply pi_func_ext, Hpi. +} +(* [ub_dom] is the union of all [pi_dom] that occur in [S] *) +pose (ub_dom := FamilyUnion (Im S pi_dom)). +(* define the map from [ub_dom] to [Y] *) +assert (forall x:X, In ub_dom x -> { y:Y | exists z:partial_injection, + In S z /\ exists i:In (pi_dom z) x, pi_func z x i = y }) + as ub_func. +{ intros x Hx. + apply constructive_definite_description. + destruct Hx as [dom x Hdom Hx]. + destruct Hdom as [pi Hpi dom Hdom]. + subst. + exists (pi_func pi x Hx). + split. + { exists pi. split; eauto. } + (* uniqueness *) + intros y [pi0 [Hpi0 [Hx0 Hy]]]. + subst y. + apply HSeq; assumption. +} +(* show that [ub_func] is injective *) +assert (forall (x1 x2:X) (i1:In ub_dom x1) (i2:In ub_dom x2), + proj1_sig (ub_func x1 i1) = proj1_sig (ub_func x2 i2) -> x1 = x2) + as ub_inj. +{ intros x1 x2 i1 i2 Hx. + (* destruct [ub_func] *) + destruct (ub_func x1 i1) as [y1 [piy1 [Hpiy1S [Hpiy1x Hpiy1]]]] in Hx. + destruct (ub_func x2 i2) as [y2 [piy2 [Hpiy2S [Hpiy2x Hpiy2]]]] in Hx. + simpl in Hx. subst y1 y2. + (* destruct [i1] and [i2], i.e. the fact that [x1, x2] lie in the domain of + [ub_func] *) + destruct i1 as [S1 x1 i1 Hx1]. + destruct i2 as [S2 x2 i2 Hx2]. + destruct i1 as [pi1 Hpi1 S1 HS1]. + destruct i2 as [pi2 Hpi2 S2 HS2]. + subst S1 S2. + (* use the fact that we're dealing with a chain. + Here it is essential, that the domains are included in eachother. + *) + specialize (HS piy1 piy2 Hpiy1S Hpiy2S) as [HpiyS|HpiyS]. + - assert (In (pi_dom piy2) x1) as Hpiy2x1. + { apply (pi_dom_inc _ _ HpiyS). + assumption. + } + apply (pi_inj piy2 x1 x2 Hpiy2x1 Hpiy2x). + rewrite <- Hx. + symmetry. + apply pi_func_ext. + assumption. + - assert (In (pi_dom piy1) x2) as Hpiy1x2. + { apply (pi_dom_inc _ _ HpiyS). + assumption. + } + apply (pi_inj piy1 x1 x2 Hpiy1x Hpiy1x2). + rewrite Hx. + apply pi_func_ext. + assumption. +} +exists (Build_partial_injection ub_dom + (fun (x:X) (i:In ub_dom x) => proj1_sig (ub_func x i)) ub_inj). +(* show maximality *) +intros pi Hpi. +constructor; simpl. +{ apply FamilyUnion_In_Included. + apply Im_def. + assumption. +} +intros x Hpix Hubx. +destruct (ub_func x Hubx) as [y [pi0 [Hpi0 [Hpi0x Hy]]]]. +subst y. simpl. +apply HSeq; assumption. +Qed. + +Lemma premaximal_partial_injection: + exists x:partial_injection, premaximal partial_injection_ord x. +Proof. +apply ZornsLemmaForPreorders. +- exact partial_injection_preord. +- exact partial_injection_chain_ub. +Qed. + +Lemma premaximal_pi_is_full_or_surj: + forall x:partial_injection, premaximal partial_injection_ord x -> + pi_dom x = Full_set \/ + forall y:Y, exists x0:X, exists i:(In (pi_dom x) x0), + pi_func x x0 i = y. +Proof. +intros pi Hpi. +destruct (classic (exists x0:X, ~ In (pi_dom pi) x0)) as [Hnsurj|Hnsurj]. +2: { + left. + apply Extensionality_Ensembles; split. + { intros ? ?; constructor. } + intros x _. + apply NNPP. + intros Hx. + contradict Hnsurj. + exists x; assumption. +} +right. +destruct Hnsurj as [x Hx]. +intros y. +(* assume for a contradiction, that [y] has no preimage *) +apply NNPP. +intros Hy. + +(* we construct another partial injection which is strictly larger + than [pi] *) +pose (pi_dom_ext := Add (pi_dom pi) x). +(* the function maps like [pi], except it maps [x] to [y] *) +assert (forall (x':X), In pi_dom_ext x' -> + { y':Y | (exists i2:In (pi_dom pi) x', y' = pi_func pi x' i2) \/ + (x' = x /\ y' = y) }) as pi_func_ext. +{ intros x0 Hx0. + apply constructive_definite_description. + destruct Hx0 as [x0 Hx0|x0 Hx0]. + - exists (pi_func pi x0 Hx0). + split. + + left. exists Hx0. reflexivity. + + intros y0 [[Hy0 Hy1]|[]]; subst. + * f_equal. apply proof_irrelevance. + * contradiction. + - destruct Hx0. + exists y. split. + + right; tauto. + + intros y0 [[Hy0 Hy1]|[]]; subst; auto. + contradiction. +} + +pose (pi_func_ext0 := fun (x:X) (i:In pi_dom_ext x) => + proj1_sig (pi_func_ext x i)). + +(* prove that [pi_func_ext0] agrees with [pi] *) +assert (forall (x1:X) (i:In (pi_dom pi) x1) (i2:In pi_dom_ext x1), + pi_func_ext0 x1 i2 = pi_func pi x1 i) as pi_func_ext_ext. +{ intros x0 Hx0 Hx0_ext. + unfold pi_func_ext0. + destruct (pi_func_ext x0 Hx0_ext) + as [y0 Hy0]. + simpl. + destruct Hy0 as [[? ?]|[]]; subst. + 2: contradiction. + f_equal. apply proof_irrelevance. +} + +(* prove that [pi_func_ext0] maps [x] to [y] *) +assert (forall (i:In pi_dom_ext x), pi_func_ext0 x i = y) as + pi_func_ext_x. +{ intros Hx0. + unfold pi_func_ext0. + destruct (pi_func_ext x Hx0) as [y0 Hy0]. + simpl. destruct Hy0 as [[? ?]|[]]; subst; tauto. +} + +(* prove that [pi_func_ext0] is injective *) +assert (forall (x1 x2:X) (i1:In pi_dom_ext x1) (i2:In pi_dom_ext x2), + pi_func_ext0 x1 i1 = pi_func_ext0 x2 i2 -> x1 = x2) + as pi_inj_ext. +{ intros x1 x2 Hx1 Hx2 Hxx. + destruct Hx1 as [x1 Hx1|x1 Hx1], + Hx2 as [x2 Hx2|x2 Hx2]. + - rewrite (pi_func_ext_ext x1 Hx1) in Hxx. + rewrite (pi_func_ext_ext x2 Hx2) in Hxx. + apply pi_inj in Hxx. + assumption. + - rewrite (pi_func_ext_ext x1 Hx1) in Hxx. + destruct Hx2. + rewrite pi_func_ext_x in Hxx. + contradict Hy. + eauto. + - destruct Hx1. + rewrite (pi_func_ext_ext x2 Hx2) in Hxx. + rewrite pi_func_ext_x in Hxx. + contradict Hy. + eauto. + - destruct Hx1, Hx2. + reflexivity. +} + +pose (pi_ext := Build_partial_injection pi_dom_ext pi_func_ext0 pi_inj_ext). +assert (partial_injection_ord pi pi_ext) as Hord. +{ constructor. + - apply Union_increases_l. + - intros. symmetry. apply pi_func_ext_ext. +} + +apply Hpi in Hord. +contradict Hx. +apply (pi_dom_inc _ _ Hord). +simpl. +right. +constructor. +Qed. + +Theorem le_cardinal_total : + le_cardinal X Y \/ le_cardinal Y X. +Proof. +pose proof premaximal_partial_injection + as [pi Hpi]. +apply premaximal_pi_is_full_or_surj in Hpi. +destruct Hpi as [Hpi|Hpi]. +- left. + assert (forall x0:X, In (pi_dom pi) x0) as Hpi0. + { rewrite Hpi. constructor. } + exists (fun x0:X => pi_func pi x0 (Hpi0 x0)). + red; intros. + apply pi_inj in H. + assumption. +- right. + (* similar to [bijective_impl_invertible] *) + assert (forall y:Y, { x0:X | exists i:In (pi_dom pi) x0, pi_func pi x0 i = y }) + as F. + { intros y. + apply constructive_definite_description. + pose proof (Hpi y) as [x Hx]. + exists x. split; auto. + destruct Hx as [Hx Hy]. + subst. + intros x0 [Hx0 Hxx]. + apply pi_inj in Hxx. + symmetry. assumption. + } + exists (fun y:Y => proj1_sig (F y)). + intros y0 y1 Hy. + destruct (F y0) as [x0 [Hx0 Hxy0]] in Hy. + destruct (F y1) as [x1 [Hx1 Hxy1]] in Hy. + simpl in Hy. subst. + f_equal. apply proof_irrelevance. +Qed. + +End le_cardinal_total. + +Lemma cardinal_no_inj_equiv_lt_cardinal (A B : Type) : + (forall f : A -> B, ~ injective f) <-> + lt_cardinal B A. +Proof. +split. +- intros. + split. + + (* |B| ≤ |A| *) + destruct (le_cardinal_total B A). + { assumption. } + destruct H0 as [f Hf]. + specialize (H f Hf). + contradiction. + + (* |B| ≠ |A| *) + intro. + destruct H0 as [f [g [Hgf Hfg]]]. + pose proof (invertible_impl_bijective g). + destruct H0 as [Hg0 Hg1]. + { exists f; split; assumption. } + apply (H g Hg0). +- intros [[f Hf]] g Hg. + contradict H. + apply CSB_inverse_map with (f := f) (g := g); + assumption. +Qed. + +Theorem le_cardinal_ens_total {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : + le_cardinal_ens U V \/ le_cardinal_ens V U. +Proof. + destruct (le_cardinal_total (sig U) (sig V)) as [[f Hf]|[f Hf]]; + [left|right]. + - eapply le_cardinal_ens_sig_injective; eauto. + - eapply le_cardinal_ens_sig_injective; eauto. +Qed. diff --git a/theories/ZornsLemma/Cardinals/Diagonalization.v b/theories/ZornsLemma/Cardinals/Diagonalization.v new file mode 100644 index 00000000..8a3c582f --- /dev/null +++ b/theories/ZornsLemma/Cardinals/Diagonalization.v @@ -0,0 +1,124 @@ +(** Proves that the powerset of a set has larger cardinality than the + set itself, in different statements. Uses this to show that the + order of cardinals is unbounded. *) +From ZornsLemma Require Import + Cardinals.Cardinals + Cardinals.CardinalsEns + FunctionProperties + FunctionPropertiesEns + Powerset_facts. + +Lemma Prop_contradiction_neq (P Q : Prop) (HP : P) : + ~ (P /\ Q) -> + P <> Q. +Proof. + intros ? ?. subst. + tauto. +Qed. + +Lemma P_neq_not_P: forall (P:Prop), P <> ~P. +Proof. +unfold not; intros. +assert (~P). +{ unfold not; intro. + assert (P->False). + { rewrite <- H. + assumption. + } + tauto. +} +assert P. +{ rewrite H. + assumption. +} +contradiction. +Qed. + +Lemma cantor_diag: forall (X:Type) (f:X->(X->bool)), + ~ surjective f. +Proof. +intros. +red; intro. +pose (g := fun x:X => negb (f x x)). +pose proof (H g). +destruct H0. +assert (f x x = g x). +{ rewrite H0. + reflexivity. +} +unfold g in H1. +destruct (f x x). +- discriminate H1. +- discriminate H1. +Qed. + +Lemma cantor_diag2: forall (X:Type) (f:X->(X->Prop)), + ~ surjective f. +Proof. +unfold not; intros. +pose (g := fun x:X => ~ f x x). +pose proof (H g). +destruct H0. +assert (f x x = g x). +{ rewrite H0. + reflexivity. +} +unfold g in H1. +contradiction P_neq_not_P with (f x x). +Qed. + +Lemma cardinals_unbounded: forall kappa:Type, + lt_cardinal kappa (Ensemble kappa). +Proof. +intros ?. +split. +- exists Singleton. + red; intros. + apply Powerset_facts.Singleton_injective. + assumption. +- intros [f Hf]. + apply (cantor_diag2 _ f). + apply invertible_impl_bijective. + apply Hf. +Qed. + +Lemma cantor_diag2_ens {X : Type} (U : Ensemble X) + (f : X -> (Ensemble X)) : + ~ surjective_ens f U (fun V : Ensemble X => Included V U). +Proof. + intros Hf. + pose (g := (fun x : X => In U x /\ ~ In (f x) x) : Ensemble X). + pose proof (Hf g) as [x [Hx Hxg]]. + { intros x [Hx _]. apply Hx. } + assert (f x x = g x). + { rewrite Hxg. reflexivity. } + unfold g in H. + unfold In in H. + destruct (classic (f x x)). + - apply (Prop_contradiction_neq + (f x x) (U x /\ ~ f x x)); tauto. + - apply (Prop_contradiction_neq + (U x /\ ~ f x x) (f x x)); try tauto. + congruence. +Qed. + +Lemma cardinals_unbounded_ens {X : Type} (U : Ensemble X) : + lt_cardinal_ens + U (fun V : Ensemble X => Included V U). +Proof. + split. + - right. exists Singleton. split. + + intros x Hx y Hy. + inversion Hy; subst; clear Hy. + assumption. + + intros x0 x1 Hx0 Hx1 Hx. + apply Singleton_injective in Hx. + assumption. + - intros H. + apply eq_cardinal_ens_sym in H. + destruct H as [[H _]|[f Hf]]. + + apply (H Empty_set). + + destruct Hf as [Hf0 [Hf1 Hf2]]. + apply (cantor_diag2_ens U f). + assumption. +Qed. diff --git a/theories/ZornsLemma/Cardinals/LeastCardinalsEns.v b/theories/ZornsLemma/Cardinals/LeastCardinalsEns.v new file mode 100644 index 00000000..4ab600b1 --- /dev/null +++ b/theories/ZornsLemma/Cardinals/LeastCardinalsEns.v @@ -0,0 +1,136 @@ +(** ** Definitions concerning least cardinals *) +From ZornsLemma Require Import + Cardinals.CardinalsEns + Cardinals.Comparability + Cardinals.CSB + Families + Image. + +(** [U] is an element of [P] with minimal cardinality, + where [P : Family X] *) +Definition least_cardinal_subset + {X : Type} (P : Family X) (U : Ensemble X) : Prop := + In P U /\ + forall V : Ensemble X, + In P V -> le_cardinal_ens U V. + +(** [U] is an element of [P] with minimal cardinality, + where [P] is a collection of arbitrary ensembles. *) +Definition least_cardinal + (P : forall {X : Type} (U : Ensemble X), Prop) + {X : Type} (U : Ensemble X) : Prop := + P U /\ + (forall (Y : Type) (V : Ensemble Y), + P V -> le_cardinal_ens U V). + +Definition least_cardinal_ext + {X : Type} (P : Family X) {Y : Type} (V : Ensemble Y) := + least_cardinal + (fun Z W => + exists U : Ensemble X, + In P U /\ eq_cardinal_ens U W) V. + +Lemma least_cardinal_ext_subset + {X : Type} (P : Family X) (U : Ensemble X) : + least_cardinal_subset P U -> + least_cardinal_ext P U. +Proof. + intros [HU0 HU1]. + split. + - exists U; split; auto. reflexivity. + - intros Y V [U' [HU'0 HU'1]]. + specialize (HU1 U' HU'0). + eapply le_cardinal_ens_Proper_r; eauto. +Qed. + +Lemma least_cardinal_ext_to_subset + {X : Type} (P : Family X) {Y : Type} (V : Ensemble Y) : + least_cardinal_ext P V -> + exists U : Ensemble X, + least_cardinal_subset P U /\ eq_cardinal_ens U V. +Proof. + intros [[U [HU0 HU1]] HV1]. + exists U. split; auto. + split; auto. + intros W HW. + apply eq_cardinal_ens_sym in HU1. + eapply le_cardinal_ens_Proper_l; eauto. + apply HV1. exists W; split; auto. + reflexivity. +Qed. + +Lemma least_cardinal_unique P {X : Type} (U : Ensemble X) + {Y : Type} (V : Ensemble Y) : + least_cardinal P U -> + least_cardinal P V -> + eq_cardinal_ens U V. +Proof. + intros [HU0 HU1] [HV0 HV1]. + specialize (HU1 Y V HV0). + specialize (HV1 X U HU0). + apply le_cardinal_ens_antisymmetry; + assumption. +Qed. + +Lemma le_cardinal_ens_wf {X : Type} (F : Family X) : + Inhabited F -> + exists U, least_cardinal_subset F U. +Proof. +Admitted. + +Corollary least_cardinal_ext_exists {X : Type} (F : Family X) : + Inhabited F -> + exists U : Ensemble X, least_cardinal_ext F U. +Proof. + intros HF. + destruct (le_cardinal_ens_wf F HF) as [U HU]. + exists U. + apply least_cardinal_ext_subset. + assumption. +Qed. + +Lemma least_cardinal_exists + (P : forall {X : Type} (U : Ensemble X), Prop) {X : Type} (U : Ensemble X) : + P U -> exists (Y : Type) (V : Ensemble Y), least_cardinal (@P) V. +Proof. + intros HU. + pose (F := fun V : Ensemble X => + exists (Y : Type) (W : Ensemble Y), + P Y W /\ eq_cardinal_ens V W). + assert (F U) as HU0. + { exists X, U; split; auto; reflexivity. } + (* every ensemble that satisfies [P] has a representative of the + possibly smaller cardinality in [X]. *) + assert (forall {Y : Type} (W : Ensemble Y), + P Y W -> exists (V : Ensemble X), + F V /\ le_cardinal_ens V W) as HFmin. + { intros Y W HW. + destruct (le_cardinal_ens_total U W). + { exists U; auto. } + destruct H as [[]|]. + { exists Empty_set. split. + - exists Y, W. split; auto. + apply eq_cardinal_ens_empty. + apply H0. + - apply le_cardinal_ens_Empty_set. + } + destruct H as [f [Hf0 Hf1]]. + exists (Im W f). split. + - exists Y, W. split; auto. + apply eq_cardinal_ens_sym. + apply eq_cardinal_ens_Im_injective. + assumption. + - apply eq_cardinal_ens_le. + apply eq_cardinal_ens_sym. + apply eq_cardinal_ens_Im_injective. + assumption. + } + destruct (le_cardinal_ens_wf F) as [V [[Y [W [HV0 HV1]]] HV2]]. + { exists U. assumption. } + exists Y, W. split; auto. + intros Z Q HQ. + eapply le_cardinal_ens_Proper_l; eauto. + specialize (HFmin Z Q HQ) as [R [HR0 HR1]]. + specialize (HV2 R HR0). + eapply le_cardinal_ens_transitive; eauto. +Qed. diff --git a/theories/ZornsLemma/CardinalsEns.v b/theories/ZornsLemma/CardinalsEns.v deleted file mode 100644 index 49f2399b..00000000 --- a/theories/ZornsLemma/CardinalsEns.v +++ /dev/null @@ -1,1058 +0,0 @@ -(** Instead of comparing cardinalities of elements of [Type], - compare cardinalities of ensembles. - With this technique, we can avoid problems w.r.t. type universes - that occur with the approach of [ZornsLemma.Cardinals]. - - On the other hand, we need classical logic more often, because a - statement like [eq_cardinal_ens] decides whether the ensemble and - a type are inhabited or not. - - Similarly, we can not define [eq_cardinal_ens] via - [inverse_map_ens], because that leads to a notion incompatible - with [le_cardinal_ens]. Namely it would reqiure classical logic - to prove [eq_cardinal_ens -> le_cardinal_ens]. -*) -From Coq Require Import - ClassicalChoice - Description - Lia - PeanoNat - Program.Subset. -From ZornsLemma Require Import - Cardinals - CountableTypes - CSB - DecidableDec - Families - Finite_sets - FiniteTypes - FunctionProperties - FunctionPropertiesEns - InverseImage - Powerset_facts - Proj1SigInjective - ReverseMath.AddSubtract. -From Coq Require Import - RelationClasses. - -Definition eq_cardinal_ens {A B : Type} - (U : Ensemble A) (V : Ensemble B) : Prop := - ((B -> False) /\ forall a : A, ~ In U a) \/ - exists f : A -> B, - range f U V /\ bijective_ens f U V. -Definition le_cardinal_ens {A B : Type} - (U : Ensemble A) (V : Ensemble B) : Prop := - ((B -> False) /\ forall a : A, ~ In U a) \/ - exists f : A -> B, - range f U V /\ injective_ens f U. -Definition lt_cardinal_ens {A B : Type} - (U : Ensemble A) (V : Ensemble B) : Prop := - le_cardinal_ens U V /\ - ~ eq_cardinal_ens V U. -Definition ge_cardinal_ens {A B : Type} - (U : Ensemble A) (V : Ensemble B) : Prop := - (forall b : B, ~ In V b) \/ - exists f : A -> B, - range f U V /\ surjective_ens f U V. - -Instance eq_cardinal_ens_Reflexive (A : Type) : - Reflexive (@eq_cardinal_ens A A). -Proof. - right. - exists id. split; auto. - - reflexivity. - - apply bijective_ens_id. -Qed. - -Lemma eq_cardinal_ens_sym_dec {A B : Type} - (HA : inhabited A \/ ~ inhabited A) - (U : Ensemble A) (V : Ensemble B) - (HVdec : forall b : B, In V b \/ ~ In V b) : - eq_cardinal_ens U V -> - eq_cardinal_ens V U. -Proof. - intros [[H0 H1]|[f [Hf0 Hf1]]]. - - right. - exists (fun b : B => - False_rect A (H0 b)). - split; [|split]; intros ? ?; try contradiction. - firstorder. - - destruct HA. - 2: { - left. split. - { intros a; apply H; constructor; auto. } - intros b Hb. - destruct Hf1 as [_ Hf1]. - specialize (Hf1 b Hb) as [a [Ha0 Ha1]]. - apply H. constructor; auto. - } - right. - destruct H as [a0]. - pose proof (bijective_impl_invertible_ens_dec - f U V a0 HVdec Hf0 Hf1) as [g Hfg]. - exists g. split. - + apply (inverse_map_ens_surjective_ens_range f); auto. - apply Hf1. - + apply (inverse_map_ens_range_bijective_ens f); auto. -Qed. - -Lemma eq_cardinal_ens_sym {A B : Type} - (U : Ensemble A) (V : Ensemble B) : - eq_cardinal_ens U V -> - eq_cardinal_ens V U. -Proof. - apply eq_cardinal_ens_sym_dec. - - apply classic. - - intros ?. apply classic. -Qed. - -Lemma eq_cardinal_ens_trans {A B C : Type} - (U : Ensemble A) (V : Ensemble B) (W : Ensemble C) : - eq_cardinal_ens U V -> eq_cardinal_ens V W -> - eq_cardinal_ens U W. -Proof. - intros [[H0 H1]|[f [Hf0 Hf1]]]. - { intros [[H2 H3]|[g [Hg0 Hg1]]]. - { left. split; auto. } - destruct (classic (inhabited C)). - 2: now left; split; auto. - right. - destruct H as [c]. - exists (fun _ => c); split; [|split]. - - intros x Hx. specialize (H1 x Hx); contradiction. - - intros ? ? Hx. specialize (H1 _ Hx); contradiction. - - intros z Hz. - destruct Hg1 as [Hg1 Hg2]. - specialize (Hg2 z Hz) as [b Hb]. - contradiction. - } - intros [[H0 H1]|[g [Hg0 Hg1]]]. - { left. split; auto. - intros a Ha. - apply (H1 (f a)). - apply Hf0. assumption. - } - right. exists (compose g f). - split. - - eapply range_compose; eauto. - - eapply bijective_ens_compose; eauto. -Qed. - -Lemma eq_cardinal_ens_le {A B : Type} - (U : Ensemble A) (V : Ensemble B) : - eq_cardinal_ens U V -> - le_cardinal_ens U V. -Proof. - intros [H|[f [Hf0 [Hf1 _]]]]. - { left; auto. } - right. exists f; split; auto. -Qed. - -Section compose. - Context {A B C : Type} - (U : Ensemble A) (V : Ensemble B) (W : Ensemble C). - - Lemma le_cardinal_ens_transitive : - le_cardinal_ens U V -> - le_cardinal_ens V W -> - le_cardinal_ens U W. - Proof. - intros HUV [[H0 H1]|[g [Hg0 Hg1]]]. - { left. split; auto. - destruct HUV as [[H2 H3]|[f [Hf0 Hf1]]]. - { assumption. } - intros a Ha. - apply (H1 (f a)). - apply (Hf0 a Ha). - } - destruct HUV as [[H0 H1]|[f [Hf0 Hf1]]]. - { destruct (classic (inhabited C)). - - right. - destruct H as [c0]. - exists (fun _ => c0). split. - + intros a Ha. firstorder. - + intros a0 a1 Ha0 Ha1; firstorder. - - left. split; auto. - } - right. exists (compose g f). - split. - - eapply range_compose; eauto. - - eapply injective_ens_compose; eauto. - Qed. -End compose. - -Lemma le_cardinal_ens_Proper_r {X Y Z : Type} - (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : - eq_cardinal_ens V W -> - le_cardinal_ens U V -> le_cardinal_ens U W. -Proof. - intros H0 H1. - apply eq_cardinal_ens_le in H0. - eapply le_cardinal_ens_transitive; eauto. -Qed. - -Lemma le_cardinal_ens_Proper_l {X Y Z : Type} - (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : - eq_cardinal_ens U V -> - le_cardinal_ens U W -> le_cardinal_ens V W. -Proof. - intros H0 H1. - apply eq_cardinal_ens_sym in H0. - apply eq_cardinal_ens_le in H0. - eapply le_cardinal_ens_transitive; eauto. -Qed. - -Lemma le_cardinal_ens_Empty_set (X : Type) {Y : Type} - (U : Ensemble Y) : - le_cardinal_ens (@Empty_set X) U. -Proof. - destruct (classic (inhabited Y)). - - destruct H as [y]. - right. exists (fun _ => y). - firstorder. - - left. firstorder. -Qed. - -Lemma eq_cardinal_ens_empty {X Y : Type} (U : Ensemble Y) : - eq_cardinal_ens (@Empty_set X) U <-> - (forall y : Y, ~ In U y). -Proof. - split. - - intros [|[f [Hf0 [Hf1 Hf2]]]] y Hy. - + tauto. - + specialize (Hf2 y Hy) as [x [Hx Hxy]]. - contradiction. - - intros HU. - destruct (classic (inhabited Y)). - 2: { - left; auto with sets. - } - right. - destruct H as [y0]. - exists (fun _ => y0). split; firstorder. -Qed. - -Lemma eq_cardinal_ens_Im_injective - {X Y : Type} (U : Ensemble X) (f : X -> Y) : - injective_ens f U -> - eq_cardinal_ens U (Im U f). -Proof. - intros Hf. - right. exists f. - split. - - apply range_char_Im. - reflexivity. - - split. - + assumption. - + apply surjective_ens_Im. -Qed. - -Lemma le_cardinal_ens_Im {X Y : Type} (f : X -> Y) - (U : Ensemble X) : - le_cardinal_ens (Im U f) U. -Proof. - destruct (classic (Inhabited U)). - 2: { - destruct (classic (inhabited X)). - - destruct H0 as [x0]. - right. exists (fun _ => x0). - split; intros ? **. - + contradict H. - inversion H0; subst; clear H0. - firstorder. - + contradict H. - inversion H0; subst; clear H0. - firstorder. - - left; split; [firstorder|]. - intros y Hy. - inversion Hy; subst; clear Hy. - apply H; exists x. assumption. - } - destruct H as [x0 Hx0]. - pose proof - (surjective_ens_right_inverse - U (Im U f) f x0 Hx0) as [g [Hg0 Hg1]]. - { apply range_char_Im. - reflexivity. - } - { apply surjective_ens_Im. } - right. exists g; split; auto. - intros y0 y1 Hy0 Hy1. - pose proof (Hg1 y0 Hy0). - pose proof (Hg1 y1 Hy1). - congruence. -Qed. - -Lemma eq_cardinal_ens_sig {X : Type} (P : X -> Prop) : - eq_cardinal_ens (@Full_set (sig P)) P. -Proof. - right. - exists (@proj1_sig X P). - split; [|split]. - - intros p _. apply proj2_sig. - - intros p0 p1 _ _. - destruct p0, p1. - apply subset_eq_compat. - - intros x Hx. - exists (exist P x Hx). - split; [constructor|reflexivity]. -Qed. - -Lemma le_cardinal_ens_Included {X : Type} - (U V : Ensemble X) : - Included U V -> - le_cardinal_ens U V. -Proof. - right. exists id. firstorder. -Qed. - -Theorem CSB_ens {X Y : Type} - (U : Ensemble X) (V : Ensemble Y) - (f : X -> Y) (g : Y -> X) : - range f U V -> - range g V U -> - injective_ens f U -> - injective_ens g V -> - exists h : X -> Y, - range h U V /\ - bijective_ens h U V. -Proof. - intros. - assert (exists h0 : sig U -> sig V, bijective h0) - as [h0 Hh]. - { apply CSB with (f := range_restr f U V H) - (g := range_restr g V U H0); - apply injective_ens_char; assumption. - } - destruct (classic (inhabited Y)). - 2: { - assert (X -> False) as HX. - { intros x. - apply H3. constructor. - apply (f x). - } - exists (fun x => False_rect Y (HX x)). - repeat split; intros ? ?; try contradiction. - contradict H3; constructor; auto. - } - clear f g H H0 H1 H2. - destruct H3 as [y0]. - exists (sig_fn_extend (compose (@proj1_sig Y V) h0) y0). - assert (range (compose (proj1_sig (P:=V)) h0) - Full_set V). - { apply (range_compose _ Full_set). - - apply range_full. - - intros ? _. apply proj2_sig. - } - split; [|split]. - - apply sig_fn_extend_range; assumption. - - apply sig_fn_extend_injective_ens. - apply injective_compose. - + apply Hh. - + intros ? ?. apply proj1_sig_injective. - - apply sig_fn_extend_surjective_ens. - intros y Hy. - destruct Hh as [_ Hh]. - specialize (Hh (exist V y Hy)) as [[x Hx0] Hx1]. - exists (exist U x Hx0); split; [constructor|]. - unfold compose. rewrite Hx1. - reflexivity. -Qed. - -Corollary le_cardinal_ens_antisymmetry - {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : - le_cardinal_ens U V -> - le_cardinal_ens V U -> - eq_cardinal_ens U V. -Proof. - intros [H|[f [Hf0 Hf1]]]. - { left. assumption. } - intros [H|[g [Hg0 Hg1]]]. - { apply eq_cardinal_ens_sym. - left. assumption. - } - right. - apply (CSB_ens _ _ f g); assumption. -Qed. - -Lemma le_lt_cardinal_ens_transitive {X Y Z : Type} - (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : - le_cardinal_ens U V -> - lt_cardinal_ens V W -> - lt_cardinal_ens U W. -Proof. - intros HUV [HVW HVWn]. - split. - { eapply le_cardinal_ens_transitive; eauto. } - intros Heq. - contradict HVWn. - apply eq_cardinal_ens_sym in Heq. - apply le_cardinal_ens_antisymmetry; auto. - eapply le_cardinal_ens_Proper_l; eauto. -Qed. - -Lemma le_cardinal_ens_surj {X Y : Type} - (U : Ensemble X) (V : Ensemble Y) : - le_cardinal_ens U V <-> - ge_cardinal_ens V U. -Proof. - split. - - intros [[H0 H1]|[f [Hf0 Hf1]]]. - { right. exists (fun y : Y => False_rect X (H0 y)). - split; intros ? ?; firstorder; try contradiction. - } - destruct (classic (Inhabited U)). - 2: { - left. firstorder. - } - destruct H as [x0 Hx0]. - right. - pose proof (injective_ens_left_inverse U V f x0 - Hx0 Hf0 Hf1) as [g [Hg0 Hg1]]. - exists g; split; auto. - intros x Hx. - exists (f x). split; auto. - symmetry. apply Hg1. - assumption. - - intros [H|[f [Hf0 Hf1]]]. - { destruct (classic (inhabited Y)). - { destruct H0 as [y]. - right. exists (fun _ => y). - split; intros ? ?; firstorder. - } - left. split; auto. - } - destruct (classic (Inhabited V)). - 2: { - destruct (classic (inhabited Y)). - { destruct H0 as [y0]. - right. exists (fun _ => y0). - firstorder. - } - left. firstorder. - } - destruct H as [y Hy]. - pose proof (surjective_ens_right_inverse V U f y Hy Hf0 Hf1) - as [g [Hg0 Hg1]]. - right. exists g; split; auto. - intros x0 x1 Hx0 Hx1 Hx. - pose proof (Hg1 x0 Hx0). - pose proof (Hg1 x1 Hx1). - congruence. -Qed. - -Lemma le_cardinal_ens_sig_injective - {X Y : Type} (U : Ensemble X) (V : Ensemble Y) - (f : sig U -> sig V) : - injective f -> le_cardinal_ens U V. -Proof. - destruct (classic (inhabited Y)). - 2: { - left. split; auto. - intros x Hx. - contradict H. - constructor. - apply (proj1_sig (f (exist U x Hx))). - } - destruct H as [y0]. - right. - exists (sig_fn_extend (compose (@proj1_sig Y V) f) y0). - split. - - apply sig_fn_extend_range. - intros [x Hx] _. - apply (proj2_sig (f (exist U x Hx))). - - apply sig_fn_extend_injective_ens. - apply injective_compose; auto. - intros ? ?. apply proj1_sig_injective. -Qed. - -Theorem le_cardinal_ens_total {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : - le_cardinal_ens U V \/ le_cardinal_ens V U. -Proof. - destruct (types_comparable (sig U) (sig V)) as [[f Hf]|[f Hf]]; - [left|right]. - - eapply le_cardinal_ens_sig_injective; eauto. - - eapply le_cardinal_ens_sig_injective; eauto. -Qed. - -Lemma nat_minimal_element_property_dec - (U : Ensemble nat) (HUdec : forall n : nat, In U n \/ ~ In U n) - (HUinh : Inhabited U) : - exists m : nat, In U m /\ forall n : nat, In U n -> m <= n. -Proof. - destruct HUinh as [N HN]. - revert U HUdec HN. - induction N. - { intros. - exists 0. split; auto. lia. - } - intros U HUdec HN. - destruct (HUdec 0) as [HU0|HU0]. - { exists 0. split; auto. lia. } - specialize (IHN (compose U S)) as [m [Hm0 Hm1]]; - auto. - { intros ?. apply HUdec. } - destruct (HUdec m) as [HUm|HUm]. - { exists m; split; auto; intros n Hn. - destruct n; try contradiction. - apply Hm1 in Hn. lia. - } - exists (S m). split; auto. - intros n Hn. - destruct n; try contradiction. - apply le_n_S. - apply Hm1. - assumption. -Qed. - -Lemma nat_bounded_ens_has_max_dec - (U : Ensemble nat) - (HUdec : forall n : nat, In U n \/ ~ In U n) - (N : nat) : - (forall n : nat, In U n -> n < N) -> - Inhabited U -> - exists n : nat, In U n /\ - forall m : nat, In U m -> m <= n. -Proof. - intros HN HU. - induction N. - { destruct HU as [u Hu]. - specialize (HN u Hu). lia. - } - clear HU. - specialize (HUdec N) as [HN0|HN0]. - - exists N; split; auto. - intros m Hm. specialize (HN m Hm). - lia. - - apply IHN. - intros n Hn. - specialize (HN n Hn). - assert (n <> N). - { intros ?; congruence. } - lia. -Qed. - -(** if a set [U] has an element [o] and an injective function [succ] - (possibly defined on a larger set than [U]) such that - [o] is not in the image of [succ], and - [U] satisfies an induction principle, then [U] is countably infinite *) -Lemma peano_ensemble_countably_infinite {X : Type} - (U : Ensemble X) (o : X) (succ : X -> X) : - In U o -> - (forall x : X, In U x -> In U (succ x)) -> - injective_ens succ U -> - (forall x : X, In U x -> o <> succ x) -> - (forall P : Ensemble X, - P o -> - (forall x, In U x -> P x -> P (succ x)) -> - forall x, In U x -> P x) -> - eq_cardinal_ens (@Full_set nat) U. -Proof. - intros HUo HUsucc Hsucc_inj Hsucc_o HUind. - right. - pose (g := fix g (n : nat) : { n : X | In U n } := - match n with - | O => exist U o HUo - | S n => exist U (succ (proj1_sig (g n))) - (HUsucc (proj1_sig (g n)) (proj2_sig (g n))) - end). - exists (fun n => proj1_sig (g n)). - split; [|split]. - - intros x Hx. - clear Hx. - induction x. - { simpl. assumption. } - simpl. apply HUsucc, IHx. - - intros x0 x1 Hx0 Hx1 Hx. - clear Hx0 Hx1. - revert x1 Hx. - induction x0; intros x1 Hx. - { simpl in Hx. - destruct x1. - { reflexivity. } - simpl in Hx. - apply Hsucc_o in Hx; try contradiction. - apply proj2_sig. - } - simpl in Hx. - destruct x1. - { simpl in Hx. - symmetry in Hx. - apply Hsucc_o in Hx; try contradiction. - apply proj2_sig. - } - simpl in Hx. - apply Hsucc_inj in Hx; try now apply proj2_sig. - apply IHx0 in Hx. congruence. - - red. apply HUind. - + exists 0. split; constructor. - + intros x Hx [y [Hy Hy0]]. - subst. - exists (S y); split; [constructor|]. - simpl. reflexivity. -Qed. - -Theorem nat_unbounded_impl_countably_infinite_dec - (U : Ensemble nat) (HU : forall n : nat, exists m : nat, In U m /\ n < m) - (HUdec : forall n : nat, In U n \/ ~ In U n) : - eq_cardinal_ens U (@Full_set nat). -Proof. - (* we use [nat_minimal_element_property_dec] to note that [U] is - well-founded by [lt]. - Then show: - Hu: the set [U] has a least element [u] - Hf: the set [U] has a "successor" function [f] - Hfu: [u] is not in the image of [f] - Hf_inj: the function [f] is injective on [U] - HU0: every element of [U] is either [u] or lies in the image of [f] - - Combine these in [peano_ensemble_countably_infinite] - to obtain a bijection (even an order-isomorphism) - between [U] and [Full_set]. - *) - assert (exists u : nat, In U u /\ (forall n : nat, In U n -> u <= n)) as Hu. - { specialize (HU 0) as [m [Hm0 Hm1]]. - apply nat_minimal_element_property_dec; auto. - exists m. assumption. - } - assert (exists f : nat -> nat, - (forall n : nat, - In U n -> - In U (f n)) /\ - (forall n : nat, - In U n -> - n < f n) /\ - (forall n : nat, - In U n -> - forall m : nat, - In U m -> - n < m -> f n <= m)) as Hf. - { cut (forall n : nat, - { fn : nat | - (In U n -> - In U fn /\ n < fn /\ - forall m : nat, In U m -> n < m -> fn <= m) /\ - (~ In U n -> fn = 0) }). - { intros F. - exists (fun n => proj1_sig (F n)). - repeat split; intros n Hn; - pose proof (proj1 (proj2_sig (F n)) Hn) as [Hn0 [Hn1 Hn2]]; - auto. - } - intros n. - apply constructive_definite_description. - destruct (HUdec n) as [Hn0|Hn0]. - 2: { - exists 0. repeat split; try contradiction. - intuition. - } - destruct - (nat_minimal_element_property_dec - (fun m => In U m /\ n < m)) as [k [[Hk0 Hk1] Hk2]]. - { unfold In. - intros m. - destruct (Nat.lt_ge_cases n m). - 2: { - right. intros []. lia. - } - specialize (HUdec m) as [|]. - - left; tauto. - - right; intros []; tauto. - } - { destruct (HU n) as [m Hm]. - exists m. assumption. - } - exists k. repeat split; try tauto. - { firstorder. } - intros l [Hl _]. - specialize (Hl Hn0) as [Hl0 [Hl1 Hl2]]. - specialize (Hk2 l (conj Hl0 Hl1)). - specialize (Hl2 k Hk0 Hk1). - lia. - } - destruct Hu as [u [Hu0 Hu1]]. - destruct Hf as [f [Hf0 [Hf1 Hf2]]]. - assert (forall x : nat, In U x -> u <> f x) as Hfu. - { intros x Hx. - specialize (Hu1 x Hx). - specialize (Hf1 x Hx). - lia. - } - (* show that [f] is injective on [U] *) - assert (injective_ens f U) as Hf_inj. - { intros x0 x1 Hx0 Hx1 Hx. - destruct (Nat.lt_trichotomy x0 x1) as [Hxx|[Hxx|Hxx]]; auto. - - specialize (Hf2 x0 Hx0 x1 Hx1 Hxx). - specialize (Hf1 x1 Hx1). lia. - - specialize (Hf2 x1 Hx1 x0 Hx0 Hxx). - specialize (Hf1 x0 Hx0). lia. - } - assert (forall x : nat, - In U x -> x = u \/ exists y : nat, In U y /\ x = f y) as HU0. - { intros x Hx. - destruct (Nat.eq_dec x u); auto. - right. - (* [y] must be the greatest element of [U] which satisfies [y < x]. *) - unshelve epose proof (nat_bounded_ens_has_max_dec - (fun y => In U y /\ y < x) _ x) - as [y Hy]. - - intros k. unfold In. - destruct (Nat.lt_ge_cases k x). - 2: { - right. intros []. lia. - } - specialize (HUdec k) as [|]. - + left; tauto. - + right; intros []; tauto. - - intros k [Hk0 Hk1]. auto. - - exists u. split; auto. - specialize (Hu1 x Hx). lia. - - exists y. split; try apply Hy. - destruct Hy as [[Hy0 Hy1] Hy2]. - unfold In at 1 in Hy2. - apply Nat.le_antisymm. - 2: now apply Hf2; auto. - apply Nat.nlt_ge. - intros Hfy. - specialize (Hy2 (f y) (conj (Hf0 y Hy0) Hfy)). - specialize (Hf1 y Hy0). - lia. - } - assert (forall P : (forall x : nat, Prop), - P u -> - (forall (x : nat) (Hx : In U x), - P x -> P (f x)) -> - forall (x : nat), In U x -> P x) as HUind. - { intros P HP0 HP1 x. - apply (Wf_nat.lt_wf_rect x (fun x => In U x -> P x)). - clear x. - intros x Hind Hx. - destruct (HU0 x Hx) as [Hx0|[y [Hy Hy0]]]; subst; auto. - } - apply eq_cardinal_ens_sym_dec. - { left. constructor. apply 0. } - { assumption. } - apply peano_ensemble_countably_infinite with u f; - auto. -Qed. - -Lemma nat_unbounded_impl_countably_infinite - (U : Ensemble nat) (HU : forall n : nat, exists m : nat, In U m /\ n < m) : - eq_cardinal_ens U (@Full_set nat). -Proof. - apply nat_unbounded_impl_countably_infinite_dec; - auto. - intros ?. apply classic. -Qed. - -Lemma Finite_as_lt_cardinal_ens - {X : Type} (U : Ensemble X) : - Finite U <-> lt_cardinal_ens U (@Full_set nat). -Proof. - split. - - (* -> *) - (* this proof directly constructs a function [X -> nat] using [classic_dec]. - Another proof would do induction over [Finite X] and construct the - function [X -> nat] inductively *) - intros HU. - split. - + apply Finite_ens_type in HU. - apply FiniteT_nat_embeds in HU. - destruct HU as [f Hf]. - right. - exists (fun x : X => - match classic_dec (In U x) with - | left Hx => f (exist U x Hx) - | right _ => 0 - end). - split. - * apply range_full. - * intros x0 x1 Hx0 Hx1. - destruct (classic_dec _); try contradiction. - destruct (classic_dec _); try contradiction. - intros Hx. - apply Hf in Hx. - inversion Hx; subst; clear Hx. - reflexivity. - + intros [[_ H]|H]. - { exact (H 0 ltac:(constructor)). } - destruct H as [f [Hf0 Hf1]]. - red in Hf0. - apply InfiniteTypes.nat_infinite. - apply Finite_ens_type in HU. - pose (f0 := fun n : nat => exist U (f n) (Hf0 n ltac:(constructor))). - assert (invertible f0). - { apply bijective_impl_invertible. - split. - - intros n0 n1 Hn. - inversion Hn; subst; clear Hn. - apply Hf1 in H0; auto; constructor. - - intros [x Hx]. - destruct Hf1 as [_ Hf1]. - specialize (Hf1 x Hx) as [n [_ Hn]]. - exists n. subst. unfold f0. - apply subset_eq. reflexivity. - } - destruct H as [g Hg0 Hg1]. - eapply bij_finite with (f := g); eauto. - eexists; eauto. - - (* <- *) - intros [[[H0 H1]|[f [Hf0 Hf1]]] H2]. - { specialize (H0 0). contradiction. } - destruct (classic (exists n : nat, forall x : X, In U x -> f x < n)). - 2: { - contradict H2. - assert (eq_cardinal_ens (Im U f) (@Full_set nat)). - { apply nat_unbounded_impl_countably_infinite. - intros n. apply NNPP. - intros Hn. contradict H. - exists (S n). intros x Hx. - apply NNPP. intros Hx0. - contradict Hn. exists (f x). - split. - { apply Im_def; auto. } - lia. - } - apply eq_cardinal_ens_Im_injective in Hf1. - apply eq_cardinal_ens_sym. - eapply eq_cardinal_ens_trans; eauto. - } - destruct H as [n Hn]. - (* [n] is an upper bound of the image of [U] under [f] *) - assert (Finite (Im U f)). - { apply nat_Finite_bounded_char. - exists n. intros m Hm. - destruct Hm as [x Hx m Hm]; subst. - apply Hn; auto. - } - apply Finite_injective_image with f; - auto. -Qed. - -Lemma Countable_as_le_cardinal_ens {X : Type} (U : Ensemble X) : - Countable U <-> le_cardinal_ens U (@Full_set nat). -Proof. - split. - - intros [f Hf]. - pose proof (eq_cardinal_ens_sig U). - eapply le_cardinal_ens_Proper_l; eauto. - right. exists f. split; [|firstorder]. - intros ? ?. constructor. - - intros [[]|[f [_ Hf]]]. - { contradict (H 0). } - exists (fun p => f (proj1_sig p)). - intros [x0 H0] [x1 H1] Hx. - simpl in Hx. - specialize (Hf x0 x1 H0 H1 Hx). - apply subset_eq_compat. - assumption. -Qed. - -(** for each point in [U] at most one point lands in [inverse_image f U] *) -Lemma inverse_image_injective_cardinal_le - {X Y : Type} (f : X -> Y) (U : Ensemble Y) : - injective f -> - le_cardinal_ens (inverse_image f U) U. -Proof. - intros Hf. - right. exists f. - split. - - apply range_char_inverse_image. - reflexivity. - - apply injective_injective_ens, Hf. -Qed. - -Corollary injective_finite_inverse_image - {X Y : Type} (f : X -> Y) (U : Ensemble Y) : - injective f -> - Finite U -> - Finite (inverse_image f U). -Proof. - intros Hf HU. - apply Finite_as_lt_cardinal_ens. - apply Finite_as_lt_cardinal_ens in HU. - apply (inverse_image_injective_cardinal_le f U) in Hf. - eapply le_lt_cardinal_ens_transitive; eauto. -Qed. - -(** ** Definitions concerning least cardinals *) - -(** [U] is an element of [P] with minimal cardinality, - where [P : Family X] *) -Definition least_cardinal_subset - {X : Type} (P : Family X) (U : Ensemble X) : Prop := - In P U /\ - forall V : Ensemble X, - In P V -> le_cardinal_ens U V. - -(** [U] is an element of [P] with minimal cardinality, - where [P] is a collection of arbitrary ensembles. *) -Definition least_cardinal - (P : forall {X : Type} (U : Ensemble X), Prop) - {X : Type} (U : Ensemble X) : Prop := - P U /\ - (forall (Y : Type) (V : Ensemble Y), - P V -> le_cardinal_ens U V). - -Definition least_cardinal_ext - {X : Type} (P : Family X) {Y : Type} (V : Ensemble Y) := - least_cardinal - (fun Z W => - exists U : Ensemble X, - In P U /\ eq_cardinal_ens U W) V. - -Lemma least_cardinal_ext_subset - {X : Type} (P : Family X) (U : Ensemble X) : - least_cardinal_subset P U -> - least_cardinal_ext P U. -Proof. - intros [HU0 HU1]. - split. - - exists U; split; auto. reflexivity. - - intros Y V [U' [HU'0 HU'1]]. - specialize (HU1 U' HU'0). - eapply le_cardinal_ens_Proper_r; eauto. -Qed. - -Lemma least_cardinal_ext_to_subset - {X : Type} (P : Family X) {Y : Type} (V : Ensemble Y) : - least_cardinal_ext P V -> - exists U : Ensemble X, - least_cardinal_subset P U /\ eq_cardinal_ens U V. -Proof. - intros [[U [HU0 HU1]] HV1]. - exists U. split; auto. - split; auto. - intros W HW. - apply eq_cardinal_ens_sym in HU1. - eapply le_cardinal_ens_Proper_l; eauto. - apply HV1. exists W; split; auto. - reflexivity. -Qed. - -Lemma least_cardinal_unique P {X : Type} (U : Ensemble X) - {Y : Type} (V : Ensemble Y) : - least_cardinal P U -> - least_cardinal P V -> - eq_cardinal_ens U V. -Proof. - intros [HU0 HU1] [HV0 HV1]. - specialize (HU1 Y V HV0). - specialize (HV1 X U HU0). - apply le_cardinal_ens_antisymmetry; - assumption. -Qed. - -Lemma le_cardinal_ens_wf {X : Type} (F : Family X) : - Inhabited F -> - exists U, least_cardinal_subset F U. -Proof. -Admitted. - -Corollary least_cardinal_ext_exists {X : Type} (F : Family X) : - Inhabited F -> - exists U : Ensemble X, least_cardinal_ext F U. -Proof. - intros HF. - destruct (le_cardinal_ens_wf F HF) as [U HU]. - exists U. - apply least_cardinal_ext_subset. - assumption. -Qed. - -Lemma least_cardinal_exists - (P : forall {X : Type} (U : Ensemble X), Prop) {X : Type} (U : Ensemble X) : - P U -> exists (Y : Type) (V : Ensemble Y), least_cardinal (@P) V. -Proof. - intros HU. - pose (F := fun V : Ensemble X => - exists (Y : Type) (W : Ensemble Y), - P Y W /\ eq_cardinal_ens V W). - assert (F U) as HU0. - { exists X, U; split; auto; reflexivity. } - (* every ensemble that satisfies [P] has a representative of the - possibly smaller cardinality in [X]. *) - assert (forall {Y : Type} (W : Ensemble Y), - P Y W -> exists (V : Ensemble X), - F V /\ le_cardinal_ens V W) as HFmin. - { intros Y W HW. - destruct (le_cardinal_ens_total U W). - { exists U; auto. } - destruct H as [[]|]. - { exists Empty_set. split. - - exists Y, W. split; auto. - apply eq_cardinal_ens_empty. - apply H0. - - apply le_cardinal_ens_Empty_set. - } - destruct H as [f [Hf0 Hf1]]. - exists (Im W f). split. - - exists Y, W. split; auto. - apply eq_cardinal_ens_sym. - apply eq_cardinal_ens_Im_injective. - assumption. - - apply eq_cardinal_ens_le. - apply eq_cardinal_ens_sym. - apply eq_cardinal_ens_Im_injective. - assumption. - } - destruct (le_cardinal_ens_wf F) as [V [[Y [W [HV0 HV1]]] HV2]]. - { exists U. assumption. } - exists Y, W. split; auto. - intros Z Q HQ. - eapply le_cardinal_ens_Proper_l; eauto. - specialize (HFmin Z Q HQ) as [R [HR0 HR1]]. - specialize (HV2 R HR0). - eapply le_cardinal_ens_transitive; eauto. -Qed. - -(** ** Cantor *) -Lemma Prop_contradiction_neq (P Q : Prop) (HP : P) : - ~ (P /\ Q) -> - P <> Q. -Proof. - intros ? ?. subst. - tauto. -Qed. - -(* in analogy to [Cardinals.cantor_diag2] *) -Lemma cantor_diag2 {X : Type} (U : Ensemble X) - (f : X -> (Ensemble X)) : - ~ surjective_ens f U (fun V : Ensemble X => Included V U). -Proof. - intros Hf. - pose (g := (fun x : X => In U x /\ ~ In (f x) x) : Ensemble X). - pose proof (Hf g) as [x [Hx Hxg]]. - { intros x [Hx _]. apply Hx. } - assert (f x x = g x). - { rewrite Hxg. reflexivity. } - unfold g in H. - unfold In in H. - destruct (classic (f x x)). - - apply (Prop_contradiction_neq - (f x x) (U x /\ ~ f x x)); tauto. - - apply (Prop_contradiction_neq - (U x /\ ~ f x x) (f x x)); try tauto. - congruence. -Qed. - -Lemma cardinals_unbounded {X : Type} (U : Ensemble X) : - lt_cardinal_ens - U (fun V : Ensemble X => Included V U). -Proof. - split. - - right. exists Singleton. split. - + intros x Hx y Hy. - inversion Hy; subst; clear Hy. - assumption. - + intros x0 x1 Hx0 Hx1 Hx. - apply Singleton_injective in Hx. - assumption. - - intros H. - apply eq_cardinal_ens_sym in H. - destruct H as [[H _]|[f Hf]]. - + apply (H Empty_set). - + destruct Hf as [Hf0 [Hf1 Hf2]]. - apply (cantor_diag2 U f). - assumption. -Qed. diff --git a/theories/ZornsLemma/CountableTypes.v b/theories/ZornsLemma/CountableTypes.v index 9e18e64d..ea23a015 100644 --- a/theories/ZornsLemma/CountableTypes.v +++ b/theories/ZornsLemma/CountableTypes.v @@ -14,32 +14,31 @@ From Coq Require Import QArith ZArith. From ZornsLemma Require Import - CSB + Cardinals DecidableDec DependentTypeChoice Finite_sets FiniteTypes + FunctionProperties FunctionPropertiesEns IndexedFamilies - InfiniteTypes. + InverseImage. Local Close Scope Q_scope. Set Asymmetric Patterns. Definition CountableT (X : Type) : Prop := - exists f : X -> nat, injective f. + le_cardinal X nat. Lemma CountableT_is_FiniteT_or_countably_infinite (X : Type) : - CountableT X -> {FiniteT X} + {exists f : X -> nat, bijective f}. + CountableT X -> {FiniteT X} + {eq_cardinal X nat}. Proof. intros. apply exclusive_dec. -- intro. - destruct H0 as [? [f ?]]. +- intros []. contradiction nat_infinite. - apply bij_finite with _ f; trivial. - apply bijective_impl_invertible; trivial. + apply bij_finite with X; auto. - destruct (classic (FiniteT X)). + left; trivial. + right. @@ -139,15 +138,16 @@ induction H. intros. pose proof (equal_f H4). apply H5. -- destruct H1 as [f1], IHFiniteT as [f0]. +- destruct H1 as [f [f1 Hf]]. + destruct IHFiniteT as [f0 Hf0]. exists (fun h => f0 (fun x => h (f x))). intros h1 h2 ?. - apply H3 in H4. - pose proof (equal_f H4). - simpl in H5. + apply Hf0 in H1. + pose proof (equal_f H1). + simpl in H2. extensionality y. - rewrite <- (H2 y). - apply H5. + rewrite <- (proj2 Hf y). + apply H2. Qed. Lemma inj_countable {X Y : Type} (f : X -> Y) : @@ -185,10 +185,11 @@ induction H. injection H1 as H1 + discriminate H1 + trivial. now destruct (H0 _ _ H1). - destruct IHFiniteT as [g], - H0 as [finv]. + H0 as [f [finv]]. exists (fun y:Y => g (finv y)). intros y1 y2 ?. - apply H1 in H3. + apply H1 in H2. + destruct H0. congruence. Qed. @@ -386,3 +387,397 @@ all: inversion Hx; subst; clear Hx; destruct (proof_irrelevance _ Hx0 Hx1); reflexivity. Qed. + +Definition countable_img_inj {X Y : Type} (f : X -> Y) (U : Ensemble X) : + injective_ens f U -> + CountableT X -> + Countable (Im U f) := + @le_cardinal_img_inj_ens X Y nat f U. + +Lemma Countable_as_le_cardinal_ens {X : Type} (U : Ensemble X) : + Countable U <-> le_cardinal_ens U (@Full_set nat). +Proof. + split. + - intros [f Hf]. + pose proof (eq_cardinal_ens_sig U). + eapply le_cardinal_ens_Proper_l; eauto. + right. exists f. split; [|firstorder]. + intros ? ?. constructor. + - intros [[]|[f [_ Hf]]]. + { contradict (H 0). } + exists (fun p => f (proj1_sig p)). + intros [x0 H0] [x1 H1] Hx. + simpl in Hx. + specialize (Hf x0 x1 H0 H1 Hx). + apply subset_eq_compat. + assumption. +Qed. + +(** ** Unbounded subsets of [nat] are countably infinite *) +Lemma nat_minimal_element_property_dec + (U : Ensemble nat) (HUdec : forall n : nat, In U n \/ ~ In U n) + (HUinh : Inhabited U) : + exists m : nat, In U m /\ forall n : nat, In U n -> m <= n. +Proof. + destruct HUinh as [N HN]. + revert U HUdec HN. + induction N. + { intros. + exists 0. split; auto. lia. + } + intros U HUdec HN. + destruct (HUdec 0) as [HU0|HU0]. + { exists 0. split; auto. lia. } + specialize (IHN (compose U S)) as [m [Hm0 Hm1]]; + auto. + { intros ?. apply HUdec. } + destruct (HUdec m) as [HUm|HUm]. + { exists m; split; auto; intros n Hn. + destruct n; try contradiction. + apply Hm1 in Hn. lia. + } + exists (S m). split; auto. + intros n Hn. + destruct n; try contradiction. + apply le_n_S. + apply Hm1. + assumption. +Qed. + +Lemma nat_bounded_ens_has_max_dec + (U : Ensemble nat) + (HUdec : forall n : nat, In U n \/ ~ In U n) + (N : nat) : + (forall n : nat, In U n -> n < N) -> + Inhabited U -> + exists n : nat, In U n /\ + forall m : nat, In U m -> m <= n. +Proof. + intros HN HU. + induction N. + { destruct HU as [u Hu]. + specialize (HN u Hu). lia. + } + clear HU. + specialize (HUdec N) as [HN0|HN0]. + - exists N; split; auto. + intros m Hm. specialize (HN m Hm). + lia. + - apply IHN. + intros n Hn. + specialize (HN n Hn). + assert (n <> N). + { intros ?; congruence. } + lia. +Qed. + +(** if a set [U] has an element [o] and an injective function [succ] + (possibly defined on a larger set than [U]) such that + [o] is not in the image of [succ], and + [U] satisfies an induction principle, then [U] is countably infinite *) +Lemma peano_ensemble_countably_infinite {X : Type} + (U : Ensemble X) (o : X) (succ : X -> X) : + In U o -> + (forall x : X, In U x -> In U (succ x)) -> + injective_ens succ U -> + (forall x : X, In U x -> o <> succ x) -> + (forall P : Ensemble X, + P o -> + (forall x, In U x -> P x -> P (succ x)) -> + forall x, In U x -> P x) -> + eq_cardinal_ens (@Full_set nat) U. +Proof. + intros HUo HUsucc Hsucc_inj Hsucc_o HUind. + right. + pose (g := fix g (n : nat) : { n : X | In U n } := + match n with + | O => exist U o HUo + | S n => exist U (succ (proj1_sig (g n))) + (HUsucc (proj1_sig (g n)) (proj2_sig (g n))) + end). + exists (fun n => proj1_sig (g n)). + split; [|split]. + - intros x Hx. + clear Hx. + induction x. + { simpl. assumption. } + simpl. apply HUsucc, IHx. + - intros x0 x1 Hx0 Hx1 Hx. + clear Hx0 Hx1. + revert x1 Hx. + induction x0; intros x1 Hx. + { simpl in Hx. + destruct x1. + { reflexivity. } + simpl in Hx. + apply Hsucc_o in Hx; try contradiction. + apply proj2_sig. + } + simpl in Hx. + destruct x1. + { simpl in Hx. + symmetry in Hx. + apply Hsucc_o in Hx; try contradiction. + apply proj2_sig. + } + simpl in Hx. + apply Hsucc_inj in Hx; try now apply proj2_sig. + apply IHx0 in Hx. congruence. + - red. apply HUind. + + exists 0. split; constructor. + + intros x Hx [y [Hy Hy0]]. + subst. + exists (S y); split; [constructor|]. + simpl. reflexivity. +Qed. + +Theorem nat_unbounded_impl_countably_infinite_dec + (U : Ensemble nat) (HU : forall n : nat, exists m : nat, In U m /\ n < m) + (HUdec : forall n : nat, In U n \/ ~ In U n) : + eq_cardinal_ens U (@Full_set nat). +Proof. + (* we use [nat_minimal_element_property_dec] to note that [U] is + well-founded by [lt]. + Then show: + Hu: the set [U] has a least element [u] + Hf: the set [U] has a "successor" function [f] + Hfu: [u] is not in the image of [f] + Hf_inj: the function [f] is injective on [U] + HU0: every element of [U] is either [u] or lies in the image of [f] + + Combine these in [peano_ensemble_countably_infinite] + to obtain a bijection (even an order-isomorphism) + between [U] and [Full_set]. + *) + assert (exists u : nat, In U u /\ (forall n : nat, In U n -> u <= n)) as Hu. + { specialize (HU 0) as [m [Hm0 Hm1]]. + apply nat_minimal_element_property_dec; auto. + exists m. assumption. + } + assert (exists f : nat -> nat, + (forall n : nat, + In U n -> + In U (f n)) /\ + (forall n : nat, + In U n -> + n < f n) /\ + (forall n : nat, + In U n -> + forall m : nat, + In U m -> + n < m -> f n <= m)) as Hf. + { cut (forall n : nat, + { fn : nat | + (In U n -> + In U fn /\ n < fn /\ + forall m : nat, In U m -> n < m -> fn <= m) /\ + (~ In U n -> fn = 0) }). + { intros F. + exists (fun n => proj1_sig (F n)). + repeat split; intros n Hn; + pose proof (proj1 (proj2_sig (F n)) Hn) as [Hn0 [Hn1 Hn2]]; + auto. + } + intros n. + apply constructive_definite_description. + destruct (HUdec n) as [Hn0|Hn0]. + 2: { + exists 0. repeat split; try contradiction. + intuition. + } + destruct + (nat_minimal_element_property_dec + (fun m => In U m /\ n < m)) as [k [[Hk0 Hk1] Hk2]]. + { unfold In. + intros m. + destruct (Nat.lt_ge_cases n m). + 2: { + right. intros []. lia. + } + specialize (HUdec m) as [|]. + - left; tauto. + - right; intros []; tauto. + } + { destruct (HU n) as [m Hm]. + exists m. assumption. + } + exists k. repeat split; try tauto. + { firstorder. } + intros l [Hl _]. + specialize (Hl Hn0) as [Hl0 [Hl1 Hl2]]. + specialize (Hk2 l (conj Hl0 Hl1)). + specialize (Hl2 k Hk0 Hk1). + lia. + } + destruct Hu as [u [Hu0 Hu1]]. + destruct Hf as [f [Hf0 [Hf1 Hf2]]]. + assert (forall x : nat, In U x -> u <> f x) as Hfu. + { intros x Hx. + specialize (Hu1 x Hx). + specialize (Hf1 x Hx). + lia. + } + (* show that [f] is injective on [U] *) + assert (injective_ens f U) as Hf_inj. + { intros x0 x1 Hx0 Hx1 Hx. + destruct (Nat.lt_trichotomy x0 x1) as [Hxx|[Hxx|Hxx]]; auto. + - specialize (Hf2 x0 Hx0 x1 Hx1 Hxx). + specialize (Hf1 x1 Hx1). lia. + - specialize (Hf2 x1 Hx1 x0 Hx0 Hxx). + specialize (Hf1 x0 Hx0). lia. + } + assert (forall x : nat, + In U x -> x = u \/ exists y : nat, In U y /\ x = f y) as HU0. + { intros x Hx. + destruct (Nat.eq_dec x u); auto. + right. + (* [y] must be the greatest element of [U] which satisfies [y < x]. *) + unshelve epose proof (nat_bounded_ens_has_max_dec + (fun y => In U y /\ y < x) _ x) + as [y Hy]. + - intros k. unfold In. + destruct (Nat.lt_ge_cases k x). + 2: { + right. intros []. lia. + } + specialize (HUdec k) as [|]. + + left; tauto. + + right; intros []; tauto. + - intros k [Hk0 Hk1]. auto. + - exists u. split; auto. + specialize (Hu1 x Hx). lia. + - exists y. split; try apply Hy. + destruct Hy as [[Hy0 Hy1] Hy2]. + unfold In at 1 in Hy2. + apply Nat.le_antisymm. + 2: now apply Hf2; auto. + apply Nat.nlt_ge. + intros Hfy. + specialize (Hy2 (f y) (conj (Hf0 y Hy0) Hfy)). + specialize (Hf1 y Hy0). + lia. + } + assert (forall P : (forall x : nat, Prop), + P u -> + (forall (x : nat) (Hx : In U x), + P x -> P (f x)) -> + forall (x : nat), In U x -> P x) as HUind. + { intros P HP0 HP1 x. + apply (Wf_nat.lt_wf_rect x (fun x => In U x -> P x)). + clear x. + intros x Hind Hx. + destruct (HU0 x Hx) as [Hx0|[y [Hy Hy0]]]; subst; auto. + } + apply eq_cardinal_ens_sym_dec. + { left. constructor. apply 0. } + { assumption. } + apply peano_ensemble_countably_infinite with u f; + auto. +Qed. + +Lemma nat_unbounded_impl_countably_infinite + (U : Ensemble nat) (HU : forall n : nat, exists m : nat, In U m /\ n < m) : + eq_cardinal_ens U (@Full_set nat). +Proof. + apply nat_unbounded_impl_countably_infinite_dec; + auto. + intros ?. apply classic. +Qed. + +(** The following proofs are in this file, because they require + [FiniteT] and [nat_unbounded_impl_countably_infinite]. *) +Lemma Finite_as_lt_cardinal_ens + {X : Type} (U : Ensemble X) : + Finite U <-> lt_cardinal_ens U (@Full_set nat). +Proof. + split. + - (* -> *) + (* this proof directly constructs a function [X -> nat] using [classic_dec]. + Another proof would do induction over [Finite X] and construct the + function [X -> nat] inductively *) + intros HU. + split. + + apply Finite_ens_type in HU. + apply FiniteT_nat_embeds in HU. + destruct HU as [f Hf]. + right. + exists (fun x : X => + match classic_dec (In U x) with + | left Hx => f (exist U x Hx) + | right _ => 0 + end). + split. + * apply range_full. + * intros x0 x1 Hx0 Hx1. + destruct (classic_dec _); try contradiction. + destruct (classic_dec _); try contradiction. + intros Hx. + apply Hf in Hx. + inversion Hx; subst; clear Hx. + reflexivity. + + intros [[_ H]|H]. + { exact (H 0 ltac:(constructor)). } + destruct H as [f [Hf0 Hf1]]. + red in Hf0. + apply nat_infinite. + apply Finite_ens_type in HU. + pose (f0 := fun n : nat => exist U (f n) (Hf0 n ltac:(constructor))). + assert (invertible f0). + { apply bijective_impl_invertible. + split. + - intros n0 n1 Hn. + inversion Hn; subst; clear Hn. + apply Hf1 in H0; auto; constructor. + - intros [x Hx]. + destruct Hf1 as [_ Hf1]. + specialize (Hf1 x Hx) as [n [_ Hn]]. + exists n. subst. unfold f0. + apply subset_eq. reflexivity. + } + destruct H as [g Hg0]. + apply bij_finite with (sig U). + { assumption. } + exists g, f0. apply inverse_map_sym, Hg0. + - (* <- *) + intros [[[H0 H1]|[f [Hf0 Hf1]]] H2]. + { specialize (H0 0). contradiction. } + destruct (classic (exists n : nat, forall x : X, In U x -> f x < n)). + 2: { + contradict H2. + assert (eq_cardinal_ens (Im U f) (@Full_set nat)). + { apply nat_unbounded_impl_countably_infinite. + intros n. apply NNPP. + intros Hn. contradict H. + exists (S n). intros x Hx. + apply NNPP. intros Hx0. + contradict Hn. exists (f x). + split. + { apply Im_def; auto. } + lia. + } + apply eq_cardinal_ens_Im_injective in Hf1. + apply eq_cardinal_ens_sym. + eapply eq_cardinal_ens_trans; eauto. + } + destruct H as [n Hn]. + (* [n] is an upper bound of the image of [U] under [f] *) + apply Finite_injective_image with f; + auto. + apply nat_Finite_bounded_char. + exists n. intros m Hm. + destruct Hm as [x Hx m Hm]; subst. + apply Hn; auto. +Qed. + +Corollary injective_finite_inverse_image + {X Y : Type} (f : X -> Y) (U : Ensemble Y) : + injective f -> + Finite U -> + Finite (inverse_image f U). +Proof. + intros Hf HU. + apply Finite_as_lt_cardinal_ens. + apply Finite_as_lt_cardinal_ens in HU. + apply (inverse_image_injective_cardinal_le f U) in Hf. + eapply le_lt_cardinal_ens_transitive; eauto. +Qed. diff --git a/theories/ZornsLemma/Families.v b/theories/ZornsLemma/Families.v index 8e52eec5..c9bc9456 100644 --- a/theories/ZornsLemma/Families.v +++ b/theories/ZornsLemma/Families.v @@ -1,9 +1,11 @@ -From Coq Require Import Classical_Prop. -From Coq Require Import Classical_sets. -From Coq Require Import Morphisms. -From ZornsLemma Require Export EnsemblesTactics. -From ZornsLemma Require Import Image ImageImplicit. -From ZornsLemma Require Import EnsemblesImplicit. +From Coq Require Import + Morphisms. +From ZornsLemma Require Export + EnsemblesTactics. +From ZornsLemma Require Import + EnsemblesImplicit + Image + ImageImplicit. From Coq Require Export Ensembles. Set Implicit Arguments. @@ -25,6 +27,7 @@ Inductive FamilyIntersection: Ensemble T := End Families. +#[export] Instance FamilyUnion_Proper {X : Type} : Proper (Same_set ==> Same_set) (@FamilyUnion X). Proof. @@ -33,6 +36,15 @@ Proof. exists S; firstorder. Qed. +#[export] +Instance FamilyIntersection_Proper {X : Type} : + Proper (Same_set ==> Same_set) (@FamilyIntersection X). +Proof. + intros F0 F1 HF. + split; intros _ [x Hx]; constructor; intros S HS; + apply Hx, HF, HS. +Qed. + Section FamilyFacts. Variable T:Type. diff --git a/theories/ZornsLemma/Filters.v b/theories/ZornsLemma/Filters.v index 612f1b86..37093ffd 100644 --- a/theories/ZornsLemma/Filters.v +++ b/theories/ZornsLemma/Filters.v @@ -41,10 +41,11 @@ induction H. apply filter_intersection. + apply IHFiniteT; auto. + apply H0. -- rewrite IndexedIntersection_surj_fn with S f. +- destruct H1 as [f Hf]. + rewrite IndexedIntersection_surj_fn with S f. 2: { - apply invertible_impl_bijective in H1. - apply H1. + apply invertible_impl_bijective. + assumption. } apply IHFiniteT; auto. Qed. diff --git a/theories/ZornsLemma/FiniteIntersections.v b/theories/ZornsLemma/FiniteIntersections.v index 3a315d66..fed2ae93 100644 --- a/theories/ZornsLemma/FiniteIntersections.v +++ b/theories/ZornsLemma/FiniteIntersections.v @@ -88,10 +88,10 @@ induction H. - rewrite IndexedIntersection_option_Intersection. constructor 3; auto. constructor 2; trivial. -- rewrite IndexedIntersection_surj_fn with V f. +- destruct H1 as [f Hf]. + rewrite IndexedIntersection_surj_fn with V f. 2: { - apply invertible_impl_bijective in H1. - destruct H1. assumption. + apply invertible_impl_bijective; auto. } apply IHFiniteT. auto. diff --git a/theories/ZornsLemma/FiniteTypes.v b/theories/ZornsLemma/FiniteTypes.v index 6b5bc04d..c946590c 100644 --- a/theories/ZornsLemma/FiniteTypes.v +++ b/theories/ZornsLemma/FiniteTypes.v @@ -1,41 +1,34 @@ From Coq Require Import Arith + ClassicalChoice Description FunctionalExtensionality - Lia. + Lia + Program.Subset. From ZornsLemma Require Import + Cardinals DecidableDec + FiniteImplicit Finite_sets FunctionProperties + FunctionPropertiesEns Image IndexedFamilies + InverseImage Powerset_facts. (* load ProofIrrelevance last, so [proof_irrelevance] is not provided - by [classic] *) -From Coq Require Import ProofIrrelevance. + by [classic]. Similarly [RelationClasses] must provide [Equivalence] *) +From Coq Require Import + ProofIrrelevance + RelationClasses. Set Asymmetric Patterns. Inductive FiniteT : Type -> Prop := | empty_finite: FiniteT False | add_finite: forall T:Type, FiniteT T -> FiniteT (option T) - | bij_finite: forall (X Y:Type) (f:X->Y), FiniteT X -> - invertible f -> FiniteT Y. - -Lemma True_finite: FiniteT True. -Proof. -apply bij_finite with (option False) - (fun _ => I). -{ constructor; constructor. } -exists (True_rect None). -- destruct x as [[]|]. - remember (True_rect (@None False) I) as LHS. - destruct LHS as [[]|]. - reflexivity. -- exact (fun y:True => match y with - | I => refl_equal I - end). -Qed. + | bij_finite: forall (X Y:Type), + FiniteT X -> eq_cardinal X Y -> FiniteT Y. Lemma finite_dec_exists: forall (X:Type) (P:X->Prop), FiniteT X -> (forall x:X, P x \/ ~ P x) -> @@ -62,7 +55,7 @@ induction H. destruct x. -- apply H1. -- assumption. -- destruct H0. +- destruct H0 as [f [g []]]. intros. specialize (IHFiniteT (fun x:X => P (f x)) (fun x:X => H2 (f x))) as [|]. @@ -99,7 +92,7 @@ induction H. exists (Some x). assumption. - intros. - destruct H0. + destruct H0 as [f [g []]]. case (IHFiniteT (fun x:X => P (f x)) (fun x:X => H1 (f x))). + left. @@ -124,7 +117,7 @@ induction H. specialize (IHFiniteT t t0) as [|]; [left|right]; congruence. } -destruct H0. +destruct H0 as [f [g []]]. specialize (IHFiniteT (g x) (g y)) as [|]. - left. rewrite <- H1. @@ -162,7 +155,7 @@ induction H. end). destruct x1; auto. - intros. - destruct H0. + destruct H0 as [f [g []]]. pose proof (IHFiniteT (fun x:X => B (f x)) (fun x:X => R (f x)) (fun x:X => H1 (f x))). @@ -180,123 +173,96 @@ Proof. intros. apply finite_dep_choice; assumption. Qed. +Lemma True_finite: FiniteT True. +Proof. +apply bij_finite with (option False). +{ do 2 constructor. } +apply eq_cardinal_option_False_True. +Qed. + +Lemma finite_sum: forall X Y:Type, FiniteT X -> FiniteT Y -> + FiniteT (X+Y). +Proof. +intros. +induction H0. +- apply bij_finite with X; auto. + apply eq_cardinal_sum_False. +- apply bij_finite with (option (X + T)). + { constructor; auto. } + apply eq_cardinal_sum_option_r. +- apply bij_finite with (X + X0)%type; auto. + apply eq_cardinal_sum_Proper; auto. + reflexivity. +Qed. + +Lemma FiniteT_sig_Singleton {X : Type} (x0 : X) : + FiniteT { x : X | In (Singleton x0) x }. +Proof. + apply bij_finite with (option False). + { do 2 constructor. } + apply eq_cardinal_sig_Singleton. +Qed. + Lemma Finite_ens_type: forall {X:Type} (S:Ensemble X), Finite S -> FiniteT { x:X | In S x }. Proof. intros. induction H. -- apply bij_finite with False (False_rect _). - + constructor. - + assert (g:{x:X | In Empty_set x}->False). - { intro. - destruct X0. - destruct i. - } - exists g. - * destruct x. - * destruct y. - destruct g. -- assert (Included A (Add A x)). - { auto with sets. } - assert (In (Add A x) x). - { auto with sets. } - pose (g := fun (y: option {x:X | In A x}) => - match y return {x0:X | In (Add A x) x0} with - | Some (exist y0 i) => exist (fun x2:X => In (Add A x) x2) y0 (H1 y0 i) - | None => exist (fun x2:X => In (Add A x) x2) x H2 - end). - apply bij_finite with _ g. - + apply add_finite. - assumption. - + assert (h:forall x0:X, In (Add A x) x0 -> - { In A x0 } + { x0 = x }). - { intros; apply exclusive_dec. - - intuition. - destruct H6; auto. - - destruct H3. - + left; assumption. - + right; destruct H3; reflexivity. - } - pose (ginv := fun s:{x0:X | In (Add A x) x0} => - match s return option {x:X | In A x} with - | exist x0 i => match (h x0 i) with - | left iA => Some (exist _ x0 iA) - | right _ => None - end - end). - exists ginv. - * intro; destruct x0. - -- destruct s. - simpl. - remember (h x0 (H1 x0 i)) as sum; destruct sum. - ++ destruct (proof_irrelevance _ i i0). - reflexivity. - ++ contradiction H0. - rewrite <- e; assumption. - -- simpl. - remember (h x H2) as sum; destruct sum. - ++ contradiction H0. - ++ reflexivity. - * intro. - unfold ginv. - destruct y. - destruct (h x0 i). - -- simpl. - generalize (H1 x0 i0); intro. - destruct (proof_irrelevance _ i i1). - reflexivity. - -- simpl. - destruct e. - destruct (proof_irrelevance _ H2 i). - reflexivity. +- apply bij_finite with False; [now constructor|]. + apply eq_cardinal_False_sig_Empty_set. +- eapply bij_finite with (sig A + sig (Singleton x))%type. + + apply finite_sum; auto. + apply FiniteT_sig_Singleton. + + eapply eq_cardinal_sig_disjoint_Union_sum. + apply Extensionality_Ensembles; split. + 2: intros ? ?; contradiction. + intros y []. destruct H2. contradiction. Qed. Lemma FiniteT_img: forall (X Y:Type) (f:X->Y), FiniteT X -> (forall y1 y2:Y, y1=y2 \/ y1<>y2) -> Finite (Im Full_set f). Proof. -intros. -induction H. +intros X Y f HX HY. +induction HX. - replace (Im Full_set f) with (@Empty_set Y). { constructor. } apply Extensionality_Ensembles; split; red; intros. + destruct H. + destruct H. destruct x. - assert ((exists x:T, f (Some x) = f None) \/ - (forall x:T, f (Some x) <> f None)). + (forall x:T, f (Some x) <> f None)) as [H|H]. { apply finite_dec_exists. { assumption. } intro. - apply H0. + apply HY. } - case H1. - + intro. - pose (g := fun (x:T) => f (Some x)). + all: clear HY. + + pose (g := fun (x:T) => f (Some x)). replace (Im Full_set f) with (Im Full_set g). - { apply IHFiniteT. } + { apply IHHX. } apply Extensionality_Ensembles; split; red; intros. - * destruct H3. subst. exists (Some x). + * destruct H0. subst. exists (Some x). -- constructor. -- reflexivity. - * destruct H3. subst. destruct x. + * destruct H0. subst. destruct x. -- exists t. ++ constructor. ++ reflexivity. - -- destruct H2. exists x. + -- destruct H as [x]; exists x. ++ constructor. - ++ destruct H3. subst. symmetry. assumption. - + intros. - pose (g := fun x:T => f (Some x)). + ++ symmetry. assumption. + + pose (g := fun x:T => f (Some x)). replace (Im Full_set f) with (Add (Im Full_set g) (f None)). { constructor. - - apply IHFiniteT. - - red; intro. destruct H3. - contradiction (H2 x). + - apply IHHX. + - red; intro. destruct H0. + contradiction (H x). symmetry; assumption. } apply Extensionality_Ensembles; split; red; intros. * red; intros. - destruct H3, H3. + destruct H0, H0. -- exists (Some x). ++ constructor. ++ assumption. @@ -304,24 +270,30 @@ induction H. ++ constructor. ++ reflexivity. * red; intros. - destruct H3. + destruct H0. destruct x. -- left. exists t. ++ constructor. ++ assumption. -- right. auto with sets. -- pose (g := fun (x:X) => f (f0 x)). +- destruct H as [f0 Hf0]. + pose (g := fun (x:X) => f (f0 x)). replace (Im Full_set f) with (Im Full_set g). - { apply IHFiniteT. } - apply Extensionality_Ensembles; split; red; intros. - + destruct H2. exists (f0 x). - * constructor. - * assumption. - + destruct H2, H1. subst. - rewrite <- H4 with x. - exists (g0 x). - * constructor. - * reflexivity. + { apply IHHX. } + unfold g. + rewrite (Im_compose f0 f). + rewrite <- (proj1 (Im_Full_set_surj f0)); auto. + apply invertible_impl_bijective. + assumption. +Qed. + +Lemma Finite_full_impl_FiniteT (X : Type) : + Finite (@Full_set X) -> FiniteT X. +Proof. + intros HX. + apply bij_finite with (sig (@Full_set X)). + - apply Finite_ens_type. assumption. + - apply eq_cardinal_sig_Full_set. Qed. Lemma surj_finite: forall (X Y:Type) (f:X->Y), @@ -330,99 +302,40 @@ Lemma surj_finite: forall (X Y:Type) (f:X->Y), FiniteT Y. Proof. intros. -apply bij_finite with {y:Y | In (Im Full_set f) y} - (@proj1_sig _ (fun y:Y => In (Im Full_set f) y)). -- apply Finite_ens_type. - apply FiniteT_img; assumption. -- assert (forall y:Y, In (Im Full_set f) y). - { intro. - destruct (H0 y). - exists x; auto with sets. - } - pose (proj1_sig_inv := fun y:Y => - exist (fun y0:Y => In (Im Full_set f) y0) y (H2 y)). - exists proj1_sig_inv. - + destruct x. - simpl. unfold proj1_sig_inv. - destruct (proof_irrelevance _ (H2 x) i); trivial. - + intros; simpl; reflexivity. +apply bij_finite with {y:Y | In Full_set y}. +2: apply eq_cardinal_sig_Full_set. +rewrite (proj1 (Im_Full_set_surj f)); auto. +apply Finite_ens_type. +apply FiniteT_img; auto. Qed. Lemma finite_subtype: forall (X:Type) (P:X->Prop), FiniteT X -> (forall x:X, P x \/ ~ P x) -> FiniteT {x:X | P x}. Proof. -intros. +intros X P H HP. induction H. -- apply bij_finite with False (False_rect _). - + constructor. - + exists (@proj1_sig _ _). - * destruct x. - * intro s; destruct s; destruct x. -- destruct (H0 None). - + pose (g := fun (x:option {x:T | P (Some x)}) => - match x return {x:option T | P x} with - | Some (exist x0 i) => exist (fun x:option T => P x) (Some x0) i - | None => exist (fun x:option T => P x) None H1 - end). - apply bij_finite with _ g. - * apply add_finite. - apply IHFiniteT. - intro; apply H0. - * pose (ginv := fun (s:{x0:option T | P x0}) => - match s return option {x:T | P (Some x)} with - | exist (Some x0) i => Some (exist (fun y:T => P (Some y)) x0 i) - | exist None _ => None - end). - exists ginv. - -- destruct x as [[x0]|]; simpl; reflexivity. - -- destruct y as [[x0|]]; simpl. - ++ reflexivity. - ++ destruct (proof_irrelevance _ H1 p). - reflexivity. - + pose (g := fun (x:{x:T | P (Some x)}) => - match x return {x:option T | P x} with - | exist x0 i => exist (fun x:option T => P x) (Some x0) i - end). - apply bij_finite with _ g. - * apply IHFiniteT. - intro; apply H0. - * pose (ginv := fun s:{x0:option T | P x0} => - match s return {x:T | P (Some x)} with - | exist (Some x0) i => exist (fun x:T => P (Some x)) x0 i - | exist None i => False_rect _ (H1 i) - end). - exists ginv. - -- destruct x; simpl. - reflexivity. - -- destruct y as [[x0|]]. - ++ simpl. reflexivity. - ++ contradiction H1. -- pose (g := fun (x:{x:X | P (f x)}) => - match x with - | exist x0 i => exist (fun x:Y => P x) (f x0) i - end). - apply (bij_finite _ _ g). - + apply IHFiniteT. - intro; apply H0. - + destruct H1. - assert (forall y:Y, P y -> P (f (g0 y))). - { intros; rewrite H2; assumption. } - pose (ginv := fun (y:{y:Y | P y}) => - match y with - | exist y0 i => exist (fun x:X => P (f x)) (g0 y0) (H3 y0 i) - end). - exists ginv. - * destruct x; simpl. - generalize (H3 (f x) p). - rewrite H1. - intro; destruct (proof_irrelevance _ p p0). - reflexivity. - * destruct y; simpl. - generalize (H3 x p). - rewrite H2. - intro; destruct (proof_irrelevance _ p p0). - reflexivity. +- apply bij_finite with False. + { constructor. } + apply eq_cardinal_empty_type. + apply proj1_sig. +- destruct (HP None). + + eapply bij_finite. + 2: apply eq_cardinal_sig_option_In; auto. + constructor. + apply IHFiniteT. + intros x. apply HP. + + eapply bij_finite. + 2: apply eq_cardinal_sig_option_nIn; auto. + apply IHFiniteT. + unfold compose. + intros x. apply HP. +- destruct H0 as [f Hf]. + apply bij_finite with (sig (compose P f)). + 2: apply eq_cardinal_sig_comp_invertible; auto. + apply IHFiniteT. + unfold compose. + intros x. apply HP. Qed. Lemma inj_finite: forall (X Y:Type) (f:X->Y), @@ -432,46 +345,19 @@ Lemma inj_finite: forall (X Y:Type) (f:X->Y), FiniteT X. Proof. intros. -assert (forall y:{y:Y | exists x:X, f x = y}, {x:X | f x = proj1_sig y}). -{ intro. destruct y. simpl. - apply constructive_definite_description. - destruct e. - exists x0. - red; split. - { assumption. } - intros. - apply H0. - transitivity x. - - assumption. - - symmetry; assumption. +apply bij_finite with { y : Y | Im Full_set f y }. +{ apply finite_subtype; auto. + intros y. + specialize (H1 y) as [[x Hx]|Hy]; [left|right]. + - subst. apply Im_def; constructor. + - intros Hy0. + destruct Hy0 as [x Hx y Hy0]. + subst. contradict Hy; exists x; reflexivity. } -pose (g := fun y:{y:Y | exists x:X, f x = y} => - proj1_sig (X0 y)). -apply bij_finite with _ g. -{ apply finite_subtype. - + assumption. - + assumption. -} -pose (ginv := fun (x:X) => exist (fun y:Y => exists x:X, f x = y) - (f x) (ex_intro _ x (refl_equal _))). -exists ginv. -- destruct x as [y [x e]]. - unfold g; simpl. - match goal with |- context [X0 ?arg] => destruct (X0 arg) end. - simpl. - unfold ginv; simpl. - simpl in e0. - repeat match goal with |- context [ex_intro ?f ?x ?e] => - generalize (ex_intro f x e) end. - rewrite <- e0. - intros; destruct (proof_irrelevance _ e1 e2). - reflexivity. -- intro; unfold ginv. - unfold g; simpl. - match goal with |- context [X0 ?arg] => destruct (X0 arg) end. - simpl. - simpl in e. - auto. +clear H1. +transitivity (sig (@Full_set X)). +- apply eq_cardinal_sig_injective_image; auto. +- apply eq_cardinal_sig_Full_set. Qed. Lemma finite_inj_surj: forall (X:Type) (f:X->X), @@ -564,22 +450,24 @@ induction H. congruence. * exists None. symmetry; assumption. -- destruct H1. - pose (f' := fun (x:X) => g (f (f0 x))). - assert (surjective f'). +- destruct H1 as [g [h Hgh]]. + pose (f' := fun (x:X) => h (f (g x))). + assert (surjective f') as Hf'. { apply IHFiniteT. - red; intros. - unfold f' in H3. - assert (f (f0 x) = f (f0 y)). - { congruence. } - apply H0 in H4. - congruence. + apply injective_compose. + 2: apply invertible_impl_bijective; exists g; + apply inverse_map_sym; + assumption. + apply injective_compose; auto. + apply invertible_impl_bijective; exists h; auto. } red; intro. - destruct (H3 (g y)). - unfold f' in H4. - exists (f0 x). - congruence. + specialize (Hf' (h y)) as [x Hx]. + unfold f' in Hx. + exists (g x). + apply inverse_map_sym in Hgh. + unshelve eapply (proj1 (invertible_impl_bijective h _)); auto. + exists g; assumption. Qed. Lemma finite_surj_inj: forall (X:Type) (f:X->X), @@ -594,10 +482,9 @@ destruct H1 as [g]. assert (surjective g). { apply finite_inj_surj. { assumption. } - red; intros. - rewrite <- H1 with x. - rewrite <- H1 with y. - rewrite H2; reflexivity. + eapply injective_compose_conv. + unfold compose. + intros ? ? ?. rewrite !H1 in H2; assumption. } red; intros. destruct (H2 x). @@ -608,92 +495,19 @@ subst. reflexivity. Qed. -Lemma finite_sum: forall X Y:Type, FiniteT X -> FiniteT Y -> - FiniteT (X+Y). -Proof. -intros. -induction H0. -- apply bij_finite with _ inl. - { assumption. } - pose (g := fun (x:X+False) => match x with - | inl x => x - | inr f => False_rect X f - end). - exists g. - + intro; simpl. reflexivity. - + destruct y. - * simpl. reflexivity. - * destruct f. -- pose (g := fun (x:option (X+T)) => match x with - | Some (inl x) => inl _ x - | Some (inr t) => inr _ (Some t) - | None => inr _ None - end). - apply bij_finite with _ g. - { apply add_finite. assumption. } - pose (ginv := fun (x:X + option T) => match x with - | inl x => Some (inl _ x) - | inr (Some t) => Some (inr _ t) - | inr None => None - end). - exists ginv. - + destruct x as [[x|t]|]; trivial. - + destruct y as [x|[t|]]; trivial. -- pose (g := fun (x:X+X0) => match x with - | inl x0 => inl _ x0 - | inr x0 => inr _ (f x0) - end). - destruct H1. - pose (ginv := fun (x:X+Y) => match x with - | inl x0 => inl _ x0 - | inr y0 => inr _ (g0 y0) - end). - apply bij_finite with _ g. - + assumption. - + exists ginv. - * destruct x as [x0|x0]; trivial. - simpl. - rewrite H1; reflexivity. - * destruct y as [x|y0]; trivial. - simpl. - rewrite H2; reflexivity. -Qed. - Lemma finite_prod: forall (X Y:Type), FiniteT X -> FiniteT Y -> FiniteT (X*Y). Proof. intros. induction H0. -- apply bij_finite with _ (False_rect _). - + constructor. - + exists (@snd X False). - * destruct x. - * destruct y. - destruct f. -- pose (g := fun (x:X*T + X) => match x with - | inl (pair x0 t) => pair x0 (Some t) - | inr x0 => pair x0 None - end). - pose (ginv := fun (x:X * option T) => match x with - | (x0, Some t) => inl _ (x0, t) - | (x0, None) => inr _ x0 - end). - apply bij_finite with _ g. - + apply finite_sum; assumption. - + exists ginv. - * destruct x as [[x0 t]|x0]; trivial. - * destruct y as [x0 [t|]]; trivial. -- pose (g := fun (y:X*X0) => match y with - | pair x x0 => pair x (f x0) - end). - destruct H1. - pose (ginv := fun (y:X*Y) => let (x,y0) := y in - (x, g0 y0)). - apply bij_finite with _ g. - { assumption. } - exists ginv. - + destruct x as [x x0]; unfold ginv, g; try rewrite H1; trivial. - + destruct y as [x y]; unfold ginv, g; try rewrite H2; trivial. +- apply bij_finite with False. + { constructor. } + apply eq_cardinal_prod_False. +- apply bij_finite with (X * T + X)%type. + 2: apply eq_cardinal_prod_option_r. + apply finite_sum; assumption. +- apply bij_finite with (X * X0)%type; auto. + apply eq_cardinal_prod_Proper; auto; reflexivity. Qed. Lemma finite_exp: forall X Y:Type, FiniteT X -> FiniteT Y -> @@ -701,42 +515,14 @@ Lemma finite_exp: forall X Y:Type, FiniteT X -> FiniteT Y -> Proof. intros. induction H. -- pose (g := fun (x:True) (f:False) => False_rect Y f). - pose (ginv := fun (_:False->Y) => I). - apply bij_finite with _ g. - + apply True_finite. - + exists ginv. - * destruct x as []. - trivial. - * intro; extensionality f. - destruct f. -- pose (g := fun (p:(T->Y)*Y) (x:option T) => - let (f,y0) := p in - match x with - | Some x0 => f x0 - | None => y0 - end). - pose (ginv := fun (f:option T->Y) => - (fun x:T => f (Some x), f None)). - apply bij_finite with _ g. - { apply finite_prod; assumption. } - exists ginv. - + destruct x as [f y0]; try extensionality t; - try destruct t as [t0|]; trivial. - + intro. - extensionality t; destruct t as [t0|]; trivial. -- destruct H1. - pose (g0 := fun (h:X->Y) (y:Y0) => h (g y)). - apply bij_finite with _ g0. - { assumption. } - pose (g0inv := fun (h:Y0->Y) (x:X) => h (f x)). - exists g0inv. - + intro. - extensionality x0; unfold g0; unfold g0inv; simpl. - rewrite H1; reflexivity. - + intro. - extensionality y0; unfold g0; unfold g0inv; simpl. - rewrite H2; reflexivity. +- apply bij_finite with (option False). + { do 2 constructor. } + apply eq_cardinal_fun_from_False. +- apply bij_finite with ((T -> Y) * Y)%type. + 2: apply eq_cardinal_fun_option_l. + apply finite_prod; assumption. +- apply bij_finite with (X -> Y)%type; auto. + apply eq_cardinal_fun_l; assumption. Qed. Lemma injection_preserves_cardinal: forall (X Y:Type) @@ -797,6 +583,7 @@ Proof. * destruct x; try contradiction. exists t; auto. - intros. + destruct H0 as [f Hf]. specialize (IHFiniteT (fun x : X => In U (f x))). @@ -809,11 +596,11 @@ Proof. 1: apply injection_preserves_cardinal. 1: assumption. + red; intros. - apply invertible_impl_bijective in H0. - destruct H0. apply H0 in H3. assumption. + apply invertible_impl_bijective in H2; + assumption. + extensionality_ensembles. * subst. assumption. - * destruct H0. + * destruct Hf as [g []]. exists (g x); auto. unfold In at 1. rewrite H4. assumption. @@ -915,16 +702,17 @@ constructor. Qed. Lemma FiniteT_nat_cardinal_bijection: - forall (X Y:Type) (H:FiniteT X) (g:X->Y) (Hinv:invertible g), - FiniteT_nat_cardinal Y (bij_finite X Y g H Hinv) = + forall (X Y:Type) (H:FiniteT X) (Heq : eq_cardinal X Y), + FiniteT_nat_cardinal Y (bij_finite X Y H Heq) = FiniteT_nat_cardinal X H. Proof. intros. apply FiniteT_nat_cardinal_cond. -apply invertible_impl_bijective in Hinv. -destruct Hinv as [g_inj g_surj]. -rewrite Im_Full_set_surj in g_surj. -rewrite g_surj. +destruct Heq as [f Hf]. +apply invertible_impl_bijective in Hf. +destruct Hf as [f_inj f_surj]. +rewrite (proj1 (Im_Full_set_surj f)). +2: { assumption. } apply injection_preserves_cardinal; trivial. apply FiniteT_nat_cardinal_def. Qed. @@ -934,8 +722,8 @@ Lemma unique_FiniteT_nat_cardinal: f False empty_finite = 0 /\ (forall (X:Type) (H:FiniteT X), f (option X) (add_finite X H) = S (f X H)) /\ - (forall (X Y:Type) (H:FiniteT X) (g:X->Y) (Hinv:invertible g), - f Y (bij_finite X Y g H Hinv) = f X H). + (forall (X Y:Type) (H:FiniteT X) (Heq : eq_cardinal X Y), + f Y (bij_finite X Y H Heq) = f X H). Proof. match goal with |- @ex ?T (@unique ?T ?f) => apply -> (@unique_existence T f) end. @@ -958,7 +746,7 @@ split. destruct (proof_irrelevance _ (add_finite T HFinite) HFinite0). rewrite Hoption_f, Hoption_g, IHHFinite. reflexivity. + intro. - destruct (proof_irrelevance _ (bij_finite _ _ f0 HFinite H) HFinite0). + destruct (proof_irrelevance _ (bij_finite _ _ HFinite H) HFinite0). now rewrite Hbijection_f, Hbijection_g, IHHFinite. Qed. @@ -1008,12 +796,12 @@ induction H. apply n_Sn in H2. contradiction. - intro. - destruct H1. - apply IHFiniteT. - exists (compose x f). - apply invertible_impl_bijective in H0. - destruct H0. - apply surjective_compose; assumption. + destruct H0 as [f Hf]. + destruct H1 as [h Hh]. + contradict IHFiniteT. + exists (compose h f). + apply surjective_compose; auto. + apply invertible_impl_bijective; auto. Qed. Lemma FiniteT_nat_embeds {X : Type} : @@ -1035,44 +823,27 @@ induction H. apply H0 in H3. rewrite H3. reflexivity. + reflexivity. -- destruct IHFiniteT as [g]. - destruct H0 as [f']. - exists (fun y => g (f' y)). - apply injective_compose. - 2: { assumption. } - destruct (invertible_impl_bijective f'). - 2: { assumption. } - exists f; assumption. +- destruct H0 as [f [g Hfg]]. + destruct IHFiniteT as [h Hh]. + exists (compose h g). + apply injective_compose; auto. + apply invertible_impl_bijective. + exists f. + apply inverse_map_sym; assumption. Qed. Lemma FiniteT_unit : FiniteT unit. Proof. - unshelve eapply bij_finite with (X := option False). - - intros. constructor. - - repeat constructor. - - unshelve econstructor. - + intros. exact None. - + intros. destruct x; intuition. - + intros. destruct y; intuition. + apply bij_finite with (option False). + { do 2 constructor. } + apply eq_cardinal_unit_option_False. Qed. Lemma FiniteT_bool : FiniteT bool. Proof. - unshelve eapply bij_finite with (X := option (option False)). - - intros. - refine (match H with - | None => true - | Some _ => false - end). - - repeat constructor. - - unshelve econstructor. - + intros. - apply (match H with - | true => None - | false => Some None - end). - + intros. destruct x as [[]|]; intuition. - + intros. destruct y as [|]; intuition. + apply bij_finite with (unit + unit)%type. + 2: apply eq_cardinal_bool_sum_unit. + apply finite_sum; apply FiniteT_unit. Qed. Lemma finite_nat_initial_segment: forall n:nat, @@ -1093,6 +864,122 @@ apply Extensionality_Ensembles; split; intros m Hm; cbv in *; lia. Qed. +Lemma infinite_nat_inj: forall X:Type, ~ FiniteT X -> + exists f:nat->X, injective f. +Proof. +intros. +assert (inhabited (forall S:Ensemble X, Finite S -> + { x:X | ~ In S x})). +{ pose proof (choice (fun (x:{S:Ensemble X | Finite S}) (y:X) => + ~ In (proj1_sig x) y)). + simpl in H0. + match type of H0 with | ?A -> ?B => assert B end. + { apply H0. + intros. + apply NNPP. + red; intro. + pose proof (not_ex_not_all _ _ H1); clear H1. + destruct x. + assert (x = Full_set). + { apply Extensionality_Ensembles; red; split; auto with sets. } + subst. + contradict H. + apply Finite_full_impl_FiniteT. + assumption. + } + clear H0. + destruct H1. + exists. + intros. + exists (x (exist _ S H1)). + exact (H0 (exist _ S H1)). +} +destruct H0. + +assert (forall (n:nat) (g:forall m:nat, m X), + { x:X | forall (m:nat) (Hlt:m x }). +{ intros. + assert (Finite (fun x:X => exists m:nat, exists Hlt:m + g (proj1_sig x) (proj2_sig x)). + + match goal with |- @Finite X ?S => assert (S = + Im Full_set h) end. + - apply Extensionality_Ensembles; red; split; red; intros; destruct H0. + + destruct H0. + now exists (exist (fun m:nat => m < n) x0 x1). + + destruct x. + now exists x, l. + - rewrite H0; apply FiniteT_img. + + apply finite_nat_initial_segment. + + intros. + apply classic. + } + destruct (X0 _ H0). + unfold In in n0. + exists x. + intros; red; intro. + contradiction n0; exists m; exists Hlt; exact H1. +} +pose (f := Fix Wf_nat.lt_wf (fun n:nat => X) + (fun (n:nat) (g:forall m:nat, mX) => proj1_sig (X1 n g))). +simpl in f. +assert (forall n m:nat, m f m <> f n). +{ pose proof (Fix_eq Wf_nat.lt_wf (fun n:nat => X) + (fun (n:nat) (g:forall m:nat, mX) => proj1_sig (X1 n g))). + fold f in H0. + simpl in H0. + match type of H0 with | ?A -> ?B => assert (B) end. + - apply H0. + intros. + replace f0 with g. + { reflexivity. } + extensionality y; extensionality p; symmetry; apply H1. + - intros. + specialize (H1 n). + destruct X1 in H1. + simpl in H1. + destruct H1. + auto. +} +exists f. +red; intros m n ?. +destruct (Compare_dec.lt_eq_lt_dec m n) as [[Hlt|Heq]|Hlt]; trivial. +- contradiction (H0 n m). +- now contradiction (H0 m n). +Qed. + +Lemma nat_infinite: ~ FiniteT nat. +Proof. +red; intro. +assert (surjective S). +{ apply finite_inj_surj; trivial. + red; intros. + injection H0; trivial. +} +destruct (H0 0). +discriminate H1. +Qed. + +Lemma FiniteT_cardinality {X : Type} : + FiniteT X <-> lt_cardinal X nat. +Proof. +split; intros. +- split. + + destruct (FiniteT_nat_embeds H) as [f]. + exists f. assumption. + + intros H0. + apply nat_infinite. + apply bij_finite with X; assumption. +- destruct H as [[f Hf] H]. + apply NNPP. intro. + destruct (infinite_nat_inj _ H0) as [g]. + contradict H. + apply CSB_inverse_map with (f := f) (g := g); + auto. +Qed. + Lemma finite_indexed_union {A T : Type} {F : IndexedFamily A T} : FiniteT A -> (forall a, Finite (F a)) -> @@ -1121,15 +1008,15 @@ induction H; econstructor. eassumption. ** now right. -- replace (IndexedUnion F) with (IndexedUnion (fun x => F (f x))). +- destruct H0 as [f Hf]. + replace (IndexedUnion F) with (IndexedUnion (fun x => F (f x))). + apply IHFiniteT. intro. apply H1. + extensionality_ensembles. * econstructor. eassumption. - * destruct H0. - rewrite <- (H3 a) in H2. - econstructor. - eassumption. + * destruct Hf as [g Hfg]. + exists (g a). rewrite (proj2 Hfg). + assumption. Qed. diff --git a/theories/ZornsLemma/FunctionProperties.v b/theories/ZornsLemma/FunctionProperties.v index d7e2b89b..abbcee2a 100644 --- a/theories/ZornsLemma/FunctionProperties.v +++ b/theories/ZornsLemma/FunctionProperties.v @@ -9,32 +9,46 @@ Definition surjective {X Y:Type} (f:X->Y) := Definition bijective {X Y:Type} (f:X->Y) := injective f /\ surjective f. -Inductive invertible {X Y:Type} (f:X->Y) : Prop := - | intro_invertible: forall g:Y->X, - (forall x:X, g (f x) = x) -> (forall y:Y, f (g y) = y) -> - invertible f. +Definition inverse_map {X Y : Type} + (f : X -> Y) (g : Y -> X) := + (forall x, g (f x) = x) /\ + (forall y, f (g y) = y). + +Definition invertible {X Y:Type} (f:X->Y) : Prop := + exists g : Y -> X, inverse_map f g. + +Lemma inverse_map_sym {X Y : Type} + (f : X -> Y) (g : Y -> X) : + inverse_map f g -> inverse_map g f. +Proof. +unfold inverse_map. tauto. +Qed. + +Lemma inverse_map_unique {X Y : Type} + (f : X -> Y) (g0 g1 : Y -> X) : + inverse_map f g0 -> inverse_map f g1 -> + forall y : Y, g0 y = g1 y. +Proof. +intros Hg0 Hg1 y. +transitivity (g0 (f (g1 y))). +- rewrite (proj2 Hg1). reflexivity. +- rewrite (proj1 Hg0). reflexivity. +Qed. Lemma unique_inverse: forall {X Y:Type} (f:X->Y), invertible f -> - exists! g:Y->X, (forall x:X, g (f x) = x) /\ - (forall y:Y, f (g y) = y). + exists! g:Y->X, inverse_map f g. Proof. -intros. -destruct H. +intros X Y f [g Hfg]. exists g. -red; split. -{ tauto. } -intros. -destruct H1. +split. +{ assumption. } +intros h Hfh. extensionality y. -transitivity (g (f (x' y))). -- rewrite H2. reflexivity. -- rewrite H. reflexivity. +eapply inverse_map_unique; eassumption. Qed. Definition function_inverse {X Y:Type} (f:X->Y) - (i:invertible f) : { g:Y->X | (forall x:X, g (f x) = x) /\ - (forall y:Y, f (g y) = y) } - := + (i:invertible f) : { g:Y->X | inverse_map f g } := (constructive_definite_description _ (unique_inverse f i)). @@ -59,7 +73,7 @@ assert (forall y:Y, {x:X | f x = y}). pose (g := fun y:Y => proj1_sig (X0 y)). pose proof (fun y:Y => proj2_sig (X0 y)). simpl in H1. -exists g. +exists g. split. - intro. apply H. unfold g; rewrite H1. @@ -72,7 +86,7 @@ Lemma invertible_impl_bijective: forall {X Y:Type} (f:X->Y), invertible f -> bijective f. Proof. intros. -destruct H. +destruct H as [g []]. split. - red; intros. congruence. @@ -90,6 +104,12 @@ red; split; red; intros. - exists y. reflexivity. Qed. +Lemma id_inverse_map (X : Type) : + inverse_map (@id X) (@id X). +Proof. + split; reflexivity. +Qed. + Lemma injective_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : injective f -> injective g -> injective (compose g f). Proof. @@ -120,14 +140,20 @@ split. - apply surjective_compose; assumption. Qed. +Lemma inverse_map_compose {X Y Z : Type} + (f0 : X -> Y) (f1 : Y -> X) (g0 : Y -> Z) (g1 : Z -> Y) : + inverse_map f0 f1 -> inverse_map g0 g1 -> + inverse_map (compose g0 f0) (compose f1 g1). +Proof. +unfold inverse_map, compose; intuition; congruence. +Qed. + Lemma invertible_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : invertible f -> invertible g -> invertible (compose g f). Proof. -intros. -destruct H as [f'], H0 as [g']. -exists (compose f' g'); intros; unfold compose. -- rewrite H0. apply H. -- rewrite H1. apply H2. +intros [f0 Hf] [g0 Hg]. +exists (compose f0 g0). +apply inverse_map_compose; assumption. Qed. Lemma surjective_compose_conv {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : diff --git a/theories/ZornsLemma/FunctionPropertiesEns.v b/theories/ZornsLemma/FunctionPropertiesEns.v index 7ef8521c..73b6045f 100644 --- a/theories/ZornsLemma/FunctionPropertiesEns.v +++ b/theories/ZornsLemma/FunctionPropertiesEns.v @@ -1,12 +1,21 @@ (** Similar to [ZornsLemma.FunctionProperties] but focused on properties restricted to ensembles. *) -From Coq Require Import ClassicalChoice Description Program.Subset. +From Coq Require Import + ClassicalChoice + Description + Program.Subset. From ZornsLemma Require Import - DecidableDec EnsemblesImplicit - Families FunctionProperties Image InverseImage Powerset_facts + DecidableDec + EnsemblesImplicit + Families + FunctionProperties + Image + InverseImage + Powerset_facts Proj1SigInjective. -From Coq Require Import RelationClasses. +From Coq Require Import + RelationClasses. Section FunctionPropertiesEns. Context {A B : Type} @@ -111,6 +120,7 @@ Proof. reflexivity. Qed. +#[export] Instance range_id_refl {A : Type} : Reflexive (@range A A id). Proof. diff --git a/theories/ZornsLemma/IndexedFamilies.v b/theories/ZornsLemma/IndexedFamilies.v index 2813164e..beae94b2 100644 --- a/theories/ZornsLemma/IndexedFamilies.v +++ b/theories/ZornsLemma/IndexedFamilies.v @@ -1,7 +1,8 @@ From ZornsLemma Require Export Families. From ZornsLemma Require Import EnsemblesImplicit - FunctionProperties. + FunctionProperties + ImageImplicit. Set Implicit Arguments. @@ -124,11 +125,13 @@ Lemma IndexedIntersection_surj_fn surjective f -> IndexedIntersection V = IndexedIntersection (fun x => V (f x)). Proof. -intros. -apply Extensionality_Ensembles; split; red; intros. -- destruct H0. constructor. intros. apply H0. -- destruct H0. constructor. intros. destruct (H a). - subst. apply H0. +intros Hf. +apply Extensionality_Ensembles; split. +- intros x Hx. destruct Hx as [x Hx]. + constructor. intros b. apply Hx. +- intros x Hx. destruct Hx as [x Hx]. + constructor. intros a. + specialize (Hf a) as [b Hb]. subst. apply Hx. Qed. Lemma image_indexed_union (X Y I : Type) (F : IndexedFamily I X) (f : X -> Y) : diff --git a/theories/ZornsLemma/InfiniteTypes.v b/theories/ZornsLemma/InfiniteTypes.v index 7679d18c..7862369e 100644 --- a/theories/ZornsLemma/InfiniteTypes.v +++ b/theories/ZornsLemma/InfiniteTypes.v @@ -25,14 +25,9 @@ assert (inhabited (forall S:Ensemble X, Finite S -> assert (x = Full_set). { apply Extensionality_Ensembles; red; split; auto with sets. } subst. - contradiction H. - apply bij_finite with (f:=@proj1_sig _ (fun x:X => In Full_set x)). - { apply Finite_ens_type; assumption. } - exists (fun x:X => exist _ x (Full_intro _ x)). - - destruct x; simpl. - generalize (Full_intro X x). - intro i0; destruct (proof_irrelevance _ i i0); trivial. - - trivial. + contradict H. + apply Finite_full_impl_FiniteT. + assumption. } clear H0. destruct H1. diff --git a/theories/ZornsLemma/InverseImage.v b/theories/ZornsLemma/InverseImage.v index 32c08fba..95dfb353 100644 --- a/theories/ZornsLemma/InverseImage.v +++ b/theories/ZornsLemma/InverseImage.v @@ -7,7 +7,8 @@ From ZornsLemma Require Import Definition inverse_image {X Y:Type} (f:X->Y) (T:Ensemble Y) : Ensemble X := [ x:X | In T (f x) ]. -Global Hint Unfold inverse_image : sets. +#[global] +Hint Unfold inverse_image : sets. Lemma inverse_image_increasing: forall {X Y:Type} (f:X->Y) (T1 T2:Ensemble Y), Included T1 T2 -> @@ -95,7 +96,9 @@ apply Extensionality_Ensembles; split; red; intros. constructor; trivial. Qed. -Global Hint Resolve inverse_image_increasing : sets. +#[global] +Hint Resolve inverse_image_increasing : sets. +#[global] Hint Rewrite @inverse_image_empty @inverse_image_full @inverse_image_intersection @inverse_image_union @inverse_image_complement @inverse_image_composition : sets. @@ -280,6 +283,23 @@ Proof. assumption. Qed. +Lemma inverse_map_image_inverse_image {X Y : Type} + (f : X -> Y) (g : Y -> X) : + inverse_map f g -> + forall (U : Ensemble X), + Im U f = inverse_image g U. +Proof. + intros [Hfg0 Hfg1] U. + apply Extensionality_Ensembles; split; red. + - intros y Hy. + destruct Hy as [x Hx y Hy]. + subst. constructor. + congruence. + - intros y [Hy]. + rewrite <- Hfg1. + apply Im_def. assumption. +Qed. + Lemma inverse_image_image_surjective_locally {X Y} (f : X -> Y) (T : Ensemble Y) : (forall y, In T y -> exists x, f x = y) -> Im (inverse_image f T) f = T. diff --git a/theories/ZornsLemma/Powerset_facts.v b/theories/ZornsLemma/Powerset_facts.v index e4923120..ae908b8d 100644 --- a/theories/ZornsLemma/Powerset_facts.v +++ b/theories/ZornsLemma/Powerset_facts.v @@ -114,6 +114,7 @@ apply Extensionality_Ensembles; split; red; intros. - destruct H. split; assumption. Qed. +#[export] Instance Disjoint_Symmetric (A : Type) : Symmetric (@Disjoint A). Proof. diff --git a/theories/ZornsLemma/ReverseMath/AddSubtract.v b/theories/ZornsLemma/ReverseMath/AddSubtract.v index b7baa4f2..3aad90c1 100644 --- a/theories/ZornsLemma/ReverseMath/AddSubtract.v +++ b/theories/ZornsLemma/ReverseMath/AddSubtract.v @@ -1,7 +1,11 @@ (* “This is why we can’t have nice things.” *) -From ZornsLemma Require Import EnsemblesImplicit. -From Coq Require Import Morphisms Setoid. +From Coq Require Import + Morphisms + Setoid. +From ZornsLemma Require Import + EnsemblesImplicit. +#[export] Instance In_Same_set_Proper {Z : Type} : Proper (Same_set ==> eq ==> iff) (@In Z). Proof. diff --git a/theories/ZornsLemma/ReverseMath/ReverseCSB.v b/theories/ZornsLemma/ReverseMath/ReverseCSB.v index 4a23574d..66f14c88 100644 --- a/theories/ZornsLemma/ReverseMath/ReverseCSB.v +++ b/theories/ZornsLemma/ReverseMath/ReverseCSB.v @@ -32,12 +32,13 @@ Proof. + destruct (p None) eqn:?. * right. intros. destruct o; auto. * left. exists None. assumption. - - specialize (IHFiniteT (fun x => p (f x))) as [[o]|]. + - destruct H0 as [f Hf]. + specialize (IHFiniteT (fun x => p (f x))) as [[o]|]. + left. exists (f o). assumption. + right. intros. - destruct H0 as [g]. - rewrite <- (H2 o). - apply H1. + destruct Hf as [g Hfg]. + rewrite <- (proj2 Hfg o). + apply H0. Qed. (* Lemma 7 of the above paper. *) @@ -80,7 +81,8 @@ Proof. apply functional_extensionality. auto. Qed. -Global Instance N_equiv_Equivalence : Equivalence N_equiv. +#[export] +Instance N_equiv_Equivalence : Equivalence N_equiv. Proof. unfold N_equiv. split; red; intros.