[B] Change order of Cardinals, Finite, Countable …

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

@@ -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

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.
 

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.

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) :

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.

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<n -> X),
+  { x:X | forall (m:nat) (Hlt:m<n), g m Hlt <> x }).
+{ intros.
+  assert (Finite (fun x:X => exists m:nat, exists Hlt:m<n,
+             g m Hlt = x)).
+  { pose (h := fun x:{m:nat | m<n} =>
+      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, m<n->X) => proj1_sig (X1 n g))).
+simpl in f.
+assert (forall n m:nat, m<n -> f m <> f n).
+{ pose proof (Fix_eq Wf_nat.lt_wf (fun n:nat => X)
+    (fun (n:nat) (g:forall m:nat, m<n->X) => 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.

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) :