Prove 2.3 assuming 1.6

wp.v

@@ -3,6 +3,7 @@
 (***** Partie 1 : definition de While ****************************************)
 
 Require Import ZArith.BinInt.
+Require Import Omega.
 Import Z.
 
 Definition Var := nat.
@@ -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,36 +393,51 @@ 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 **************************************************)