Require Import Assertions.
Require Import Atoms.

Inductive kernel: Type :=
 | Kle_iter (n:nat) (label: option alabel) (body last next: kernel)
 | Kgjoin (min max:Z) (pf: Z → kernel)
 | Kiat (inst: atom)
 | Kseq (pf pn:kernel)
 | Kjoin (pl pr:kernel)
 | Kjoinch (pl pr: kernel) (convexhull: assertion)
 | Kloop (body:kernel) (inv: assertion)
 | Kclone (x:var) (body:kernel)
 | Kdeflabel (label: alabel) (res:Z) (p: kernel)
 | Kbranch2 (label: alabel) (p: bool → kernel)
 | Kbranch (label: alabel) (p: Z → kernel).

Fixpoint Kwlp_iter (n:nat) (k: (state→ Prop) → state → Prop) (post: state→ Prop) (s:state) :=
  match n with
  | O ⇒ post s
  | (S n) ⇒ Kwlp_iter n k (k post) s
  end.

Fixpoint Kwlp_le_iter (n:nat) (k: (state→ Prop) → state → Prop) (post: state→ Prop) (s:state) :=
  match n with
  | O ⇒ post s
  | (S n) ⇒ Kwlp_le_iter n k post s ∧ Kwlp_iter (S n) k post s
  end.

Fixpoint Kwlp (p: kernel) (post: state→ Prop) (s:state) {struct p}: Prop :=
  match p with
  | Kle_iter n _ body last next ⇒
      Kwlp_le_iter n (Kwlp body) (Kwlp next post) s
      ∧ Kwlp_iter (S n) (Kwlp body) (Kwlp last post) s
  | Kgjoin min max pf ⇒ ∀ z, min ≤ z ≤ max → Kwlp (pf z) post s
  | Kiat inst ⇒ awlp inst post s
  | Kseq pf pn ⇒ Kwlp pf (Kwlp pn post) s
  | Kjoin pl pr ⇒ (Kwlp pl post s) ∧ (Kwlp pr post s)
  | Kjoinch pl pr _ ⇒ (Kwlp pl post s) ∧ (Kwlp pr post s)
  | Kloop body _ ⇒
    ∃ inv: state→Prop,
        (inv s)
     ∧ (∀ s', inv s' → Kwlp body inv s')
     ∧ (∀ s', inv s' → post s')
  | Kclone x body ⇒ Kwlp body (fun s' ⇒ post (add (vid x) (s (vid x)) s')) s
  | Kdeflabel _ _ p ⇒ Kwlp p post s
  | Kbranch2 _ p ⇒ (Kwlp (p true) post s) ∨ (Kwlp (p false) post s)
  | Kbranch l pf ⇒ ∃ z, (labmin l) ≤ z ≤ (labmax l) ∧ Kwlp (pf z) post s
 end.

Section Kiter_proofs.

Variable k: (state→ Prop) → state → Prop.

Hypothesis k_monotonic: ∀ (P Q: state → Prop) s, k P s → (∀ s, P s → Q s) → k Q s.

Lemma Kiter_monotonic n:
   ∀ (P Q: state → Prop) s, Kwlp_iter n k P s → (∀ s, P s → Q s) → Kwlp_iter n k Q s.
Proof.
  induction n; simpl; firstorder.
Qed.

Hint Resolve Kiter_monotonic: echecker.

Lemma Kle_iter_monotonic n:
   ∀ (P Q: state → Prop) s, Kwlp_le_iter n k P s → (∀ s, P s → Q s) → Kwlp_le_iter n k Q s.
Proof.
  induction n; simpl; firstorder eauto with echecker.
Qed.

End Kiter_proofs.

Hint Resolve Kle_iter_monotonic Kiter_monotonic: echecker.

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

Hint Resolve Kwlp_monotonic: echecker.

Fixpoint Kangel_wlp (p: kernel) (post: state→ Prop) (s:state) {struct p}: Prop :=
  match p with
  | Kclone x body ⇒ Kangel_wlp body (fun s' ⇒ post (add (vid x) (s (vid x)) s')) s
  | Kiat inst ⇒ angel_awlp inst post s
  | Kseq pf pn ⇒ Kangel_wlp pf (Kangel_wlp pn post) s
  | Kjoin pl pr ⇒ (Kangel_wlp pl post s) ∨ (Kangel_wlp pr post s)
  | Kbranch2 _ p ⇒ (Kwlp (p true) (fun s ⇒ True) s → Kangel_wlp (p true) post s) ∧ (Kwlp (p false) (fun s ⇒ True) s → Kangel_wlp (p false) post s)
  | Kbranch l p ⇒ ∀ z, (labmin l) ≤ z ≤ (labmax l) → Kwlp (p z) (fun s ⇒ True) s → Kangel_wlp (p z) post s
  | _ ⇒ False
 end.

Lemma Kangel_wlp_monotonic p:
  ∀ (P Q: state → Prop) s, Kangel_wlp p P s →
    (∀ s, P s → Q s) → Kangel_wlp p Q s.
Proof.
  induction p; simpl; try (intuition (eauto with angel; fail)).
Qed.

Hint Resolve Kangel_wlp_monotonic: echecker angel.

Lemma Kangel_wlp_duality p :
  ∀ P s, Kangel_wlp p P s → ~(Kwlp p (fun s ⇒ ~(P s)) s).
Proof.
  induction p; simpl; try (intuition (eauto with angel; fail)).
  intros P s H H1.
  eapply (IHp1 _ _ H).
  eapply Kwlp_monotonic; eauto.
  clear H1 H.
  firstorder.
  intros P s H0. case H0; clear H0; intros H1 H2.
  intro H0; case H0; clear H0.
  intros H0. lapply H1.
  clear H1 H2; firstorder.
  eapply Kwlp_monotonic; eauto.
  intros H0. lapply H2.
  clear H1 H2; firstorder.
  eapply Kwlp_monotonic; eauto.
  intros P s H0 H1.
  case H1; clear H1.
  intros z; intuition.
  case (H z P s); clear H.
  apply H0; intuition.
  eapply Kwlp_monotonic; eauto.
  eapply Kwlp_monotonic; eauto.
Qed.

Require Import Classical_Prop.
Lemma Kangel_wlp_correctness p R s s':
  Kwlp p R s → Kangel_wlp p (eq s') s → R s'.
Proof.
  intros H H0.
  apply NNPP.
  intros H1.
  apply (Kangel_wlp_duality _ _ _ H0); clear H0.
  eapply Kwlp_monotonic; eauto.
  intros s0 H0 H2; subst.
  tauto.
Qed.