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

wp.v

@@ -109,6 +109,55 @@ Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
         end
     end.
 
+Fixpoint nth_iterate (instr: Instr) (n: nat) : Instr :=
+    match n with
+    | 0 => skip
+    | S m => seq (nth_iterate instr m) instr
+    end.
+
+Definition satisfies_expr (mem: MemCpo) (expr: Expr) : Prop := match mem with
+| CpoError _ => False
+| CpoElem _ mem0 => (expr mem0 <> 0) % Z
+end.
+Infix "|=e" := satisfies_expr (at level 32).
+
+Definition expr_neg (expr: Expr) : Expr :=
+    fun mem => match expr mem with
+    | 0%Z => 1%Z
+    | _ => 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)
+         /\ interp (while guard body) mem = interp (nth_iterate body n) mem.
+Proof.
+    intros notError.
+    elim (certain_termination_exists_minimal body guard mem).
+    intros n. intros [notBeforeN atN]. exists n.
+    split.
+Admitted.
+
 (***** Validite, prouvabilite pour Hoare *************************************)
 
 Definition Assert := Mem -> Prop.
@@ -222,6 +271,46 @@ Proof.
     - simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
 Qed.
 
+Lemma interp_of_error (s: Instr):
+    interp s (MemError) = MemError.
+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),
@@ -229,18 +318,18 @@ Theorem hoare_provability_implies_consequence :
             -> ( |= [| pre |] s [| post |] ) % assert.
 Proof.
     intros pre instr post. intros deduction.
-    induction deduction; intros mem preInMem; simpl.
+    induction deduction; intros mem preInMem.
     - exact preInMem.
-    - trivial.
+    - simpl; trivial.
     - exact preInMem.
     - apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
       apply IHdeduction. apply H. exact preInMem.
-    - destruct (interp s1 (MemElem mem)) eqn:mRel.
-        admit.
-        apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
-        specialize IHdeduction1 with mem as IH1_mem.
-        rewrite mRel in IH1_mem. apply IH1_mem. assumption.
-    - destruct (expr mem =? 0)%Z eqn:branchEqn.
+    - simpl; destruct (interp s1 (MemElem mem)) eqn:mRel.
+        * fold MemError. rewrite (interp_of_error s2); simpl; trivial.
+        * apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
+          specialize IHdeduction1 with mem as IH1_mem.
+          rewrite mRel in IH1_mem. apply IH1_mem. assumption.
+    - simpl; destruct (expr mem =? 0)%Z eqn:branchEqn.
         * apply (IHdeduction2 mem). unfold assertOfExpr.
           unfold assertAnd. split.
             + assumption.
@@ -249,3 +338,60 @@ Proof.
           unfold assertAnd. split.
             + assumption.
             + rewrite <- Z.eqb_eq. congruence.
+    - unfold conseq_or_bottom.
+      destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel.
+      * trivial.
+      * 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 **************************************************)
+
+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)
+| ifelse guard sIf sElse =>
+        (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.
+Proof.
+    (* TODO *)
+Admitted.