Implement and prove wps

This mostly reverts commit c2c58119be.
The theorems will be slightly different and should be way cleaner.

wp.v

@@ -3,6 +3,8 @@
 (***** Partie 1 : definition de While ****************************************)
 
 Require Import ZArith.BinInt.
+Require Import FunctionalExtensionality.
+Require Import Omega.
 Import Z.
 
 Definition Var := nat.
@@ -223,7 +225,6 @@ Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
     forall pre, forall post,
     forall pre', forall post',
     forall s,
-
     (|- [| pre' |] s [| post' |]) % assert ->
       (assertImplLogical pre pre') ->
       (assertImplLogical post' post) ->
@@ -297,6 +298,20 @@ Proof.
     unfold MemElem; unfold MemError; congruence.
 Qed.
 
+Lemma expr_neg_consistency (expr: Expr):
+  forall mem, expr_neg expr mem <> 0%Z -> (~ assertOfExpr expr)%assert mem.
+Proof.
+  intros mem. intros src.
+  unfold assertNot. unfold assertOfExpr. destruct (expr mem) eqn:exprRel.
+  + congruence.
+  + elimtype False.
+    unfold expr_neg in src; rewrite exprRel in src. apply src.
+    congruence.
+  + elimtype False.
+    unfold expr_neg in src; rewrite exprRel in src. apply src.
+    congruence.
+Qed.
+
 Lemma Sn_noerror_n_noerror (n: nat) (s: Instr) (sMem: Mem) (m: Mem):
   interp (nth_iterate s (S n)) (MemElem sMem)  = MemElem m
   -> exists m0, interp (nth_iterate s n) (MemElem sMem) = MemElem m0
@@ -312,6 +327,42 @@ Proof.
     * rewrite <- nRel; simpl. apply HSn.
 Qed.
 
+
+Lemma greater_n_noerror (n1 n2: nat) (s: Instr) (sMem: Mem) (m: Mem):
+  n1 < n2
+  -> interp (nth_iterate s n2) (MemElem sMem) = MemElem m
+  -> exists m0, interp (nth_iterate s n1) (MemElem sMem) = MemElem m0.
+Proof.
+  intros nRel eventuallySound.
+  assert (forall nDecr, nDecr <= n2 - n1 ->
+    exists m0,
+    interp (nth_iterate s (n2 - nDecr)) (MemElem sMem) = MemElem m0).
+    * intros mDecr mDecrRel. induction mDecr.
+      + exists m.
+        assert (n2 = n2 - 0).
+        { unfold Nat.sub. destruct n2; trivial. }
+        { rewrite <- H. assumption. }
+      + assert (mDecr <= n2 - n1).
+        { omega. }
+        { elim (IHmDecr H). intros memNext memNextRel.
+          elim (Sn_noerror_n_noerror (n2 - (S mDecr)) s sMem memNext).
+          intros memNow [memNowRel memNowInterp].
+          exists memNow. apply memNowRel.
+          assert (S (n2 - S mDecr) = n2 - mDecr). omega.
+          rewrite H0. apply memNextRel.
+        }
+    * assert (n2 - n1 <= n2 - n1). omega. elim (H (n2 - n1) H0).
+      intros memRes memResRel. exists memRes.
+      assert (n2 - (n2 - n1) = n1). omega. rewrite H1 in memResRel.
+      assumption.
+Qed.
+
+Lemma unwrap_CpoElem (T: Type) :
+  forall m1 m2, CpoElem T m1 = CpoElem T m2 -> m1 = m2.
+Proof.
+  intros m1 m2 cpoEq. congruence.
+Qed.
+
 Theorem hoare_provability_implies_consequence :
   forall (pre: Assert), forall (s: Instr), forall (post: Assert),
   ( |- [| pre |] s [| post |] ) % assert
@@ -342,56 +393,264 @@ Proof.
     destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel.
     * trivial.
     * elim (certain_termination sBody expr (MemElem mem)).
-        intros n. intros [lastIter [notLastIter isWhile] ].
+      intros n [lastIter [notLastIter isWhile] ].
       rewrite isWhile in interpRel.
-        split.
-        + 
-          apply conseq_or_bottom_is_conseq. unfold MemElem.
+      destruct n.
+      {
+        simpl in lastIter. simpl in interpRel; unfold MemElem in interpRel.
+        unfold assertAnd. apply (unwrap_CpoElem Mem) in interpRel. split.
+        { rewrite interpRel in preInMem; assumption. }
+        { apply expr_neg_consistency; rewrite <- interpRel; assumption. }
+      }
+      unfold assertAnd; split.
+      + apply conseq_or_bottom_is_conseq. unfold MemElem.
         rewrite <- interpRel.
-          induction n; simpl.
-            { assumption. }
-            { elim (Sn_noerror_n_noerror n sBody mem m interpRel).
-              intros memN [relMemN stepMemN].
+        assert (forall n1, n1 <= (S n) ->
+          conseq_or_bottom inv
+            (interp (nth_iterate sBody n1) (MemElem mem))).
+        { induction n1.
+          { intros obvious. simpl. assumption. }
+          { intros order; simpl.
+            unfold hoare_consequence in IHdeduction.
+            assert (n1 < S n) as nOrder. omega.
+            elim (greater_n_noerror n1 (S n) sBody mem m nOrder interpRel).
+            intros memN relMemN.
             specialize (IHdeduction memN) as IHmem.
-              rewrite stepMemN in IHmem.
             rewrite relMemN.
-              rewrite relMemN in IHn.
-              rewrite stepMemN.
             apply IHmem.
             unfold assertAnd; split.
-                { admit. }
+            { rewrite relMemN in IHn1; unfold MemElem in IHn1.
+              apply IHn1. omega.
+            }
             { unfold assertOfExpr.
-                  specialize (notLastIter n).
+              specialize (notLastIter n1).
               rewrite relMemN in notLastIter.
               unfold satisfies_expr in notLastIter; simpl in notLastIter.
-                  apply notLastIter. unfold Peano.lt. trivial. }
+              apply notLastIter. assumption.
+            }
+          }
+        }
+        {
+          apply H. omega.
         }
       + unfold assertNot; unfold assertOfExpr. rewrite interpRel in lastIter.
         unfold satisfies_expr in lastIter.
         unfold expr_neg in lastIter.
         destruct (expr m); simpl; congruence.
       + rewrite interpRel; unfold MemError; congruence.
-Admitted.
+Qed.
 
 (***** Weakest precondition **************************************************)
 
 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)
+| 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 sIf cond)
      /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
-| while guard body => assertTop
+| while guard body => assertBot
 end.
 
-Theorem wp_correctness (instr: Instr) (post: Assert) :
+Lemma assertImplElim {a b: Assert} :
+  forall (m: Mem), (assertImpl a b) m -> a m -> b m.
+Proof.
+  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.
+
+Lemma preBottomIsCorrect {instr post}:
+  (|= [|assertBot|] instr [|post|]) % assert.
+Proof.
+  unfold hoare_consequence. intros mem.
+  unfold assertBot.
+  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.
+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).
+  * apply preBottomIsProvable.
+Qed.
+
+Theorem wp_correctness (instr: Instr) :
+  forall post,
     ( |= [| wp instr post |] instr [| post |] ) % assert.
 Proof.
-    (* TODO *)
-Admitted.
+  intros post.
+  apply hoare_provability_implies_consequence.
+  apply wp_correctness_provable.
+Qed.
+
+(***** Assertions syntaxiques******** ****************************************)
+
+Inductive SynAssert : Type:=
+| ATop: SynAssert
+| ABot: SynAssert
+| ANeg: SynAssert -> SynAssert
+| AAnd: SynAssert -> SynAssert -> SynAssert
+| AOr: SynAssert -> SynAssert -> SynAssert
+| AImplies: SynAssert -> SynAssert -> SynAssert
+| AExpr: Expr -> SynAssert
+| AForall: Var -> SynAssert -> SynAssert
+| AExists: Var -> SynAssert -> SynAssert
+| ASubstZ: Var -> Z -> SynAssert -> SynAssert
+| ASubstE: Var -> Expr -> SynAssert -> SynAssert.
+
+Fixpoint aInterp (src: SynAssert): Assert :=
+  fun (mem: Mem) => match src with
+  | ATop => True
+  | ABot => False
+  | ANeg x => ~ (aInterp x mem)
+  | AAnd x y => (aInterp x mem) /\ (aInterp y mem)
+  | AOr x y => (aInterp x mem) \/ (aInterp y mem)
+  | AImplies x y => (~ (aInterp x mem)) \/ (aInterp y mem)
+  | AExpr exp => exp mem <> 0%Z
+  | AForall v x => forall (z: Z), aInterp x (mem [v <- z])
+  | AExists v x => exists (z: Z), aInterp x (mem [v <- z])
+  | ASubstZ v z x => aInterp x (mem [v <- z])
+  | ASubstE v e x => aInterp x (mem [v <- (e mem)])
+  end.
+
+Fixpoint wps (instr: Instr) (asser: SynAssert) : SynAssert := match instr with
+| skip => asser
+| abort => ATop
+| assign x expr => ASubstE x expr asser
+| seq s1 s2 => wps s1 (wps s2 asser)
+| ifelse guard sIf sElse =>
+    AAnd
+      (AImplies (AExpr guard) (wps sIf asser))
+      (AImplies (ANeg (AExpr guard)) (wps sElse asser))
+| while guard body => ABot
+end.
+
+Lemma aInterpConsistent (instr: Instr):
+  forall post, aInterp (wps instr post) = wp instr (aInterp post).
+Proof.
+  induction instr; intros post; simpl; trivial.
+  * (* sequence *)
+    rewrite <- (IHinstr2 post).
+    rewrite (IHinstr1 (wps instr2 post)).
+    congruence.
+  * (* if/else *)
+    rewrite <- (IHinstr2 post).
+    rewrite <- (IHinstr1 post).
+    unfold assertAnd; unfold assertImpl; unfold assertOfExpr; unfold assertOr;
+      unfold assertNot; simpl.
+    apply functional_extensionality; intros mem; simpl. congruence.
+Qed.
+
+Theorem wps_correctness (instr: Instr):
+  forall post,
+    ( |= [| aInterp (wps instr post) |] instr [| aInterp post |] ) % assert.
+Proof.
+  intro post.
+  rewrite (aInterpConsistent instr).
+  apply wp_correctness.
+Qed.
+
+(* vim: ts=2 sw=2
+*)