Require Export Sierpinski.Hartogs.

Definition sum_fun X Y Z (p : X -> Z) (q : Y -> Z) :=
  fun z : X + Y => match z with inl x => p x | inr y => q y end.

Lemma biject_sum_prod X Y Z :
  biject (((X -> Z) * (Y -> Z)) : Type) (((X + Y) -> Z) : Type).
Proof.
  exists (fun pq : (X -> Z) * (Y -> Z) => let (p, q) := pq in sum_fun p q).
  exists (fun pq => (fun x => pq (inl x), fun y => pq (inr y))). split.
  - intros [p q]. cbn. reflexivity.
  - intros pq. apply FE. now intros [x|y].
Qed.

Lemma biject_sum_assoc X Y Z :
  biject (X + (Y + Z)) (X + Y + Z).
Proof.
  exists (fun z => match z with inl x => inl (inl x) | inr (inl y) => inl (inr y) | inr (inr z) => inr z end).
  exists (fun z => match z with inl (inl x) => inl x | inl (inr y) => inr (inl y) | inr z => inr (inr z) end).
  split. now intros [x|[y|z]]. now intros [[x|y]|z].
Qed.

Lemma biject_sum_bool X :
  biject (X + X) (bool * X).
Proof.
  exists (fun x => match x with inl x => (true, x) | inr x => (false, x) end).
  exists (fun x => match x with (true, x) => inl x | (false, x) => inr x end).
  split. intros []; reflexivity. intros [[]]; reflexivity.
Qed.

Lemma biject_unit_nat :
  biject (unit + nat) (nat : Type).
Proof.
  exists (fun x => match x with inl _ => 0 | inr n => S n end).
  exists (fun n => match n with 0 => inl tt | S n => inr n end).
  split. now intros [[]|n]. now intros [].
Qed.

Lemma biject_unit_fun X :
  biject X (unit -> X).
Proof.
  exists (fun x => fun _ => x), (fun f => f tt). split; trivial.
  intros f. apply FE. now intros [].
Qed.

Local Axiom UC : forall X (p : X -> Prop), (exists! x, p x) -> sig p.

Lemma SXM (X : Prop) :
  X + ~ X.
Proof.
  destruct (@UC bool (fun b => if b then X else ~ X)) as [b Hb].
  - destruct (XM X) as [H|H].
    + exists true. split; trivial. intros []; tauto.
    + exists false. split; trivial. intros []; tauto.
  - destruct b. now left. now right.
Qed.

Lemma biject_bool_prop :
  biject (bool : Type) (Prop : Type).
Proof.
  exists (fun b : bool => if b then True else False).
  exists (fun P => if SXM P then true else false).
  split.
  - intros []; destruct SXM; tauto.
  - intros P. destruct SXM; apply PE; tauto.
Qed.

Lemma biject_bool_subsingleton :
  biject (bool : Type) ((unit -> Prop) : Type).
Proof.
  rewrite <- biject_unit_fun. apply biject_bool_prop.
Qed.

Lemma biject_pred_sum X (p : X -> Prop) :
  biject X (sig p + sig (fun x => ~ p x)).
Proof.
  unshelve eexists. 2: unshelve eexists. 3: split.
  - intros x. destruct (SXM (p x)) as [H|H]; [left | right]; now exists x.
  - intros [[x _]|[x _]]; exact x.
  - cbn. intros x. now destruct SXM.
  - cbn. intros [[x Hx]|[x Hx]]; destruct SXM; try contradiction.
    + repeat f_equal. apply PI.
    + repeat f_equal. apply PI.
Qed.

Definition ran X Y (f : X -> Y) :=
  fun y => exists x, y = f x.

Lemma biject_ran (X Y : Type) (f : X -> Y) :
  injective f -> biject X (sig (ran f)).
Proof.
  intros Hf. unshelve eexists. 2: unshelve eexists. 3: split.
  - intros x. exists (f x). exists x. reflexivity.
  - intros [y H]. destruct (@UC _ (fun x => y = f x)) as [x _]; try exact x.
    destruct H as [x Hx]. exists x. split; try apply Hx. intros x' ->. now apply Hf.
  - cbn. intros x. destruct UC as [x' H]. now apply Hf.
  - cbn. intros [y [x ->]]. apply exist_eq. now destruct UC as [x' H].
Qed.

Lemma infinite_unit X :
  infinite X -> biject (unit + X) X.
Proof.
  intros [f Hf]. rewrite (@biject_pred_sum X (ran f)).
  rewrite <- biject_ran; trivial. rewrite biject_sum_assoc.
  rewrite biject_unit_nat. reflexivity.
Qed.

Fact infinite_power X :
  infinite X -> biject ((X -> Prop) + (X -> Prop)) (X -> Prop).
Proof.
  intros H. rewrite biject_sum_bool. rewrite biject_bool_subsingleton.
  rewrite biject_sum_prod. apply biject_power. now apply infinite_unit.
Qed.

Lemma Cantor X (f : X -> X -> Prop) :
  { p | forall x, f x <> p }.
Proof.
  exists (fun x => ~ f x x). intros x H.
  enough (f x x <-> ~ f x x) by tauto.
  pattern (f x) at 1. now rewrite H.
Qed.

Definition clean_sum X Y Z (f : X -> Y + Z) :
  (forall x y, f x <> inl y) -> X -> Z.
Proof.
  intros H x. destruct (f x) as [y|z] eqn : Hx.
  - exfalso. now apply (H x y).
  - exact z.
Defined.

Lemma clean_sum_spec' Y Z (a : Y + Z) (Ha : forall y, a <> inl y) :
  inr (match a as s return (a = s -> Z) with
       | inl y => fun Hx : a = inl y => False_rect Z (Ha y Hx)
       | inr z => fun _ : a = inr z => z
       end eq_refl) = a.
Proof.
  destruct a. firstorder congruence. reflexivity.
Qed.

Lemma clean_sum_spec X Y Z (f : X -> Y + Z) (Hf : forall x y, f x <> inl y) x :
  inr (clean_sum Hf x) = f x.
Proof.
  unfold clean_sum. apply clean_sum_spec'.
Qed.

Fact Cantor_biject_inject X Y :
  biject (X -> Prop) (X + Y) -> biject (X + X) X -> inject (X -> Prop) Y.
Proof.
  intros H1 H2. assert (biject (X + Y) ((X -> Prop) * (X -> Prop))) as (f&g&Hgf&Hfg).
  - eapply biject_trans; try apply biject_sym, H1.
    eapply biject_trans; try apply biject_power, biject_sym, H2.
    symmetry. apply biject_sum_prod.
  - pose (f' x := fst (f (inl x))). destruct (Cantor f') as [p Hp].
    pose (g' q := g (p, q)). assert (H' : forall q x, g' q <> inl x).
    + intros q x H. apply (Hp x). unfold f'. rewrite <- H. unfold g'. now rewrite Hfg.
    + exists (clean_sum H'). intros q q' H. assert (Hqq' : g' q = g' q').
      * rewrite <- !(clean_sum_spec H'). now rewrite H.
      * unfold g' in Hqq'. change (snd (p, q) = snd (p, q')).
        rewrite <- (Hfg (p, q)), <- (Hfg (p, q')). now rewrite Hqq'.
Qed.

Lemma Cantor_rel X (R : X -> (X -> Prop) -> Prop) :
  functional_rel R -> { p | forall x, ~ R x p }.
Proof.
  intros HR. pose (pc x := forall p, R x p -> ~ p x).
  exists pc. intros x H. enough (pc x <-> ~ pc x) by tauto. split.
  - intros Hx. now apply Hx.
  - intros Hx p Hp. now rewrite (HR _ _ _ Hp H).
Qed.

Fact Cantor_inject_inject X Y :
  inject (X -> Prop) (X + Y) -> inject (X + X) X -> inject (X -> Prop) Y.
Proof.
  intros H1 H2. assert (inject ((X -> Prop) * (X -> Prop)) (X + Y)) as (f&Hf).
  - eapply inject_trans; try apply H1.
    eapply inject_trans; try apply inject_power_morph, H2.
    apply biject_inject, biject_sum_prod.
  - pose (R x p := exists q, f (p, q) = inl x). destruct (@Cantor_rel _ R) as [p Hp].
    { intros x p p' [q Hq] [q' Hq']. injection (Hf (p, q) (p', q')); congruence. }
    pose (f' q := f (p, q)). assert (H' : forall q x, f' q <> inl x).
    + intros q x H. apply (Hp x). exists q. apply H.
    + exists (clean_sum H'). intros q q' H. assert (Hqq' : f' q = f' q').
      * rewrite <- !(clean_sum_spec H'). now rewrite H.
      * apply Hf in Hqq'. congruence.
Qed.

Definition GCH :=
  forall X Y, infinite X -> inject X Y -> inject Y (X -> Prop) -> inject Y X \/ inject (X -> Prop) Y.

Definition powfix X :=
  forall n, inject (powit X n + powit X n) (powit X n).

Lemma Sierpinski_step X n :
  GCH -> infinite X -> powfix X -> inject (HN X) (powit X n) -> inject X (HN X).
Proof.
  intros gch H1 H2 Hi. induction n.
  - now apply HN_ninject in Hi.
  - destruct (gch (powit X n) (powit X n + HN X)) as [H|H].
    + now apply infinite_powit.
    + exists inl. congruence.
    + eapply inject_trans.
      * apply inject_sum; try apply Hi. apply inject_power.
      * rewrite <- powit_shift. apply (H2 (S n)).
    + apply IHn. eapply inject_trans; try apply H. exists inr. congruence.
    + apply inject_trans with (powit X (S n)); try apply inject_powit.
      cbn. rewrite powit_shift. apply (Cantor_inject_inject H). apply (H2 n).
Qed.

Theorem Sierpinski' X :
  GCH -> infinite X -> inject X (HN (X -> Prop)).
Proof.
  intros gch HX. eapply inject_trans; try apply inject_power.
  apply Sierpinski_step with 3; try apply gch.
  - apply infinite_inject with X; trivial. apply inject_power.
  - intros n. rewrite !powit_shift. now apply biject_inject, infinite_power, infinite_powit.
  - apply HN_inject.
Qed.

Theorem Sierpinski X :
  GCH -> inject X (HN (nat + X -> Prop)).
Proof.
  intros gch. eapply inject_trans.
  2: apply Sierpinski'; trivial.
  - exists inr. congruence.
  - exists inl. congruence.
Qed.

Lemma WO_HN X :
  WO_type (HN X).
Proof.
  exists (fun a b => le (pi1 a) (pi1 b)). split.
  - apply HN_refl.
  - apply HN_trans.
  - apply HN_antisym.
  - apply HN_wf.
Qed.

Lemma GCH_WO X :
  GCH -> WO_type X.
Proof.
  intros gch. eapply WO_transport.
  - now apply Sierpinski.
  - apply WO_HN.
Qed.

Definition ACR_type X :=
  forall p : X -> Prop, ex p -> { q | q <<= p /\ exists! x, q x }.

Definition AC_type X :=
  forall p : X -> Prop, ex p -> sig p.

Lemma ACR_AC X :
  ACR_type X -> AC_type X.
Proof.
  intros H p Hp. destruct (H p Hp) as [q[H1 H2]].
  destruct (UC H2) as [x Hx]. exists x. apply H1, Hx.
Qed.

Lemma WO_ACR X R :
  @WO X R -> ACR_type X.
Proof.
  intros HR p Hp % HR. exists (fun x => p x /\ (forall y : X, p y -> R x y)). firstorder.
Qed.

Definition ACS_type Y :=
  forall X (R : X -> Y -> Prop), total_rel R -> exists f, forall x, R x (f x).

Lemma WO_ACS X :
  WO_type X -> ACS_type X.
Proof.
  intros [R HR % WO_ACR % ACR_AC] Y S HS.
  exists (fun y => pi1 (HR _ (HS y))). intros y. apply pi2.
Qed.

Theorem GCH_ACS Y :
  GCH -> ACS_type Y.
Proof.
  intros H. apply WO_ACS, GCH_WO, H.
Qed.