Require Import base ord wp.states wp.gc tower.tarski tower.direct_induction wp.prelim.

Implicit Types (P Q : Pred state) (x y z : state).
Implicit Types (a : action) (b : guard) (G : gc) (s t : cmd).

Definition gtest G : state -> bool :=
  fun x => has (fun p : guard => p x) (unzip1 G).
Coercion gtest : gc >-> Funclass.

Definition pt := {mono Pred state -> Pred state}.

Program Definition wpG (wp : cmd -> pt) (G : gc) : pt :=
  @mk_mfun [proType of Pred state] [proType of Pred state]
           (fun Q x => forall b s, (b,s) \in G -> b x -> wp s Q x) _.
Next Obligation.
  move: x y H => P Q le_P_Q x h b s mem bx. move: x {h bx mem} (h b s mem bx).
  case: (wp s) => /= f h. exact: h.
Qed.

Definition wpF (wp : cmd -> pt) (s : cmd) : pt.
  refine (@mk_mfun [proType of Pred state] [proType of Pred state]
    (fun Q =>
       match s with
       | Skip => Q
       | Assn a => Q \o a
       | Seq s t => wp s (wp t Q)
       | Case G => fun x => gtest G x /\ wpG wp G Q x
       | Do G => fun x => if gtest G x then wpG wp G (wp (Do G) Q) x else Q x
       end) _).
  move=> P Q le_P_Q. case: s => //.
  - move=> a x. exact: le_P_Q.
  - move=> s t. apply: mono. exact: mono.
  - move=> G x [gx h]. split=> //. move: {gx} h. rewrite -prop_leE.
    move: x. rewrite -prod_leE. exact: mono.
  - move=> G x. case: ifP => // _. move: x. rewrite -prod_leE. apply: mono. exact: mono.
Defined.

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

Fact wp_mono (wp : cmd -> pt) s P Q x :
  P ≤ Q -> wp s P x -> wp s Q x.
Proof.
  move=> le_P_Q. rewrite -prop_leE. move: x. rewrite -prod_leE. exact: mono.
Qed.

Lemma wpG_eqn (wp : cmd -> pt) (G : gc) (Q : Pred state) :
  wpG wp G Q = ∀ p : guard * cmd | p \in G, (guardE p.1 : state -> Prop) → wp p.2 Q.
Proof.
  apply: le_eq.
  - focus=> -[b s] mem. hnf=> x. hnf=> h. rewrite prod_impE prop_impE/=. exact: h.
  - move=> x /=. hnf=> h b s mem bx. move: h. rewrite prod_allE prop_allE.
    move/(_ (b,s)). rewrite/infguard prod_allE prop_allE. move/(_ mem).
    rewrite prod_impE prop_impE /=. exact.
Qed.

Definition Gtest (G : gc) : Pred state := gtest G.
Definition NGtest (G : gc) : Pred state := fun x => ~~gtest G x.

Lemma wp_do_eqn (wp : cmd -> pt) (G : gc) (Q : Pred state) :
  wpF wp (Do G) Q =
  ((Gtest G → wpG wp G (wp (Do G) Q)) ∧ (NGtest G → Q)).
Proof.
  apply: le_eq.
  - focus; hnf=> x/=; rewrite prod_impE prop_impE ?/Gtest ?/NGtest; hnf; by case: ifP.
  - hnf=> x. rewrite prod_meetE !prod_impE prop_meetE !prop_impE /Gtest /NGtest. hnf.
    cbn. case: ifPn => _; intuition; by eauto.
Qed.

Global Instance wpG_mono : monotone wpG.
Proof.
  move=> /= wp wlp wp_wlp G Q x /= h b s mem bx. apply: wp_wlp. exact: h mem bx.
Qed.

Global Instance wpF_mono : monotone wpF.
Proof.
  move=> /= wp wlp wp_wlp s Q; case: s => //=.
  - move=> s t. rewrite (wp_wlp t Q). exact: wp_wlp.
  - move=> G x /= [h1 h2]. split=>//b s mem bx. apply: wp_wlp. exact: h2 mem bx.
  - move=> G x. case: ifP => _ // h b s mem bx.
    apply: wp_mono; last first. apply: wp_wlp. apply: h mem bx.
    exact: wp_wlp.
Qed.

Lemma wp_skip Q : wp Skip Q = Q.
Proof. by rewrite/wp -lfpE. Qed.

Lemma wp_act a Q : wp (Assn a) Q = a \; Q.
Proof. by rewrite/wp -lfpE. Qed.

Lemma wp_seq s t Q : wp (Seq s t) Q = wp s (wp t Q).
Proof. by rewrite{1}/wp -lfpE. Qed.

Lemma wp_case G Q : wp (Case G) Q = (Gtest G ∧ wpG wp G Q).
Proof.
  rewrite{1}/wp -lfpE/=. fext=> x. by rewrite prod_meetE prop_meetE.
Qed.

Definition wp_loop G Q : Pred state -> Pred state :=
  fun P x => if gtest G x then wpG wp G P x else Q x.

Global Instance wp_loop_mono G Q : monotone (wp_loop G Q).
Proof.
  move=> /= P1 P2 P12 x. rewrite/wp_loop. case: ifP => // _.
  move: x. rewrite -prod_leE. exact: mono.
Qed.

Opaque lfp gfp.

Lemma wp_do G Q : wp (Do G) Q = lfp (wp_loop G Q).
Proof.
  apply: le_eq.
  - rewrite/wp. pattern (lfp wpF). apply: direct_induction. move=> I F dF ih.
    rewrite prod_exE mfun_exE. focus=> i. exact: ih.
    move=> pt Cpt ih. hnf=>x /=. rewrite -lfpE {1}/wp_loop. case: ifP => // _.
    move=> h b s mem bx. apply (C_lfp _ Cpt). apply: wp_mono. exact: ih.
    exact: h mem bx.
  - apply direct_induction. exact _. move=> I F dF ih. focus. exact: ih.
    move=> pt _ ih. hnf=> x. rewrite/wp -lfpE /wp_loop/=. case: ifP => //= _.
    hnf=> h b s mem bx. apply: wp_mono. exact: ih. exact: h mem bx.
Qed.

Lemma wlp_skip Q : wlp Skip Q = Q.
Proof. by rewrite/wlp -gfpE. Qed.

Lemma wlp_act a Q : wlp (Assn a) Q = a \; Q.
Proof. by rewrite/wlp -gfpE. Qed.

Lemma wlp_seq s t Q : wlp (Seq s t) Q = wlp s (wlp t Q).
Proof. by rewrite{1}/wlp -gfpE. Qed.

Lemma wlp_case G Q : wlp (Case G) Q = (Gtest G ∧ wpG wlp G Q).
Proof.
  rewrite{1}/wlp -gfpE/=. fext=> x. by rewrite prod_meetE prop_meetE.
Qed.

Definition wlp_loop G Q : Pred state -> Pred state :=
  fun P x => if gtest G x then wpG wlp G P x else Q x.

Global Instance wlp_loop_mono G Q : monotone (wlp_loop G Q).
Proof.
  move=> /= P1 P2 P12 x. rewrite/wlp_loop. case: ifP => // _.
  move: x. rewrite -prod_leE. exact: mono.
Qed.

Lemma wlp_do G Q : wlp (Do G) Q = gfp (wlp_loop G Q).
Proof.
  apply: le_eq.
  - apply direct_coinduction. exact _. move=> I F dF ih. focus. exact: ih.
    move=> pt _ ih. hnf=> x. rewrite/wlp -gfpE /wlp_loop/=. case: ifP => //= _.
    hnf=> h b s mem bx. apply: wp_mono. exact: ih. exact: h mem bx.
  - rewrite/wlp. pattern (gfp wpF). apply: direct_coinduction. move=> I F dF ih.
    rewrite prod_allE mfun_allE. focus=> i. exact: ih.
    move=> pt Tpt ih. hnf=>x /=. rewrite -gfpE {1}/wlp_loop. case: ifP => // _.
    move=> h b s mem bx. apply (T_gfp _ Tpt). apply: wp_mono. exact: ih.
    exact: h mem bx.
Qed.

Inductive wps (Q : Pred state) : cmd -> Pred state :=
| wps_skip x : Q x -> wps Q Skip x
| wps_act a x : Q (a x) -> wps Q (Assn a) x
| wps_seq (P : Pred state) s t x :
    wps P s x ->
    (forall y, P y -> wps Q t y) ->
    wps Q (Seq s t) x
| wps_case G x :
    gtest G x ->
    (forall b s, (b,s) \in G -> b x -> wps Q s x) ->
    wps Q (Case G) x
| wps_do_true (P : Pred state) G x :
    wps P (Case G) x ->
    (forall y, P y -> wps Q (Do G) y) ->
    wps Q (Do G) x
| wps_do_false G x :
    ~~gtest G x ->
    Q x ->
    wps Q (Do G) x.

Lemma wps_to_wp Q s x :
  wps Q s x -> wp s Q x.
Proof.
  elim=> {Q s x}.
  - move=> Q x qx. by rewrite wp_skip.
  - move=> Q a x qax. by rewrite wp_act.
  - move=> Q P s t x _ ih1 _ ih2. rewrite wp_seq. exact: wp_mono ih2 ih1.
  - move=> Q G x gx _ ih. by rewrite wp_case prod_meetE prop_meetE.
  - move=> Q P G x _ ih1 _ ih2. move: ih1. rewrite wp_case prod_meetE prop_meetE.
    case=> Gx ih1. rewrite/wp -lfpE/=. rewrite ifT // => b s mem bx.
    apply: wp_mono ih2 _. cbn in ih1. exact: ih1 mem bx.
  - move=> Q G x ng qx. by rewrite wp_do -lfpE {1}/wp_loop ifN.
Qed.

Lemma wp_to_wps s :
  forall Q, wp s Q ≤ wps Q s.
Proof with cbv; eauto using @wps.
  elim: s.
  - move=> Q. rewrite wp_skip...
  - move=> a Q. rewrite wp_act...
  - move=> s t ih1 ih2 Q. rewrite wp_seq; hnf=> x; hnf=> h.
    apply: (wps_seq (P := wp t Q)). exact: ih1. move=> y h'. exact: ih2.
  - move=> G ih Q; hnf=> x; hnf. rewrite wp_case prod_meetE prop_meetE => -[gx h].
    apply: wps_case => // b s mem bx. apply: ih. exact: mem. apply: h mem bx.
  - move=> G ih Q. rewrite wp_do. apply: lfp_above_ind => //.
    hnf=> x; rewrite/wp_loop. case: ifPn => gx; hnf=> h.
    + apply: (wps_do_true (P := wps Q (Do G))) => //.
      apply: wps_case => // b d mem bx. apply: ih. exact: mem. exact: h mem bx.
    + exact: wps_do_false.
Qed.

Lemma wp_wps_equiv Q s :
  wp s Q = wps Q s.
Proof.
  apply: le_eq. exact: wp_to_wps. exact: wps_to_wp.
Qed.

Inductive wlps (Q : Pred state) : cmd -> Pred state :=
| wlps_skip x : Q x -> wlps Q Skip x
| wlps_act a x : Q (a x) -> wlps Q (Assn a) x
| wlps_seq (P : Pred state) s t x :
    wlps P s x ->
    (forall y, P y -> wlps Q t y) ->
    wlps Q (Seq s t) x
| wlps_case G x :
    gtest G x ->
    (forall b s, (b,s) \in G -> b x -> wlps Q s x) ->
    wlps Q (Case G) x
| wlps_do (I : Pred state) G x :
    I x ->
    (forall y, I y -> gtest G y -> wlps I (Case G) y) ->
    (forall y, I y -> ~~gtest G y -> Q y) ->
    wlps Q (Do G) x.

Lemma wlps_to_wlp Q s x :
  wlps Q s x -> wlp s Q x.
Proof.
  elim=> {Q s x}.
  - move=> Q x qx. by rewrite wlp_skip.
  - move=> Q a x qax. by rewrite wlp_act.
  - move=> Q P s t x _ ih1 _ ih2. rewrite wlp_seq. exact: wp_mono ih2 ih1.
  - move=> Q G x gx _ ih. by rewrite wlp_case prod_meetE prop_meetE.
  - move=> Q I G x ix _ ih1 ih2. rewrite wlp_do gfp_def prod_exE prop_exE. exists I.
    rewrite/supguard prod_exE prop_exE. eexists=>//. hnf=> y; hnf=> iy.
    rewrite/wlp_loop. case: ifPn; last by exact: ih2.
    move=> gy b s mem b_y. move: (ih1 y iy gy). rewrite wlp_case prod_meetE prop_meetE.
    case=> _. apply; by eauto.
Qed.

Lemma wlp_to_wlps s :
  forall Q, wlp s Q ≤ wlps Q s.
Proof with cbv; eauto using @wlps.
  elim: s.
  - move=> Q. rewrite wlp_skip...
  - move=> a Q. rewrite wlp_act...
  - move=> s t ih1 ih2 Q. rewrite wlp_seq; hnf=> x; hnf=> h.
    apply: (wlps_seq (P := wlp t Q)). exact: ih1. move=> y h'. exact: ih2.
  - move=> G ih Q; hnf=> x; hnf. rewrite wlp_case prod_meetE prop_meetE => -[gx h].
    apply: wlps_case => // b s mem bx. apply: ih. exact: mem. apply: h mem bx.
  - move=> G ih1 Q. rewrite wlp_do gfp_def. focus=> /=I ih2.
    hnf=> x; hnf=> ix. apply: wlps_do ix _ _ => y iy gy.
    + move: (ih2 y iy). rewrite/wlp_loop ifT // => h. apply: wlps_case => //.
      move=> b s mem b_y. apply: ih1. exact: mem. exact: h mem b_y.
    + move: (ih2 y iy). by rewrite/wlp_loop ifN.
Qed.

Lemma wlp_wlps_equiv Q s :
  wlp s Q = wlps Q s.
Proof.
  apply: le_eq. exact: wlp_to_wlps. exact: wlps_to_wlp.
Qed.

Section HoareRules.

Definition triple P s Q :=
  forall x, P x -> wlps Q s x.

Definition tripleG P G Q :=
  forall b s, (b,s) \in G -> triple (P ∧ guardE b) s Q.

Lemma hoare_skip Q : triple Q Skip Q.
Proof. exact: wlps_skip. Qed.

Lemma hoare_act Q a : triple (a \; Q) (Assn a) Q.
Proof. exact: wlps_act. Qed.

Lemma hoare_seq P Q R s t :
  triple P s Q -> triple Q t R -> triple P (Seq s t) R.
Proof.
  move=> h1 h2 x px. exact: wlps_seq (h1 x px) h2.
Qed.

Lemma hoare_case P Q G :
  P ≤ Gtest G -> tripleG P G Q -> triple P (Case G) Q.
Proof.
  move=> h1 h2 x px. apply: wlps_case. exact: h1.
  move=> b s mem bx. apply: h2 mem _ _.
  by rewrite prod_meetE prop_meetE.
Qed.

Lemma hoare_do I G :
  tripleG (I ∧ Gtest G) G I -> triple I (Do G) (I ∧ NGtest G).
Proof.
  move=> h x ix. apply: wlps_do ix _ _.
  - move=> y iy gy. apply: wlps_case => //b s mem bx.
    apply: h mem _ _. by rewrite !prod_meetE !prop_meetE.
  - move=> y iy gy. by rewrite prod_meetE prop_meetE.
Qed.

End HoareRules.

Definition wp_distributive (wlp wp : cmd -> pt) :=
  forall s P Q, wp s P ∧ wlp s Q ≤ wp s (P ∧ Q).

Lemma inf_closed_wp_distributive wlp : inf_closed (wp_distributive wlp).
Proof.
  move=> I F ih s P Q. hnf=> x. rewrite prod_meetE prop_meetE.
  hnf. case. rewrite !prod_allE !mfun_allE !prod_allE !prop_allE => h1.
  move=> h2 i. apply: (ih i). rewrite prod_meetE prop_meetE. by split.
Qed.

Lemma sup_closed_wp_distributive wlp : sup_closed (wp_distributive wlp).
Proof.
  move=> I F ih s P Q. rewrite prod_exE mfun_exE meetEx.
  focus=> i. rewrite mfun_exE. apply: exI (i) _. exact: ih.
Qed.

Lemma wpF_distributive wlp wp :
  wp_distributive wlp wp -> wp_distributive (wpF wlp) (wpF wp).
Proof.
  move=> ih. case.
  - by move=> P Q /=.
  - move=> a P Q /=. hnf=> x /=. by rewrite !prod_meetE.
  - move=> s t P Q /=. rewrite ih. apply: mono. exact: ih.
  - move=> G P Q /=. hnf=> x /=. rewrite prod_meetE prop_meetE.
    hnf; case=> -[gx h1] [_ h2]. split=> // b s memG bx.
    apply: ih. rewrite prod_meetE prop_meetE. split.
    exact: h1 bx. exact: h2 bx.
  - move=> G P Q /=. hnf=> x /=. rewrite prod_meetE. case: ifP => _; last first.
      by rewrite prod_meetE. rewrite prop_meetE. hnf; case=> h1 h2 b s mem bx.
    apply: wp_mono. apply: ih. apply: ih. rewrite prod_meetE prop_meetE.
    split. exact: h1 bx. exact: h2 bx.
Qed.

Corollary wlp_distributes_over_wp :
  wp_distributive wlp wp.
Proof.
  rewrite/wp. apply direct_induction. exact _.
  move=> /= I F _ ih. apply: sup_closed_wp_distributive. exact: ih.
  move=> /=wp _. rewrite {2}/wlp-gfpE. exact: wpF_distributive.
Qed.

Corollary wp_is_distributive :
  wp_distributive wp wp.
Proof.
  rewrite{2}/wp. apply direct_induction. exact _.
  move=> /= I F _ ih. apply: sup_closed_wp_distributive. exact: ih.
  move=> /=pt _. rewrite {2}/wp-lfpE. exact: wpF_distributive.
Qed.

Corollary wlp_is_distributive :
  wp_distributive wlp wlp.
Proof.
  rewrite{2}/wlp. apply direct_coinduction. exact _.
  move=> /= I F _ ih. apply: inf_closed_wp_distributive. exact: ih.
  move=> /=pt _. rewrite {2}/wlp-gfpE. exact: wpF_distributive.
Qed.

Definition continuous {X} (wp : X -> pt) :=
  forall I (F : I -> Pred state), I ->
    directed F -> forall u, wp u (sup F) ≤ ∃ i, wp u (F i).

Lemma wp_wpG_continuous wp :
  continuous wp -> continuous (wpG wp).
Proof.
  move=> wp_cont I F i0 dF G x h.
  have: ∀ p | p \in filter (fun p : guard*cmd => guardE p.1 x) G, ∃ i, wp p.2 (F i) x.
  {
    move=> /=[b s]. rewrite mem_filter => /andP[/=bx mem].
    case/(_ _)/Wrap: (wp_cont I F i0 dF s x). exact: h mem bx.
    rewrite prod_exE. exact.
  }
  rewrite continuous_directed_meet_sup //=.
  rewrite !prod_exE !prop_exE. case=> i h'.
  exists i. move=> b s mem bx. move: (h' (b,s)).
  rewrite/infguard prop_allE mem_filter/=. apply. exact/andP.
  move=> i j. case: (dF i j) => k h1 h2. exists k; hnf=> p; exact: wp_mono.
Qed.

Lemma wp_continuous :
  continuous wp.
Proof.
  rewrite/wp. apply direct_induction. exact _.
  - move=> I /= F _ ih J G j0 dG s. rewrite prod_exE mfun_exE. focus=> i.
    rewrite ih //. focus=> j. apply: exI (j) _. rewrite mfun_exE.
    exact: exI (i) le_refl.
  - move=> /=wp _ wp_cont I F i0 dF s. case: s I i0 F dF => //.
    + move=> a I i0 F dF. hnf=> x /=. by rewrite !prod_exE /=.
    + move=> s t I i0 F dF /=. rewrite !wp_cont //.
      move=> i j. case: (dF i j) => k h1 h2. exists k; exact: mono.
    + move=> G I i0 F dF x. case=> gx h. move: (@wp_wpG_continuous wp wp_cont I F i0 dF G x h).
      rewrite !prod_exE !prop_exE. case=> i h'. by exists i.
    + move=> G I i0 F dF /= x. rewrite !prod_exE !prop_exE. case: ifP => // gx.
      move=> h. case/(_ _)/Wrap: (@wp_wpG_continuous wp wp_cont I (fun i => wp (Do G) (F i)) i0 _ G x).
      move=> i j. case: (dF i j) => k h1 h2. exists k; exact: mono.
      rewrite !prod_exE prop_exE prop_leE. case.
      * move=> b s mem bx. move: {h gx bx} (h b s mem bx).
        rewrite -prop_leE. move: x. rewrite -prod_leE. apply: mono. exact: wp_cont.
        move=> i h'. exists i => b s mem bx. exact: h' mem bx.
Qed.