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.