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).
  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.

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)).
  move=> h1 h2. apply: (h2). exact: t_inc. exact: parameterized_tower_ind.

Lemma 7.29: Accumulation rule for the companion

Lemma accumulate x y :
  (x f (t (x y))) <-> (x f (t y)).
  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.

Fact 7.30: Companion coinduction

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

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.
  move=> h1 x h2. apply/companion_coind. rewrite {1}h2.
  apply: mono. exact: h1.

End ParameterizedTower.