Section 3: Tower-based Companions

Require Import prelim.

Section Companion.
Variables (A : clat) (f : A -> A).
Hypothesis (fP : monotone f).
Implicit Types (P : Pred A) (g : A -> A) (x y z : A).

Definition 2

Inductive T : Pred A :=
| T_step x : T x -> T (f x)
| T_lim I (F : I -> A) : (forall i, T (F i)) -> T (inf F).

Definition t (x : A) := \inf_(y | T y /\ x <= y) y.

Fact 3

Lemma T_t x : T (t x).
Proof. rewrite/t inf_inf. by apply: T_lim => -[y [ty _]] /=. Qed.

Global Instance t_closure : is_closure t.
Proof.
split=> [<-{y}|]. by apply: infIc => i [].
move=> le_x_ty. apply: infEc le_refl. split=> //. exact: T_t.
Qed.

Global Instance t_monotone : monotone t. exact _. Qed.

Lemma t_inc x : x <= t x.
Proof. exact: closure_inc. Qed.

Lemma t_idem x : t (t x) = t x.
Proof. exact: closure_idem. Qed.

Lemma t_img x : T x <-> t x = x.
Proof.
split=> [tx|<-]. apply: closure_stable. exact: infEc le_refl. exact: T_t.
Qed.

Fact 4

Lemma t_f x : f (t x) = t (f (t x)).
Proof.
apply: le_eq. exact: t_inc. apply: infEc le_refl. split=> //.
apply: T_step. exact: T_t.
Qed.

Definition 5

Definition inf_closed P := forall I (F : I -> A), (forall i, P (F i)) -> P (inf F).

Lemma inf_closed_le x : inf_closed (ord_op x).
Proof. move=> I F h. exact: infI. Qed.

Lemma inf_closed_mono g :
monotone g -> inf_closed (fun x => g x <= x).
Proof.
move=> gP I F h. apply: infI => i. rewrite -h. apply: mono. exact: infE.
Qed.

Theorem 6

Theorem tower_ind P :
inf_closed P ->
(forall x, P (t x) -> P (f (t x))) ->
forall x, P (t x).
Proof.
move=> Hp Hf x. apply: (Hp) => y. apply: (Hp) => -[ty _]. elim: ty => {y}.
- move=> y /t_img <-. exact: Hf.
- move=> I F _. exact: Hp.
Qed.

Lemma 7

Lemma nu_t :
nu f = t bot.
Proof.
apply: le_eq. apply: tower_ind. exact: inf_closed_le. move=> x <-.
exact: nu_postfix. apply: nu_tarski. rewrite t_f. apply: mono. exact: botE.
Qed.

Lemma 8

Section UptoLemma.
Variable g : A -> A.
Hypothesis gP : monotone g.

Lemma upto :
(forall x, g (t x) <= t x -> g (f (t x)) <= f (t x)) ->
(forall x, g (t x) <= t x).
Proof.
move=> h x. apply tower_ind => {x} //. exact: inf_closed_mono.
Qed.

Lemma upto_below :
(forall x, g (t x) <= t x) -> g <= t.
Proof.
move=> h x. by rewrite -h {1}[x]t_inc.
Qed.

Lemma upto_char :
g <= t ->
forall x, g (t x) <= t x -> g (f (t x)) <= f (t x).
Proof.
move=> h1 x h2. by rewrite h1 -t_f.
Qed.
End UptoLemma.

Lemma 9

Lemma t_fold x :
f (t x) <= t x.
Proof.
apply: upto x => x h. exact: mono.
Qed.

Lemma 10

Definition compatible g := monotone g /\ (forall x, g (f x) <= f (g x)).

Lemma compat_below g :
compatible g -> g <= t.
Proof.
move=> [gP gC]. apply: upto_below. apply: upto => x eqn.
rewrite -{2}eqn. exact: gC.
Qed.

Lemma 11

Lemma t_compat :
compatible t.
Proof.
split. exact _. move=> x. by rewrite t_f -[t x]t_inc.
Qed.

Corollary 12

Corollary t_greatest_compatible :
t = \sup_(g | compatible g) g.
Proof.
apply: le_eq.
- move=> x. exact: supIc t_compat le_refl.
- apply: supEc => g gC. exact: compat_below.
Qed.
End Companion.