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).

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

  Section DoubleInd.
    Variable (R : X -> X -> Prop).
    Hypothesis step : forall x y, T x -> T y -> R x y -> R y x -> R x (f y).
    Hypothesis limit : forall I (F : I -> X) x, T x ->
      (forall i, T (F i)) -> (forall 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.

  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 ->
    (forall x, P (t x) -> P (f (t x))) ->
    (forall x, P (t x)).
  Proof.
    move=> h1 h2 x. move: (t x) (T_t x) => {x} x. elim=> {x}[x tx ih|I F _]; last first.
    exact: h1. move/t_img: tx => eqn. rewrite -eqn. apply: h2. 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 :
      (forall 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 -> (forall 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 :
      (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_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 /\ forall 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) :=
    forall 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 :
      forall g : X -> X,
        monotone g ->
        (forall x, g (tt x) ≤ tt x -> g (f (tt x)) ≤ f (tt x)) ->
        forall x, g (tt x) ≤ tt x.

    Lemma upto_to_tower_induction (P : Pred X) :
      inf_closed P ->
      (forall x, P x -> P (f x)) ->
      forall x, P (tt x).
    Proof.
      move=> h1 h2 x. apply/(@closure_of_image X P h1). 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 l1. apply/closure_of_image => //. apply: h2. exact/closure_of_image.
    Qed.
  End UptoLemmaCharacterization.
End Tower.