Nearly prove Th2.3, assuming 1.6 and one small subgoal

wp.v

@@ -112,7 +112,7 @@ Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
 Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr :=
     match n with
     | 0 => skip
-    | S m => seq instr (nth_iterate instr m)
+    | S m => seq (nth_iterate instr m) instr
     end.
 
 Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with
@@ -127,14 +127,35 @@ Definition expr_neg (expr: Expr) : Expr :=
     | _ => 0%Z
     end.
 
+Lemma certain_termination_exists body guard mem :
+    interp (while guard body) mem <> MemError ->
+        exists n: nat,
+            interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
+Proof.
+    intros noError.
+Admitted.
+
+Lemma certain_termination_exists_minimal body guard mem :
+    interp (while guard body) mem <> MemError ->
+        exists n: nat,
+            (forall p: nat, p < n ->
+                interp (nth_iterate (ifonly guard body) p) mem |=e guard)
+         /\ interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
+Proof.
+    intros not_error.
+Admitted.
+
 Lemma certain_termination body guard mem :
     interp (while guard body) mem <> MemError ->
         exists n: nat,
             (interp (nth_iterate body n) mem) |=e (expr_neg guard)
-         /\ forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard
+         /\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard)
          /\ interp (while guard body) mem = interp (nth_iterate body n) mem.
 Proof.
-    intros notError. 
+    intros notError.
+    elim (certain_termination_exists_minimal body guard mem).
+    intros n. intros [notBeforeN atN]. exists n.
+    split.
 Admitted.
 
 (***** Validite, prouvabilite pour Hoare *************************************)
@@ -256,6 +277,40 @@ Proof.
     unfold MemError. destruct s; cbv; trivial.
 Qed.
 
+Lemma conseq_or_bottom_is_conseq (y: Assert) (m: Mem) :
+    conseq_or_bottom y (MemElem m) -> y m.
+Proof.
+    intros src; unfold conseq_or_bottom; simpl; trivial.
+Qed.
+
+Lemma unfold_one_iter (s: Instr) (m: Mem) (n: nat):
+    interp (nth_iterate s (S n)) (MemElem m)
+    = interp s (interp (nth_iterate s n) (MemElem m)).
+Proof.
+    simpl; congruence.
+Qed.
+
+Lemma error_leads_to_no_success s:
+    forall m, interp s MemError <> MemElem m.
+Proof.
+    intros mem. unfold interp; destruct s; simpl ;
+        unfold MemElem; unfold MemError; 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
+       /\ interp s (MemElem m0) = MemElem m.
+Proof.
+    intro HSn.
+    destruct (interp (nth_iterate s n) (MemElem sMem)) eqn:nRel.
+    - rewrite (unfold_one_iter s sMem n) in HSn.
+      rewrite nRel in HSn. apply error_leads_to_no_success in HSn.
+      elimtype False. apply HSn.
+    - exists m0; unfold MemElem. split.
+      * trivial.
+      * rewrite <- nRel; simpl. apply HSn.
+Qed.
 
 Theorem hoare_provability_implies_consequence :
     forall (pre: Assert), forall (s: Instr), forall (post: Assert),
@@ -286,9 +341,36 @@ Proof.
     - unfold conseq_or_bottom.
       destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel.
       * trivial.
-      * unfold assertAnd. split.
-        + specialize (IHdeduction m) as IHdeduction_m.
-          unfold conseq_or_bottom in IHdeduction_m.
+      * elim (certain_termination sBody expr (MemElem mem)).
+        intros n. intros [lastIter [notLastIter isWhile] ].
+        rewrite isWhile in interpRel.
+        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].
+              specialize (IHdeduction memN) as IHmem.
+              rewrite stepMemN in IHmem.
+              rewrite relMemN.
+              rewrite relMemN in IHn.
+              rewrite stepMemN.
+              apply IHmem.
+              unfold assertAnd; split.
+                { admit. }
+                { unfold assertOfExpr.
+                  specialize (notLastIter n).
+                  rewrite relMemN in notLastIter.
+                  unfold satisfies_expr in notLastIter; simpl in notLastIter.
+                  apply notLastIter. unfold Peano.lt. trivial. }
+            }
+        + 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.
 
 (***** Weakest precondition **************************************************)