From ce98c01f41b3eb7956b2b92b1f2cd3dc7f5a377a Mon Sep 17 00:00:00 2001 From: Columbus240 <8899730+Columbus240@users.noreply.github.com> Date: Fri, 15 Sep 2023 12:32:37 +0200 Subject: [PATCH] =?UTF-8?q?[B]=20Change=20order=20of=20Cardinals,=20Finite?= =?UTF-8?q?,=20Countable=20=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Moves the definition of `eq_cardinal` to Cardinals, where it belongs. But to allow this, the statements `countable_img_inj` and `FiniteT_cardinality` had to be moved to Countable and FiniteTypes respectively. In addition, `CountableT_cardinality` was removed, because `CountableT` could be redefined in terms of `le_cardinal`, making the lemma even more trivial. Also, removes the file InfiniteTypes, because it has become empty. --- _CoqProject | 1 - theories/Topology/CountabilityAxioms.v | 3 +- theories/ZornsLemma/Cardinals.v | 48 +++------ theories/ZornsLemma/CardinalsEns.v | 18 ++-- theories/ZornsLemma/CountableTypes.v | 12 ++- theories/ZornsLemma/FiniteTypes.v | 140 +++++++++++++++++++++---- theories/ZornsLemma/IndexedFamilies.v | 15 +-- theories/ZornsLemma/InfiniteTypes.v | 108 ------------------- 8 files changed, 163 insertions(+), 182 deletions(-) delete mode 100644 theories/ZornsLemma/InfiniteTypes.v diff --git a/_CoqProject b/_CoqProject index b8dfcf7e..1c1f82dc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -64,7 +64,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/theories/Topology/CountabilityAxioms.v b/theories/Topology/CountabilityAxioms.v index d59796b5..921939b5 100644 --- a/theories/Topology/CountabilityAxioms.v +++ b/theories/Topology/CountabilityAxioms.v @@ -12,8 +12,7 @@ From ZornsLemma Require Export From ZornsLemma Require Import Classical_Wf DecidableDec - FiniteIntersections - InfiniteTypes. + FiniteIntersections. From Coq Require Import RelationClasses. diff --git a/theories/ZornsLemma/Cardinals.v b/theories/ZornsLemma/Cardinals.v index d2bb890e..b3666769 100644 --- a/theories/ZornsLemma/Cardinals.v +++ b/theories/ZornsLemma/Cardinals.v @@ -6,17 +6,16 @@ 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 EnsemblesSpec. 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 ZornsLemma Require Import CSB. 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. @@ -34,6 +33,17 @@ split. apply injective_compose; auto. Qed. +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. + Instance le_cardinal_PartialOrder : PartialOrder eq_cardinal le_cardinal. Proof. @@ -86,12 +96,6 @@ Proof. 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. @@ -535,30 +539,6 @@ destruct (types_comparable T0 T1) as [[f]|[f]]; 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. -- 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 cardinal_no_inj_equiv_lt_cardinal (A B : Type) : (forall f : A -> B, ~ injective f) <-> lt_cardinal B A. diff --git a/theories/ZornsLemma/CardinalsEns.v b/theories/ZornsLemma/CardinalsEns.v index ccbc9a7b..57b19b82 100644 --- a/theories/ZornsLemma/CardinalsEns.v +++ b/theories/ZornsLemma/CardinalsEns.v @@ -776,7 +776,7 @@ Proof. { exact (H 0 ltac:(constructor)). } destruct H as [f [Hf0 Hf1]]. red in Hf0. - apply InfiniteTypes.nat_infinite. + 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). @@ -792,9 +792,9 @@ Proof. apply subset_eq. reflexivity. } destruct H as [g Hg0]. - eapply bij_finite with _. - 2: exists g, f0; split; apply Hg0. - assumption. + 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. } @@ -818,14 +818,12 @@ Proof. } 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. + apply nat_Finite_bounded_char. + exists n. intros m Hm. + destruct Hm as [x Hx m Hm]; subst. + apply Hn; auto. Qed. Lemma Countable_as_le_cardinal_ens {X : Type} (U : Ensemble X) : diff --git a/theories/ZornsLemma/CountableTypes.v b/theories/ZornsLemma/CountableTypes.v index 4fca4fe2..95365ad6 100644 --- a/theories/ZornsLemma/CountableTypes.v +++ b/theories/ZornsLemma/CountableTypes.v @@ -14,12 +14,12 @@ From Coq Require Import QArith ZArith. From ZornsLemma Require Import + Cardinals CSB DecidableDec DependentTypeChoice Finite_sets - FunctionPropertiesEns - InfiniteTypes. + FunctionPropertiesEns. From ZornsLemma Require Export FiniteTypes IndexedFamilies. @@ -29,7 +29,7 @@ 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}. @@ -390,3 +390,9 @@ 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. diff --git a/theories/ZornsLemma/FiniteTypes.v b/theories/ZornsLemma/FiniteTypes.v index 9d4ed866..49cd4727 100644 --- a/theories/ZornsLemma/FiniteTypes.v +++ b/theories/ZornsLemma/FiniteTypes.v @@ -1,9 +1,12 @@ From Coq Require Import Arith + ClassicalChoice Description FunctionalExtensionality Lia. From ZornsLemma Require Import + Cardinals + CSB DecidableDec FiniteImplicit Finite_sets @@ -19,20 +22,6 @@ From Coq Require Import Set Asymmetric Patterns. -Definition eq_cardinal (X Y : Type) : Prop := - exists (f : X -> Y) (g : Y -> X), inverse_map f g. - -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. - Inductive FiniteT : Type -> Prop := | empty_finite: FiniteT False | add_finite: forall T:Type, FiniteT T -> FiniteT (option T) @@ -1230,6 +1219,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)) -> @@ -1266,8 +1371,7 @@ induction H; + extensionality_ensembles. * econstructor. eassumption. - * destruct Hf as [g [Hgf Hfg]]. - rewrite <- (Hfg a) in H0. - econstructor. - eassumption. + * destruct Hf as [g Hfg]. + exists (g a). rewrite (proj2 Hfg). + assumption. Qed. 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 deleted file mode 100644 index 54ea3a6b..00000000 --- a/theories/ZornsLemma/InfiniteTypes.v +++ /dev/null @@ -1,108 +0,0 @@ -From Coq Require Import - Arith - ClassicalChoice - FunctionalExtensionality - Lia. -From ZornsLemma Require Export FiniteTypes. -From ZornsLemma Require Import - EnsemblesImplicit - EnsemblesSpec - FunctionProperties. - -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 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 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 (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.