Require Export Atoms.

Inductive prog: Type :=

 

 | iat (inst: atom)

 

 | seq (pf pn:prog)

 

 | join (pl pr:prog)
 
 

 | loop (body:prog).

Bind Scope prog_scope with prog.
Delimit Scope prog_scope with prog.

Notation "p1 -; p2" := (seq p1 p2)
  (at level 95, right associativity): prog_scope.

Coercion iat: atom >-> prog.

Open Scope prog_scope.

Notation "'ifc' c 'then' p1 'else' p2 'fi'" :=(join (ensure c -; p1) (ensure (not c) -; p2))
   (at level 95): prog_scope.

Notation "'while' c 'do' p 'done'" := (loop (ensure c -; p) -; ensure (not c))
   (at level 95): prog_scope.

Inductive sem: prog → state → option state → Prop :=
 | sem_iat inst s s0:
     asem inst s s0 → sem (iat inst) s s0
 | sem_seq pf pn s0 s1 s2:
     sem pf s0 (Some s1)
     → sem pn s1 s2
     → sem (pf -; pn) s0 s2
 | sem_seq_ko pf pn s:
     sem pf s None
     → sem (pf -; pn) s None
 | sem_join_l pl pr s0 s1:
     sem pl s0 s1
     → sem (join pl pr) s0 s1
 | sem_join_r pl pr s0 s1:
     sem pr s0 s1
     → sem (join pl pr) s0 s1
 | sem_loop_stop body s:
     sem (loop body) s (Some s)
 | sem_loop_continue body s0 s1 s2:
     sem body s0 (Some s1)
      → sem (loop body) s1 s2
     → sem (loop body) s0 s2
 | sem_loop_ko body s :
     sem body s None
       → sem (loop body) s None.

Hint Resolve sem_iat sem_seq sem_seq_ko sem_join_l sem_join_r sem_loop_stop sem_loop_continue sem_loop_ko: sem.

Definition is_ok (p: prog) := ∀ s s', sem p s s' → s' ≠ None.

Fixpoint wlp (p: prog) (post: state→ Prop) (s:state) : Prop :=
  match p with
 | iat inst ⇒ awlp inst post s
 | seq pf pn ⇒ wlp pf (wlp pn post) s
 | join pl pr ⇒ (wlp pl post s) ∧ (wlp pr post s)
 | loop body ⇒
    ∃ inv: state→Prop,
        (inv s)
     ∧ (∀ s', inv s' → wlp body inv s')
     ∧ (∀ s', inv s' → post s')
 end.

Lemma wlp_monotonic p:
  ∀ (P Q: state → Prop) s, wlp p P s →
    (∀ s, P s → Q s) → wlp p Q s.
Proof.
  induction p; simpl; intuition simpl; eauto with echecker.
  firstorder.
Qed.

Hint Resolve wlp_monotonic: echecker.

Theorem wlp_correctness p s s': (sem p s s') → ∀ post, wlp p post s → ok s' post.
Proof.
  induction 1; simpl in × |- *; intuition eauto with echecker.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
Qed.

Lemma wlp_isok p: (∀ s, wlp p (fun _ ⇒ True) s) → is_ok p.
Proof.
  unfold is_ok. intros H s s' H0 H1; subst.
  exact (wlp_correctness _ _ _ H0 _ (H s)).
Qed.

Theorem wlp_complete p: ∀ post s, (∀ s', sem p s s' → ok s' post) → wlp p post s.
Proof.
  induction p; simpl in × |- *; intuition eauto with sem echecker.
  intros; eapply awlp_complete. eauto with sem.
  eapply wlp_monotonic.
  eapply IHp1.
  2: intros s0 H0; eapply IHp2; pattern s0; eapply H0.
  intros s'; case s'; simpl; intros; eauto with sem.
  case (H None); eauto with sem.
  constructor 1 with (x:=fun s ⇒ ∀ s', sem (loop p) s s' → ok s' post).
  constructor 1.
  eauto with echecker sem.
  constructor 1; intros s' H0.
  eapply wlp_monotonic.
  eapply IHp.
  2: intros s1 H1; pattern s1; apply H1.
  intros s1; case s1; simpl; intros; eauto with sem.
  case (H0 None); eauto with sem.
  apply (H0 (Some s')). eauto with sem.
Qed.

Lemma isok_wlp p s: is_ok p → wlp p (fun _ ⇒ True) s.
Proof.
  unfold is_ok; intros; apply wlp_complete.
  intros s'; case s'; simpl; firstorder.
Qed.

Definition seq_outskip (pf pn: prog): prog :=
  match pn with
  | skip ⇒ pf
  | _ ⇒ pf -; pn
  end.

Fixpoint normalize_rec (pf pn: prog): prog :=
  match pf with
  | seq pf' pn' ⇒ normalize_rec pf' (normalize_rec pn' pn)
  | join pl pr ⇒ seq_outskip (join (normalize_rec pl skip) (normalize_rec pr skip)) pn
  | loop body ⇒ seq_outskip (loop (normalize_rec body skip)) pn
  | skip ⇒ pn
  | iat inst ⇒ seq_outskip inst pn
 end.

Definition normalize p := normalize_rec p skip.

Lemma wlp_seq_outskip_fwd pf:
  ∀ pn (P: state→Prop) s, wlp pf (wlp pn P) s → wlp (seq_outskip pf pn) P s.
Proof.
  intros pn; case pn; simpl; eauto with checker echecker.
  intros inst; case inst; simpl; eauto with echecker.
Qed.
Hint Resolve wlp_seq_outskip_fwd: checker.

Lemma wlp_normalize_rec_fwd pf:
   ∀ pn (P: state→Prop) s, (wlp pf (wlp pn P) s) → (wlp (normalize_rec pf pn) P s).
Proof.
  induction pf; simpl; try (intuition eauto with checker echecker; fail); intros pn P s H.
  generalize H; clear H; case inst; simpl; intros; eauto with checker.
  apply wlp_seq_outskip_fwd; simpl.
  intuition eauto with echecker.
  apply wlp_seq_outskip_fwd; simpl.
  case H; clear H.
  intros invariant; intuition.
  constructor 1 with (x:=invariant).
  intuition eauto with echecker.
Qed.

Lemma normalize_fwd_correctness p:
   ∀ (P: state→Prop) s, (wlp p P s) → (wlp (normalize p) P s).
Proof.
  unfold normalize; intros; apply wlp_normalize_rec_fwd. simpl; eauto with echecker.
Qed.

Lemma wlp_seq_outskip_bck pf:
  ∀ pn (P: state→Prop) s, wlp (seq_outskip pf pn) P s → wlp pf (wlp pn P) s.
Proof.
  intros pn; case pn; simpl; eauto with checker echecker.
  intros inst; case inst; simpl; eauto with echecker.
Qed.
Hint Resolve wlp_seq_outskip_bck: checker.

Lemma wlp_normalize_rec_bck pf:
   ∀ pn (P: state→Prop) s, (wlp (normalize_rec pf pn) P s) → (wlp pf (wlp pn P) s).
Proof.
  induction pf; try (simpl; intuition eauto with checker echecker; fail).
  intros pn P s H; apply wlp_seq_outskip_bck. generalize H; clear H; case inst; simpl; auto with checker.
  simpl; intros pn P s H. generalize (wlp_seq_outskip_bck _ _ _ _ H); simpl.
  intuition eauto with echecker.
  simpl; intros pn P s H. generalize (wlp_seq_outskip_bck _ _ _ _ H); simpl.
  firstorder.
Qed.

Lemma normalize_bck_correctness p:
   ∀ (P: state→Prop) s, (wlp (normalize p) P s) → (wlp p P s).
Proof.
  unfold normalize; intros; eapply wlp_monotonic.
  eapply wlp_normalize_rec_bck; eauto.
  simpl; auto.
Qed.

Fixpoint prog_eq (p1 p2: prog) : bool :=
 match p1,p2 with
 | iat inst1, iat inst2 ⇒ atom_eq inst1 inst2 &&& true
 | seq pf1 pn1, seq pf2 pn2 ⇒
    prog_eq pf1 pf2 &&& prog_eq pn1 pn2
 | join pl1 pr1, join pl2 pr2 ⇒
    prog_eq pl1 pl2 &&& prog_eq pr1 pr2
 | loop body1, loop body2 ⇒
    prog_eq body1 body2
 | _,_ ⇒ false
 end.

Lemma prog_eq_wlp p1 p2: ∀ post s, prog_eq p1 p2=true → wlp p1 post s → wlp p2 post s.
Proof.
  decide_eqb_eq p1 p2; eqtrue.
  intros; eauto with eqtrue.
  intros; eauto with echecker.
  intuition.
  firstorder.
Qed.

Lemma prog_eq_normalize_wlp p1 p2: ∀ post s, prog_eq (normalize p1) (normalize p2)=true → wlp p1 post s → wlp p2 post s.
Proof.
  intros; apply normalize_bck_correctness.
  eapply prog_eq_wlp; eauto.
  apply normalize_fwd_correctness.
  auto.
Qed.

Lemma prog_eq_isok p1 p2: prog_eq (normalize p1) (normalize p2) = true → is_ok p1 → is_ok p2.
Proof.
  intros; apply wlp_isok.
  intros; eapply prog_eq_normalize_wlp; eauto.
  apply isok_wlp; auto.
Qed.