MEH

wp.v

@@ -480,7 +480,12 @@ Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
 | ifelse guard sIf sElse =>
     ((assertOfExpr guard -> wp sIf cond)
      /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
-| while assert guard body => assertBot
+| while assert guard body =>
+    let invar := aInterp assert in
+    let aGuard := assertOfExpr guard in
+    (invar
+     /\ (\-/m (aGuard -> invar -> wp body invar))
+     /\ (\-/m (~ aGuard -> invar -> cond))) % assert
 end.
 
 Lemma assertImplElim {a b: Assert} :
@@ -568,6 +573,41 @@ Proof.
     - apply assertBotAndStuff.
 Qed.
 
+Lemma wpWhilePre (inv: SynAssert) guard body:
+  forall post,
+  assertImplLogical
+    (wp (while inv guard body) post)
+    (aInterp inv).
+Proof.
+  intros post. unfold assertImplLogical. intros mem src.
+Admitted.
+
+Lemma wpWhilePost (inv: SynAssert) (guard: Expr):
+  forall post,
+  assertImplLogical
+    (aInterp inv /\ ~ assertOfExpr guard)%assert
+    post.
+Proof.
+  intros post. unfold assertImplLogical. intros mem src.
+Admitted.
+
+Lemma weakenPre {instr post a b} :
+  assertImplLogical a b
+  -> (|- [|b|] instr [|post|])%assert
+  -> (|- [|a|] instr [|post|])%assert.
+Proof.
+  intros impl prf.
+  apply (H_conseq a post b post); trivial.
+  - apply assertImplSelf.
+Qed.
+
+Lemma weakenPreAnd {instr post} (a b: Assert):
+  (|- [|a|] instr [|post|])%assert
+  -> (|- [|a /\ b|] instr [|post|])%assert.
+Proof.
+  apply weakenPre. unfold assertImplLogical. intros mem [hyp _]. assumption.
+Qed.
+
 Theorem wp_correctness_provable (instr: Instr) :
   forall post,
     ( |- [| wp instr post |] instr [| post |] ) % assert.
@@ -603,7 +643,34 @@ Proof.
         intros mem. intros [ [disjunctIf disjunctElse] isElse].
         apply (assertImplElim mem disjunctElse isElse).
       + apply (assertImplSelf post).
-  * apply preBottomIsProvable.
+  * apply H_conseq
+      (pre':=
+    + eapply H_while. eapply H_conseq.
+      - apply IHinstr.
+      - intros mem. intros [H1 H2].
+      - intros mem hyp. exact hyp.
+    + intros mem [ H1 [ H2 H3 ] ]. eapply H2. unfold assertImpl in H2.
+      destruct H2 with (mem:=mem) as [l | r].
+      - exfalso. apply l. split; eauto. assert ((aInterp s) mem); eauto.
+        unfold assertNot in l; unfold assertAnd in l. destruct l.
+        destruct H3 with (mem:=mem) as [a | b].
+      - exact r.
+  * apply (H_conseq
+      (wp (while s e instr) post) (post)
+      (aInterp s) ((aInterp s) /\ ~ assertOfExpr e)%assert).
+    - apply (H_while (aInterp s) s e instr).
+      specialize IHinstr with (aInterp s).
+      unfold wp in IHinstr; destruct instr; simpl in IHinstr; trivial.
+      + apply (weakenPreAnd (aInterp s) (assertOfExpr e)). assumption.
+      + assert (forall x, assertImplLogical x assertTop).
+        { intros x. unfold assertImplLogical.
+          intros mem hyp. unfold assertTop;
+          trivial. }
+        apply (weakenPre (H (aInterp s /\ assertOfExpr e)%assert)).
+        assumption.
+      +
+    - apply (wpWhilePre s e instr post).
+    - apply (wpWhilePost s e post).
 Qed.
 
 Theorem wp_correctness (instr: Instr) :