[WIP] Try proving certain_termination

DOES NOT WORK at this point, this is WIP.

README.md

@@ -2,30 +2,5 @@
 
 Projet de cours Coq (2.7.1) du MPRI — WP.
 
-Sujet
+Deadline : probablement jusqu'à ~exam, rien de fixe.
-[ici](http://www.enseignement.polytechnique.fr/informatique/MPRI/2-7-1/wp.html).
+(Examen : probablement 30/11, ~14h)
-
-## Résultats admis
-
-* Une partie de `certain_termination` a été admise (il s'agit du lemme 1.6 du
-  sujet). En particulier, les propriétés souhaitées sur `n` sont dérivées d'un
-  lemme admis moins fort qui donne l'existence de `n`
-  (`certain_termination_exists_minimal`).
-
-* Le point (3) de ce lemme a égalememnt été admis, il aurait dû être prouvé à
-  partir de l'axiome `lub_is_first_correct`.
-
-## Résultats obtenus
-
-Toutes les étapes du sujet jusqu'à la 8 (incluse) ont été traitées,
-c'est-à-dire que `wp` et `wps` sont définies et prouvées correctes, à
-l'exception des boucles `while`. Les invariants sont présents dans la
-structure, mais on pose `wp(while _, φ) = Bottom`. Autrement dit, **dès lors
-qu'un `while` est présent**, `wp(_, _)` devient **bottom**. Ceci est toujours
-vrai, et est prouvé dans le projet.
-
-## Ce qui n'est **pas** fait
-
-Les invariants ne sont **pas** pris en compte. Tout est en place pour, mais
-j'ai manqué de temps sur la fin pour finir ce projet. J'ai simplement eu du mal
-à adapter la preuve de `wp` (et la preuve de `wps` aurait immédiatement suivi).

wp.v

@@ -233,8 +233,27 @@ Proof.
   - intros p infN. assert (p <= n). omega.
     rewrite (before_n_useless_guard beforeN p H ).
     apply beforeN; trivial.
-  - admit.
+  - assert (n <= n). omega. rewrite (before_n_useless_guard beforeN n H).
-Admitted.
+    destruct mem as [mem0|] eqn:memRel.
+    { simpl in notError. exfalso; apply notError; trivial. }
+    remember (fun n => interp (nth_iterate (ifonly guard body) n) mem)
+      as chain eqn:chainRel.
+    assert (chain (S n) = MemError) as nLastValid.
+    {
+      rewrite chainRel. rewrite memRel. fold MemElem; fold MemElem in atN.
+      rewrite (unfold_one_iter (ifonly guard body) m n).
+      remember (interp (nth_iterate (ifonly guard body) n) (MemElem m))
+        as memN.
+      simpl.
+      destruct memN; trivial.
+      simpl in atN. unfold expr_neg in atN.
+      destruct (guard m0); simpl; trivial.
+      * exfalso. apply atN. congruence.
+    assert (forall n, chain n cpo<= chain (S n)) as incrChainRel.
+    * intros n0. rewrite chainRel. unfold cpo_leq.
+      destruct (n0 <=? n).
+    assert (find_lub_correct
+Qed.
 
 (***** Validite, prouvabilite pour Hoare *************************************)