Update README

README.md

@@ -2,5 +2,30 @@
 
 Projet de cours Coq (2.7.1) du MPRI — WP.
 
-Deadline : probablement jusqu'à ~exam, rien de fixe.
-(Examen : probablement 30/11, ~14h)
+Sujet
+[ici](http://www.enseignement.polytechnique.fr/informatique/MPRI/2-7-1/wp.html).
+
+## 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

@@ -76,6 +76,12 @@ Axiom find_lub_correct:
   is_chain chain -> is_lub_of chain (find_lub chain).
 Arguments find_lub_correct {T} {chain} _.
 
+Axiom lub_is_first_correct:
+  forall (T: Type), forall (n: nat), forall (chain: Sequence (cpo T)),
+  is_chain chain
+  -> chain n = CpoError T
+  -> chain (S n) <> CpoError T
+  -> find_lub chain = chain (S n).
 (***** Interpretation ********************************************************)
 
 Definition subst: Mem -> Var -> Z -> Mem :=
@@ -160,6 +166,55 @@ Proof.
   intros not_error.
 Admitted.
 
+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 bool_prop_contradict {x: Z}:
+  (x <> 0)%Z -> (x =? 0)%Z = true -> False.
+Proof.
+  intros diff equ. apply diff.
+  unfold eqb in equ; destruct x; simpl; trivial;
+    exfalso; apply (Bool.Bool.diff_false_true); assumption.
+Qed.
+
+Lemma before_n_useless_guard {body guard n mem}:
+  (forall p, p < n
+    -> (interp (nth_iterate (ifonly guard body) p) mem) |=e guard)
+  -> forall p, p <= n ->
+    (interp (nth_iterate body p) mem)
+    = (interp (nth_iterate (ifonly guard body) p) mem).
+Proof.
+  intros matchGuard p infN.
+  induction p.
+  - unfold nth_iterate; trivial.
+  - assert (p < n). omega. assert (p <= n). omega.
+    apply IHp in H0 as IHp0.
+    destruct mem eqn:mRel; [simpl; trivial | ].
+    fold MemElem; rewrite (unfold_one_iter body m p);
+      rewrite (unfold_one_iter (ifonly guard body) m p).
+    fold MemElem in IHp0; rewrite IHp0.
+    remember (interp (nth_iterate body p) (MemElem m))
+      as stepMem eqn:stepMemRel.
+    remember (interp (nth_iterate (ifonly guard body) p) (MemElem m))
+      as fancyStepMem eqn:fancyStepMemRel.
+    specialize matchGuard with p.
+    apply matchGuard in H as matchGuardP.
+    fold MemElem in matchGuardP.
+    rewrite <- fancyStepMemRel in matchGuardP.
+    rewrite <- IHp0 in matchGuardP.
+    destruct fancyStepMem.
+    * destruct body; simpl; trivial.
+    * unfold satisfies_expr in matchGuardP.
+      destruct (guard m0 =? 0)%Z eqn:guardRel.
+      + rewrite IHp0 in matchGuardP.
+        exfalso; apply (bool_prop_contradict matchGuardP guardRel).
+      + unfold ifonly; simpl; rewrite guardRel; congruence.
+Qed.
+
 Lemma certain_termination assert body guard mem :
   interp (while assert guard body) mem <> MemError ->
     exists n: nat,
@@ -168,9 +223,17 @@ Lemma certain_termination assert body guard mem :
      /\ interp (while assert guard body) mem = interp (nth_iterate body n) mem.
 Proof.
   intros notError.
-  elim (certain_termination_exists_minimal assert body guard mem).
-  intros n. intros [notBeforeN atN]. exists n.
-  split.
+  destruct (certain_termination_exists_minimal assert body guard mem) as [n];
+    trivial.
+  destruct H as [beforeN atN].
+  exists n.
+  split; [|split].
+  - assert (n <= n). omega. rewrite (before_n_useless_guard beforeN n H).
+    assumption.
+  - intros p infN. assert (p <= n). omega.
+    rewrite (before_n_useless_guard beforeN p H ).
+    apply beforeN; trivial.
+  - admit.
 Admitted.
 
 (***** Validite, prouvabilite pour Hoare *************************************)
@@ -297,13 +360,6 @@ 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.