From c161437c7f3c020f883c27a3ae26aedc29d83d05 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 7 Dec 2017 18:09:59 +0100
Subject: [PATCH] Totally prove wp correctness

---
 wp.v | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 75 insertions(+), 4 deletions(-)

diff --git a/wp.v b/wp.v
index b8c4f4e..535d245 100644
--- a/wp.v
+++ b/wp.v
@@ -476,8 +476,70 @@ Proof.
   intros F; exfalso; exact F.
 Qed.
 
+Lemma leftWeaken {instr post}:
+  forall pre,
+  (|- [|pre|] instr [|post|])%assert
+  -> (|- [|assertBot|] instr [|post|])%assert.
+Proof.
+  intros pre orig.
+  apply (H_conseq
+    assertBot post
+    pre post).
+  - assumption.
+  - unfold assertImplLogical. intros mem.
+    unfold assertBot. intros F; exfalso; assumption.
+  - apply (assertImplSelf post).
+Qed.
+
+Lemma assertBotAndStuff {res}:
+  forall assert, assertImplLogical (assertBot /\ assert)%assert (res).
+Proof.
+  intros assert. unfold assertImplLogical. unfold assertBot. unfold assertAnd.
+  intros mem [F _]. exfalso. assumption.
+Qed.
+
+Lemma preBottomIsProvable {instr post}:
+  (|- [|assertBot|] instr [|post|]) % assert.
+Proof.
+  revert post.
+  induction instr; intros post.
+  * apply (leftWeaken post); apply (H_skip post).
+  * apply (H_abort assertBot post).
+  * apply (leftWeaken (post [[ v <- expr e]])%assert ).
+    apply (H_assign post v e).
+  * specialize IHinstr2 with post; specialize IHinstr1 with assertBot.
+    apply (H_seq assertBot assertBot post).
+    assumption. assumption.
+  * apply (H_if assertBot post e instr1 instr2).
+    - apply (H_conseq
+        (assertBot /\ assertOfExpr e)%assert post
+        assertBot post).
+      + apply IHinstr1.
+      + apply (assertBotAndStuff (assertOfExpr e)).
+      + apply (assertImplSelf post).
+    - apply (H_conseq
+        (assertBot /\ ~ assertOfExpr e)%assert post
+        assertBot post).
+      + apply IHinstr2.
+      + apply (assertBotAndStuff (assertNot (assertOfExpr e))).
+      + apply (assertImplSelf post).
+  * apply (H_conseq
+      assertBot post
+      assertBot (assertBot /\ ~ (assertOfExpr e))%assert).
+    - apply (H_while assertBot e instr).
+      apply (H_conseq
+        (assertBot /\ assertOfExpr e)%assert assertBot
+        assertBot assertBot).
+      + apply IHinstr.
+      + apply (assertBotAndStuff (assertOfExpr e)).
+      + apply assertImplSelf.
+    - apply assertImplSelf.
+    - apply assertBotAndStuff.
+Qed.
+
 Theorem wp_correctness_provable (instr: Instr) :
-  forall post, ( |- [| wp instr post |] instr [| post |] ) % assert.
+  forall post,
+    ( |- [| wp instr post |] instr [| post |] ) % assert.
 Proof.
   induction instr; intros post; simpl.
   * apply (H_skip post).
@@ -487,8 +549,7 @@ Proof.
     remember (wp instr1 mid) as pre eqn:preRel.
     specialize IHinstr2 with post.
     specialize IHinstr1 with mid.
-    rewrite <- midRel in IHinstr2.
-    rewrite <- preRel in IHinstr1.
+    rewrite <- midRel in IHinstr2; rewrite <- preRel in IHinstr1.
     apply (H_seq pre mid post instr1 instr2).
     assumption. assumption.
   * remember ((assertOfExpr e -> wp instr1 post)
@@ -511,7 +572,17 @@ Proof.
         intros mem. intros [ [disjunctIf disjunctElse] isElse].
         apply (assertImplElim mem disjunctElse isElse).
       + apply (assertImplSelf post).
-  * 
+  * apply preBottomIsProvable.
+Qed.
+
+Theorem wp_correctness (instr: Instr) :
+  forall post,
+    ( |= [| wp instr post |] instr [| post |] ) % assert.
+Proof.
+  intros post.
+  apply hoare_provability_implies_consequence.
+  apply wp_correctness_provable.
+Qed.
 
 (* vim: ts=2 sw=2
 *)