Require Import Classical.
Require Import Preliminaries CompletePartialOrder.

Set Implicit Arguments.

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.

Lemma Reach_le x y : x |> y -> x <= y.

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.

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.

Linearity of General Towers

Lemma Reach_linearity_succ x y :
  x |> y \/ y |> x -> f x |> y \/ y |> f x.

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.

Theorem Reach_linearity c x y :
  c |> x -> c |> y -> x |> y \/ y |> x.

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.

Corollary le_Reach c x y :
c |> x -> c |> y -> x <= y -> x |> y.

Fixed Point Theorem

Lemma fixed_point_reach a b :
a |> b -> f b <= b -> forall x, a |> x -> x |> b.

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.

Fact join_Reach_greatest c :
  Sup (Reach c) -> forall y, c |> y -> y <= (join (Reach c)).

Lemma join_Reach_fix c:
  Sup (Reach c) -> f (join (Reach c)) <= join (Reach c).

Lemma complete_fixed_point c :
  Sup (Reach c) -> exists2 x, c <= x & f x <= x.

Well-Ordering of General Towers

Variable c : T.

Lemma Reach_sandwich x y : x |> y -> y |> f x -> y = x \/ y = f x.

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.

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.

Lemma Reach_wf x : c |> x -> wf x.

Lemma Reach_ELE (p : T -> Prop) :
  ex p -> p <<= Reach c -> exists2 x, p x & forall y, p y -> x |> y.

Theorem Reach_wo : wo_on (Reach c) (@le T).

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.

Theorem BourbakiWittWo x :
exists2 y, x <= y & f y <= y.

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.

Theorem BourbakiWitt x :
exists2 y, x <= y & f y <= y.

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.

  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).

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.

  Lemma linear_Chains : linears (@Reach T f c).

  Lemma ChainsP : @Reach T f c <<= chain R.

  Theorem GeneralHausdorff :
    exists (p : set X ), c <<= p /\ chain R p /\ (forall x : X, chain R (setU1 p x) -> p x ).

End GeneralHausdorff.