Require Import Setoid Morphisms.

Require Export Sierpinski.Sierpinski.

Definition biject_rel X Y :=
  exists (R : X -> Y -> Prop), total_rel R /\ functional_rel R /\ injective_rel R /\ surjective_rel R.

Lemma biject_inject_rel X Y :
  biject_rel X Y -> inject_rel X Y.
Proof.
  intros [R HR]. exists R. repeat split; apply HR.
Qed.

Lemma inject_rel_trans X Y Z :
  inject_rel X Y -> inject_rel Y Z -> inject_rel X Z.
Proof.
  intros (R&HR1&HR2&HR3) (S&HS1&HS2&HS3).
  exists (fun x z => exists y, R x y /\ S y z). repeat split.
  - intros x. destruct (HR1 x) as [y Hy]. destruct (HS1 y) as [z Hz]. now exists z, y.
  - intros x z z' [y[H1 H2]] [y'[H3 H4]]. rewrite (HR2 _ _ _ H3 H1) in H4. now rewrite (HS2 _ _ _ H2 H4).
  - intros z x x' [y[H1 H2]] [y'[H3 H4]]. rewrite (HS3 _ _ _ H4 H2) in H3. now rewrite (HR3 _ _ _ H1 H3).
Qed.

Lemma inject_rel_sum X Y X' Y' :
  inject_rel X X' -> inject_rel Y Y' -> inject_rel (X + Y) (X' + Y').
Proof.
  intros (R&HR1&HR2&HR3) (S&HS1&HS2&HS3).
  exists (fun a b => match a, b with inl x, inl x' => R x x' | inr y, inr y' => S y y' | _, _ => False end). repeat split.
  - intros [x|y].
    + destruct (HR1 x) as [x' Hx']. now exists (inl x').
    + destruct (HS1 y) as [y' Hy']. now exists (inr y').
  - intros [x|y] [x'|y'] [x''|y'']; intuition; f_equal; firstorder.
  - intros [x|y] [x'|y'] [x''|y'']; intuition; f_equal; firstorder.
Qed.

Lemma inject_rel_power_morph X Y :
  inject_rel X Y -> inject_rel (X -> Prop) (Y -> Prop).
Proof.
  intros (R&HR1&HR2&HR3). apply inject_inject_rel.
  exists (fun p => fun y => exists x, p x /\ R x y).
  intros p q H. apply incl_antisym.
  - intros x Hx. destruct (HR1 x) as [y Hy]. assert (Hp : exists x', p x' /\ R x' y) by now exists x.
    pattern y in Hp. rewrite H in Hp. destruct Hp as [x'[H1 H2]]. now rewrite (HR3 y x x').
  - intros x Hx. destruct (HR1 x) as [y Hy]. assert (Hp : exists x', q x' /\ R x' y) by now exists x.
    pattern y in Hp. rewrite <- H in Hp. destruct Hp as [x'[H1 H2]]. now rewrite (HR3 y x x').
Qed.

Lemma biject_biject_rel X Y :
  biject X Y -> biject_rel X Y.
Proof.
  intros (f & g & Hgf & Hfg). exists (fun x y => y = f x). repeat split.
  - intros x. exists (f x). reflexivity.
  - intros x y y' H ->. apply H.
  - intros y x x' -> H. now rewrite <- (Hgf x), <- (Hgf x'), H.
  - intros y. exists (g y). now rewrite Hfg.
Qed.

Lemma biject_rel_refl X :
  biject_rel X X.
Proof.
  apply biject_biject_rel, biject_refl.
Qed.

Lemma biject_rel_sym X Y :
  biject_rel X Y -> biject_rel Y X.
Proof.
  intros [R HR]. exists (fun y x => R x y). repeat split; apply HR.
Qed.

Lemma biject_rel_trans X Y Z :
  biject_rel X Y -> biject_rel Y Z -> biject_rel X Z.
Proof.
  intros (R&HR1&HR2&HR3&HR4) (S&HS1&HS2&HS3&HS4).
  exists (fun x z => exists y, R x y /\ S y z). repeat split.
  - intros x. destruct (HR1 x) as [y Hy]. destruct (HS1 y) as [z Hz]. now exists z, y.
  - intros x z z' [y[H1 H2]] [y'[H3 H4]]. rewrite (HR2 _ _ _ H3 H1) in H4. now rewrite (HS2 _ _ _ H2 H4).
  - intros z x x' [y[H1 H2]] [y'[H3 H4]]. rewrite (HS3 _ _ _ H4 H2) in H3. now rewrite (HR3 _ _ _ H1 H3).
  - intros z. destruct (HS4 z) as [y Hy]. destruct (HR4 y) as [x Hx]. now exists x, y.
Qed.

Instance biject_rel_equiv :
  Equivalence biject_rel.
Proof.
  split.
  - intros X. apply biject_rel_refl.
  - intros X Y. apply biject_rel_sym.
  - intros X Y Z. apply biject_rel_trans.
Qed.

Instance biject_rel_sum :
  Proper (biject_rel ==> biject_rel ==> biject_rel) sum.
Proof.
  intros X X' (R&HR1&HR2&HR3&HR4) Y Y' (S&HS1&HS2&HS3&HS4).
  exists (fun a b => match a, b with inl x, inl x' => R x x' | inr y, inr y' => S y y' | _, _ => False end). repeat split.
  - intros [x|y].
    + destruct (HR1 x) as [x' Hx']. now exists (inl x').
    + destruct (HS1 y) as [y' Hy']. now exists (inr y').
  - intros [x|y] [x'|y'] [x''|y'']; intuition; f_equal; firstorder.
  - intros [x|y] [x'|y'] [x''|y'']; intuition; f_equal; firstorder.
  - intros [x'|y'].
    + destruct (HR4 x') as [x Hx]. now exists (inl x).
    + destruct (HS4 y') as [y Hy]. now exists (inr y).
Qed.

Instance biject_rel_prod :
  Proper (biject_rel ==> biject_rel ==> biject_rel) prod.
Proof.
  intros X X' (R&HR1&HR2&HR3&HR4) Y Y' (S&HS1&HS2&HS3&HS4).
  exists (fun a b => R (fst a) (fst b) /\ S (snd a) (snd b)). repeat split.
  - intros [x y]; cbn. destruct (HR1 x) as [x' Hx'], (HS1 y) as [y' Hy']. now exists (x', y').
  - intros [x y] [x' y'] [x'' y''] [H1 H2] [H3 H4]; cbn in *. f_equal; firstorder.
  - intros [x y] [x' y'] [x'' y''] [H1 H2] [H3 H4]; cbn in *. f_equal; firstorder.
  - intros [x' y']; cbn. destruct (HR4 x') as [x Hx], (HS4 y') as [y Hy]. now exists (x, y).
Qed.

Instance biject_rel_power :
  Proper (biject_rel ==> biject_rel) (fun X => X -> Prop).
Proof.
  intros X Y (R&HR1&HR2&HR3&HR4).
  exists (fun p q => forall x y, R x y -> p x <-> q y). repeat split.
  - intros p. exists (fun y => forall x, R x y -> p x). firstorder. now rewrite (HR3 _ _ _ H1 H).
  - intros p q q' Hq Hq'. apply FE. intros y. apply PE. destruct (HR4 y) as [x Hx].
    rewrite <- (Hq x); trivial. now apply Hq'.
  - intros q p p' Hp Hp'. apply FE. intros x. apply PE. destruct (HR1 x) as [y Hy].
    rewrite (Hp' x y); trivial. now apply Hp.
  - intros q. exists (fun x => forall y, R x y -> q y). firstorder. now rewrite (HR2 _ _ _ H1 H).
Qed.

Lemma biject_rel_bool_subsingleton :
  biject_rel bool (unit -> Prop).
Proof.
  exists (fun (b : bool) p => if b then p = (fun _ => True) else p = (fun _ => False)). repeat split.
  - intros b. exists (if b then (fun _ => True) else (fun _ => False)). now destruct b.
  - intros [] p p' -> ->; reflexivity.
  - intros p [] [] -> H; trivial; exfalso.
    + change ((fun _ : unit => False) tt). now rewrite <- H.
    + change ((fun _ : unit => False) tt). now rewrite H.
  - intros p. destruct (XM (p tt)) as [H|H].
    + exists true. apply FE. intros []. apply PE. tauto.
    + exists false. apply FE. intros []. apply PE. tauto.
Qed.

Lemma biject_rel_pred_sum X (p : X -> Prop) :
  biject_rel X (sig p + sig (fun x => ~ p x)).
Proof.
  exists (fun x a => x = match a with inl (exist _ y _) => y | inr (exist _ y _) => y end). repeat split.
  - intros x. destruct (XM (p x)) as [H|H].
    + exists (inl (exist p x H)). reflexivity.
    + exists (inr (exist _ x H)). reflexivity.
  - intros x [[y Hy]|[y Hy]] [[y' Hy']|[y' Hy']] -> ->; try contradiction.
    all: f_equal; now apply exist_eq.
  - intros [[y Hy]|[y Hy]] x x' -> ->; reflexivity.
  - intros [[y Hy]|[y Hy]]; now exists y.
Qed.

Lemma biject_rel_ran X Y (f : X -> Y) :
  injective f -> biject_rel X (sig (ran f)).
Proof.
  intros Hf. exists (fun x a => f x = pi1 a). repeat split.
  - intros x. unshelve eexists. exists (f x). now exists x. reflexivity.
  - intros x a a' ->. apply exist_pi1.
  - intros a x x' <- H. now apply Hf.
  - intros [y[x Hx]]. cbn. now exists x.
Qed.

Lemma infinite_unit_rel X :
  infinite X -> biject_rel (unit + X) X.
Proof.
  intros [f Hf].
  eapply biject_rel_trans; try apply biject_rel_sum.
  - apply biject_rel_refl.
  - apply (@biject_rel_pred_sum X (ran f)).
  - eapply biject_rel_trans; try apply biject_biject_rel, biject_sum_assoc.
    assert (H : biject_rel (unit + sig (ran f)) (sig (ran f))).
    + eapply biject_rel_trans; try apply biject_rel_sum.
      * apply biject_rel_refl.
      * symmetry. now apply biject_rel_ran.
      * eapply biject_rel_trans; try apply biject_biject_rel, biject_unit_nat.
        now apply biject_rel_ran.
    + eapply biject_rel_trans; try apply biject_rel_sum; try apply H.
      * apply biject_rel_refl.
      * symmetry. apply biject_rel_pred_sum.
Qed.

Fact infinite_power_rel X :
  infinite X -> biject_rel ((X -> Prop) + (X -> Prop)) (X -> Prop).
Proof.
  intros H.
  eapply biject_rel_trans; try apply biject_biject_rel, biject_sum_bool.
  eapply biject_rel_trans; try apply biject_rel_prod.
  - apply biject_rel_bool_subsingleton.
  - apply biject_rel_refl.
  - eapply biject_rel_trans; try apply biject_biject_rel, biject_sum_prod.
    apply biject_rel_power. now apply infinite_unit_rel.
Qed.

Lemma WO_transport_rel X Y :
  inject_rel X Y -> WO_type Y -> WO_type X.
Proof.
  intros (R&HR1&HR2&HR3) [r []].
  exists (fun x x' => forall y y', R x y -> R x' y' -> r y y'). split.
  - intros x y y' H1 H2. rewrite (HR2 _ _ _ H2 H1). apply WO_refl.
  - intros x1 x2 x3 H1 H2 y1 y3 H3 H4. destruct (HR1 x2) as [y2 Hy]. intuition eauto.
  - intros x x' H1 H2. destruct (HR1 x) as [y Hy], (HR1 x') as [y' Hy'].
    rewrite (WO_antisym y y') in Hy; intuition eauto.
  - intros p [x Hx]. destruct (WO_wf (fun y => exists x, R x y /\ p x)) as [y[[x'[H1 H2]] Hy]].
    + destruct (HR1 x) as [y Hy]. now exists y, x.
    + exists x'. split; trivial. intros z Hz y1 y2 H3 H4. rewrite (HR2 _ _ _ H3 H1). apply Hy. now exists z.
Qed.

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

Definition ACSR_type Y :=
  forall X (R : X -> Y -> Prop), total_rel R -> exists R', total_rel R' /\ functional_rel R' /\ forall x y, R' x y -> R x y.

Fact Cantor_inject_inject_rel X Y :
  inject_rel (X -> Prop) (X + Y) -> inject_rel (X + X) X -> inject_rel (X -> Prop) Y.
Proof.
  intros H1 H2. assert (inject_rel ((X -> Prop) * (X -> Prop)) (X + Y)) as (R&HR1&HR2&HR3).
  - eapply inject_rel_trans; try apply H1.
    eapply inject_rel_trans; try apply inject_rel_power_morph, H2.
    apply biject_inject_rel, biject_biject_rel, biject_sum_prod.
  - pose (R' x p := exists q, R (p, q) (inl x)). destruct (@Cantor_rel _ R') as [p Hp].
    { intros x p p' [q Hq] [q' Hq']. specialize (HR3 _ _ _ Hq Hq'). congruence. }
    exists (fun q y => R (p, q) (inr y)). repeat split.
    + intros q. destruct (HR1 (p, q)) as [[x|y] H]; try now exists y.
      exfalso. apply (Hp x). now exists q.
    + intros q y y' Hy Hy'. specialize (HR2 _ _ _ Hy Hy'). congruence.
    + intros y q q' Hq Hq'. specialize (HR3 _ _ _ Hq Hq'). congruence.
Qed.

Definition powfix_rel X :=
  forall n, inject_rel (powit X n + powit X n) (powit X n).

Lemma Sierpinski_step_rel X n :
  GCHR -> infinite X -> powfix_rel X -> inject_rel (HN X) (powit X n) -> inject_rel X (HN X).
Proof.
  intros gch H1 H2 Hi. induction n.
  - now apply HN_ninject_rel in Hi.
  - destruct (gch (powit X n) (powit X n + HN X)) as [H|H].
    + now apply infinite_powit.
    + apply inject_inject_rel. exists inl. congruence.
    + eapply inject_rel_trans.
      * apply inject_rel_sum; try apply Hi. apply inject_inject_rel, inject_power.
      * cbn. rewrite <- powit_shift. apply (H2 (S n)).
    + apply IHn. eapply inject_rel_trans; try apply H.
      apply inject_inject_rel. exists inr. congruence.
    + apply inject_rel_trans with (powit X (S n)); try apply inject_inject_rel, inject_powit.
      cbn. rewrite powit_shift. apply (Cantor_inject_inject_rel H). apply H2.
Qed.

Theorem Sierpinski_rel' X :
  GCHR -> infinite X -> inject_rel X (HN (X -> Prop)).
Proof.
  intros gch HX. eapply inject_rel_trans; try apply inject_inject_rel, inject_power.
  apply Sierpinski_step_rel with 3; try apply gch.
  - apply infinite_inject with X; trivial. apply inject_power.
  - intros n. rewrite !powit_shift.
    now apply biject_inject_rel, infinite_power_rel, infinite_powit.
  - apply inject_inject_rel, HN_inject.
Qed.

Theorem Sierpinski_rel X :
  GCHR -> inject_rel X (HN (nat + X -> Prop)).
Proof.
  intros gch. eapply inject_rel_trans.
  2: apply Sierpinski_rel'; trivial.
  - apply inject_inject_rel. exists inr. congruence.
  - exists inl. congruence.
Qed.

Lemma GCHR_WO X :
  GCHR -> WO_type X.
Proof.
  intros gch. eapply WO_transport_rel.
  - now apply Sierpinski_rel.
  - apply WO_HN.
Qed.

Lemma WO_ACSR X :
  WO_type X -> ACSR_type X.
Proof.
  intros [R HR % WO_ACR] Y S HS.
  exists (fun y => pi1 (HR (S y) (HS y))). repeat split.
  - intros y. destruct HR as (p & Hp & x & Hx). cbn. exists x. apply Hx.
  - intros y x x' H1 H2. destruct HR as (p & Hp & z & H3 & H4). cbn in *. firstorder congruence.
  - intros y x. destruct HR as (p & Hp & z & H3 & H4). cbn. apply Hp.
Qed.

Theorem GCHR_ACSR Y :
  GCHR -> ACSR_type Y.
Proof.
  intros H. apply WO_ACSR, GCHR_WO, H.
Qed.

(* adapted from pred_ext_and_rel_choice_imp_EM in Coq.Logic.Diaconescu. *)

Lemma ACSR_bool_rel (HB : ACSR_type bool) :
  exists R : (bool -> Prop) -> bool -> Prop, forall P : bool -> Prop, (exists b : bool, P b) -> exists b : bool, P b /\ R P b /\ (forall b' : bool, R P b' -> b = b').
Proof.
  pose (R' := fun (x : { p : bool -> Prop | exists b, p b }) b => pi1 x b).
  assert (HR' : total_rel R').
  - intros [p[b Hb]]. cbn. now exists b.
  - destruct (HB _ _ HR') as (R & H1 & H2 & H3).
    exists (fun p b => exists (H : exists b, p b), R (exist _ p H) b).
    intros p H. destruct (H1 (exist _ p H)) as [b Hb].
    exists b. repeat split.
    + change p with (pi1 (exist _ p H)). apply H3, Hb.
    + exists H. apply Hb.
    + intros b' [H' Hb']. apply (H2 _ _ _ Hb). rewrite (PI H H'). apply Hb'.
Qed.

Lemma Diaconescu P :
  ACSR_type bool -> P \/ ~ P.
Proof.
  pose (U b := b = true \/ P). assert (HU : exists b, U b) by (exists true; now left).
  pose (V b := b = false \/ P). assert (HV : exists b, V b) by (exists false; now left).
  intros [R HR] % ACSR_bool_rel.
  destruct (HR U HU) as (b & [H|H] & Hb); try now left.
  destruct (HR V HV) as (b' & [H'|H'] & Hb'); try now left.
  right. intros HP. enough (b = b') by congruence.
  apply Hb. enough (U = V) as -> by apply Hb'.
  apply FE. intros c. apply PE. split; intros _; now right.
Qed.