semantics.tower.cocontinuous_tower

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

Definition codirected {X : proType} {I} (F : I -> X) :=
  forall i j, exists2 k, F k ≤ F i & F k ≤ F j.

Definition is_cocontinuous {X : clat} (f : X -> X) :=
  forall I (F : I -> X), I -> codirected F -> (∀ i, f (F i)) ≤ f (∀ i, F i).

Section TowerCompanion.
  Variable (X : clat) (f : X -> X).
  Implicit Types (x y z : X).
  Local Notation T := (T f).

  Hypothesis f_mono : monotone f.
  Hypothesis f_cocontinuous : is_cocontinuous f.

  Lemma allc_sigma I (P : I -> Prop) (F : I -> X) :
    (∀ i | P i, F i) = ∀ (p : { i | P i }), F p.1.
  Proof.
    apply: le_eq; focus. case=> i pi /=. exact: allEc le_refl.
    move=> i pi. exact: allE (exist P i pi) le_refl.
  Qed.

  Lemma f_omega_cocont_strong (P : nat -> Prop) (F : nat -> X) n0 :
    P n0 ->
    (forall m n, n <= m -> F m ≤ F n) ->
    ∀ n | P n, f (F n) ≤ f (∀ n | P n, F n).
  Proof.
    move=> pn0 F_mono.
    rewrite allc_sigma f_cocontinuous -?allc_sigma //. by exists n0.
    move=> -[i pi] [j pj] /=. have H: P (maxn i j). rewrite/maxn. by case: ifP.
    exists (exist P (maxn i j) H) => /=; apply: F_mono.
    exact: leq_maxl. exact: leq_maxr.
  Qed.

  Definition chain n := iter n f ⊤.
  Definition kleene_t x := ∀ n | (x ≤ chain n), chain n.

  Global Instance kleene_t_mono :
    monotone kleene_t.
  Proof.
    move=> x y le_x_y. rewrite/kleene_t. apply: all_mono => n.
    focus=> le_y_cn. apply: allE => //. by rewrite le_x_y.
  Qed.

  Lemma T_iter n :
    T (iter n f ⊤).
  Proof.
    elim: n => [|n ih] /=. exact: T_lim. apply: T_step. exact: ih.
  Qed.

  Lemma T_kleene x :
    T (kleene_t x).
  Proof.
    apply: T_lim => n. apply: T_lim => _. exact: T_iter.
  Qed.

  Lemma chain_dec n :
    f (chain n) ≤ chain n.
  Proof.
    elim: n => //= n ih. apply: mono. exact: ih.
  Qed.

  Lemma kleene_compat x :
    kleene_t (f x) ≤ f (kleene_t x).
  Proof.
    rewrite{2}/kleene_t -(f_omega_cocont_strong (n0 := 0)) //=.
    - focus=> n le_x_cn. apply: allEc n.+1 _ le_refl => /=.
      apply: mono. exact: le_x_cn.
    - move=> m n /leP. elim=> {m} //= m _ ih. by rewrite chain_dec.
  Qed.

  Lemma kleene_t_is_t x :
    kleene_t x = t f x.
  Proof.
    apply: le_eq.
    - rewrite/t. focus=> y [ty ->{x}]. elim: ty => {y}.
      + move=> x _ ih. rewrite kleene_compat. exact: mono.
      + move=> I F _ ih. focus=> i. rewrite -(ih i). apply: mono. exact: allE.
    - apply: allEc le_refl. split. exact: T_kleene. rewrite/kleene_t. by focus.
  Qed.
End TowerCompanion.