Library mathcomp.analysis.cardinality

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice order.
From mathcomp Require Import ssrnat seq fintype bigop div prime path finmap.
Require Import boolp classical_sets.

Set Implicit Arguments.

Reserved Notation "'`I_' n" (at level 8, n at level 2, format "'`I_' n").
Reserved Notation "A '#<=' B" (at level 79, format "A '#<=' B").

Import Order.TTheory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Lemma in_inj_comp A B C (f : B → A) (h : C → B) (P : pred B) (Q : pred C) :
  {in P &, injective f} → {in Q &, injective h} → {homo h : x / Q x >-> P x} →
  {in Q &, injective (f \o h)}.

Lemma enum0 : enum 'I_0 = [::].

Lemma enum_recr n : enum 'I_n.+1 =
  rcons (map (widen_ord (leqnSn _)) (enum 'I_n)) ord_max.

Lemma eq_set0_nil (T : eqType) (S : seq T) :
  ([set x | x \in S] == set0) = (S == [::]).

Lemma eq_set0_fset0 (T : choiceType) (S : {fset T}) :
  ([set x | x \in S] == set0) = (S == fset0).

Lemma image_nat_maximum n (f : nat → nat) :
  ∃ i, i ≤ n ∧ ∀ j, j ≤ n → f j ≤ f i.

Lemma fset_nat_maximum (A : {fset nat}) : A != fset0 →
  (∃ i, i \in A ∧ ∀ j, j \in A → j ≤ i)%nat.

Definition surjective aT rT (A : set aT) (B : set rT) (f : aT → rT) :=
  ∀ u, B u → ∃ t, A t ∧ u = f t.

Section surjective_lemmas.
Variables aT rT : Type.
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).

Lemma surjective_id T : surjective setT setT (@id T).

Lemma surjective_set0 B f : surjective set0 B f → B = set0.

Lemma surjective_image A f : surjective A (f @` A) f.

Lemma surjective_image_eq0 A B f : f @` A `<=` B →
  B `\` f @` A = set0 → surjective A B f.

Lemma surjectiveE f A B :
  surjective A B f = (B `<=` f @` A).

Lemma surj_image_eq B A f :
 f @` A `<=` B → surjective A B f → f @` A = B.

Lemma can_surjective g f (A : {pred aT}) (B : {pred rT}) :
    {in B, {on A, cancel g & f}} → {homo g : x / x \in B >-> x \in A} →
  surjective A B f.

End surjective_lemmas.
Arguments can_surjective {aT rT} g [f A B].

Lemma surjective_comp T1 T2 T3 (A : set T1) (B : set T2) (C : set T3) f g:
  surjective A B f → surjective B C g → surjective A C (g \o f).

Definition set_bijective aT rT (A : set aT) (B : set rT) (f : aT → rT) :=
  [/\ {in A &, injective f}, f @` A `<=` B & surjective A B f].

Section set_bijective_lemmas.
Variables aT rT : Type.
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).

Lemma inj_of_bij A B f : set_bijective A B f → {in A &, injective f}.

Lemma sub_of_bij A B f : set_bijective A B f → f @` A `<=` B.

Lemma sur_of_bij A B f : set_bijective A B f → surjective A B f.

Lemma set_bijective1 A B f g : {in A, f =1 g} →
  set_bijective A B f → set_bijective A B g.

Lemma set_bijective_image A f :
  {in A &, injective f} → set_bijective A (f @` A) f.

Lemma set_bijective_subset A B f :
  set_bijective A B f → ∀ B0, B0 `<=` B →
  set_bijective ((f @^-1` B0) `&` A) B0 f.

End set_bijective_lemmas.

Lemma set_bijective_comp T1 T2 T3 (A : set T1) (B : set T2) (C : set T3) f g:
  set_bijective A B f → set_bijective B C g → set_bijective A C (g \o f).

Definition inverse (T : choiceType) (t0 : T) U (A : set T) (f : T → U) :=
  fun t ⇒ xget t0 ((f @^-1` [set t]) `&` A).

Section inverse_lemmas.
Variables (aT : choiceType) (t0 : aT) (rT : Type).
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).

Lemma injective_left_inverse A f :
  {in A &, injective f} → {in A, cancel f (inverse t0 A f)}.

Lemma injective_right_inverse A B f : {in A &, injective f} →
  B `<=` f @` A → {in B, cancel (inverse t0 A f) f}.

Lemma surjective_right_inverse A B f : surjective A B f →
  {in B, cancel (inverse t0 A f) f}.

End inverse_lemmas.

Notation "'`I_' n" := [set k | k < n].

Lemma II0 : `I_O = set0.

Lemma II1 : `I_1 = [set 0].

Lemma IIn_eq0 n : `I_n = set0 → n = 0.

Lemma II_recr n : `I_n.+1 = `I_n `|` [set n].

Lemma set_bijective_D1 T n (A : set T) (f : nat → T) :
  set_bijective `I_n.+1 A f → set_bijective `I_n (A `\ f n) f.

Lemma pigeonhole m n (f : nat → nat) : {in `I_m &, injective f} →
  f @` `I_m `<=` `I_n → m ≤ n.

Theorem Cantor_Bernstein T (U : pointedType) (A : set T) (B : set U)
  (f : T → U) (g : U → T) :
  {in A &, injective f} → f @` A `<=` B →
  {in B &, injective g} → g @` B `<=` A →
  ∃ f0 : T → U, set_bijective A B f0.

Definition card_le T U (A : set T) (B : set U) := ∃ f : T → U,
  {in A &, injective f} ∧ f @` A `<=` B.

Notation "A '#<=' B" := (card_le A B).

Lemma card_le_surj (T : pointedType) U (A : set T) (B : set U) :
  A #<= B → ∃ g : U → T, surjective B A g.

Lemma surj_card_le T (U : pointedType) (A : set T) (B : set U) (g : U → T) :
  A !=set0 → surjective B A g → A #<= B.

Lemma card_lexx T (A : set T) : A #<= A.

Lemma card_le0x T (U : pointedType) (S : set U) : @set0 T #<= S.

Lemma card_le_trans (T U : Type) V (B : set U) (A : set T) (C : set V) :
  A #<= B → B #<= C → A #<= C.

Lemma card_le0P T (U : pointedType) (A : set T) : A #<= @set0 U ↔ A = set0.

Lemma card_le_II n m : n ≤ m ↔ `I_n #<= `I_m.

Definition card_eq T U (A : set T) (B : set U) := A #<= B ∧ B #<= A.

Notation "A '#=' B" := (card_eq A B) (at level 79, format "A '#=' B").

Lemma card_eq_sym T U (A : set T) (B : set U) : A #= B → B #= A.

Lemma card_eq_trans T U V (A : set T) (B : set U) (C : set V) :
  A #= B → B #= C → A #= C.

Lemma card_eq0 T (U : pointedType) (A : set T) : A #= @set0 U → A = set0.

Lemma card_eq00 (T U : pointedType) : @set0 T #= @set0 U.

Lemma card_eqP (T : pointedType) (U : pointedType) (A : set T) (B : set U) :
  A #= B ↔ ∃ f : T → U, set_bijective A B f.

Lemma card_eqTT (T : pointedType) : @setT T #= @setT T.

Lemma card_eq_II n m : n = m ↔ `I_n #= `I_m.

Lemma card_eq_le T U V (A : set T) (B : set U) (C : set V) :
  A #= B → C #<= A → C #<= B.

Lemma card_eq_ge T U V (A : set T) (B : set U) (C : set V) :
  A #= C → A #<= B → C #<= B.

Lemma card_leP (T U : pointedType) (A : set T) (B : set U) :
  A #<= B ↔ ∃ C, C `<=` B ∧ A #= C.

Lemma set_bijective_inverse
    (T U : pointedType) (A : set T) (B : set U) (f : T → U) :
  set_bijective A B f → ∃ g, set_bijective B A g.

Definition countable T (A : set T) := A #<= @setT nat.

Lemma countable0 T : countable (@set0 T).

Lemma countable_injective T (A : set T) :
  countable A ↔ ∃ f : T → nat, {in A &, injective f}.

Lemma countable_trans T U (A : set T) (B : set U) (f : T → U) : countable B →
  {in A &, injective f} → f @` A `<=` B → countable A.

Definition set_finite (T : choiceType) (A : set T) :=
  ∃ A' : {fset T}, A = [set x | x \in A'].

Lemma set_finiteP (T : pointedType) (A : set T) :
  set_finite A ↔ ∃ n, A #= `I_n.

Lemma set_finite_seq (T : choiceType) (s : seq T) :
  set_finite [set i | i \in s].

Lemma set_finite_countable (T : pointedType) (A : set T) :
  set_finite A → countable A.

Lemma set_finite0 (T : pointedType) : set_finite (@set0 T).

Section set_finite_bijection.




Lemma set_finite_bijective (T : pointedType) (A : set T) n S : A !=set0 →
  A #= `I_n → S `<=` A →
  ∃ f, set_bijective `I_n A f ∧
    ∃ k, k ≤ n ∧ (f @^-1` S) `&` `I_n = `I_k.

End set_finite_bijection.


Lemma subset_set_finite (T : pointedType) (A B : set T) : A `<=` B →
  set_finite B → set_finite A.

Lemma subset_card_le (T : pointedType) (A B : set T) : A `<=` B →
  set_finite B → A #<= B.


Lemma injective_set_finite (T U : pointedType) (A : set T) (B : set U)
  (f : T → U) : {in A &, injective f} →
  f @` A `<=` B → set_finite B → set_finite A.

Lemma injective_card_le (T U : pointedType) (A : set T) (B : set U)
  (f : T → U) : {in A &, injective f} →
  f @` A `<=` B → set_finite B → A #<= B.

Corollary set_finite_preimage (T U : pointedType) (B : set U) (f : T → U) :
  {in (f @^-1` B) &, injective f} → set_finite B → set_finite (f @^-1` B).


Lemma surjective_set_finite
  (T : pointedType) (U : pointedType) (A : set T) (B : set U) (f : T → U) :
  surjective A B f → set_finite A → set_finite B.

Lemma surjective_card_le
  (T : pointedType) (U : pointedType) (A : set T) (B : set U) (f : T → U) :
  surjective A B f → set_finite A → B #<= A.

Lemma set_finite_diff (T : pointedType) (A B : set T) : set_finite A →
  set_finite (A `\` B).

Lemma card_le_diff (T : pointedType) (A B : set T) : set_finite A →
  A `\` B #<= A.

Lemma set_finite_inter_set0_union (T : pointedType) (A B : set T) :
  set_finite A → set_finite B → A `&` B = set0 → set_finite (A `|` B).

Lemma set_finite_inter (T : pointedType) (A B : set T) :
  (set_finite A ∨ set_finite B) → set_finite (A `&` B).

Section infinite_subset_enum.
Variable (T : pointedType) (A : set T).
Hypothesis infiniteA : ¬ set_finite A.

Lemma ex_in_D : ∀ s : seq T, ∃ a, a \in A `\` [set i | i \in s].

End infinite_subset_enum.

Section infinite_nat_subset_enum.
Variable A : set nat.
Hypothesis infiniteA : ¬ set_finite A .

Definition min_of_D s := ex_minn (ex_in_D infiniteA s).

Definition min_of_D_seq := fix f n :=
  if n is n.+1 then rcons (f n) (min_of_D (f n))
  else [:: min_of_D [::]].

Definition infsub_enum n := last O (min_of_D_seq n).

Lemma min_of_D_seqE n :
  min_of_D_seq n = [seq infsub_enum (nat_of_ord i) | i in 'I_n.+1].

Lemma increasing_infsub_enum n : infsub_enum n < infsub_enum n.+1.

Lemma sorted_infsub_enum n :
  sorted ltn [seq infsub_enum (nat_of_ord i) | i in 'I_n.+1].

Lemma injective_infsub_enum : injective infsub_enum.

Lemma subset_infsub_enum : infsub_enum @` setT `<=` A.

Lemma infinite_nat_subset_countable : A !=set0 → A #= @setT nat.

End infinite_nat_subset_enum.

Definition enumeration T (S : set T) (e : nat → T) := S = e @` setT.

Lemma enumeration_id : enumeration setT id.

Lemma enumeration_set0 T (e : nat → T) : ¬ enumeration set0 e.

Section enumeration_wo_repetitions.
Variable (T : pointedType) (A : set T).
Hypothesis infiniteA : ¬ set_finite A.
Variables (e : nat → T) (Ae : enumeration A e).

Lemma ex_enum_notin (s : seq T) : ∃ m, e m \notin s.

Definition min_of_e s := ex_minn (ex_enum_notin s).

Definition min_of_e_seq := fix h n :=
  if n is n.+1 then rcons (h n) (e (min_of_e (h n)))
  else [:: e 0].

Definition smallest_of_e n := ex_minn (ex_enum_notin (min_of_e_seq n)).

Definition enum_wo_rep n := last point (min_of_e_seq n).

Lemma enum_wo_repE n : enum_wo_rep n.+1 = e (smallest_of_e n).

Lemma min_of_e_seqE n :
  min_of_e_seq n = [seq enum_wo_rep (nat_of_ord i) | i in 'I_n.+1].

Lemma smallest_of_e_notin_enum_wo_rep j :
  e (smallest_of_e j) \notin [seq enum_wo_rep (nat_of_ord i) | i in 'I_j.+1].

Lemma injective_enum_wo_rep : injective enum_wo_rep.

Lemma surjective_enum_wo_rep : surjective setT A enum_wo_rep.

Lemma set_bijective_enum_wo_rep : set_bijective setT A enum_wo_rep.

End enumeration_wo_repetitions.

Lemma enumeration_enum_wo_rep (T : pointedType) (A : set T) (e : nat → T)
  (nfinA : ¬ set_finite A) (Ae : enumeration A e) :
  enumeration A (enum_wo_rep nfinA Ae).

Lemma countable_enumeration (T : pointedType) (A : set T) :
  countable A ↔ (A = set0 ∨ ∃ e, enumeration A e).

Section infinite_nat.

Lemma infinite_nat : ¬ set_finite (@setT nat).

End infinite_nat.

Section countably_infinite_prod_nat.

Lemma infinite_prod_nat : ¬ set_finite (@setT (nat × nat)).

Definition nat_of_pair := fun '(n, m) ⇒ 2 ^ n × 3 ^ m.

Let primes23 n m : primes (nat_of_pair (n.+1, m.+1)) = [:: 2; 3].

Let prime_decomp23 n m :
  prime_decomp (nat_of_pair (n.+1, m.+1)) = [:: (2, n.+1); (3, m.+1)].

Lemma nat_of_pair_inj : {in setT &, injective nat_of_pair}.

Lemma countable_prod_nat : countable (@setT (nat × nat)).

Let decomp_two (n : nat) : n ≠ O → {pq | (n == 2 ^ pq.1 × pq.2) && odd pq.2}.

Lemma countably_infinite_prod_nat : @setT (nat × nat) #= @setT nat.

End countably_infinite_prod_nat.