Section 6: Parameterized Tower Induction

Require Import prelim companion.

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

Lemma 30

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 31

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.

Corollary 32

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.