(** 
* Bourbaki's tower theorem
* Bourbaki-Witt fixed point theorem 
* Zermelo's well-ordering theorem

The proof of Bourbaki's tower theorem (R, BL1, BL2, Bourbaki) follows the original proof in [[Bourbaki 1949]].

See the slides and the paper for ITP 2015 for more information (Transfinite constructions in classical type theory by Gert Smolka, Steven Schäfer, and Christian Doczkal).

Gert Smolka, August 2015 
*)

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

Require Setoid.

Parameter XM : forall P, P \/ ~ P.

Lemma DN P :
  ~ ~ P <-> P.
Proof.
  generalize (XM P). tauto.
Qed.

Notation "'set' X" := (X -> Prop) (at level 70).
Notation "p <<= q" := (forall x, p x -> q x) (at level 70).
Definition inhab X (p : set X) := exists x, p x.

(** Partially ordered types *)

Structure pot :=
  { pot_X :> Type;
    pot_le : pot_X -> pot_X -> Prop;
    pot_refl : forall x, pot_le x x;
    pot_anti : forall x y, pot_le x y -> pot_le y x -> x = y;
    pot_trans : forall x y z, pot_le x y -> pot_le y z -> pot_le x z }.
  
Notation "x <= y" := (pot_le x y).
Notation "x < y" := (x <= y /\ x <> y).

Section POT.
  Variable X : pot.

  Implicit Types x y z u : X.
  Implicit Types p q : set X.

  Definition sup p x := forall z, x <= z <-> forall y, p y -> y <= z.
  Definition min p x := p x /\ ~ exists y, p y /\ y < x.
  Definition chain p := forall x y, p x -> p y -> x <= y \/ y <= x.
  Definition wf p := forall q, q <<= p -> inhab q -> inhab (min q).
  Definition well_order := chain (fun x => True) /\ wf (fun x => True).

  Fact le_lt x y :
    x <= y -> x = y \/ x < y.
  Proof.
    intros A. destruct (XM (x=y)); auto.
  Qed.

  Fact lt_neq x :
    ~ x < x.
  Proof.
    intros [_ A]. auto.
  Qed.

  Fact lt_le x y :
    x < y -> x <= y.
  Proof.
    intuition.
  Qed.

  Fact lt_le' x y z :
    x < y -> y <= z -> x < z.
  Proof.
    intros [A B] C. split.
    - eapply pot_trans; eauto.
    - contradict B. subst z. apply pot_anti; auto.
  Qed.

  Fact lt_not_le x y :
    x < y -> ~ y <= x.
  Proof.
    intros A B. eapply lt_neq, (lt_le' A B).
  Qed.

  Fact chain_not_le p x y :
    chain p -> p x -> p y -> ~ x <= y -> y < x.
  Proof.
    intros A B C. destruct (A _ _ C B) as [D|D].
    - apply le_lt in D as [D|D]; [subst |now auto].
      intros D. exfalso. apply D, pot_refl.
    - tauto.
  Qed.

  Fact sup_le x p u :
    p x -> sup p u -> x <= u.
  Proof.
    intros A B. apply B; auto using pot_refl.
  Qed.

  Fact sup_le' x y p u :
    x <= y -> p y -> sup p u -> x <= u.
  Proof.
    intros A B C. eapply pot_trans. exact A.
    revert B C. apply sup_le.
  Qed.
  
  Fact sup_ex p u x :
    sup p u -> x < u -> exists y, p y /\ ~ y <= x.
  Proof.
    intros A B. apply DN. intros C.
    cut (u <= x). now apply lt_not_le.
    apply A. intros y D. apply DN.
    contradict C. eauto.
  Qed.

  Fact sup_ex' x u p :
    sup p u -> ~ u <= x -> exists y, p y /\ ~ y <= x.
  Proof.
    intros A B.
    apply DN. contradict B.
    apply A. intros y C. apply DN.
    contradict B. exists y. auto.
  Qed.

  Inductive ind p : set X :=
  | indI x : (forall y, p y -> y < x -> ind p y) -> ind p x.

  Lemma ind_iff p x :
    ind p x <-> forall y, p y -> y < x -> ind p y .
  Proof.
    split; intros A.
    - destruct A as [x A]. auto.
    - now constructor.
  Qed.

  Fact ind_wf p :
    p <<= ind p -> wf p.
  Proof.
    intros H q A [x B].
    assert (C := H x (A x B)).
    induction C as [x _ IH].
    destruct (XM (min q x)) as [D|D].
    - exists x. exact D.
    - unfold min in D.
      assert (exists y, q y /\ y < x /\ p y) as [y [E [F G]]].
      { apply DN. contradict D. split. exact B.
        contradict D. destruct D as [y [D E]]. exists y. auto. }
      eauto.
  Qed.

  Fact wf_ind p :
    wf p -> p <<= ind p.
  Proof.
    intros A. apply DN. intros B.
    unfold wf, min in A.
    destruct (A (fun z => p z /\ ~ ind p z)) as [x [[C D] E]].
    - tauto.
    - apply DN. contradict B. intros x C.
      apply DN. contradict B. exists x. auto.
    - apply D. constructor. intros y F G.
      apply DN. contradict E. eauto.
  Qed.

End POT.

(** * Bourbaki's tower theorem *)

Section Bourbaki.
  Variable X : pot.
  Variable a : X.
  Variable f : X -> X.
  Variable f_inc : forall x, x <= f x.

  Implicit Types x y z u : X.
  Implicit Types p q : set X.  

  Inductive T : set X :=
  | Ta : T a
  | Tf x : T x -> T (f x)
  | Tsup p u : p <<= T -> inhab p -> sup p u -> T u.

  Fact f_inc' x y :
    x <= y -> x <= f y.
  Proof.
    intros A. eapply pot_trans. exact A. apply f_inc.
  Qed.

  Fact f_inc'' x y :
    f x <= y -> x <= y.
  Proof.
    intros A. eapply pot_trans; eauto using f_inc.
  Qed.

  Fact T_a_least x :
    T x -> a <= x.
  Proof.
    intros A.
    induction A as [|x _ IH|p u _ IH C D].
    - apply pot_refl.
    - now apply f_inc'.
    - destruct C as [x C]. specialize (IH x C).
      revert IH C D. apply sup_le'.
  Qed.

  Definition R x := T x /\ forall y, T y -> y < x -> f y <= x.

  Lemma BL1 x y :
    T x -> R y -> x <= y \/ f y <= x.
  Proof.
    intros A B.
    induction A as [|x C IH|p u _ IH C D].
    - left. destruct B as [B _]. now apply T_a_least.
    - destruct IH as [IH|IH].
      + apply le_lt in IH as [IH|IH].
        * right. subst y. apply pot_refl.
        * left. apply B; auto.
      + right. now apply f_inc'.
    - destruct (XM (u <= y)) as [E|E].
      + auto.
      + right. destruct (sup_ex' D E) as [z [F G]].
        destruct (IH z F) as [H|H].
        * exfalso. auto.
        * apply (sup_le' H F D).
  Qed.

  Lemma BL2 :
    T <<= R.
  Proof.
    intros x A.
    induction A as [|x A IH|p u A IH B C].
    - split. exact Ta.
      intros y A B. contradiction (lt_not_le B (T_a_least A)).
    - split. now apply Tf.
      intros y B C.
      destruct (BL1 B IH) as [D|D].
      + destruct (XM (y=x)) as [E|E].
        * subst y. apply pot_refl.
        * apply f_inc'. apply IH; auto.
      + contradiction (lt_not_le C D).
    - split. exact (Tsup A B C).
      intros y D E. destruct (sup_ex C E) as [x [F G]].
      assert (F' := IH _ F).
      destruct (BL1 D F') as [H|H].
      + apply pot_trans with (y:=x).
        * apply F'. exact D. split. exact H.
          intros K. subst y. auto.
        * revert C. apply sup_le, F.
      + exfalso. apply G. now apply f_inc''.
  Qed.

  Theorem Bourbaki x y :
    T x -> T y -> x <= y \/ f y <= x.
  Proof.
    auto using BL1, BL2.
  Qed.

  Corollary T_chain :
    chain T.
  Proof.
    intros x y A B.
    destruct (Bourbaki A B) as [C|C].
    + auto.
    + right. now apply f_inc''.
  Qed.

  Corollary T_f_monotone x y :
    T x -> T y -> x <= y -> f x <= f y.
  Proof.
    intros A B C. destruct (Bourbaki B A) as [D|D].
    - cut (x = y).
      { intros E. subst y. apply pot_refl. }
      apply pot_anti; auto.
    - now apply f_inc'.
  Qed.

  Corollary T_f_succ x y :
    T x -> T y -> x < f y -> x <= y.
  Proof.
    intros A B C.
    destruct (Bourbaki A B) as [D|D].
    - exact D.
    - contradiction (lt_not_le C D).
  Qed.

  Corollary T_sup u :
    sup T u -> T u.
  Proof.
    apply Tsup. now auto. exists a. apply Ta.
  Qed.

  Corollary T_sup_FP u :
    sup T u <-> f u = u /\ T u.
  Proof.
    split.
    - intros A. split; [|now apply T_sup].
      apply pot_anti; [|exact (f_inc u)].
      apply (sup_le (Tf (T_sup A)) A). 
    - intros [A B]. intros x. split; [|now auto].
      intros C y D. eapply pot_trans; [|exact C]. clear x C.
      induction D as [|y D IH|p v _ IH E F].
      +  apply T_a_least, B.
      + rewrite <- A. apply T_f_monotone; auto.
      + apply F, IH.
  Qed.

  Lemma T_wf :
    wf T.
  Proof.
    apply ind_wf. intros x A.
    induction A as [|x A IH|p u A IH B C]; constructor; intros y D E.
    - exfalso. apply (lt_not_le E), T_a_least, D.
    - apply (T_f_succ D A) in E.
      apply le_lt in E as [E|E].
      + subst y; auto.
      + rewrite ind_iff in IH. auto.
    - destruct (sup_ex C E) as [z [F G]].
      apply (chain_not_le T_chain (A z F) D) in G.
      specialize (IH z F). rewrite ind_iff in IH. auto.
  Qed.

  Theorem Bourbaki_Witt :
    (forall p, wf p -> chain p -> exists u, sup p u) -> exists u, f u = u /\ a <= u.
  Proof.
    intros A. specialize (A T T_wf T_chain). destruct A as [u A].
    exists u. split. now apply T_sup_FP. now apply T_a_least, T_sup.
  Qed.

End Bourbaki.

Section SetStuff.
  Variable X : Type.
  
  Implicit Types x : X.
  Implicit Types p q r : set X.
  Implicit Types F : set (set X).

  Definition sing x : set X := fun z => z = x.
  Definition comp p : set X := fun z => ~ p z.
  Definition union F : set X := fun x => exists p, F p /\ p x.
  Definition unique p : Prop := forall x y, p x -> p y -> x = y.

  Fact sing_eq  x y :
    sing x y -> x = y.
  Proof.
    unfold sing. auto.
  Qed.

  Fact sing_eq' x y :
    sing x = sing y -> x = y.
  Proof.
    intros A. apply sing_eq. rewrite A. reflexivity.
  Qed.

  Fact union_incl p F :
    F p -> p <<= union F.
  Proof.
    intros A x B. exists p. auto.
  Qed.

  Fact incl_refl p :
    p <<= p.
  Proof.
    firstorder.
  Qed.

  Fact incl_trans p q r :
    p <<= q -> q <<= r -> p <<= r.
  Proof.
    firstorder.
  Qed.
  
End SetStuff.

(** Extensional choice types *)

Structure ect :=
  { ect_X :> Type;
    ect_ext : forall p q : set ect_X, p <<= q -> q <<= p -> p = q;
    gamma : set ect_X -> set ect_X;
    gamma_unique : forall p, unique (gamma p);
    gamma_incl : forall p, gamma p <<= p;
    gamma_inhab : forall p, inhab p -> inhab (gamma p) }.

(** * Zermelo's well-ordering theorem *)

Section Zermelo.
  Variable X : ect.
  
  Definition xset : pot := @Build_pot (set X) (fun p q => p <<= q)
                           (@incl_refl X) (@ect_ext X) (@incl_trans X).
  
  Implicit Types x y z u : X.
  Implicit Types p q r : xset.
  Implicit Types F : set xset.

  Fact sup_union F :
    sup F (union F).
  Proof.
    intros p. split.
    - intros A q B x C. apply A. exists q. auto.
    - intros A x [q [B C]]. apply (A q); auto.
  Qed.

  Fact unique_sing p x :
    unique p -> p x -> p = sing x.
  Proof.
    intros A B. apply ect_ext.
    - intros y C. apply A; auto.
    - unfold sing. congruence.
  Qed.

  Definition eta p : xset := gamma (comp p).
  Definition a : xset := fun x => False.
  Definition f p : xset := fun x => p x \/ eta p x.

  Fact f_inc p :
    p <= f p.
  Proof.
    firstorder.
  Qed.

  Fact T_union F :
    F <<= T a f -> T a f (union F).
  Proof.
    intros A. destruct (XM (inhab F)) as [B|B].
    - apply Tsup with (p := F); auto. apply sup_union.
    - cut (union F = a).
      { intros C; rewrite C. constructor. }
      apply ect_ext.
      + intros x [p [C _]]. exfalso. apply B. now exists p.
      + intros x [].
  Qed.

  Definition seg x : xset := union (fun p => T a f p /\ ~ p x).

  Fact seg_T x :
    T a f (seg x).
  Proof.
    apply T_union. tauto.
  Qed.

  Fact seg_open x :
    ~ seg x x.
  Proof.
    intros [p A]. tauto.
  Qed.

  Fact seg_eta x :
    eta (seg x) x.
  Proof.
    (* This proof is amazingly tricky. *)
    apply DN. intros A.
    assert (f (seg x) <<= seg x) as B.
    { apply union_incl. split.
      - apply Tf, seg_T.
      - contradict A. destruct A as [A|A].
        + contradiction (seg_open A).
        + exact A. }
    assert (inhab (eta (seg x))) as [y C].
    { apply gamma_inhab. exists x. apply seg_open. }
    assert (D := C). apply gamma_incl in D. apply D.
    apply B. right. exact C.
  Qed.

  Fact eta_seg x :
    eta (seg x) = sing x.
  Proof.
    apply unique_sing. now apply gamma_unique. apply seg_eta.
  Qed.
  
  Fact seg_injective x y :
    seg x = seg y -> x = y.
  Proof.
    intros A. apply sing_eq'.
    rewrite <- eta_seg, A. apply eta_seg.
  Qed.

  Definition le x y := seg x <<= seg y.
  Lemma le_refl x : le x x.
  Proof.
    unfold le. apply incl_refl.
  Qed.
  Lemma le_anti x y : le x y -> le y x -> x = y.
  Proof.
    unfold le. intros A B. apply seg_injective. apply ect_ext; auto.
  Qed.
  Lemma le_trans  x y z : le x y -> le y z -> le x z.
  Proof.
    unfold le. apply incl_trans.
  Qed.

  Definition poX : pot := @Build_pot X le le_refl le_anti le_trans.
  
  Theorem Zermelo :
    well_order poX.
  Proof.
    split.
    - intros x y _ _.
      apply (@T_chain xset a f f_inc); apply seg_T.
    - intros q A B.
      pose (Q p := exists x, q x /\ p = seg x).
      destruct (@T_wf xset a f f_inc Q) as [p C].
      + intros p [x [C D]]. subst p. apply seg_T.
      + subst Q. destruct B as [x B]. exists (seg x), x. auto.
      + destruct C as [[x [C D]] E]. subst Q p.
        exists x. split. exact C. contradict E.
        destruct E as [y [E F]].
        exists (seg y). split. now eauto.
        destruct F as [F G].   
        split. exact F.
        contradict G. apply seg_injective, G.
  Qed.

End Zermelo.

Check Zermelo.
Print Assumptions Zermelo.