Require Import Facts States ICSyntax.
Set Implicit Arguments.
Unset Strict Implicit.

Module ICSemantics (Sigma : State).
Module ICSyn := ICSyntax.ICSyntax Sigma.
Export ICSyn.

Implicit Types (P : Pred state) (Q QQ : NPred state) (x y z : state).
Implicit Types (a : action) (b : guard) (s t : term).

Definition conf := (term × state)%type.
Inductive step : conf → conf → Prop :=
| step_act a s x :
    step (Act a s, x) (s, a x)
| step_def s t x:
    step (Def s t, x) (t.[Def s s/], 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).

Inductive eval Q : term → Pred state :=
| eval_act a s x :
    eval Q s (a x) →
    eval Q (Act a s) x
| eval_if_true b s t x :
    b x →
    eval Q s x →
    eval Q (If b s t) x
| eval_if_false b s t x :
    ~~b x →
    eval Q t x →
    eval Q (If b s t) x
| eval_jump f x :
    Q f x →
    eval Q (Jump f) x
| eval_def P s t x :
    P <<= eval Q (Def s s) →
    eval (P .: Q) t x →
    eval Q (Def s t) x.

Fixpoint wp Q s :=
  match s with
    | Act a s ⇒ wp Q s \o a
    | If b s t ⇒ fun sigma ⇒ if b sigma then wp Q s sigma else wp Q t sigma
    | Jump f ⇒ Q f
    | Def s t ⇒
      let F P := wp (P .: Q) s in
      wp (Fix F .: Q) t
  end.

Lemma wp_mono Q QQ :
  (∀ n, Q n <<= QQ n) → (∀ s, wp Q s <<= wp QQ s).
Proof with eauto.
  move⇒ h1 s. elim: s Q QQ h1 ⇒ [|b s ihs t iht|s ihs t iht|] Q QQ h1 /=...
  - move⇒ x. case: ifP...
  - apply: iht ⇒ -[|n]/=... apply: fix_mono ⇒ P. by apply: ihs ⇒ -[].
Qed.

Lemma wp_equiv Q QQ s x :
  (∀ n x, Q n x ↔ QQ n x) → (wp Q s x ↔ wp QQ s x).
Proof.
  move⇒ h. split; apply: wp_mono; firstorder.
Qed.

Lemma wp_cons_mono Q s :
  monotone (fun P ⇒ wp (P .: Q) s).
Proof.
  move⇒ P1 P2 h. by apply: wp_mono ⇒ -[].
Qed.

Lemma wp_fix P Q s :
  wp (P .: Q) s <<= P → Fix (fun P ⇒ wp (P .: Q) s) <<= P.
Proof.
  move⇒ h x. elim=>{x}x P´ _ ih sx. exact/h/wp_cons_mono.
Qed.

Lemma wp_eval Q s :
  wp Q s <<= eval Q s.
Proof with eauto using eval.
  elim: s Q ⇒ [a s ihs|b s ihs t iht|s ihs t iht|f] Q x /=...
  case: ifPn... set P := Fix _. move⇒ tx. apply: (eval_def (P := P))...
  apply: wp_fix. move=>{x tx} x sx. eapply eval_def...
Qed.

Lemma eval_wp Q s :
  eval Q s <<= wp Q s.
Proof.
  move⇒ x evs. elim: evs ⇒ //={Q s x}
    [Q e s t x ->|Q e s t x/negbTE->|Q P s t x _ le _]//.
  apply: wp_cons_mono x ⇒ x/le. exact: fix_fold.
Qed.

Theorem coincidence Q s x : eval Q s x ↔ wp Q s x.
Proof. split; by [exact: eval_wp|exact: wp_eval]. Qed.

Lemma wp_ren Q (xi : var → var) s :
  wp Q s.[ren xi] = wp (xi >>> Q) s.
Proof.
  elim: s Q xi ⇒ [e s ihs|e s ihs t iht|s ihs t iht|f] Q xi //=.
  - by rewrite ihs.
  - by rewrite ihs iht.
  - asimpl; rewrite iht; f_equal; asimpl. f_ext ⇒ -[|x]//=.
    f_equal. f_ext ⇒ P. rewrite ihs. autosubst.
Qed.

Lemma wp_weaken P Q s : wp (P .: Q) s.[ren (+1)] = wp Q s.
Proof. exact: wp_ren. Qed.

Lemma wp_subst Q (theta : var → term) s :
  wp Q s.[theta] = wp (wp Q \o theta) s.
Proof.
  elim: s Q theta ⇒ [e s ihs|e s ihs t iht|s ihs t iht|f] Q theta //=.
  - by rewrite ihs.
  - by rewrite ihs iht.
  - rewrite iht. f_equal. f_ext ⇒ -[|x]//=; asimpl; last by exact: wp_weaken.
    f_equal. f_ext ⇒ P. rewrite ihs. f_equal. f_ext ⇒ -[|y] //=.
    asimpl; exact: wp_weaken.
Qed.

Lemma step_admissible Q s t x y :
  step (s,x) (t,y) → (wp Q s x ↔ wp Q t y).
Proof.
  move⇒ h. inv h ⇒ //=; last first. by rewrite ifN. by rewrite H0.
  move: s0 t0 ⇒ s t. rewrite wp_subst. split; apply: wp_mono ⇒ -[]//=.
  apply: fix_unfold. exact: wp_cons_mono. exact: fix_fold.
Qed.

Lemma mstep_admissible Q f s x y :
  mstep (s,x) (Jump f,y) → (wp Q s x ↔ Q f y).
Proof.
  suff: ∀ p q, mstep p q → (wp Q p.1 p.2 ↔ wp Q q.1 q.2).
  exact. move⇒ {f s x y} p q. elim⇒ //{q}-[s x] [t y]/= _ ih st.
  rewrite ih. exact: step_admissible.
Qed.

Definition terminates s x :=
  ∃ f y, mstep (s,x) (Jump f,y).

Lemma step_terminates s t x y :
  step (s,x) (t,y) → terminates t y → terminates s x.
Proof.
  move⇒ st [z [f h]]. ∃ z, f. exact: starRS st h.
Qed.

Lemma eval_terminates Q s x :
  eval Q s x → ∀ theta,
    (∀ f, Q f <<= terminates (theta f)) →
    terminates s.[theta] x.
Proof.
  elim⇒ {Q s x}//=; eauto using step_terminates, step.
  move⇒ Q P s t x _ ih1 _ ih2 theta h.
  apply: step_terminates (step_def _ _ _) _. asimpl.
  apply: ih2 ⇒ -[|//]/=y py. exact: ih1.
Qed.

Corollary eval_terminates_id Q s :
  eval Q s <<= terminates s.
Proof.
  move⇒ x ev. rewrite -[s]subst_id. apply: eval_terminates ev _ _.
  move⇒ {Q s x} f x _. ∃ f, x. exact: starxx.
Qed.

Theorem correspondence Q s x :
  wp Q s x ↔ ∃ f y, mstep (s,x) (Jump f,y) ∧ Q f y.
Proof.
  split⇒ [h1|[tau[f[h1 h2]]]].
  - move: (h1) ⇒ /wp_eval/eval_terminates_id[f[y h2]]. ∃ f,y.
    split⇒ //. by rewrite -(mstep_admissible _ h2).
  - by rewrite (mstep_admissible _ h1).
Qed.

Definition point_pred f x : NPred state := fun g y ⇒ f = g ∧ x = y.

Corollary wp_step_equiv f s x y :
  mstep (s,x) (Jump f,y) ↔ wp (point_pred f y) s x.
Proof.
  rewrite correspondence. split ⇒ [h|[g[z[h1[->->]]]]] //. by ∃ f,y.
Qed.

Corollary wp_terminates s x :
  wp (@Top _) s x ↔ terminates s x.
Proof.
  rewrite correspondence. by firstorder.
Qed.

Corollary wp_det Q s x :
  wp Q s x ↔ ∃ f y, wp (point_pred f y) s x ∧ Q f y.
Proof.
  rewrite correspondence. split⇒ -[f[y[h1 h2]]]; ∃ f, y; split⇒ //.
    by rewrite -wp_step_equiv. by rewrite wp_step_equiv.
Qed.

End ICSemantics.