Require Import base ord tower.tarski tower.associated_closure tower.tower.

Section ParameterizedTower.
Variable (A : clat).
Variable (f : A -> A).
Hypothesis (f_mono : monotone f).
Local Notation t := (t f).

Lemma parameterized_tower_ind (P : Pred A) u :
  inf_closed P ->
  (forall x, u ≤ t x -> P (t x) -> P (f (t x))) ->
  P (t u).
Proof.
  move=> h1 h2. suff: forall x, T f x -> u ≤ x -> P x.
  apply. exact: T_t. exact: t_inc.
  move=> x. elim=> {x}[x /t_img eqn ih h|I F _ ih h].
  rewrite -eqn. apply: h2. rewrite h -{1}eqn. exact: t_fdec. rewrite eqn.
  apply: ih. rewrite h -eqn. exact: t_fdec.
  apply: h1 => i. apply: ih. rewrite h. exact: allE.
Qed.

Lemma parameterized_tower_ind_s (P : Pred A) u :
  inf_closed P ->
  (forall x, u ≤ t x -> P (t x) -> P (f (t x))) ->
  P (f (t u)).
Proof.
  move=> h1 h2. apply: (h2). exact: t_inc. exact: parameterized_tower_ind.
Qed.

Lemma accumulate x y :
  (x ≤ f (t (x ∨ y))) <-> (x ≤ f (t y)).
Proof.
  split=> h; last first.
  - rewrite {1}h. apply: mono. apply: mono. exact: joinIr.
  - apply: parameterized_tower_ind_s. move=> I F ih. by focus.
  - move=> z l1 l2. rewrite h. apply: mono. apply/closureP. by focus.
Qed.

Fact companion_coind x :
  (x ≤ f (t x)) <-> (x ≤ gfp f).
Proof.
  by rewrite -{2}[x]joinxB accumulate t_gfp gfpE.
Qed.

Definition sound_up_to (g : A -> A) :=
  forall x, x ≤ f (g x) -> x ≤ gfp f.

Lemma below_companion_sound (g : A -> A) :
  g ≤ t -> sound_up_to g.
Proof.
  move=> h1 x h2. apply/companion_coind. rewrite {1}h2.
  apply: mono. exact: h1.
Qed.

End ParameterizedTower.