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 :=
   x y : S,
    Infinite x
    x y 𝒫 x
    x y y 𝒫 x.

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

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

Definition Axiom_Of_Choice' :=
   (I : S) (F : I S),
    ( i, inhabited (F i))
    inhabited ( 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 : 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'' :=
   (A : S),
    ( x : A, inhabited x)
     f : A big_union A,
     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 ( 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' : 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 ( 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 .

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

    transitivity (𝒫 A). {
      exact .
    }

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

    rewrite power_set_of_disjoint_union. reflexivity.

  } destruct f as [f].
  clear .

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

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

    change ( A1, a, = g a) in H.

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

    intros .
    enough ( Is_From_Left (f⁻¹ `(, ))). {
      destruct (from_left_or_right (f⁻¹ `(, ))); 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 [ H].

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

    apply H.
  }

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

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 .

  assert (x x y 𝒫 x). {
    split.
    - apply disjoint_union_is_increasing_on_left.
    - rewrite (power_set_is_increasing x) at 1.
      rewrite . rewrite . reflexivity.
  }

  assert (cases : x x y
                  x y 𝒫 x). {

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

  - left. apply disjoint_union_is_increasing_on_right.

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

Qed.


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

  enough (H : α : 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 ( := x Numeral).
  set (x' n := iter (1 + n) 𝒫 ).

  exists (hartogs_number (x' 0)).

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

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



  assert ( : (hartogs_number (x' 0) : S) x' 6) by
    apply hartogs_number_has_upper_bound.
  revert . generalize 6. intros n . induction n.
  - apply hartogs_number_is_not_smaller in . 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 . rewrite power_set_is_increasing.
          apply disjoint_union_is_increasing_on_right.
        + change (Numeral 𝒫 (x' n)).
          rewrite IHn. apply power_set_is_increasing.
      - apply .
    } destruct cases as [ | ].
    + apply IHn. assumption.
    + unfold x'. generalize (1 + n) ; clear. intros n ; induction n.
      * reflexivity.
      * rewrite IHn. rewrite power_set_is_increasing. reflexivity.
Qed.