Require Import prelim companion.

Section ParameterizedCoinduction.
Variables (A : clat) (f : A -> A).
Hypothesis (fP : monotone f).
Local Notation t := (t f).

Lemma param_tower_ind (P : Pred A) (b : A) :
  inf_closed P ->
  (forall x, b <= t x -> P (t x) -> P (f (t x))) ->
  P (t b).
Proof.
  move=> h_inf h_step. suff: forall x, b <= t x -> P (t x). apply. exact: t_inc.
  move=> x. apply tower_ind => {x}[|x ih leq].
  - move=> T F ih h. apply: h_inf => i. apply: ih. rewrite h. exact: infE.
  - have le_b_tx: b <= t x. rewrite leq. exact: t_fold.
    apply: h_step => //. exact: ih.
Qed.

Lemma param_tower_ind_s (P : A -> Prop) (b : A) :
  inf_closed P ->
  (forall x, b <= t x -> P (t x) -> P (f (t x))) ->
  P (f (t b)).
Proof.
  move=> h1 h2. apply: (h2). exact: t_inc. exact: param_tower_ind.
Qed.

Lemma accumulate x y :
  x <= f (t (x \cup y)) <-> x <= f (t y).
Proof.
  split.
  - move=> h1. apply: param_tower_ind_s. exact: inf_closed_le.
    move=> z h2 h3. rewrite h1. apply: mono. apply/closureP. exact: joinE.
  - move=> h. rewrite {1}h. apply: mono. apply: mono. exact: joinIr.
Qed.

Lemma nu_coind_t x :
  x <= f (t x) <-> x <= nu f.
Proof.
  by rewrite -{2}[x]joinxB accumulate -nu_fp nu_t.
Qed.
End ParameterizedCoinduction.