Sierpinski.Sierpinski

Require Export Sierpinski.Hartogs.

Require Import Coq.Logic.Classical.

Require Import Coq.Program.Program.
Require Import Coq.Init.Nat.

Definition Infinite (A : S) :=
  Numeral <= A.

Definition Generalized_Continuum_Hypothesis :=
  forall x y : S,
    Infinite x ->
    x <= y <= 𝒫 x ->
    x ∼ y \/ y ∼ 𝒫 x.

Definition Well_Ordering_Theorem :=
  forall x : S, inhabited (Strict_Well_Order_On x).

Definition Axiom_Of_Choice :=
  forall A B : S, forall R : A -> B -> Prop,
      (forall x, exists y, R x y) ->
      exists f : A -> B, forall x : A, R x (f x).

Definition Axiom_Of_Choice' :=
  forall (I : S) (F : I -> S),
    (forall i, inhabited (F i)) ->
    inhabited (forall i, F i).

Lemma AC_equiv :
  Axiom_Of_Choice <-> Axiom_Of_Choice'.
Proof.
  unfold Axiom_Of_Choice, Axiom_Of_Choice'.
  split; intros AC.
  - intros I F H. pose (R (i : I) (A : ⋃ i ∈ I, F i) := A ∈ F i).
    destruct (AC _ _ R) as [f Hf].
    + intros i. destruct (H i) as [A]. unshelve eexists.
      * exists A. apply in_indexed_union_iff. exists i. apply A.
      * unfold R. apply A.
    + refine (inhabits (fun i => _)). exists (f i). apply Hf.
  - intros A B R existence.
    assert (inhabitation : forall x : A, inhabited `{ y in B | R x y }). {
      intros x. destruct (existence x) as [y Hy].
      apply inhabits. exists y. apply in_comprehension_iff_typed. exact Hy.
    }
    destruct (AC _ _ inhabitation) as [f].
    exists (fun x : A => element (f x)).
    intros x. apply comprehension_condition.
Qed.

Definition Axiom_Of_Choice'' :=
  forall (A : S),
    (forall x : A, inhabited x) ->
    exists f : A -> big_union A,
    forall x, f x ∈ x.

Lemma AC_equiv' :
  Axiom_Of_Choice <-> Axiom_Of_Choice''.
Proof.
  rewrite AC_equiv.
  unfold Axiom_Of_Choice', Axiom_Of_Choice''. split.
  - intros ac A H.
    specialize (ac A id H). cbn in ac. destruct ac as [f].
    assert (forall x : A, f x ∈ big_union A). {
      setoid_rewrite in_big_union_iff. intros x. exists x. exact _.
    }
    exists (fun x : A => element (f x)).
    exact _.
  - intros ac I F H. specialize (ac `{F i | i in I}).
    assert (H' : forall x : `{ F i | i in I }, inhabited x). {
      intros [x Hx]. cbn. apply in_fun_replacement_iff in Hx.
      destruct Hx as [i ->]. apply H.
    }
    specialize (ac H'). destruct ac as [f Hf]. apply inhabits. intros i.
    assert (F i ∈ `{ F i | i in I }). {
      apply in_fun_replacement_iff. exists i. reflexivity.
    }
    exact (element (f (element (F i)))).
Qed.

Lemma Well_Ordering_to_Choice' :
  Well_Ordering_Theorem -> Axiom_Of_Choice'.
Proof.
  intros well_ordering I F H.

  destruct (well_ordering (⋃ i ∈ I, F i)) as [R].

  assert (forall i, F i ∈ 𝒫 (⋃ i ∈ I, F i)) by automation.
  exact (inhabits (fun i => least_element (element (F i)) (H i))).
Qed.

Lemma Well_Ordering_to_Choice :
  Well_Ordering_Theorem -> Axiom_Of_Choice.
Proof. rewrite AC_equiv. exact Well_Ordering_to_Choice'. Qed.

Lemma lemma1 (A B : S) :
  A ⊔ A ∼ A ->
  A ⊔ B ∼ 𝒫 A ->
  𝒫 A <= B.
Proof.
  intros H1 H2.

  assert (f : A ⊔ B ∼ 𝒫 A × 𝒫 A). {

    transitivity (𝒫 A). {
      exact H2.
    }

    transitivity (𝒫 (A ⊔ A)). {
      rewrite H1. reflexivity.
    }

    rewrite power_set_of_disjoint_union. reflexivity.

  } destruct f as [f].
  clear H1 H2.

  assert (H : exists A1 : 𝒫 A, forall A2 : 𝒫 A, Is_From_Right (f⁻¹ `(A1, A2))). {

    set (g := π1 ∘ f ∘ inj1 _ _ : A -> 𝒫 A).
    assert (H : ~ surjective g). {
      intros H. apply (cantors_theorem A).
      exact (inhabits (build_surjection g H)).
    }

    change (~ forall A1, exists a, A1 = g a) in H.

    apply not_all_ex_not in H. destruct H as [A1 H]. exists A1.

    intros A2.
    enough (~ Is_From_Left (f⁻¹ `(A1, A2))). {
      destruct (from_left_or_right (f⁻¹ `(A1, A2))); tauto.
    }
    unfold Is_From_Left. unfold g in H; cbn in g.

    intros [a contra]. apply H. exists a.
    unfold compose. rewrite <- contra.
    rewrite cancel_inverse_right. rewrite left_projection_beta.
    reflexivity.
  }
  destruct H as [A1 H].

  unshelve eset (g (A2 : 𝒫 A) := extract_from_right (f⁻¹ `(A1, A2)) : B). {

    apply H.
  }

  simple refine (inhabits (build_injection g _)).
  intros A2 A2' H1. unfold g in H1.
  apply extract_from_right_is_injective in H1.
  apply bijection_is_injective in H1.
  apply pair_is_injective_right in H1.
  exact H1.

Qed.

Lemma lemma2 (x y : S) :
  Generalized_Continuum_Hypothesis ->
  Infinite x ->
  x ⊔ x ∼ x ->
  𝒫 x ⊔ 𝒫 x ∼ 𝒫 x ->
  y <= 𝒫 x ->
  y <= x \/ 𝒫 x <= y.
Proof.
  intros gch. intros H1 H2 H3 H4.

  assert (x <= x ⊔ y <= 𝒫 x). {
    split.
    - apply disjoint_union_is_increasing_on_left.
    - rewrite (power_set_is_increasing x) at 1.
      rewrite H4. rewrite H3. reflexivity.
  }

  assert (cases : x ∼ x ⊔ y \/
                  x ⊔ y ∼ 𝒫 x). {

    apply gch; assumption.
  } destruct cases as [-> | H5].

  - left. apply disjoint_union_is_increasing_on_right.

  - right. apply lemma1.
    + assumption.
    + rewrite H5. reflexivity.

Qed.

Theorem sierpinskis_theorem :
  Generalized_Continuum_Hypothesis -> Axiom_Of_Choice.
Proof.
  intros gch. apply Well_Ordering_to_Choice. intros x.

  enough (H : exists α : O, x <= α). {
    destruct H as [α [f]].
    apply inhabits.

    apply (transport_strict_well_order (injection_as_bijection_into_image f)⁻¹).
    unshelve refine (restrict_well_order (strict_well_order_on_ordinal α)
                                         (image_of f)).
    automation.
  }



  set (x0 := x ⊔ Numeral).
  set (x' n := iter (1 + n) 𝒫 x0).

  exists (hartogs_number (x' 0)).

  transitivity (x' 0). {
    cbn. unfold x0.
    rewrite <- power_set_is_increasing.
    rewrite <- disjoint_union_is_increasing_on_left.
    reflexivity.
  }

  assert (H1 : forall n, x' n ⊔ x' n ∼ x' n). {
    intros n. change (x' n) with (𝒫 (iter n 𝒫 x0)).
    symmetry. apply power_set_equiv_power_set_plus_power_set.
    induction n.
    - cbn. unfold x0. apply disjoint_union_is_increasing_on_right.
    - change (iter (Datatypes.S n) 𝒫 x0) with (𝒫 (iter n 𝒫 x0)).
      rewrite power_set_is_increasing at 1. rewrite IHn at 1. reflexivity.
  }



  assert (H2 : (hartogs_number (x' 0) : S) <= x' 6) by
    apply hartogs_number_has_upper_bound.
  revert H2. generalize 6. intros n H2. induction n.
  - apply hartogs_number_is_not_smaller in H2. contradiction.
  - assert (cases : (hartogs_number (x' 0) : S) <= x' n \/
                    x' (1 + n) <= hartogs_number (x' 0)). {
      apply lemma2; auto.
      - unfold Infinite. clear. induction n.
        + cbn. unfold x0. rewrite <- power_set_is_increasing.
          apply disjoint_union_is_increasing_on_right.
        + change (Numeral <= 𝒫 (x' n)).
          rewrite IHn. apply power_set_is_increasing.
      - apply H1.
    } destruct cases as [ | <-].
    + apply IHn. assumption.
    + unfold x'. generalize (1 + n) x0; clear. intros n x0; induction n.
      * reflexivity.
      * rewrite IHn. rewrite power_set_is_increasing. reflexivity.
Qed.