semantics.wp.abstract

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

Section AbstractPredTrans.
Variable T X Y : Type.
Definition ptrans := T -> {mono Pred Y -> Pred X}.

Variable E : {mono ptrans -> ptrans}.

Definition wp := lfp E.
Definition wlp := gfp E.

Lemma wp_to_wlp : wp ≤ wlp.
Proof.
  rewrite/wp. apply direct_induction => //=. exact _. intros. by focus.
  move=> wp ih ->. by rewrite gfpE.
Qed.

Lemma wp_mono s P Q : P ≤ Q -> wp s P ≤ wp s Q.
Proof. by move->. Qed.

Lemma wlp_mono s P Q : P ≤ Q -> wlp s P ≤ wlp s Q.
Proof. by move->. Qed.

Definition distributive (wp : ptrans) :=
  forall s P Q, wp s P ∧ wp s Q ≤ wp s (P ∧ Q).

Lemma wlp_distributive :
  (forall wp, distributive wp -> distributive (E wp)) ->
  distributive wlp.
Proof.
  move=> h. rewrite/wlp. apply: direct_coinduction => /=[I F _ ih|wlp _]; last first.
  exact: h. move=> s P Q. rewrite !prod_allE !mfun_allE. focus=> i.
  rewrite -ih. apply: meet_mono; by cauto.
Qed.

Lemma wp_distributive :
  (forall wp, distributive wp -> distributive (E wp)) ->
  distributive wp.
Proof.
  move=> h. rewrite/wp. apply: direct_induction => /=[I F Fp ih|wp _]; last first.
  exact: h. move=> s P Q. rewrite !prod_exE !mfun_exE. rewrite meetEx. focus=> i.
  rewrite meetxE. focus=> j. case: (Fp i j) => k h1 h2. apply: exI (k) _.
  rewrite -ih. apply: meet_mono. exact: h1. exact: h2.
Qed.

Definition distributes_over (wp wlp : ptrans) :=
  forall s P Q, wp s P ∧ wlp s Q ≤ wp s (P ∧ Q).

Lemma wlp_distributes_over_wp :
  (forall wp wlp, distributes_over wp wlp -> distributes_over (E wp) (E wlp)) ->
  distributes_over wp wlp.
Proof.
  move=> h. rewrite/wp. apply direct_induction => /=. exact _.
  - move=> I F _ ih s P Q. rewrite !prod_exE !mfun_exE meetEx.
    focus=> i. apply: exI (i) _. exact: ih.
  - move=> wp _ /h. by rewrite gfpE.
Qed.

Lemma wp_distributive_over :
  (forall wp wlp, distributes_over wp wlp -> distributes_over (E wp) (E wlp)) ->
  distributive wp.
Proof.
  move=> /wlp_distributes_over_wp h s P Q.
  rewrite -h. apply: meet_mono => //. exact: wp_to_wlp.
Qed.

Lemma wlp_distributes_over :
  (forall wp wlp, distributes_over wp wlp -> distributes_over (E wp) (E wlp)) ->
  distributive wlp.
Proof.
  move=> h. apply: wlp_distributive => wlp. exact: h.
Qed.

Lemma wlp_to_wp s Q :
  (forall wp wlp, distributes_over wp wlp -> distributes_over (E wp) (E wlp)) ->
  wp s Q = (wlp s Q ∧ wp s ⊤).
Proof.
  move=> /wlp_distributes_over_wp h. apply: le_eq.
  - focus. exact: wp_to_wlp. apply: mono. exact: topI.
  - by rewrite meetC h meetTx.
Qed.

Definition continuous (wp : ptrans) :=
  forall I (F : I -> Pred Y) s, I -> directed F -> wp s (sup F) ≤ ∃ i, wp s (F i).

Lemma wp_continuous :
  (forall wp, continuous wp -> continuous (E wp)) ->
  continuous wp.
Proof.
  move=> h. rewrite/wp. apply direct_induction => /=. exact _.
  - move=> I F dF ih J G s j dG. rewrite !prod_exE !mfun_exE. focus=> i.
    rewrite ih //. focus=> j'. apply: exI (j') _. rewrite mfun_exE. exact: exI.
  - move=> wp _. exact: h.
Qed.

Definition deterministic (wp : ptrans) :=
  forall s Q, wp s Q ≤ ∃ y | Q y, wp s (eq y).

Lemma deterministic_sup (wp : ptrans) :
  deterministic wp -> forall I (F : I -> Pred Y) s, wp s (sup F) ≤ ∃ i, wp s (F i).
Proof.
  move=> h I F s. rewrite h. focus=> y. rewrite prod_exE prop_exE => -[i fiy].
  apply: exI (i) _. apply: mono => x eqn. by subst.
Qed.

Lemma deterministic_to_continuous wp :
  deterministic wp -> continuous wp.
Proof.
  move=> /deterministic_sup h I F s _ _. exact: h.
Qed.

Lemma wp_deterministic :
  (forall wp, deterministic wp -> deterministic (E wp)) ->
  deterministic wp.
Proof.
  move=> h. rewrite/wp. apply: direct_induction => /=.
  - move=> I F _ ih s Q. rewrite prod_exE mfun_exE. focus=> i. rewrite ih.
    focus=> y qy. apply: exIc qy _. rewrite mfun_exE. exact: exI.
  - move=> wp _. exact: h.
Qed.

Lemma continuous_directed_meet_sup (I : eqType) (J : Type) (F : I -> J -> ptrans) :
  J ->
  (forall j1 j2 : J, exists j3 : J, forall i, (F i j1 ≤ F i j3) /\ (F i j2 ≤ F i j3)) ->
  forall s : seq I,
    (∀ i | i \in s, ∃ j, F i j) = (∃ j, ∀ i | i \in s, F i j).
Proof.
  move=> j0 dF s. 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 a j) ∧ (∀ i : I | i \in t, ∃ j : J, F i j)).
    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 H. apply: exI (j3) _. focus=> i. rewrite inE => /orP[].
    + move/eqP->. apply: meetEl. by case: (H a).
    + move=> mem. apply: meetEr. apply: allEc (i) mem _. by case: (H i).
Qed.

End AbstractPredTrans.