# 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).

## Small-step Semantics

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).

## Axiomatic semantics

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.

## Lemma 9.34

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.

## Lemma 9.35

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.

## Corollary 9.36

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 9.37

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.

## Corollary 9.38

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.

## Lemma 9.39

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.

## Lemma 9.40

We say that a predicate transformer is deterministic if it commutes with arbitrary suprema. This is equivalent to Definition 9.23, as remarked in the thesis and proven in wp.abstract.

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.

## Lemma 9.41

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 9.42

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 9.43

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.

## Lemma 9.44

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 9.45

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 9.46

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.
- (*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.

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.