Fix final soundness proofs to also have correct conclusion

coq/CertificateChecker.v

@@ -37,7 +37,9 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVar
    exists vR vF m,
     eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
     eval_exp E2 defVars (toRExp e) vF m /\
-    (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
+    (forall vF m,
+        eval_exp E2 defVars (toRExp e) vF m ->
+        (Rabs (vR - vF) <= Q2R (snd (absenv e))))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
@@ -66,15 +68,16 @@ Proof.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty. }
   edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
-  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [vF [mF [eval_float err_bounded]]]; auto.
+  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
   exists vR; exists vF; exists mF; split; auto.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
   if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
-       then if (validIntervalboundsCmd f absenv P NatSet.empty)
-            then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
-            else false
+  then
+    if (validIntervalboundsCmd f absenv P NatSet.empty)
+    then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
+    else false
   else false.
 
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
@@ -90,7 +93,9 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
     exists vR vF m,
     bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
     bstep (toRCmd f) E2 defVars vF m /\
-    (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
+    (forall vF m,
+        bstep (toRCmd f) E2 defVars vF m ->
+        (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R).
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
@@ -124,6 +129,9 @@ Proof.
     as freeVars_contained by set_tac.
   edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
   rewrite absenv_eq; simpl.
-  edestruct (validErrorboundCmd_sound) as [vF [mF [eval_float bounded_float]]]; eauto.
-  exists vR; exists vF; exists mF; split; auto.
+  edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
+  exists vR; exists vF; exists mF; split; try auto.
+  split; try auto.
+  intros.
+  eapply validErrorboundCmd_sound; eauto.
 Qed.
\ No newline at end of file