# Parameterized Tower Induction

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 7.28: Parameterized Tower Induction principle

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 7.29: Accumulation rule for the companion

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 7.30: Companion coinduction

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

## Definition 7.31: Sound up-to functions

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

## Lemma 7.32: Functions below the companion are sound

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.