Require Import Classical.
Require Import Preliminaries CompletePartialOrder.

Set Implicit Arguments.
Unset Strict Implicit.

General Tower Construction

Section GeneralTower.

Let T be an S-complete partial order such that S is closed under subsets together with an increasing function f.

Variable T : CompletePartialOrder.
Variable f : T -> T.
Hypothesis f_ext : forall x, x <= f x.
Hypothesis closed_mono :
forall (p q : T -> Prop), (forall x, p x -> q x) -> Sup q -> Sup p.

One intuition for the tower construction is that we want to construct the transfinite iteration of f

y = f^a(x)

for some ordinal a. However, in type theory we do not have ordinals or transfinite iteration. The inductive type Reach can be thought of as

Reach x y := exists a : Ordinal, y = f^a(x)

Inductive Reach (a : T) : T -> Prop :=
| Reach0 : Reach a a
| Reach1 x : Reach a x -> Reach a (f x)
| ReachJ (p : T -> Prop) :
    Sup p -> (forall x, p x -> Reach a x) -> ex p ->
    Reach a (join p).

Notation "x |> y" := (Reach x y) (at level 70).

Lemma Reach_trans z x y : x |> z -> z |> y -> x |> y.
Proof. intros A B. revert A. induction B; auto using Reach. Qed.

Lemma Reach_le x y : x |> y -> x <= y.
Proof.
  induction 1; eauto using Reach, le_refl, le_trans.
  apply le_join; firstorder.
Qed.

Lemma strong_join (p : T -> Prop) c :
  Sup p -> (forall x, p x -> exists y, x <= y /\ p y /\ c |> y) ->
  ex p -> c |> join p.
Proof.
  intros cm Hp inh_p. assert (cmn : Sup (fun x => p x /\ c |> x)).
    revert cm. apply closed_mono. tauto.
  rewrite (join_eqI _ _ _ cm cmn Hp). constructor; firstorder.
Qed.

The first Lemma here is the type theoretic analog to a = 0 \/ a = b + 1 for all ordinals a. If f^a(x) = y then either a = 0 and x = y, or a = (b + 1) and f^b(f x) = y. We can formulate this as an inversion Lemma on based towers.

Lemma Reach_inv x y :
  x |> y -> x = y \/ f x |> y.
Proof.
  induction 1 as [|y Reach_x_y IH|p cl_p Reach_p IH inh_p].
  - tauto.
  - right. destruct IH; subst; now constructor.
  - destruct (classic (exists2 y, p y & x <> y)) as [[y Hxy]|H2].
    + right. apply strong_join; [assumption|intros z pz|assumption].
      destruct (IH _ pz).
      * subst. exists y. repeat (split;auto); [|firstorder].
        apply Reach_le. now apply Reach_p.
      * exists z. now firstorder.
    + assert (forall y, p y -> x = y).
      { intros. apply NNPP. intros ne. apply H2. now exists y. }
      left. apply le_tsym.
      * apply join_ub; auto. destruct inh_p as [a pa]. now rewrite (H _ pa).
      * apply join_le; auto. intros y py. now rewrite (H _ py).
Qed.

Linearity of General Towers

Lemma Reach_linearity_succ x y :
  x |> y \/ y |> x -> f x |> y \/ y |> f x.
Proof.
  intro H.
  now destruct H; destruct (Reach_inv H); subst; auto using Reach.
Qed.

Lemma Reach_linearity_aux (p q : T -> Prop) :
  Sup p ->
  (forall x, p x -> x |> join q \/ join q |> x) ->
  join p <= join q \/ join q |> join p.
Proof with eauto using Reach_le.
  intros cm ih.
  destruct (classic (exists x, p x /\ join q |> x)) as [[x[px h3]]|h3].
  - right. apply strong_join... intros y py. destruct (ih y py)...
    exists x. intuition. transitivity (join q)...
  - left. apply join_le... intros x px. apply Reach_le.
    destruct (ih x px) as [|h4]... exfalso...
Qed.

Theorem Reach_linearity c x y :
  c |> x -> c |> y -> x |> y \/ y |> x.
Proof.
  intros sx. revert y. induction sx as [|x sx ih1|p r1 h1 ih1 pd1].
  - tauto.
  - intros y h1. apply Reach_linearity_succ. now apply ih1.
  - intros y sy. induction sy as [|y sy ih2|q r2 h2 ih2 pd2].
    + right. now apply ReachJ.
    + apply or_comm. apply Reach_linearity_succ. tauto.
    + destruct (@Reach_linearity_aux p q r1); eauto.
      * intros x px. destruct (ih1 _ px (join q)); eauto using Reach.
      * destruct (@Reach_linearity_aux q p r2); eauto.
        { intros x qx. destruct (ih2 _ qx); tauto. }
        left. cutrewrite (join p = join q). constructor.
        now apply le_tsym.
Qed.

We now have the "Coincidence and Linearity" Theorem from the paper. It consists of the fact Reach_le and the two corollaries below

Corollary linearity c x y :
  c |> x -> c |> y -> x <= y \/ y <= x.
Proof.
  intros sx sy. destruct (Reach_linearity sx sy) ; eauto using Reach_le.
Qed.

Corollary le_Reach c x y :
  c |> x -> c |> y -> x <= y -> x |> y.
Proof.
  intros sx sy h. destruct (Reach_linearity sx sy); auto.
  assert (x = y). apply le_tsym; eauto using Reach_le.
  subst. constructor.
Qed.

Fixed Point Theorem

Lemma fixed_point_reach a b :
  a |> b -> f b <= b -> forall x, a |> x -> x |> b.
Proof with auto using Reach.
  intros sb h. induction 1 as [|x sx ih|p cm A ih B]...
  - destruct (Reach_inv ih); subst... apply (@le_Reach a)...
  - apply (@le_Reach a)... apply join_le...
    intros x px. apply Reach_le...
Qed.

We now have the Fixed Point Theorem from the paper

Theorem fixed_point_greatest c x :
  c |> x -> f x <= x -> forall y, c |> y -> y <= x.
Proof.
  intros cx h y cy. eapply Reach_le,fixed_point_reach; eassumption.
Qed.

Fact join_Reach_greatest c :
  Sup (Reach c) -> forall y, c |> y -> y <= (join (Reach c)).
Proof. intros S y Hy. now apply join_ub. Qed.

Lemma join_Reach_fix c:
  Sup (Reach c) -> f (join (Reach c)) <= join (Reach c).
Proof. intros cR. apply join_ub; eauto using Reach. Qed.

Lemma complete_fixed_point c :
  Sup (Reach c) -> exists2 x, c <= x & f x <= x.
Proof.
  intros ct. exists (join (Reach c)) ; apply join_ub; eauto using Reach.
Qed.

Well-Ordering of General Towers

Variable c : T.

Lemma Reach_sandwich x y : x |> y -> y |> f x -> y = x \/ y = f x.
Proof.
  intros A B. destruct (Reach_inv A). firstorder.
  right. now apply le_tsym; apply Reach_le.
Qed.

Lemma Reach_join x (p : set T) (cl_p : Sup p) :
  c |> x -> p <<= Reach c -> x <= join p -> x <> join p ->
  exists y, p y /\ x <= y.
Proof with auto.
  intros c_x Rp x_p xE. apply NNPP. intros C.
  apply xE. apply le_tsym... apply join_le...
  intros y py. destruct (linearity c_x (Rp _ py))...
  exfalso; firstorder.
Qed.

Inductive wf (x : T) : Prop :=
  wfI : c |> x -> (forall y, c |> y -> y |> x -> y <> x -> wf y) -> wf x.

Lemma wf_inv (x y : T) : c |> y -> y |> x -> wf x -> wf y.
Proof.
  destruct (classic (y = x)); [subst;tauto|].
  intros ? ? []. firstorder.
Qed.

Lemma Reach_wf x : c |> x -> wf x.
Proof with eauto using Reach_le,Reach.
  induction 1.
  - apply wfI... intros y c_y y_c nE.
    exfalso. apply nE,le_tsym...
  - apply wfI... intros y c_y y_fx C. revert IHReach. apply wf_inv...
    destruct (Reach_linearity H c_y) as [x_y|]...
    destruct (Reach_sandwich x_y y_fx);subst... congruence.
  - apply wfI... intros y c_y y_p nE.
    destruct (Reach_join H c_y H0 (Reach_le y_p) nE) as [x [px Ex]].
    generalize (H1 _ px). apply wf_inv... apply (le_Reach c_y)...
Qed.

Lemma Reach_ELE (p : T -> Prop) :
  ex p -> p <<= Reach c -> exists2 x, p x & forall y, p y -> x |> y.
Proof with auto.
  intros [x mx] H. assert (wf x) as wf_x. apply Reach_wf...
  induction wf_x as [x c_x IH1 IH2].
  destruct (classic (exists y, p y /\ y |> x /\ y <> x))
    as [[y (y1 & y2 & y3)]|C].
  - apply (IH2 y)...
  - exists x... intros y py.
    destruct (Reach_linearity c_x (H _ py))...
    destruct (classic (y = x)); subst... exfalso. firstorder.
Qed.

Theorem Reach_wo : wo_on (Reach c) (@le T).
Proof with auto.
  split.
  - repeat split.
    + intros x _. apply le_refl.
    + intros x y z _ _ _. apply le_trans.
    + intros x y _ _. apply le_tsym.
  - intros p Rp inh_p. destruct (Reach_ELE inh_p Rp) as [x x1 x2].
    exists x. firstorder using Reach_le.
Qed.

End GeneralTower.

Instances of the General Tower Construction

Bourbarki-Witt

Section BourbakiWittWo.

Variable (T : CompletePartialOrder).
Implicit Types (x y : T) (p q : T -> Prop).

Variable f : T -> T.
Hypothesis f_ext : forall x, x <= f x.

Hypothesis wo_Sup : forall p, wo_on p (@le T) <-> Sup p.

Lemma wo_Sup_mono p q : (forall x, p x -> q x) -> Sup q -> Sup p.
Proof. intros pq cl_p. now apply wo_Sup,(wo_sub pq),wo_Sup. Qed.

Theorem BourbakiWittWo x :
  exists2 y, x <= y & f y <= y.
Proof.
  apply complete_fixed_point, wo_Sup, Reach_wo; auto.
  eapply wo_Sup_mono.
Qed.

End BourbakiWittWo.

Section BourbakiWitt.

Variable T : CompletePartialOrder.
Implicit Types (x y : T) (p q : T -> Prop).

Variable f : T -> T.
Hypothesis f_ext : forall x, x <= f x.

Hypothesis chain_Sup : forall p, chain (@le T) p <-> Sup p.

Lemma chain_Sup_mono p q : (forall x, p x -> q x) -> Sup q -> Sup p.
Proof.
  intros mn cm. apply chain_Sup. intros x y mx my.
  apply chain_Sup in cm. apply cm; auto.
Qed.

Theorem BourbakiWitt x :
  exists2 y, x <= y & f y <= y.
Proof.
  apply complete_fixed_point. apply chain_Sup. intros y z sxy sxz.
  eapply (linearity f_ext chain_Sup_mono); eassumption.
Qed.

End BourbakiWitt.

General Hausdorff

Based on the general tower construction we obtain a generalized version of Hausdorff's Theorem which allows us to extend any given chain to a maximal chain

This also serves as an Example on how to instantiate the CompletePartialOrder structure.

Section GeneralHausdorff.
  Variables (X : ExtChoiceType) (R : relation X) (c : set X).
  Hypothesis chain_c : chain R c.

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

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

  Definition f p := p :|: eta p.

  Lemma unionP (M : set (set X)) (y : set X) :
    setT M -> ((forall x : set X, M x -> incl x y ) <-> incl (Union M) y).
  Proof. firstorder. Qed.

We take as the complete subset lattice over X as partial order, i.e., we allow all joins.

  Definition T := @Build_CompletePartialOrder
    (set X) setT (@incl _) (@Union _) (@sub_refl _) (@set_eqx _) (@sub_trans _) unionP.

  Lemma f_ext (x:T) : x <= f x.
  Proof. firstorder. Qed.

  Lemma linear_Chains : linears (@Reach T f c).
  Proof.
    intros p q Rp Rq.
    destruct (linearity f_ext (fun p q _ _ => I) Rp Rq); firstorder.
  Qed.

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

  Theorem GeneralHausdorff :
    exists (p : set X ), c <<= p /\ chain R p /\ (forall x : X, chain R (setU1 p x) -> p x ).
  Proof with auto.
    pose (p := join (@Reach T f c)).
    assert (@Reach T f c p).
    { constructor; firstorder. exists c; constructor. }
    exists p; repeat split...
    - apply (@Reach_le T f)... now apply f_ext.
    - now apply ChainsP.
    - intros x H1. apply NNPP. intros C.
      assert (inhab (eta p)) as [y Ey].
      { apply inhab_gamma. exists x; split... }
      assert (Hy : f p y) by firstorder.
      apply (@join_Reach_fix T f c) in Hy;[|firstorder].
      apply co_choice_eta in Ey; firstorder.
  Qed.

End GeneralHausdorff.