Require Export Conditions.
Require Import Classical_Prop.

Inductive atom: Type :=

 

 | guassign (l:list var) (post: cond)

 

 | skip

 

 | xrequire (pre: cond) (mesg: string)

 

 | ensure (post: cond)

 

 | assign (x: var) (t: term).

Definition require (pre: cond) := xrequire pre "".

Inductive asem: atom → state → option state → Prop :=
 | asem_guassign l post s0 s1:
     lframeeq l s0 s1 → oeval post s0 s1 → asem (guassign l post) s0 (Some s1)
 | asem_skip s:
     asem skip s (Some s)
 | asem_req_ok c m s:
     eval c s
     → asem (xrequire c m) s (Some s)
 | asem_req_ko c m s:
     ~(eval c s)
     → asem (xrequire c m) s None
 | asem_ensure c s:
     eval c s
     → asem (ensure c) s (Some s)
 | asem_assign x t s:
     asem (assign x t) s (Some (add (vid x) (teval t s) s)).

Hint Resolve Some asem_guassign asem_skip asem_req_ok asem_req_ko asem_ensure asem_assign: sem.

Definition awlp (p: atom) (post: state→ Prop) (s:state) : Prop :=
 match p with
 | guassign l c ⇒ ∀ s', lframeeq l s s' → oeval c s s' → post s'
 | skip ⇒ post s
 | xrequire c m ⇒ eval c s ∧ post s
 | ensure c ⇒ (eval c s) → (post s)
 | assign x t ⇒ post (add (vid x) (teval t s) s)
 end.

Lemma awlp_monotonic p:
  ∀ (P Q: state → Prop) s, awlp p P s →
    (∀ s, P s → Q s) → awlp p Q s.
Proof.
  destruct p; simpl; intuition simpl; eauto.
Qed.

Hint Resolve ok_monotonic awlp_monotonic: echecker.

Lemma awlp_correctness p s s': (asem p s s') → ∀ post, awlp p post s → ok s' post.
Proof.
  destruct 1; simpl in × |- *; intuition eauto with echecker.
Qed.

Hint Resolve awlp_correctness: echecker.

Lemma awlp_complete p: ∀ post s, (∀ s', asem p s s' → ok s' post) → awlp p post s.
Proof.
  destruct p; simpl in × |- *; intros; try (refine (H (Some _) _); eauto with sem).
  case (classic (eval pre s)).
  intuition refine (H (Some _) _); eauto with sem.
  intros; case (H None). eauto with sem.
Qed.

Definition atom_eq (inst1 inst2: atom) :=
  match inst1, inst2 with
  | guassign l1 post1, guassign l2 post2 ⇒ lvar_eq l1 l2 &&& cond_eq post1 post2
  | skip, skip ⇒ true
  | xrequire pre1 _, xrequire pre2 _ ⇒ cond_eq pre1 pre2
  | ensure post1, ensure post2 ⇒ cond_eq post1 post2
  | assign x1 t1, assign x2 t2 ⇒ var_eq x1 x2 &&& term_eq t1 t2
  | _, _ ⇒ false
  end.

Lemma atom_eq_awlp (inst1 inst2: atom) post s: atom_eq inst1 inst2=true → awlp inst1 post s → awlp inst2 post s.
Proof.
  decide_eqb_eq inst1 inst2; eqtrue.
  intros H1 H2 s' H3 H4.
  apply H2.
  eapply lvar_eq_lframeeq; eauto.
  erewrite cond_eq_oeval; eauto.
  intuition.
  erewrite <- cond_eq_eval; eauto.
  intros H0 H1 H2; apply H1.
  erewrite cond_eq_eval; eauto.
  intros; erewrite <- var_eq_eq; eauto.
  erewrite <- term_eq_eval; eauto.
Qed.

Hint Resolve atom_eq_awlp: eqtrue.

Definition angel_awlp (p: atom) (post: state→ Prop) (s:state) : Prop :=
 match p with
 | guassign l c ⇒ ∃ s', lframeeq l s s' ∧ oeval c s s' ∧ post s'
 | skip ⇒ post s
 | xrequire c m ⇒ (eval c s) → post s
 | ensure c ⇒ (eval c s) ∧ (post s)
 | assign x t ⇒ post (add (vid x) (teval t s) s)
 end.

Lemma angel_awlp_monotonic p:
  ∀ (P Q: state → Prop) s, angel_awlp p P s →
    (∀ s, P s → Q s) → angel_awlp p Q s.
Proof.
  destruct p; simpl; firstorder.
Qed.

Lemma angel_awlp_duality p P s: angel_awlp p P s → ~(awlp p (fun s ⇒ ~(P s)) s).
Proof.
  destruct p; simpl; firstorder.
Qed.

Hint Resolve angel_awlp_monotonic angel_awlp_duality: angel.