Finish proving wp_correctness

wp.v

@@ -441,20 +441,30 @@ Qed.
 
 (***** Weakest precondition **************************************************)
 
-Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
+Fixpoint wp (instr: Instr) (condOpt: option Assert) : option Assert :=
-| skip =>
+  match condOpt with
-    cond
+  | None => None
+  | Some cond => match instr with
+    | skip =>
+        Some cond
     | abort =>
-    assertTop
+        Some assertTop
-| assign x expr =>
+    | assign x expr =>
-    cond [[ x <- expr expr ]]
+        Some (cond [[ x <- expr expr ]])
-| seq s1 s2 =>
+    | seq s1 s2 =>
-    wp s1 (wp s2 cond)
+        wp s1 (wp s2 condOpt)
-| ifelse guard sIf sElse =>
+    | ifelse guard sIf sElse =>
-    ((assertOfExpr guard -> wp sIf cond)
+        match (wp sIf condOpt, wp sElse condOpt) with
-    /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
+        | (None, _) | (_, None) => None
-| while guard body => assertTop
+        | (Some wpIf, Some wpElse) =>
-end.
+            Some (
+              ((assertOfExpr guard -> wpIf)
+              /\ (~ (assertOfExpr guard) -> wpElse)) % assert)
+        end
+    | while guard body =>
+        None
+    end
+  end.
 
 Lemma assertImplElim {a b: Assert} :
   forall (m: Mem), (assertImpl a b) m -> a m -> b m.
@@ -472,42 +482,120 @@ Proof.
   unfold assertImplLogical. intros mem x. assumption.
 Qed.
 
-Theorem wp_correctness_provable (instr: Instr) :
+Definition whatever_or_none (whatever: Assert -> Instr -> Assert -> Prop)
-  forall post, ( |- [| wp instr post |] instr [| post |] ) % assert.
+  (pre: option Assert) (instr: Instr) (post: option Assert) : Prop :=
+  match (pre, post) with
+  | (Some _, None) => False
+  | (None, _) => True
+  | (Some pre0, Some post0) => whatever pre0 instr post0
+  end.
+
+Definition provable_or_none := whatever_or_none hoare_provability.
+Notation "|-opt [| pre |] instr [| post |]" :=
+    (provable_or_none pre instr post) (at level 30) : assert.
+
+Definition consequence_or_none := whatever_or_none hoare_consequence.
+Notation "|=opt [| pre |] instr [| post |]" :=
+    (consequence_or_none pre instr post) (at level 30) : assert.
+
+Lemma postnone_is_okay {instr post}:
+  (forall post0, (|-opt [|wp instr (Some post0)|] instr [|Some post0|])%assert)
+  -> (|-opt [|wp instr post|] instr [|post|])%assert.
 Proof.
-  induction instr; intros post; simpl.
+  intros prf. destruct post.
-  * apply (H_skip post).
+  - apply prf.
-  * apply (H_abort assertTop post).
+  - unfold provable_or_none; unfold whatever_or_none.
-  * apply (H_assign post v e).
+    unfold wp; destruct instr; trivial.
-  * remember (wp instr2 post) as mid eqn:midRel.
+Qed.
+
+Theorem wp_correctness_provable (instr: Instr) :
+  forall post, ( |-opt [| wp instr post |] instr [| post |] ) % assert.
+Proof.
+  induction instr; intros post; apply postnone_is_okay; intros post0.
+  * apply (H_skip post0).
+  * apply (H_abort assertTop post0).
+  * apply (H_assign post0 v e).
+  * remember (wp instr2 (Some post0)) as mid eqn:midRel.
     remember (wp instr1 mid) as pre eqn:preRel.
-    specialize IHinstr2 with post.
+    simpl; rewrite <- midRel; rewrite <- preRel.
-    specialize IHinstr1 with mid.
+    specialize IHinstr2 with (Some post0) as IHpost.
-    rewrite <- midRel in IHinstr2.
+    specialize IHinstr1 with mid as IHmid.
-    rewrite <- preRel in IHinstr1.
+    rewrite <- midRel in IHpost; rewrite <- preRel in IHmid.
-    apply (H_seq pre mid post instr1 instr2).
+    destruct mid as [mid0 | ] eqn:mid0Rel.
-    assumption. assumption.
+    destruct pre as [pre0 | ] eqn: pre0Rel.
-  * remember ((assertOfExpr e -> wp instr1 post)
+    apply (H_seq pre0 mid0 post0).
-              /\ (~ assertOfExpr e -> wp instr2 post)) % assert
+    apply IHmid. apply IHpost.
-      as pre eqn:preRel.
+    + unfold whatever_or_none; trivial.
-    apply (H_if pre post e instr1 instr2).
+    + destruct pre.
-    - apply (H_conseq
+      - unfold provable_or_none in IHmid; unfold whatever_or_none in IHmid.
-        (pre /\ assertOfExpr e)%assert post
+        exfalso. apply IHmid.
-        (wp instr1 post) post instr1
+      - unfold whatever_or_none; trivial.
-        (IHinstr1 post)).
+  * specialize IHinstr1 with (Some post0);
-      + rewrite preRel. unfold assertImplLogical.
+    specialize IHinstr2 with (Some post0).
-        intros mem. intros [ [disjunctIf disjunctElse] isIf].
+    destruct (wp instr1 (Some post0)) as [preIf | ] eqn:preIfRel;
-        apply (assertImplElim mem disjunctIf isIf).
+    destruct (wp instr2 (Some post0)) as [preElse | ] eqn:preElseRel.
-      + apply (assertImplSelf post).
+    remember ((assertOfExpr e -> preIf)
-    - apply (H_conseq
+              /\ (~ assertOfExpr e -> preElse)) % assert
-        (pre /\ ~ assertOfExpr e)%assert post
+              as pre0 eqn:pre0Rel.
-        (wp instr2 post) post instr2
+    assert (wp (ifelse e instr1 instr2) (Some post0) = (Some pre0)).
-        (IHinstr2 post)).
+    {
-      + rewrite preRel. unfold assertImplLogical.
+      rewrite pre0Rel; simpl; rewrite preIfRel; rewrite preElseRel; congruence.
-        intros mem. intros [ [disjunctIf disjunctElse] isElse].
+    }
-        apply (assertImplElim mem disjunctElse isElse).
+    {
-      + apply (assertImplSelf post).
+      rewrite H.
-  * 
+      apply (H_if pre0 post0 e instr1 instr2).
+      - apply (H_conseq
+          (pre0 /\ assertOfExpr e)%assert post0
+          preIf post0 instr1
+          IHinstr1).
+        + rewrite pre0Rel. unfold assertImplLogical.
+          intros mem [ [disjunctIf disjunctElse] isIf].
+          apply (assertImplElim mem disjunctIf isIf).
+        + apply (assertImplSelf post0).
+      - apply (H_conseq
+          (pre0 /\ ~ assertOfExpr e)%assert post0
+          preElse post0 instr2
+          IHinstr2).
+        + rewrite pre0Rel. unfold assertImplLogical.
+          intros mem [ [disjunctIf disjunctElse] isElse].
+          apply (assertImplElim mem disjunctElse isElse).
+        + apply (assertImplSelf post0).
+    }
+
+    - unfold provable_or_none; simpl; rewrite preElseRel;
+        rewrite preIfRel; trivial.
+    - unfold provable_or_none; simpl; rewrite preElseRel;
+        rewrite preIfRel; trivial.
+    - unfold provable_or_none; simpl; rewrite preElseRel;
+        rewrite preIfRel; trivial.
+  * unfold wp; unfold provable_or_none; unfold whatever_or_none; trivial.
+Qed.
+
+Lemma provable_opt_implies_provable {pre instr post} :
+  (|-opt [|Some pre|] instr [|Some post|])%assert
+  -> (|- [|pre|] instr [|post|])%assert.
+Proof.
+  intros prf.
+  unfold provable_or_none in prf; unfold whatever_or_none in prf. assumption.
+Qed.
+
+Theorem wp_correctness (instr: Instr) :
+  forall post, ( |=opt [| wp instr post |] instr [| post |] ) % assert.
+Proof.
+  intros post.
+  destruct post as [post0 | ] eqn:post0Rel.
+  remember (wp instr (Some post0)) as pre eqn:preRel.
+  destruct pre as [ pre0 | ] eqn:pre0Rel.
+  - unfold consequence_or_none; unfold whatever_or_none.
+    apply hoare_provability_implies_consequence.
+    apply provable_opt_implies_provable.
+    rewrite preRel.
+    apply wp_correctness_provable.
+  - unfold consequence_or_none; unfold whatever_or_none; trivial.
+  - unfold wp.
+    destruct instr; unfold consequence_or_none; unfold
+    whatever_or_none; trivial.
+Qed.
 
 (* vim: ts=2 sw=2
 *)