From 2431f66b076eb9636807c13e47c9bfcc412d3483 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Wed, 6 Dec 2017 11:17:17 +0100
Subject: [PATCH] Stash th2.3 for now

---
 wp.v | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/wp.v b/wp.v
index dde3ed2..44bf484 100644
--- a/wp.v
+++ b/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.
+