semantics.tower.tower

Require Import base ord tower.tarski tower.associated_closure.

Section Tower.
  Variable (X : clat) (f : X X).
  Implicit Types (x y z : X).

The tower for f

  Inductive T : Pred X :=
  | T_step x : T x T (f x)
  | T_lim I (F : I X) : ( i, T (F i)) T (inf F).

The double induction principle

  Section DoubleInd.
    Variable (R : X X Prop).
    Hypothesis step : x y, T x T y R x y R y x R x (f y).
    Hypothesis limit : I (F : I X) x, T x
      ( i, T (F i)) ( i, R x (F i)) R x (inf F).

    Lemma T_ind2 x y :
      T x T y R x y.
    Proof with eauto.
      move tx ty; elim: ty x tx {y} [x tx ih y ty|]...
      apply: step... elim: ty...
    Qed.

  End DoubleInd.

  Hypothesis f_mono : monotone f.

  Lemma tower_dec x : T x f x x.
  Proof.
    elim {x}[x _|I F _ ih]. exact: mono.
    focus i. rewrite -ih. apply: mono. exact: allE.
  Qed.


The companion for f

  Definition t x := y | T y (x y), y.

  Lemma T_t x : T (t x).
  Proof. apply: T_lim i. by apply: T_lim -[]. Qed.

  Global Instance t_closure : is_closure t.
  Proof.
    split [{y}|le_x_ty]. rewrite/t. by focus y [].
    apply: allEc le_refl. split //. exact: T_t.
  Qed.


  Global Instance t_monotone : monotone t.
  Proof. 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|]; last by exact: T_t.
    apply: closure_stable. exact: allEc le_refl.
  Qed.


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


  Theorem tower_induction (P : X Prop) :
    inf_closed P
    ( x, P (t x) P (f (t x)))
    ( x, P (t x)).
  Proof.
    move x. move: (t x) (T_t x) {x} x. elim {x}[x tx ih|I F _]; last first.
    exact: . move/t_img: tx eqn. rewrite -eqn. apply: . by rewrite eqn.
  Qed.


  Lemma t_gfp :
    t = gfp f.
  Proof.
    apply: le_eq.
    - apply: gfp_below_coind //. rewrite t_f. exact: mono.
    - apply: tower_induction. move I F ih. focus i. exact: ih.
      move x le. rewrite -gfpE. exact: mono.
  Qed.


  Section UptoLemma.
    Variable g : X X.
    Hypothesis g_mono : monotone g.

    Lemma decreasing_is_below_companion :
      ( x, g (t x) t x) g t.
    Proof.
      move dec x. rewrite {1}[x]t_inc. exact: dec.
    Qed.


    Lemma below_companion_to_upto :
      g t ( x, g (t x) t x g (f (t x)) f (t x)).
    Proof. move le_g_t x _. by rewrite le_g_t -t_f. Qed.

    Lemma upto_lemma :
      ( x, g (t x) t x g (f (t x)) f (t x))
       x, g (t x) t x.
    Proof.
      move h x. apply: (tower_induction (P := fun x g x x)) //.
      move I F ih. focus i. rewrite -ih. apply: mono. exact: allE.
    Qed.

  End UptoLemma.

  Lemma t_fdec x :
    f (t x) t x.
  Proof.
    apply: upto_lemma {x} x. exact: mono.
  Qed.


  Definition compatible (g : X X) :=
    monotone g x, g (f x) f (g x).

  Lemma t_compat x :
    t (f x) f (t x).
  Proof.
    rewrite t_f. apply: mono. apply: mono. exact: t_inc.
  Qed.


  Lemma t_greatest_compatible :
    t = g | compatible g, g.
  Proof.
    apply: le_eq.
    - apply: exIc (t) _ le_refl. split[|x]. exact: t_monotone. exact: t_compat.
    - focus g [g_mono g_compat]. hnf x. apply: decreasing_is_below_companion.
      apply: upto_lemma {x} x h. rewrite g_compat. apply: mono. exact: h.
  Qed.


  Definition respectful (g : X X) :=
     x y, x y x f y g x f (g y).

  Lemma t_greatest_respectful :
    t = g | respectful g, g.
  Proof.
    apply: le_eq.
    - apply: exIc (t) _ le_refl x y le_x_y . exact: t_compat.
    - focus g g_resp. have: g mceil g. move x. exact: exIc (x) _ _.
      apply: decreasing_is_below_companion. apply: upto_lemma.
      move y h /=. focus x le_x_fty. rewrite (g_resp x (t y)) //.
      + apply: mono. rewrite -{2}h. exact: exIc (t y) _ _.
      + rewrite le_x_fty. exact: t_fdec.
  Qed.


  Section UptoLemmaCharacterization.
    Variable tt : X X.
    Hypothesis upto :
       g : X X,
        monotone g
        ( x, g (tt x) tt x g (f (tt x)) f (tt x))
         x, g (tt x) tt x.

    Lemma upto_to_tower_induction (P : Pred X) :
      inf_closed P
      ( x, P x P (f x))
       x, P (tt x).
    Proof.
      move x. apply/(@closure_of_image X P ). apply: upto.
      - move {x} x y le_x_y. rewrite/closure_of. focus z [pz le_y_z].
        apply: allEc (z) _ le_refl. split //. by rewrite le_x_y.
      - move {x} x . apply/closure_of_image //. apply: . exact/closure_of_image.
    Qed.

  End UptoLemmaCharacterization.
End Tower.