From cd467dc8b05f2059b96345e77e3f0b2f6f4090ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 7 Dec 2017 16:55:47 +0100
Subject: [PATCH] Revert before introduction of option Assert

This mostly reverts commit c2c58119be4ae8b1f25b12d3e9b34a276d8ca015.
The theorems will be slightly different and should be way cleaner.
---
 wp.v | 124 ++++++++++++++++-------------------------------------------
 1 file changed, 34 insertions(+), 90 deletions(-)

diff --git a/wp.v b/wp.v
index 2d2d063..b8c4f4e 100644
--- a/wp.v
+++ b/wp.v
@@ -476,98 +476,42 @@ Proof.
   intros F; exfalso; exact F.
 Qed.
 
-Theorem wp_correctness (instr: Instr):
-  forall post, ( |= [| wp instr post |] instr [| post |] ) % assert.
+Theorem wp_correctness_provable (instr: Instr) :
+  forall post, ( |- [| wp instr post |] instr [| post |] ) % assert.
 Proof.
-  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.
+  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.
-    simpl; rewrite <- midRel; rewrite <- preRel.
-    specialize IHinstr2 with (Some post0) as IHpost.
-    specialize IHinstr1 with mid as IHmid.
-    rewrite <- midRel in IHpost; rewrite <- preRel in IHmid.
-    destruct mid as [mid0 | ] eqn:mid0Rel.
-    destruct pre as [pre0 | ] eqn: pre0Rel.
-    apply (H_seq pre0 mid0 post0).
-    apply IHmid. apply IHpost.
-    + unfold whatever_or_none; trivial.
-    + destruct pre.
-      - unfold provable_or_none in IHmid; unfold whatever_or_none in IHmid.
-        exfalso. apply IHmid.
-      - unfold whatever_or_none; trivial.
-  * 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.
-    remember ((assertOfExpr e -> preIf)
-              /\ (~ assertOfExpr e -> preElse)) % assert
-              as pre0 eqn:pre0Rel.
-    assert (wp (ifelse e instr1 instr2) (Some post0) = (Some pre0)).
-    {
-      rewrite pre0Rel; simpl; rewrite preIfRel; rewrite preElseRel; congruence.
-    }
-    {
-      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. apply preBottomIsCorrect.
-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.
+    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
 *)