# semantics.tower.gfp_companion

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

Section GfpCompanion.
Variable (X : clat) (f : X -> X).
Hypothesis f_mono : monotone f.

Definition ν {T : clat} (f : T -> T) : T :=
gfp_below f .

Definition co : X -> X :=
ν (fun (t : X -> X) (x : X) =>
y | x f y, f (t y)).

Lemma coE x :
co x = ( y | x f y, f (co y)).
Proof.
rewrite{1}/co/ν -gfp_belowE // => {x} x y le_x_y.
hnf=>z1. focus=> z2 le_z_fz. apply: allEc (z2) le_z_fz _.
apply: mono. apply: le_x_y.
Qed.

Lemma co_upto g :
(forall x y, x f y -> g x f (g y)) -> g co.
Proof.
move=> g_resp. apply: gfp_below_coind => //.
hnf=>x; focus=> y le_x_fy. exact: g_resp.
Qed.

Lemma co_compatible x :
co (f x) f (co x).
Proof.
rewrite {1}coE. exact: allEc le_refl.
Qed.

Lemma co_greatest_compatible (g : X -> X) :
monotone g -> (forall x, g (f x) f (g x)) -> g co.
Proof.
move=> g_mono g_compat. apply: co_upto=> x y le_x_fy.
rewrite le_x_fy. exact: g_compat.
Qed.

Lemma co_monotone :
mceil co co :> (_ -> _).
Proof.
apply: co_greatest_compatible => y /=.
focus=> x le_x_fy. rewrite {1}coE. apply: allEc (y) le_x_fy _.
apply: mono. exact: exIc (y) _ _.
Qed.

Global Instance co_mono : monotone co.
Proof.
move=> x y le_x_y. move: co_monotone.
rewrite prod_leE =>/(_ y) <-. exact: exIc (x) _ _.
Qed.

Lemma companion_co :
t f = co.
Proof.
apply: le_eq. apply: co_greatest_compatible => x. rewrite t_f.
apply: mono. apply: mono. exact: t_inc.
rewrite t_greatest_compatible. apply: exIc (co) _ le_refl.
split=> //. exact: co_mono. exact: co_compatible.
Qed.
End GfpCompanion.