semantics.wp.prelim

Require Import base ord tower tower.tarski tower.direct_induction.

Section Kleene.
Variable (X : clat) (f : X -> X).
Hypothesis f_mono : monotone f.
Hypothesis f_cont : forall I (F : I -> X), I -> directed F -> f (sup F) ≤ ∃ i, f (F i).

Lemma iter_mono (m n : nat) :
  m <= n -> iter m f ⊥ ≤ iter n f ⊥.
Proof.
  move/leP. elim=>//m' _ -> /=. move: m' {m n}.
  elim=> //=n ih. apply: mono. exact: ih.
Qed.

Lemma kleene_fp :
  lfp f = ∃ n, iter n f ⊥.
Proof.
  apply: le_eq; last first. focus. elim=> //=n ih. rewrite -lfpE.
  apply: mono. exact: ih.

  apply: lfp_above_ind => //. rewrite f_cont.
  - focus=> n. exact: exI (n.+1) _.
  - exact 0.
  - move=> m n. exists (maxn m n); apply: iter_mono. exact: leq_maxl. exact: leq_maxr.
Qed.
End Kleene.

Section ContinuousSup.
Variable (I : eqType) (J : Type) (X : frame) (F : J -> I -> X).
Variable j0 : J.
Hypothesis dF : directed F.

Lemma continuous_directed_meet_sup (s : seq I) :
  (∀ i | i \in s, ∃ j, F j i) = (∃ j, ∀ i | i \in s, F j i).
Proof.
  apply: le_eq; last first. focus=> j i mem. apply: exI (j) _.
  exact: allEc (i) mem le_refl. elim: s => [|a t ih].
  - apply: exI (j0) _. focus=> i. by rewrite in_nil.
  - transitivity ((∃ j, F j a) ∧ (∀ i : I | i \in t, ∃ j : J, F j i)).
    focus. apply: allEc (a) _ le_refl. by rewrite inE eqxx.
    move=> i mem. apply: allEc (i) _ le_refl. by rewrite inE mem orbT.
    rewrite ih. rewrite meetEx. focus=> j1. rewrite meetxE. focus=> j2.
    case: (dF j1 j2) => j3 h1 h2. apply: exI (j3) _. focus=> i. rewrite inE => /orP[].
    + move/eqP->. apply: meetEl. exact: h1.
    + move=> mem. apply: meetEr. apply: allEc (i) mem _. exact: h2.
Qed.
End ContinuousSup.