Require Import Classical.
Require Import Preliminaries.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Tower.
  Variable (X : ExtType) (eta : set X -> set X).
  Implicit Types (p q : set X) (F : set X -> Prop).

  Hypothesis eta_ext : forall p x, eta p x -> ~ p x.
  Hypothesis eta_uniq : forall p, unique (eta p).

  Definition adj p := p :|: eta p.

  Inductive Stage : set X -> Prop :=
  | StgA p : Stage p -> Stage (adj p)
  | StgU F : F <<= Stage -> Stage (Union F).

  Lemma eta_full_empty : ~ inhab (eta (Union Stage)).
  Proof.
    intros [x H]. apply (eta_ext H).
    exists (adj (Union Stage)); firstorder using Stage.
  Qed.

  Lemma compare_union p F :
    (forall q, F q -> cmp p q) -> cmp p (Union F).
  Proof.
    intros F_cmp. destruct (classic (exists2 q, F q & p <<= q)) as [[q fq pq]|n].
    - left. intros x px. exists q; auto.
    - right; intros x [q fq qx]. destruct (F_cmp _ fq); firstorder.
  Qed.

  Lemma compare_adj p q :
    p <<= adj q -> q <<= adj p -> cmp (adj p) (adj q).
  Proof with auto.
    intros pq qp. destruct (classic (eta q <<= p)); [|destruct (classic (eta p <<= q))].
    - right; intros x [|]... left...
    - left; intros x [|]... left...
    - cutrewrite (p = q); [firstorder|]. apply set_ext. intros x. split.
      + intros px. destruct (pq _ px)... exfalso. apply H. intros y eqy.
        now rewrite <- (eta_uniq H1 eqy).
      + intros qx. destruct (qp _ qx)... exfalso. apply H0. intros y epy.
        now rewrite <- (eta_uniq H1 epy).
  Qed.

  Theorem linearity : linears Stage.
  Proof.
    intros p q sp. revert q. induction sp.
    - intros q sq. induction sq as [q sq IHsq|F sF IHF].
      + destruct IHsq. left. left. now auto.
        destruct (IHsp (adj q)). now apply StgA.
        now apply compare_adj. right. left. now auto.
      + now apply compare_union.
    - intros p sp. apply or_comm. apply compare_union. intros q fq.
      apply or_comm. now apply H0.
  Qed.

  Hypothesis eta_greedy : forall p, inhab (complement p) -> inhab (eta p).

  Lemma adj_fix p : adj p <<= p -> (forall x, p x).
  Proof.
    unfold adj. intros H x. apply NNPP. intros npx.
    destruct (@eta_greedy p); firstorder.
  Qed.

  Lemma StgU_full x : Union Stage x.
  Proof. apply adj_fix. apply sub_union. now repeat constructor. Qed.

  Lemma StgT : Stage setT.
  Proof.
    cutrewrite (setT = Union Stage);[now constructor|].
    apply set_ext; firstorder using StgU_full.
  Qed.

  Lemma sandwich p q : p << q -> q <<= adj p -> adj p <<= q.
  Proof.
    intros [p1 p2] p3 x. destruct (classic (p x));[firstorder|].
    intros [|eta_x];[tauto|]. apply NNPP. intros C.
    apply p2. apply set_eq;[intros y qy|tauto].
    destruct (p3 _ qy) as [?|eta_y];[tauto|].
    now rewrite (eta_uniq eta_x eta_y) in C.
  Qed.

  Lemma adj_incl p q : Stage p -> Stage q -> p << q -> adj p <<= q.
  Proof with auto using StgA.
    intros Sp Sq pq. destruct (@linearity (adj p) q)...
    now apply sandwich.
  Qed.

  Lemma tower_least (F : set (set X)) :
    F <<= Stage -> inhab F -> F (Inter F).
  Proof with auto using StgA.
    intros stg_F inh_F. apply Peirce. intros C.
    assert (HF : forall q, F q -> Inter F << q).
    { intros q Fq. split. firstorder. intros H.
      now rewrite (set_ext H) in Fq. }
    pose (p := Union (fun q => Stage q /\ q <<= Inter F)).
    assert (stg_p : Stage p) by (apply StgU; tauto).
    assert (p_IF : p <<= Inter F) by firstorder.
    assert (H1 : forall q, F q -> adj p <<= q).
    { intros q Fq. apply adj_incl... apply HF in Fq. firstorder. }
    assert (H2 : adj p <<= Inter F) by firstorder.
    assert (H3 : adj p <<= p). apply sub_union...
    assert (H4 : F === set1 setT).
    { apply (inter_full inh_F). intros x. apply H2. left. now apply adj_fix. }
    rewrite (inter_eq H4), inter1. now firstorder.
  Qed.

  Theorem tower_wo : wo_on Stage (@incl _).
  Proof.
    split. apply po_incl.
    intros F F1 F2. exists (Inter F). split;[|firstorder].
    now apply tower_least.
  Qed.

  Corollary tower_inter F :
    F <<= Stage -> Stage (Inter F).
  Proof.
    intros stg_F. destruct (classic (inhab F)) as [H|H].
    - now apply stg_F,tower_least.
    - cutrewrite (Inter F = setT) ;[apply StgT|].
      apply set_ext; firstorder.
  Qed.

  Lemma eta_fix p : eta p <<= p -> (forall x, ~ eta p x).
  Proof. firstorder. Qed.

  Lemma etaN_full p : (forall x, ~ eta p x) -> (forall x, p x).
  Proof. intros H x. apply NNPP. firstorder. Qed.

  Lemma eta_ssub_neq p q :
    Stage p -> Stage q -> p << q -> eta p <> eta q.
  Proof with auto.
    intros Sp Sq pq E.
    assert (H : eta q <<= q).
    { rewrite <- E. generalize (adj_incl Sp Sq pq). firstorder. }
    assert (forall x, ~ eta p x).
    { intros x. rewrite E. now apply eta_fix. }
    destruct pq as [pq nE]. apply nE,set_eq...
    intros x _. now apply etaN_full.
  Qed.

  Lemma eta_inj p q :
    Stage p -> Stage q -> eta p = eta q -> p = q.
  Proof with auto.
    intros Sp Sq E. apply set_ext. apply NNPP. intros C.
    destruct (@linearity p q); auto.
    - revert E. apply eta_ssub_neq;firstorder.
    - apply eq_sym in E. revert E. apply eta_ssub_neq;firstorder.
  Qed.

End Tower.

Arguments linearity [X] [eta] eta_ext eta_uniq p q Sp Sq.

Module Hausdorff.
Section Hausdorff.
  Variables (X : ExtChoiceType) (R : X -> X -> Prop).
  Implicit Types (p q : set X) (F : set X -> Prop).

  Definition chain p := forall x y, p x -> p y -> R x y \/ R y x.

  Definition eta p := gamma (fun x => ~ p x /\ chain (setU1 p x)).

  Lemma unique_eta p : unique (eta p).
  Proof. apply gamma_unique. Qed.

  Lemma co_choice_eta p x : eta p x -> ~p x.
  Proof. intros epx. apply gammaP1 in epx. tauto. Qed.

  Local Notation Stage := (Stage eta).

  Lemma linear_Chains : linears Stage.
  Proof. apply linearity; auto using unique_eta, co_choice_eta. Qed.

  Lemma ChainsP : Stage <<= chain.
  Proof.
    intros p. induction 1.
    - unfold eta.
      destruct (gamma0Vx (fun z : X => ~ p z /\ chain (setU1 p z))) as [E|[x [_ px] E]];
      unfold adj.
      + now rewrite E, setU0.
      + now rewrite E.
    - apply chainU; auto. apply (sub_linear H). apply linear_Chains.
  Qed.

  Theorem Hausdorff :
    exists M, chain M /\ (forall x, chain (setU1 M x) -> M x).
  Proof.
    pose (M := Union Stage). exists M. split.
    - apply chainU. apply linear_Chains. apply ChainsP.
    - intros x H1. apply NNPP. intros H2.
      apply (@eta_full_empty _ eta). apply co_choice_eta.
      apply inhab_gamma. exists x. firstorder.
  Qed.

End Hausdorff.
End Hausdorff.
Export Hausdorff.

Module Zermelo.
Section Zermelo.
  Variables (X : ExtChoiceType).
  Implicit Types (x : X) (p q : set X).

  Definition eta p := gamma (fun x => ~ p x).

  Lemma cochoice_eta p x : eta p x -> ~ p x.
  Proof. apply gammaP1. Qed.

  Lemma greedy_eta p : inhab (fun x => ~ p x) -> inhab (eta p).
  Proof. apply inhab_gamma. Qed.

  Lemma unique_eta p : unique (eta p).
  Proof. apply gamma_unique. Qed.

  Local Notation Stage := (Stage eta).
  Local Notation adj := (adj eta).

  Definition bar x := Union (fun p => Stage p /\ ~ p x).

  Lemma stage_bar x : Stage (bar x).
  Proof. constructor. firstorder. Qed.

  Lemma barN x : ~ bar x x.
  Proof. firstorder. Qed.

  Lemma barP x : eta (bar x) = set1 x.
  Proof.
    apply unique_eq1;[apply gamma_unique|].
    apply NNPP. intros H.
    cut (bar x = setT). { intros E. apply (@barN x). now rewrite E. }
    apply set_ext,set_eq;[tauto|intros y _].
    apply (adj_fix cochoice_eta greedy_eta). apply sub_union. split.
    + constructor. constructor. tauto.
    + intros [|]; auto. apply (@barN x).
  Qed.

  Lemma inj_bar : injective bar.
  Proof.
    intros x y E.
    assert (H : eta (bar x) = eta (bar y)). congruence.
    rewrite barP,barP in H. eapply eq_sub in H. now apply H.
  Qed.

  Definition bar_rel x y := bar x <<= bar y.

  Theorem wo_bar_rel : wo_on setT bar_rel.
  Proof.
    change (wo_on setT (fun x y => incl (bar x) (bar y))).
    generalize (tower_wo cochoice_eta unique_eta greedy_eta).
    apply transfer_on;unfold into; auto using inj_bar, stage_bar.
  Qed.

  Lemma bar_sub p x : p x -> Stage p -> bar x <<= p /\ bar x <> p.
  Proof with auto using StgA,stage_bar.
    intros px Sp. split.
    - destruct (linearity cochoice_eta unique_eta (bar x) p)...
      exfalso. apply (@barN x)...
    - intros C. subst. apply (@barN x)...
  Qed.

  Definition Seg R x := fun z => R z x /\ z <> x.

  Lemma bar_seg x : bar x = Seg bar_rel x.
  Proof.
    apply set_ext,set_eq; unfold Seg, bar_rel; intros z.
    - intros xz. destruct (bar_sub xz). apply stage_bar.
      split;[assumption|congruence].
    - intros [zx nzx].
      assert (H : bar z << bar x).
      { intuition. apply set_ext,inj_bar in H. firstorder. }
      eapply (@adj_incl _ _ cochoice_eta unique_eta _ _ _ _ H).
      right. rewrite barP; tauto.
      Grab Existential Variables. apply stage_bar. apply stage_bar.
  Qed.

  Definition agrees R := forall x, gamma (complement (Seg R x)) = set1 x.

  Lemma agrees_bar : agrees bar_rel.
  Proof. intros x. rewrite <- bar_seg. apply barP. Qed.

  Theorem Zermelo : exists2 R, wo_on setT R & agrees R.
  Proof. exists bar_rel. apply wo_bar_rel. apply agrees_bar. Qed.

  Fact bar_suj p : Stage p -> inhab (complement p) -> exists x, p = bar x.
  Proof with auto using stage_bar.
    intros Sp E. destruct (greedy_eta E) as [x rx].
    exists x. apply (eta_inj cochoice_eta unique_eta greedy_eta)...
    rewrite barP. apply unique_eq1... apply unique_eta.
  Qed.

End Zermelo.

Section Extension.
  Variables (X : ExtChoiceType) (R : relation X).

  Definition min p x := p x /\ (forall y, p y -> R y x -> y = x).

  Hypothesis well_founded_R : forall p, inhab p -> inhab (min p).

  Definition gamma' p := gamma (min p).

  Lemma gammaP1' p : gamma' p <<= p.
  Proof. eapply sub_trans. apply gammaP1. firstorder. Qed.

  Lemma gammaP2' p : inhab p -> single (gamma' p).
  Proof. intros H. apply gammaP2. now apply well_founded_R. Qed.

  Definition X' := Build_ExtChoiceType gammaP1' gammaP2'.

  Theorem Extension :
    exists2 R' : relation X, (forall x y, R x y -> R' x y) & wo_on setT R'.
  Proof with auto.
    destruct (@Zermelo X') as [R' woR' agrR']. exists R'...
    intros y x Ryx. apply NNPP. intros C. destruct woR' as (W1 & W2).
    assert (M : @gamma X' (complement (Seg R' x)) <<= min (complement (Seg R' x))).
    { unfold gamma; simpl; unfold gamma'. apply gammaP1. }
    assert (Seg R' y x).
    { unfold lt,Seg. destruct (@ELE_linear _ _ _ W2 x y I I);[|firstorder].
      split... intros E. subst... }
    rewrite agrR' in M. destruct (M _ (eq_refl)) as [_ M2].
    rewrite (M2 y) in H; firstorder.
  Qed.

End Extension.
End Zermelo.
Export Zermelo.