From Companion Require Import prelim companion.

Definition chain {A : proType} I (F : I -> A) :=
  forall i j, F i <= F j \/ F j <= F i.

Section ClassicalTowers.
  Variables (A : clat) (f : A -> A).
  Hypothesis (fP : monotone f).

  Local Notation T := (T f).
  Local Notation t := (t f).

  Section TowerDoubleInd.
    Variable R : Rel A.
    Hypothesis step : forall x y,
        T x -> T y -> R x y -> R y x -> R y (f x).
    Hypothesis limit : forall I (F : I -> A) x,
        T x -> (forall i, T (F i)) -> (forall i, R x (F i)) -> R x (inf F).

    Lemma T_ind2 x y :
      T x -> T y -> R x y.
    Proof.
      move=> tp tq. elim: tq x tp => {y}[x tx ih y ty|I F tF ih x tx].
      - apply: step => //; last by exact: ih. elim: ty => {y}; eauto.
      - apply: limit => // i. exact: ih.
    Qed.
  End TowerDoubleInd.

  Lemma tower_dec x : T x -> f x <= x.
  Proof. move=> /t_img<-. exact: t_fold. Qed.

  Hypothesis xm : forall P, P \/ ~P.

  Lemma xm_lb I (F : I -> A) x :
    is_lb F x \/ exists i, ~x <= F i.
  Proof.
    case: (xm (exists i, ~x <= F i)) => h. by right. left=> i.
    case: (xm (x <= F i)) => g //. case: h. by exists i.
  Qed.

  Lemma tower_f_linear x y :
    T x -> T y -> x <= y \/ y <= f x.
  Proof.
    move: x y. apply T_ind2 => [x y tx ty ih _|I F x tx tF ih].
    - case: ih => le1. right. exact: mono. by left.
    - case: (xm_lb F x) => [lb|[i neq]].
      + left. exact: infI.
      + case: (ih i) => le //. right. exact: infE le.
  Qed.

  Corollary tower_linear x y :
    T x -> T y -> x <= y \/ y <= x.
  Proof.
    move=> tx ty. case: (tower_f_linear tx ty) => h. by left.
    right. rewrite h. exact: tower_dec.
  Qed.

  Corollary tower_ind_classical (P : Pred A) :
    (forall I (F : I -> A), chain F -> (forall i, P (F i)) -> P (inf F)) ->
    (forall x, P (t x) -> P (f (t x))) ->
    forall x, P (t x).
  Proof.
    move=> h1 h2. suff: forall x, T x -> P x. move=> h x. apply: h. exact: T_t.
    move=> x. elim=> {x}[x /t_img tx ih|I F tF ih]. rewrite -tx. apply: h2.
    by rewrite tx. apply: h1 ih. move=> i j. apply: tower_linear; exact: tF.
  Qed.
End ClassicalTowers.