Stash th2.3 for now

wp.v

@@ -109,6 +109,34 @@ 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 instr (nth_iterate instr m)
+    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 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. 
+Admitted.
+
 (***** Validite, prouvabilite pour Hoare *************************************)
 
 Definition Assert := Mem -> Prop.
@@ -255,3 +283,11 @@ Proof.
           unfold assertAnd. split.
             + assumption.
             + rewrite <- Z.eqb_eq. congruence.
+    - 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.
+Admitted.
+