From 260ac05c6e97e4a51b7f908317c15f8d6bca53c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 7 Dec 2017 16:24:27 +0100
Subject: [PATCH] Progress towards proved wp with option Assert

---
 wp.v | 84 ++++++++++++++++++++----------------------------------------
 1 file changed, 28 insertions(+), 56 deletions(-)

diff --git a/wp.v b/wp.v
index 3fa47d8..2d2d063 100644
--- a/wp.v
+++ b/wp.v
@@ -441,30 +441,16 @@ Qed.
 
 (***** Weakest precondition **************************************************)
 
-Fixpoint wp (instr: Instr) (condOpt: option Assert) : option Assert :=
-  match condOpt with
-  | None => None
-  | Some cond => match instr with
-    | skip =>
-        Some cond
-    | abort =>
-        Some assertTop
-    | assign x expr =>
-        Some (cond [[ x <- expr expr ]])
-    | seq s1 s2 =>
-        wp s1 (wp s2 condOpt)
-    | ifelse guard sIf sElse =>
-        match (wp sIf condOpt, wp sElse condOpt) with
-        | (None, _) | (_, None) => None
-        | (Some wpIf, Some wpElse) =>
-            Some (
-              ((assertOfExpr guard -> wpIf)
-              /\ (~ (assertOfExpr guard) -> wpElse)) % assert)
-        end
-    | while guard body =>
-        None
-    end
-  end.
+Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
+| skip => cond
+| abort => assertTop
+| assign x expr => (cond [[ x <- expr expr ]])
+| seq s1 s2 => wp s1 (wp s2 cond)
+| ifelse guard sIf sElse =>
+    ((assertOfExpr guard -> wp sIf cond)
+     /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
+| while guard body => assertBot
+end.
 
 Lemma assertImplElim {a b: Assert} :
   forall (m: Mem), (assertImpl a b) m -> a m -> b m.
@@ -482,40 +468,25 @@ Proof.
   unfold assertImplLogical. intros mem x. assumption.
 Qed.
 
-Definition whatever_or_none (whatever: Assert -> Instr -> Assert -> Prop)
-  (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.
+Lemma preBottomIsCorrect {instr post}:
+  (|= [|assertBot|] instr [|post|]) % assert.
 Proof.
-  intros prf. destruct post.
-  - apply prf.
-  - unfold provable_or_none; unfold whatever_or_none.
-    unfold wp; destruct instr; trivial.
+  unfold hoare_consequence. intros mem.
+  unfold assertBot.
+  intros F; exfalso; exact F.
 Qed.
 
-Theorem wp_correctness_provable (instr: Instr) :
-  forall post, ( |-opt [| wp instr post |] instr [| post |] ) % assert.
+Theorem wp_correctness (instr: Instr):
+  forall post, ( |= [| 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.
+  induction instr; intros post.
+  * apply hoare_provability_implies_consequence.
+    apply (H_skip post).
+  * apply hoare_provability_implies_consequence.
+    apply (H_abort assertTop post).
+  * apply hoare_provability_implies_consequence. apply (H_assign post v e).
+  * apply hoare_provability_implies_consequence.
+    remember (wp instr2 (Some post)) as mid eqn:midRel.
     remember (wp instr1 mid) as pre eqn:preRel.
     simpl; rewrite <- midRel; rewrite <- preRel.
     specialize IHinstr2 with (Some post0) as IHpost.
@@ -530,7 +501,8 @@ Proof.
       - unfold provable_or_none in IHmid; unfold whatever_or_none in IHmid.
         exfalso. apply IHmid.
       - unfold whatever_or_none; trivial.
-  * specialize IHinstr1 with (Some post0);
+  * apply hoare_provability_implies_consequence.
+    specialize IHinstr1 with (Some post0);
     specialize IHinstr2 with (Some post0).
     destruct (wp instr1 (Some post0)) as [preIf | ] eqn:preIfRel;
     destruct (wp instr2 (Some post0)) as [preElse | ] eqn:preElseRel.
@@ -568,7 +540,7 @@ Proof.
         rewrite preIfRel; trivial.
     - unfold provable_or_none; simpl; rewrite preElseRel;
         rewrite preIfRel; trivial.
-  * unfold wp; unfold provable_or_none; unfold whatever_or_none; trivial.
+  * unfold wp. apply preBottomIsCorrect.
 Qed.
 
 Lemma provable_opt_implies_provable {pre instr post} :