From 27389f132f9669d0ec954e87f5c0d379fcb28718 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 7 Dec 2017 01:09:29 +0100
Subject: [PATCH] Prove good part of wp_correctness_provable

---
 wp.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 52 insertions(+), 4 deletions(-)

diff --git a/wp.v b/wp.v
index 9bd03c5..cd258ed 100644
--- a/wp.v
+++ b/wp.v
@@ -451,15 +451,63 @@ Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
 | seq s1 s2 =>
     wp s1 (wp s2 cond)
 | ifelse guard sIf sElse =>
-    (assertOfExpr guard -> wp sIf cond
+    ((assertOfExpr guard -> wp sIf cond)
     /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
 | while guard body => assertTop
 end.
 
-Theorem wp_correctness (instr: Instr) (post: Assert) :
-  ( |= [| wp instr post |] instr [| post |] ) % assert.
+Lemma assertImplElim {a b: Assert} :
+  forall (m: Mem), (assertImpl a b) m -> a m -> b m.
 Proof.
-Admitted.
+  intros mem impl pa.
+  unfold assertImpl in impl; unfold assertOr in impl.
+  destruct impl.
+  * elimtype False. unfold assertNot in H. apply (H pa).
+  * assumption.
+Qed.
+
+Lemma assertImplSelf (a: Assert) :
+  assertImplLogical a a.
+Proof.
+  unfold assertImplLogical. intros mem x. assumption.
+Qed.
+
+Theorem wp_correctness_provable (instr: Instr) :
+  forall post, ( |- [| wp instr post |] instr [| post |] ) % assert.
+Proof.
+  induction instr; intros post; simpl.
+  * apply (H_skip post).
+  * apply (H_abort assertTop post).
+  * apply (H_assign post v e).
+  * remember (wp instr2 post) as mid eqn:midRel.
+    remember (wp instr1 mid) as pre eqn:preRel.
+    specialize IHinstr2 with post.
+    specialize IHinstr1 with mid.
+    rewrite <- midRel in IHinstr2.
+    rewrite <- preRel in IHinstr1.
+    apply (H_seq pre mid post instr1 instr2).
+    assumption. assumption.
+  * remember ((assertOfExpr e -> wp instr1 post)
+              /\ (~ assertOfExpr e -> wp instr2 post)) % assert
+      as pre eqn:preRel.
+    apply (H_if pre post e instr1 instr2).
+    - apply (H_conseq
+        (pre /\ assertOfExpr e)%assert post
+        (wp instr1 post) post instr1
+        (IHinstr1 post)).
+      + rewrite preRel. unfold assertImplLogical.
+        intros mem. intros [ [disjunctIf disjunctElse] isIf].
+        apply (assertImplElim mem disjunctIf isIf).
+      + apply (assertImplSelf post).
+    - apply (H_conseq
+        (pre /\ ~ assertOfExpr e)%assert post
+        (wp instr2 post) post instr2
+        (IHinstr2 post)).
+      + rewrite preRel. unfold assertImplLogical.
+        intros mem. intros [ [disjunctIf disjunctElse] isElse].
+        apply (assertImplElim mem disjunctElse isElse).
+      + apply (assertImplSelf post).
+  * 
 
 (* vim: ts=2 sw=2
 *)