Require Import prelim companion.

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

Let B := Eval hnf in reverse_clat A.

Definition mu := \inf_(x | f x <= x) x.

Lemma mu_tarski x : f x <= x -> mu <= x.
Proof. exact: (@nu_tarski B). Qed.

Lemma mu_fp : f mu = mu.
Proof. exact: (@nu_fp B). Qed.

End TarskiMu.

Definition sup_closed {X : clat} (P : Pred X) :=
  forall T (F : T -> X), (forall i, P (F i)) -> P (sup F).

Section TowerMu.
Variable (A : clat) (f : A -> A).
Implicit Types (x y z : A).
Context {fP : monotone f}.
Let B := Eval hnf in reverse_clat A.

Definition l (x : A) : A := @t B f x.

Global Instance l_kernel : is_kernel l.
Proof. move=>??; exact: (@t_closure B). Qed.

Global Instance l_monotone : monotone l. exact _. Qed.

Lemma l_dec x : l x <= x. exact: (@t_inc B). Qed.
Lemma l_idem x : l (l x) = l x. exact: (@t_idem B). Qed.

Lemma l_f x : f (l x) = l (f (l x)). exact: (@t_f B). Qed.

Lemma ind (P : Pred A) :
  sup_closed P ->
  (forall x, P (l x) -> P (f (l x))) ->
  forall x, P (l x).
Proof. exact: (@tower_ind B). Qed.

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

  Lemma ind_upto :
    (forall x, l x <= g (l x) -> f (l x) <= g (f (l x))) ->
    (forall x, l x <= g (l x)).
  Proof. exact: (@upto B). Qed.

  Lemma ind_upto_above :
    (forall x, l x <= g (l x)) -> l <= g.
  Proof. exact: (@upto_below B). Qed.

  Lemma ind_upto_char :
    l <= g ->
    forall x, l x <= g (l x) -> f (l x) <= g (f (l x)).
  Proof. exact: (@upto_char B). Qed.
End UptoLemma.

Lemma mu_l : mu f = l top.
Proof. exact: (@nu_t B). Qed.

Lemma l_unfold x : l x <= f (l x).
Proof. exact: (@t_fold B). Qed.

End TowerMu.