semantics.wp.icsemantics

Require Import base ars ord wp.states wp.ic tower.tarski tower.direct_induction wp.prelim data.fintype.

Implicit Types (P : Pred state) (x y z : state).
Implicit Types (a : action) (b : guard).

Definition conf n := (tm n * state)%type.
Inductive step {n} : conf n -> conf n -> Prop :=
| step_act a s x :
    step (Act a s, x) (s, a x)
| step_def s t x:
    step (Def s t, x) (inst (Def s s .: Jump) t, x)
| step_if_true b s t x :
    b x ->
    step (If b s t, x) (s, x)
| step_if_false b s t x :
    ~~b x ->
    step (If b s t, x) (t, x).
Notation mstep := (star step).

Definition ptn n := {mono (fin n -> Pred state) -> Pred state}.

Fact wpn_mono n (wp : tm n -> ptn n) (P Q : fin n -> Pred state) s 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.

Definition wpI (wp : iprod (fun n => tm n -> ptn n)) {n} (s : tm n) : ptn n.
  refine (@mk_mfun [proType of fin n -> Pred state] [proType of Pred state]
    (fun Q =>
       match s with
       | Act a s => a >> wp n s Q
       | If b s t => fun x => if b x then wp n s Q x else wp n t Q x
       | Def s t => wp n.+1 t (wp n (Def s s) Q .: Q)
       | Jump f => Q f
       end) _).
  move=> /=P Q le_P_Q. case: s => //=[a s x|b s t x|s t]/=.
  exact: wpn_mono. case: ifP => _; exact: wpn_mono.
  apply: mono. move=> /=[]//=. exact: mono.
Defined.

Global Instance wpI_mono :
  monotone (wpI : iprod (fun n => tm n -> ptn n) -> iprod (fun n => tm n -> ptn n)).
Proof.
  move=> wp wlp wp_wlp n -[a s|b s t|s t|f] Q x//=.
  exact: wp_wlp. case: ifP => _; exact: wp_wlp.
  move=> h. apply: wpn_mono; last first. apply: wp_wlp. exact: h.
  move=>/=. case=>//=. exact: wp_wlp.
Qed.

Definition wpi {n} (s : tm n) : ptn n := lfp wpI n s.
Definition wlpi {n} (s : tm n) : ptn n := gfp wpI n s.

Opaque lfp gfp.

Lemma wpi_act n a (s : tm n) Q : wpi (Act a s) Q = a >> wpi s Q.
Proof. by rewrite{1}/wpi -lfpE. Qed.

Lemma wpi_jump n (f : fin n) Q : wpi (Jump f) Q = Q f.
Proof. by rewrite{1}/wpi -lfpE. Qed.

Lemma wpi_if n b (s t : tm n) Q :
  wpi (If b s t) Q = fun x => if b x then wpi s Q x else wpi t Q x.
Proof.
  by rewrite{1}/wpi-lfpE.
Qed.

Lemma wpi_def_lfp n (s : tm n.+1) Q :
  wpi (Def s s) Q = lfp (fun P => wpi s (P .: Q)).
Proof.
  apply: le_eq.
  - rewrite{1}/wpi. pattern (lfp wpI). apply: direct_induction.
    + move=> I F _ ih. rewrite iprod_exE prod_exE mfun_exE. focus=>i. exact: ih.
    + move=> /= wp /C_lfp wp_wpi ih. rewrite-lfpE. hnf=> x; hnf=> h.
      apply: wp_wpi. apply: wpn_mono h. by case. move=> /= P P' le_P_P'. apply: mono. by case.
  - apply: lfp_above_ind => //. by rewrite{3}/wpi-lfpE.
Qed.

Lemma wpi_def n (s t : tm n.+1) Q :
  wpi (Def s t) Q = wpi t (lfp (fun P => wpi s (P .: Q)) .: Q).
Proof. by rewrite{1}/wpi-lfpE/= wpi_def_lfp. Qed.

Lemma wlpi_act n a (s : tm n) Q : wlpi (Act a s) Q = a >> wlpi s Q.
Proof. by rewrite{1}/wlpi -gfpE. Qed.

Lemma wlpi_jump n (f : fin n) Q : wlpi (Jump f) Q = Q f.
Proof. by rewrite{1}/wlpi -gfpE. Qed.

Lemma wlpi_if n b (s t : tm n) Q :
  wlpi (If b s t) Q = fun x => if b x then wlpi s Q x else wlpi t Q x.
Proof.
  by rewrite{1}/wlpi-gfpE.
Qed.

Lemma wlpi_def_gfp n (s : tm n.+1) Q :
  wlpi (Def s s) Q = gfp (fun P => wlpi s (P .: Q)).
Proof.
  apply: le_eq.
  - apply: gfp_below_coind => //. by rewrite{1}/wlpi-gfpE.
  - rewrite{2}/wlpi. pattern (gfp wpI). apply: direct_coinduction.
    + move=> I F _ ih. rewrite iprod_allE prod_allE mfun_allE. focus=>i. exact: ih.
    + move=> /= wlp /T_gfp wlp_wlpi ih. rewrite-gfpE. hnf=> x; hnf=> h.
      apply: wlp_wlpi. apply: wpn_mono; last first. apply h. by case.
      move=> /= P P' le_P_P'. apply: mono. by case.
Qed.

Lemma wlpi_def n (s t : tm n.+1) Q :
  wlpi (Def s t) Q = wlpi t (gfp (fun P => wlpi s (P .: Q)) .: Q).
Proof. by rewrite{1}/wlpi-gfpE/= wlpi_def_gfp. Qed.

Definition ren_compat (wp : forall n, tm n -> ptn n) :=
  forall m n (ξ : ren m n) (s : tm m) Q,
    wp n (rinst ξ s) Q = wp m s (ξ >> Q).

Lemma wpI_ren_compat wp :
  ren_compat wp -> ren_compat (@wpI wp).
Proof.
  move=> ih m n ξ -[a s|b s t|s t|f] Q /=.
    by rewrite ih. fext=> x. by rewrite !ih.
    rewrite ih-(@ih m n ξ)//=. by fsimpl. by [].
Qed.

Lemma wpi_ren : ren_compat (@wpi).
Proof.
  rewrite/wpi. pattern (lfp wpI). apply: direct_induction.
  - move=> /=I F _ ih m n ξ s Q. rewrite !iprod_exE !mfun_exE.
    f_equal; fext=> i x. by rewrite ih.
  - move=> /=wp _. exact: wpI_ren_compat.
Qed.

Lemma wlpi_ren : ren_compat (@wlpi).
Proof.
  rewrite/wlpi. pattern (gfp wpI). apply: direct_coinduction.
  - move=> /=I F _ ih m n ξ s Q. rewrite !iprod_allE !mfun_allE.
    f_equal; fext=> i x. by rewrite ih.
  - move=> /=wlp _. exact: wpI_ren_compat.
Qed.

Lemma wpi_weaken n (s : tm n) P Q :
  wpi (rinst shift s) (P .: Q) = wpi s Q.
Proof. by rewrite wpi_ren. Qed.

Lemma wlpi_weaken n (s : tm n) P Q :
  wlpi (rinst shift s) (P .: Q) = wlpi s Q.
Proof. by rewrite wlpi_ren. Qed.

Lemma wpi_inst m n (θ : subst m n) (s : tm m) Q :
  wpi (inst θ s) Q = wpi s (fun i => wpi (θ i) Q).
Proof.
  elim: s n θ Q => /={m}[m a s ihs|m b s ihs t iht|m s ihs t iht|m f] n θ Q.
  - by rewrite !wpi_act ihs.
  - by rewrite !wpi_if ihs iht.
  - rewrite !wpi_def iht. f_equal. fext=> -[i|]x/=.
    by rewrite wpi_weaken. rewrite wpi_jump /=. f_equal.
    apply: fext => P. rewrite ihs. f_equal. fext=>-[i|]y/=.
    by rewrite wpi_weaken. by rewrite wpi_jump.
  - by rewrite wpi_jump.
Qed.

Lemma wlpi_inst m n (θ : subst m n) (s : tm m) Q :
  wlpi (inst θ s) Q = wlpi s (fun i => wlpi (θ i) Q).
Proof.
  elim: s n θ Q => /={m}[m a s ihs|m b s ihs t iht|m s ihs t iht|m f] n θ Q.
  - by rewrite !wlpi_act ihs.
  - by rewrite !wlpi_if ihs iht.
  - rewrite !wlpi_def iht. f_equal. fext=> -[i|]x/=.
    by rewrite wlpi_weaken. rewrite wlpi_jump /=. f_equal.
    apply: fext => P. rewrite ihs. f_equal. fext=>-[i|]y/=.
    by rewrite wlpi_weaken. by rewrite wlpi_jump.
  - by rewrite wlpi_jump.
Qed.

Lemma wpi_beta n (s : tm n.+1) (t : tm n) Q :
  wpi (inst (t .: Jump) s) Q = wpi s (wpi t Q .: Q).
Proof.
  rewrite wpi_inst. f_equal; fext=>/=-[a|]//=x. by rewrite wpi_jump.
Qed.

Lemma wlpi_beta n (s : tm n.+1) (t : tm n) Q :
  wlpi (inst (t .: Jump) s) Q = wlpi s (wlpi t Q .: Q).
Proof.
  rewrite wlpi_inst. f_equal; fext=>/=-[a|]//=x. by rewrite wlpi_jump.
Qed.

Definition wpi_distributive (wlpi wpi : iprod (fun n => tm n -> ptn n)) :=
  forall n (s : tm n) (P Q : fin n -> Pred state),
    wpi n s P ∧ wlpi n s Q ≤ wpi n s (P ∧ Q).

Lemma inf_closed_wpi_distributive wlp : inf_closed (wpi_distributive wlp).
Proof.
  move=> I F ih n s P Q. hnf=> x. rewrite prod_meetE prop_meetE.
  hnf. case. rewrite !iprod_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_wpi_distributive wlp : sup_closed (wpi_distributive wlp).
Proof.
  move=> I F ih n s P Q. rewrite !iprod_exE mfun_exE meetEx.
  focus=> i. rewrite mfun_exE. apply: exI (i) _. exact: ih.
Qed.

Lemma wpI_distributive wlp wp :
  wpi_distributive wlp wp -> wpi_distributive (@wpI wlp) (@wpI wp).
Proof.
  move=> ih n. case.
  - move=> a s P Q /=; hnf=> x /=. rewrite prod_meetE prop_meetE. hnf. case=> /= h1 h2.
    apply: ih. by rewrite prod_meetE prop_meetE.
  - move=> b s t P Q; hnf=> x /=; rewrite prod_meetE prop_meetE.
    case: ifP => _; hnf; case=> h1 h2; apply: ih; by rewrite prod_meetE prop_meetE.
  - move=> s t P Q /=. rewrite ih. apply: mono.
    move=> /=-[a|]/=; by rewrite !prod_meetE /=.
  - move=> f P Q /=. by rewrite prod_meetE.
Qed.

Corollary wlpi_distributes_over_wpi :
  wpi_distributive (@wlpi) (@wpi).
Proof.
  rewrite/wpi. apply direct_induction. exact _.
  move=> /= I F _ ih. apply: sup_closed_wpi_distributive. exact: ih.
  move=> /=wp _. rewrite {2}/wlpi-gfpE. exact: wpI_distributive.
Qed.

Corollary wpi_is_distributive :
  wpi_distributive (@wpi) (@wpi).
Proof.
  rewrite{2}/wpi. apply direct_induction. exact _.
  move=> /= I F _ ih. apply: sup_closed_wpi_distributive. exact: ih.
  move=> /=pt _. rewrite {2}/wpi-lfpE. exact: wpI_distributive.
Qed.

Corollary wlpi_is_distributive :
  wpi_distributive (@wlpi) (@wlpi).
Proof.
  rewrite{2}/wlpi. apply direct_coinduction. exact _.
  move=> /= I F _ ih. apply: inf_closed_wpi_distributive. exact: ih.
  move=> /=pt _. rewrite {2}/wlpi-gfpE. exact: wpI_distributive.
Qed.

Definition deterministic (wp : iprod (fun n => tm n -> ptn n)) :=
  forall I n (F : I -> fin n -> Pred state) (s : tm n),
    wp n s (sup F) ≤ ∃ i, wp n s (F i).

Lemma deterministic_sup_closed : sup_closed deterministic.
Proof.
  move=> I/= F ih J n G s. rewrite !iprod_exE mfun_exE.
  focus=> i. rewrite ih. focus=> j.
  apply: exI (j) _. rewrite mfun_exE. exact: exI.
Qed.

Lemma wpi_deterministic : deterministic (@wpi).
Proof.
  rewrite/wpi. apply direct_induction. exact _.
  - move=> I /= F _. exact: deterministic_sup_closed.
  - move=> /=wp cwp wp_det I n F [a s|b s t|s t|f]/=.
    + move=> x /=. by rewrite wp_det !prod_exE.
    + move=> x /=. rewrite !prod_exE. case: ifP => _; by rewrite wp_det prod_exE.
    + have: (wp n (Def s s)) (∃ i, F i) .: (∃ i, F i) ≤ ∃ i, wp n (Def s s) (F i) .: F i.
      move=>/=-[a|]/=; rewrite !prod_exE //=. move->. by rewrite wp_det.
    + by rewrite prod_exE.
Qed.

Fixpoint lfp_approx {m} (n : nat) (s : tm m.+1) : tm m :=
  match n with
  | 0 => Ω
  | n.+1 => inst (lfp_approx n s .: Jump) s
  end.

Lemma wpi_Ω n Q :
  wpi (Ω : tm n) Q = ⊥.
Proof.
  apply: bot_eq. rewrite wpi_def_lfp. apply direct_induction.
  - move=> P P' leP. by rewrite !wpi_jump /=.
  - move=> I F _ ih. focus. exact: ih.
  - move=> /=P _ ih. rewrite wpi_jump /=. exact: ih.
Qed.

Lemma wpi_lfp_kleene m (s : tm m.+1) Q :
  wpi (Def s s) Q = ∃ n, wpi (lfp_approx n s) Q.
Proof.
  rewrite wpi_def_lfp kleene_fp.
  - f_equal; fext; elim=> [|n ih]//=x.
    + by rewrite wpi_Ω.
    + rewrite wpi_beta. f_equal. by fext=>-[].
  - move=> /= P P' leP. apply: mono. by case.
  - move=> I F i0 dF. rewrite -wpi_deterministic. apply: mono.
    move=>/=-[a|]/=; rewrite prod_exE //=. exact: exI (i0) _.
Qed.

Lemma wpi_step n Q (c1 c2 : conf n) :
  step c1 c2 -> wpi c1.1 Q c1.2 = wpi c2.1 Q c2.2.
Proof.
  elim=> //=.
  - move=> a s x. by rewrite wpi_act.
  - move=> s t x. by rewrite wpi_beta {1}/wpi-lfpE/=.
  - move=> b s t x bx. by rewrite wpi_if bx.
  - move=> b s t x bx. by rewrite wpi_if ifN.
Qed.

Lemma wlpi_step n Q (c1 c2 : conf n) :
  step c1 c2 -> wlpi c1.1 Q c1.2 = wlpi c2.1 Q c2.2.
Proof.
  elim=> //=.
  - move=> a s x. by rewrite wlpi_act.
  - move=> s t x. by rewrite wlpi_beta {1}/wlpi-gfpE/=.
  - move=> b s t x bx. by rewrite wlpi_if bx.
  - move=> b s t x bx. by rewrite wlpi_if ifN.
Qed.

Lemma wpi_mstep n Q (c1 c2 : conf n) :
  mstep c1 c2 -> wpi c1.1 Q c1.2 = wpi c2.1 Q c2.2.
Proof. by elim=>//{c2}c2 c3 _ ih /wpi_step<-. Qed.

Lemma wlpi_mstep n Q (c1 c2 : conf n) :
  mstep c1 c2 -> wlpi c1.1 Q c1.2 = wlpi c2.1 Q c2.2.
Proof. by elim=>//{c2}c2 c3 _ ih /wlpi_step<-. Qed.

Lemma wpi_eval n Q (s : tm n) (f : fin n) x y :
  mstep (s,x) (Jump f,y) -> wpi s Q x = Q f y.
Proof. move=>/wpi_mstep->/=. by rewrite wpi_jump. Qed.

Lemma wlpi_eval n Q (s : tm n) (f : fin n) x y :
  mstep (s,x) (Jump f,y) -> wlpi s Q x = Q f y.
Proof. move=>/wlpi_mstep->/=. by rewrite wlpi_jump. Qed.

Definition terminates {n} (s : tm n) (x : state) :=
  exists (f : fin n) (y : state), mstep (s,x) (Jump f, y).

Lemma terminates_def {n} (s t : tm n.+1) (x : state) :
  terminates (inst (Def s s .: Jump) t) x -> terminates (Def s t) x.
Proof.
  case=> f [y ms]. exists f, y. apply: starES ms. by constructor.
Qed.

Lemma wpi_terminates_subst {m n} (s : tm m) (θ : subst m n) (Q : fin m -> Pred state) :
  (forall f x, Q f x -> terminates (θ f) x) ->
  forall x, wpi s Q x -> terminates (inst θ s) x.
Proof.
  move=> h x wps. move: m n θ s x Q wps h. rewrite/wpi. apply direct_induction. exact _.
  - move=> I F _ ih m n θ s x Q. rewrite !iprod_exE mfun_exE prod_exE prop_exE. case=> i h.
    apply: ih. exact: h.
  - move=> /=wp _ ih m n θ [a s|b s t|s t|f] x Q /=.
    + move=>/ih => h /h [f[y ms]]. exists f, y. apply: starES ms. by constructor.
    + case: ifPn => bx /ih h/h[f[y ms]]; exists f, y; by eauto using starES, @step.
    + move=> h1 h2. apply: terminates_def => /=. rewrite inst_comp. apply: (ih). exact: h1.
      move=>/=-[a/= y qay|y/ih h]/=; last by exact: h. rewrite rinst_inst_comp. fsimpl.
      rewrite inst_ids. exact: h2.
    + move=> qfx h. exact: h.
Qed.

Corollary wpi_terminates n (s : tm n) Q :
  wpi s Q ≤ terminates s.
Proof.
  move=> x h. rewrite -[s]inst_ids. apply: wpi_terminates_subst h.
  move=> f y _. by exists f, y.
Qed.

Lemma wpi_operational n (s : tm n) Q x :
  wpi s Q x <-> exists f y, mstep (s,x) (Jump f,y) /\ Q f y.
Proof.
  split.
  - move=> h. case: (wpi_terminates h) => f[y ms]. exists f, y. split=>//.
    move: (wpi_mstep Q ms) => /=. by rewrite wpi_jump => <-.
  - case=> f[y [ms qy]]. move: (wpi_mstep Q ms) => /=. by rewrite wpi_jump => ->.
Qed.

(*Lemma wlpi_safe {m} (s : tm m) (Q : fin m -> Pred state) :
  forall x, (forall f y, mstep (s, x) (Jump f, y) -> Q f y) -> wlpi s Q x.
Proof.
  elim: s Q => {m}/=n a s ih|n b s ihs t iht|n s ihs t iht|n f Q x h.
  - rewrite wlpi_act /=. apply: ih. admit.
  - admit.
  - (*rewrite/wlpi-gfpE/=. rewrite -wlpi_beta.*)
    rewrite wlpi_def. apply: iht => -a|/=y ms. f y ms.
  move: m n s θ Q Q'. rewrite/wlpi. apply direct_coinduction. exact _.
  - move=> I F _ ih m n s θ Q Q' x h i. exact: ih.
  - move=> /=wlp _ ih m n a s|b s t|s t|f θ Q Q' x h /=.
    + apply: ih. move=> f y ms; apply: h.
    + case: ifPn => bx. apply: ih. admit. admit. admit.


Lemma wlpi_safe_subst {m n} (s : tm m) (θ : subst m n)
      (Q : fin m -> Pred state) (Q' : fin n -> Pred state) :
  forall x, (forall f y, mstep (inst θ s, x) (Jump f, y) -> Q' f y) -> wlpi s Q x.
Proof.
  move: m n s θ Q Q'. rewrite/wlpi. apply direct_coinduction. exact _.
  - move=> I F _ ih m n s θ Q Q' x h i. exact: ih.
  - move=> /=wlp _ ih m n a s|b s t|s t|f θ Q Q' x h /=.
    + apply: ih. move=> f y ms; apply: h.
    + case: ifPn => bx. apply: ih. admit. admit. admit.

Lemma wlpi_operational n (s : tm n) Q x :
  wlpi s Q x <-> forall f y, mstep (s,x) (Jump f,y) -> Q f y.
Proof with by eauto using @step.
  split.
  - move=> wlps f y /(wlpi_mstep Q)/=. by rewrite wlpi_jump => <-.
  - rewrite/wlpi. move: n s Q x. apply direct_coinduction. exact _.
    + move=> I F _ ih n s Q x h. hnf=> i. apply: ih. exact: h.
    + move=> /=wlp _ ih n a s|b s t|s t|f Q x h /=.
      * apply: ih. move=> f y ms. apply: h. apply: starES ms...
      * case: ifPn => bx; apply: ih => f y ms; apply: h; apply: starES ms...
      * apply: (ih) => /=-a|/=y ms. apply: h.
Qed.*)