Require Import prelim.

Section Companion.
Variables (A : clat) (f : A -> A).
Hypothesis (fP : monotone f).
Implicit Types (P : Pred A) (g : A -> A) (x y z : A).

Inductive T : Pred A :=
| T_step x : T x -> T (f x)
| T_lim I (F : I -> A) : (forall i, T (F i)) -> T (inf F).

Definition t (x : A) := \inf_(y | T y /\ x <= y) y.

Lemma T_t x : T (t x).
Proof. rewrite/t inf_inf. by apply: T_lim => -[y [ty _]] /=. Qed.

Global Instance t_closure : is_closure t.
Proof.
  split=> [<-{y}|]. by apply: infIc => i [].
  move=> le_x_ty. apply: infEc le_refl. split=> //. exact: T_t.
Qed.

Global Instance t_monotone : monotone t. exact _. Qed.

Lemma t_inc x : x <= t x.
Proof. exact: closure_inc. Qed.

Lemma t_idem x : t (t x) = t x.
Proof. exact: closure_idem. Qed.

Lemma t_img x : T x <-> t x = x.
Proof.
  split=> [tx|<-]. apply: closure_stable. exact: infEc le_refl. exact: T_t.
Qed.

Lemma t_f x : f (t x) = t (f (t x)).
Proof.
  apply: le_eq. exact: t_inc. apply: infEc le_refl. split=> //.
  apply: T_step. exact: T_t.
Qed.

Definition inf_closed P := forall I (F : I -> A), (forall i, P (F i)) -> P (inf F).

Lemma inf_closed_le x : inf_closed (ord_op x).
Proof. move=> I F h. exact: infI. Qed.

Lemma inf_closed_mono g :
  monotone g -> inf_closed (fun x => g x <= x).
Proof.
  move=> gP I F h. apply: infI => i. rewrite -h. apply: mono. exact: infE.
Qed.

Theorem tower_ind P :
  inf_closed P ->
  (forall x, P (t x) -> P (f (t x))) ->
  forall x, P (t x).
Proof.
  move=> Hp Hf x. apply: (Hp) => y. apply: (Hp) => -[ty _]. elim: ty => {y}.
  - move=> y /t_img <-. exact: Hf.
  - move=> I F _. exact: Hp.
Qed.

Lemma nu_t :
  nu f = t bot.
Proof.
  apply: le_eq. apply: tower_ind. exact: inf_closed_le. move=> x <-.
  exact: nu_postfix. apply: nu_tarski. rewrite t_f. apply: mono. exact: botE.
Qed.

Section UptoLemma.
  Variable g : A -> A.
  Hypothesis gP : monotone g.

  Lemma upto :
    (forall x, g (t x) <= t x -> g (f (t x)) <= f (t x)) ->
    (forall x, g (t x) <= t x).
  Proof.
    move=> h x. apply tower_ind => {x} //. exact: inf_closed_mono.
  Qed.

  Lemma upto_below :
    (forall x, g (t x) <= t x) -> g <= t.
  Proof.
    move=> h x. by rewrite -h {1}[x]t_inc.
  Qed.

  Lemma upto_char :
    g <= t ->
    forall x, g (t x) <= t x -> g (f (t x)) <= f (t x).
  Proof.
    move=> h1 x h2. by rewrite h1 -t_f.
  Qed.
End UptoLemma.

Lemma t_fold x :
  f (t x) <= t x.
Proof.
  apply: upto x => x h. exact: mono.
Qed.

Definition compatible g := monotone g /\ (forall x, g (f x) <= f (g x)).

Lemma compat_below g :
  compatible g -> g <= t.
Proof.
  move=> [gP gC]. apply: upto_below. apply: upto => x eqn.
  rewrite -{2}eqn. exact: gC.
Qed.

Lemma t_compat :
  compatible t.
Proof.
  split. exact _. move=> x. by rewrite t_f -[t x]t_inc.
Qed.

Corollary t_greatest_compatible :
  t = \sup_(g | compatible g) g.
Proof.
  apply: le_eq.
  - move=> x. exact: supIc t_compat le_refl.
  - apply: supEc => g gC. exact: compat_below.
Qed.
End Companion.