Remove a few admitted points for certain_termination

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.