Rework evaluation semantics to not be arguing about precondition, make this...

Rework evaluation semantics to not be arguing about precondition, make this explicit in the theorem, that we assume it. Admitted proofs that are obvious

coq/CertificateChecker.v

@@ -22,9 +22,12 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
 **)
 Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
   forall (E1 E2:env) (vR:R) (vF:R) fVars,
+    (forall v, NatSet.mem v (Expressions.freeVars e)= true ->
+          exists vR, E1 v = Some vR /\
+                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     approxEnv E1 absenv fVars NatSet.empty E2 ->
-    eval_exp 0%R E1 P (toRExp e) vR ->
-    eval_exp (Q2R machineEpsilon) E2 P (toRExp e) vF ->
+    eval_exp 0%R E1 (toRExp e) vR ->
+    eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
     CertificateChecker e absenv P = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
 (**
@@ -32,7 +35,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
    validator and the error bound validator.
 **)
 Proof.
-  intros VarEnv1 VarEnv2 ParamEnv vR vF approxC1C2 eval_real eval_float certificate_valid.
+  intros VarEnv1 VarEnv2 ParamEnv vR vF P_valid approxC1C2 eval_real eval_float certificate_valid.
   unfold CertificateChecker in certificate_valid.
   andb_to_prop certificate_valid.
   assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
@@ -45,7 +48,8 @@ Proof.
   rewrite NatSet.mem_spec in v_in_empty.
   hnf in v_in_empty.
   inversion v_in_empty.
-Qed.
+  admit.
+Admitted.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
   andb (validIntervalboundsCmd f absenv P NatSet.empty)
@@ -53,10 +57,13 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :
 
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
   forall (E1 E2:env) outVars vR vF fVars,
+    (forall v, NatSet.mem v fVars= true ->
+          exists vR, E1 v = Some vR /\
+                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     approxEnv E1 absenv fVars NatSet.empty E2 ->
     ssaPrg f fVars outVars ->
-    bstep (toRCmd f) E1 P 0 vR ->
-    bstep (toRCmd f) E2 P (Q2R machineEpsilon) vF ->
+    bstep (toRCmd f) E1 0 vR ->
+    bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
     CertificateCheckerCmd f absenv P = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
 (**
@@ -64,7 +71,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
    validator and the error bound validator.
 **)
 Proof.
-  intros E1 E2 outVars vR vF fVars approxC1C2 ssa_f eval_real eval_float
+  intros E1 E2 outVars vR vF fVars P_valid approxC1C2 ssa_f eval_real eval_float
          certificate_valid.
   unfold CertificateCheckerCmd in certificate_valid.
   andb_to_prop certificate_valid.

coq/Commands.v

@@ -29,14 +29,14 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
 (**
   Analogously define Big Step semantics for the Daisy language
  **)
-Inductive bstep : cmd R -> env -> precond -> R -> R -> Prop :=
-  let_b x e s E P v eps res:
-    eval_exp eps E P e v ->
-    bstep s (updEnv x v E) P eps res ->
-    bstep (Let x e s) E P eps res
- |ret_b e E P v eps:
-    eval_exp eps E P e v ->
-    bstep (Ret e) E P eps v.
+Inductive bstep : cmd R -> env -> R -> R -> Prop :=
+  let_b x e s E v eps res:
+    eval_exp eps E e v ->
+    bstep s (updEnv x v E) eps res ->
+    bstep (Let x e s) E eps res
+ |ret_b e E v eps:
+    eval_exp eps E e v ->
+    bstep (Ret e) E eps v.
 
 Fixpoint freeVars (f:cmd Q) :NatSet.t :=
   match f with

coq/ErrorBounds.v

@@ -7,9 +7,9 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
 Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
-Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
-  eval_exp 0%R E1 P (Const n) nR ->
-  eval_exp (Q2R machineEpsilon) E2 P (Const n) nF ->
+Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
+  eval_exp 0%R E1 (Const n) nR ->
+  eval_exp (Q2R machineEpsilon) E2 (Const n) nF ->
   (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
 Proof.
   intros eval_real eval_float.
@@ -42,13 +42,13 @@ Qed.
 *)
 
 Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (P1 P2:precond) (err1 err2 :Q):
-  eval_exp 0%R E1 P1 (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e1) e1F ->
-  eval_exp 0%R E1 P1 (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e2) e2F ->
-  eval_exp 0%R E1 P1 (Binop Plus (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) P2 (Binop Plus (Var R 1) (Var R 2)) vF ->
+      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q):
+  eval_exp 0%R E1 (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
+  eval_exp 0%R E1 (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
+  eval_exp 0%R E1 (Binop Plus (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var R 1) (Var R 2)) vF ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
   (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
@@ -70,11 +70,11 @@ Proof.
   unfold perturb; simpl.
   inversion H4; subst; inversion H5; subst.
   unfold updEnv; simpl.
-  unfold updEnv in H0,H7; simpl in *.
-  symmetry in H0, H7.
-  inversion H0; inversion H7; subst.
+  unfold updEnv in H0,H1; simpl in *.
+  symmetry in H0, H1.
+  inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H7.
+  clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -87,7 +87,7 @@ Proof.
   pose proof (Rabs_triang (e2R + - e2F) (- ((e1F + e2F) * delta))).
   pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
   eapply Rle_trans.
-  apply H4.
+  apply H1.
   rewrite <- Rplus_assoc.
   repeat rewrite <- Rsub_eq_Ropp_Rplus.
   rewrite Rabs_Ropp.
@@ -105,13 +105,13 @@ Qed.
   Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
 **)
 Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
-      (e2F:R) (vR:R) (vF:R) (E1 E2:env) P1 P2 err1 err2:
-  eval_exp 0%R E1 P1 (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e1) e1F ->
-  eval_exp 0%R E1 P1 (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e2) e2F ->
-  eval_exp 0%R E1 P1 (Binop Sub (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) P2 (Binop Sub (Var R 1) (Var R 2)) vF ->
+      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2:
+  eval_exp 0%R E1 (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) E2   (toRExp e1) e1F ->
+  eval_exp 0%R E1 (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
+  eval_exp 0%R E1 (Binop Sub (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
   (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
@@ -133,9 +133,9 @@ Proof.
   unfold perturb; simpl.
   inversion H4; subst; inversion H5; subst.
   unfold updEnv; simpl.
-  symmetry in H0, H7.
-  unfold updEnv in H0, H7; simpl in H0, H7.
-  inversion H0; inversion H7; subst.
+  symmetry in H0, H1.
+  unfold updEnv in H0, H1; simpl in H0, H1.
+  inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
@@ -161,13 +161,13 @@ Proof.
 Qed.
 
 Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (P1 P2:precond):
-  eval_exp 0%R E1 P1 (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e1) e1F ->
-  eval_exp 0%R E1 P1 (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e2) e2F ->
-  eval_exp 0%R E1 P1 (Binop Mult (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) P2 (Binop Mult (Var R 1) (Var R 2)) vF ->
+      (vR:R) (vF:R) (E1 E2:env):
+  eval_exp 0%R E1 (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
+  eval_exp 0%R E1 (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) E2  (toRExp e2) e2F ->
+  eval_exp 0%R E1  (Binop Mult (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
   (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
@@ -186,9 +186,9 @@ Proof.
   inversion mult_float; subst.
   unfold perturb; simpl.
   inversion H4; subst; inversion H5; subst.
-  symmetry in H0, H7;
+  symmetry in H0, H1;
     unfold updEnv in *; simpl in *.
-  inversion H0; inversion H7; subst.
+  inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
@@ -208,13 +208,13 @@ Proof.
 Qed.
 
 Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (P1 P2:precond):
-  eval_exp 0%R E1 P1 (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e1) e1F ->
-  eval_exp 0%R E1 P1 (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) E2 P1 (toRExp e2) e2F ->
-  eval_exp 0%R E1 P1 (Binop Div (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) P2 (Binop Div (Var R 1) (Var R 2)) vF ->
+      (vR:R) (vF:R) (E1 E2:env):
+  eval_exp 0%R E1 (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
+  eval_exp 0%R E1 (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) E2  (toRExp e2) e2F ->
+  eval_exp 0%R E1 (Binop Div (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Div (Var R 1) (Var R 2)) vF ->
   (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.
@@ -233,9 +233,9 @@ Proof.
   inversion div_float; subst.
   unfold perturb; simpl.
   inversion H4; subst; inversion H5; subst.
-  symmetry in H0, H7;
+  symmetry in H0, H1;
     unfold updEnv in *; simpl in *.
-  inversion H0; inversion H7; subst.
+  inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.

coq/ErrorValidation.v

@@ -77,24 +77,26 @@ Proof.
   - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
 Qed.
 
-
 Lemma validErrorboundCorrectVariable:
-  forall E1 E2 absenv (v:nat) nR nF e nlo nhi (P:precond) fVars dVars,
+  forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars,
     approxEnv E1 absenv fVars dVars E2 ->
-    eval_exp 0%R E1 P (toRExp (Var Q v)) nR ->
-    eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 P (toRExp (Var Q v)) nF ->
+    eval_exp 0%R E1 (toRExp (Var Q v)) nR ->
+    eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 (toRExp (Var Q v)) nF ->
     validIntervalbounds (Var Q v) absenv P dVars = true ->
+    validErrorbound (Var Q v) absenv dVars = true ->
     (forall v : NatSet.elt,
         NatSet.mem v dVars = true ->
         exists vR0 : R,
           E1 v = Some vR0 /\
           (Q2R (fst (fst (absenv (Var Q v)))) <= vR0 <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
-    validErrorbound (Var Q v) absenv dVars = true ->
+    (forall v, NatSet.mem v fVars= true ->
+          exists vR, E1 v = Some vR /\
+                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     absenv (Var Q v) = ((nlo,nhi),e) ->
     (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
   intros E1 E2 absenv v nR nF e nlo nhi P fVars dVars approxCEnv eval_real
-         eval_float bounds_valid dVars_sound error_valid absenv_var.
+         eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
   inversion eval_real; inversion eval_float; subst.
   unfold validErrorbound in error_valid.
   rewrite absenv_var in *; simpl in *.
@@ -111,10 +113,10 @@ Proof.
       * case_eq (NatSet.mem x dVars); intros case_mem; try auto.
         rewrite NatSet.mem_spec in case_mem.
         assert (NatSet.In x (NatSet.union fVars dVars)) by (rewrite NatSet.union_spec; auto).
-        rewrite <- NatSet.mem_spec in H5.
-        rewrite H5 in H4. inversion H4.
-      * rewrite H5 in error_valid.
-      inversion H0; inversion H6; subst.
+        rewrite <- NatSet.mem_spec in H2.
+        rewrite H2 in H1. inversion H1.
+      * rewrite H2 in error_valid.
+      inversion H0; inversion H3; subst.
       eapply Rle_trans.
       apply H.
       repeat (rewrite delta_0_deterministic in H3; auto).
@@ -129,12 +131,13 @@ Proof.
       { rewrite <- maxAbs_impl_RmaxAbs.
         apply contained_leq_maxAbs_val.
         unfold contained.
-        pose proof (validIntervalbounds_sound (Var Q x) A dVars (P:=P) (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid) as valid_bounds_prf.
+        pose proof (validIntervalbounds_sound (Var Q x) A P dVars (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid) as valid_bounds_prf.
         rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
-        simpl; apply valid_bounds_prf; auto. }
+        simpl; apply valid_bounds_prf; auto.
+        admit. }
     + apply IHapproxCEnv; try auto.
-      { apply (Var_load _ P _ H0 H1 H2 H3). }
-      { apply (Var_load _ _ _ H6 H7 H8 H9). }
+      { constructor; auto. }
+      { constructor; auto. }
       intros v0 mem_dVars;
         specialize (dVars_sound v0 mem_dVars).
       destruct dVars_sound as [vR0 [val_def iv_sound_val]].
@@ -144,49 +147,50 @@ Proof.
         subst.
         rewrite NatSet.mem_spec in mem_dVars.
         assert (NatSet.In x (NatSet.union fVars dVars)) by (rewrite NatSet.union_spec; auto).
-        rewrite <- NatSet.mem_spec in H5;
-          rewrite H5 in H4; inversion H4.
+        rewrite <- NatSet.mem_spec in H2;
+          rewrite H2 in H1; inversion H1.
       * exists vR0; split; auto.
+      * admit.
   - unfold updEnv in *; simpl in *.
     case_eq (v =? x); intros eq_case; rewrite eq_case in *.
     + rewrite Nat.eqb_eq in eq_case; subst.
-      symmetry in H0, H6;
-        inversion H0; inversion H6;
+      symmetry in H0, H3;
+        inversion H0; inversion H3;
           subst.
       rewrite absenv_var in H; auto.
     + unfold updEnv in *; simpl in *.
       apply IHapproxCEnv; try auto.
-      * apply (Var_load _ P _ H0 H1 H2 H3).
-      * apply (Var_load _ _ _ H6 H7 H8 H9).
+      * constructor; auto.
+      * constructor; auto.
       * rewrite absenv_var.
         case_eq (NatSet.mem v dVars);
         intros case_dVars; rewrite case_dVars in *; simpl in *; try auto.
         assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add.
         { case_eq (NatSet.mem v (NatSet.add x dVars));
-            intros case_add; rewrite case_add in *; simpl in *.
+            intros case_add; rewrite case_add in *; simpl in *; try auto.
           - rewrite NatSet.mem_spec in case_add.
             rewrite NatSet.add_spec in case_add.
             destruct case_add; subst.
             + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
-            + rewrite <- NatSet.mem_spec in H5. rewrite H5 in case_dVars.
-              inversion case_dVars.
-          - auto. }
+            + rewrite <- NatSet.mem_spec in H2. rewrite H2 in case_dVars.
+              inversion case_dVars. }
         { rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid.
           auto. }
+      * admit.
       * intros v0 mem_dVars.
         rewrite absenv_var in *; simpl in *.
         rewrite NatSet.mem_spec in mem_dVars.
         assert (NatSet.In v0 (NatSet.add x dVars)).
         { rewrite NatSet.add_spec. right; auto. }
-        { rewrite <- NatSet.mem_spec in H5.
-          specialize (dVars_sound v0 H5).
+        { rewrite <- NatSet.mem_spec in H2.
+          specialize (dVars_sound v0 H2).
           destruct dVars_sound as [vR0 [val_def iv_sound_val]].
           case_eq (v0 =? x); intros case_mem;
             rewrite case_mem in val_def; simpl in val_def.
           rewrite Nat.eqb_eq in case_mem; subst.
           - apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
             rewrite <- NatSet.mem_spec in mem_dVars.
-            rewrite mem_dVars in H4; inversion H4.
+            rewrite mem_dVars in H1; inversion H1.
           - exists vR0; split; auto. }
       * rewrite absenv_var in bounds_valid.
         case_eq (NatSet.mem v dVars); intros case_mem; try auto.
@@ -200,19 +204,20 @@ Proof.
           exfalso; apply eq_case; auto. }
         { rewrite <- NatSet.mem_spec in in_dVars.
           rewrite case_mem in in_dVars.
-          inversion in_dVars. }
-Qed.
+          inversion in_dVars.
+          admit. }
+Admitted.
 
 Lemma validErrorboundCorrectConstant:
-  forall E1 E2 absenv (n:Q) nR nF e nlo nhi (P:precond) dVars,
-    eval_exp 0%R E1 P (Const (Q2R n)) nR ->
-    eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 P (Const (Q2R n)) nF ->
+  forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars,
+    eval_exp 0%R E1 (Const (Q2R n)) nR ->
+    eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 (Const (Q2R n)) nF ->
     validErrorbound (Const n) absenv dVars = true ->
     (Q2R nlo <= nR <= Q2R nhi)%R ->
     absenv (Const n) = ((nlo,nhi),e) ->
     (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros E1 E2 absenv n nR nF e nlo nhi P dVars
+  intros E1 E2 absenv n nR nF e nlo nhi dVars
          eval_real eval_float error_valid intv_valid absenv_const.
   eapply Rle_trans.
   eapply const_abs_err_bounded; eauto.
@@ -296,13 +301,13 @@ Qed.*)
 
 Lemma validErrorboundCorrectAddition E1 E2 absenv
       (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) P1 P2 dVars:
-  eval_exp 0%R E1 P1 (toRExp e1) nR1 ->
-  eval_exp 0%R E1 P1 (toRExp e2) nR2 ->
-  eval_exp 0%R E1 P1 (toRExp (Binop Plus e1 e2)) nR ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e1) nF1 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e2) nF2 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) P2 (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars:
+  eval_exp 0%R E1 (toRExp e1) nR1 ->
+  eval_exp 0%R E1 (toRExp e2) nR2 ->
+  eval_exp 0%R E1 (toRExp (Binop Plus e1 e2)) nR ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
   validErrorbound (Binop Plus e1 e2) absenv dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -366,13 +371,13 @@ Qed.
 
 Lemma validErrorboundCorrectSubtraction E1 E2 absenv
       (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) P1 P2 dVars:
-  eval_exp 0%R E1 P1 (toRExp e1) nR1 ->
-  eval_exp 0%R E1 P1 (toRExp e2) nR2 ->
-  eval_exp 0%R E1 P1 (toRExp (Binop Sub e1 e2)) nR ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e1) nF1 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e2) nF2 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) P2 (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars:
+  eval_exp 0%R E1 (toRExp e1) nR1 ->
+  eval_exp 0%R E1 (toRExp e2) nR2 ->
+  eval_exp 0%R E1 (toRExp (Binop Sub e1 e2)) nR ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
   validErrorbound (Binop Sub e1 e2) absenv dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -447,13 +452,13 @@ Qed.
 
 Lemma validErrorboundCorrectMult E1 E2 absenv
       (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) P1 P2 dVars:
-  eval_exp 0%R E1 P1 (toRExp e1) nR1 ->
-  eval_exp 0%R E1 P1 (toRExp e2) nR2 ->
-  eval_exp 0%R E1 P1 (toRExp (Binop Mult e1 e2)) nR ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e1) nF1 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e2) nF2 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) P2 (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars:
+  eval_exp 0%R E1 (toRExp e1) nR1 ->
+  eval_exp 0%R E1 (toRExp e2) nR2 ->
+  eval_exp 0%R E1 (toRExp (Binop Mult e1 e2)) nR ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF ->
   validErrorbound (Binop Mult e1 e2) absenv dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -973,13 +978,13 @@ Qed.
 
 Lemma validErrorboundCorrectDiv E1 E2 absenv
       (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) P1 P2 dVars:
-  eval_exp 0%R E1 P1 (toRExp e1) nR1 ->
-  eval_exp 0%R E1 P1 (toRExp e2) nR2 ->
-  eval_exp 0%R E1 P1 (toRExp (Binop Div e1 e2)) nR ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e1) nF1 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) E2 P1 (toRExp e2) nF2 ->
-  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) P2 (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars:
+  eval_exp 0%R E1 (toRExp e1) nR1 ->
+  eval_exp 0%R E1 (toRExp e2) nR2 ->
+  eval_exp 0%R E1 (toRExp (Binop Div e1 e2)) nR ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 ->
+  eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF ->
   validErrorbound (Binop Div e1 e2) absenv dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -1033,7 +1038,7 @@ Proof.
     (* Error Propagation proof *)
     + clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float
             e1_real e2_float e2_real absenv_div
-            valid_err_e1 valid_err_e2 E1 E2 absenv alo ahi nR nF e1 e2 e P1 P2 L.
+            valid_err_e1 valid_err_e2 E1 E2 absenv alo ahi nR nF e1 e2 e L.
       unfold IntervalArith.contained, widenInterval in *.
       simpl in *.
       rewrite Q2R_plus, Q2R_minus in no_div_zero_float.
@@ -1900,23 +1905,27 @@ Qed.
 Theorem validErrorbound_sound (e:exp Q):
   forall E1 E2 fVars dVars absenv nR nF err P elo ehi,
     approxEnv E1 absenv fVars dVars E2 ->
-    eval_exp 0%R E1 P (toRExp e) nR ->
-    eval_exp (Q2R RationalSimps.machineEpsilon) E2 P (toRExp e) nF ->
+    eval_exp 0%R E1 (toRExp e) nR ->
+    eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e) nF ->
     validErrorbound e absenv dVars = true ->
     validIntervalbounds e absenv P dVars = true ->
     (forall v : NatSet.elt, NatSet.mem v dVars = true ->
                        exists vr, E1 v = Some vr /\
-                       (Q2R (fst (fst (absenv (Var Q v)))) <= vr <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
+                             (Q2R (fst (fst (absenv (Var Q v)))) <= vr <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
+    (forall v, NatSet.mem v fVars= true ->
+          exists vR, E1 v = Some vR /\
+                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     absenv e = ((elo,ehi),err) ->
     (Rabs (nR - nF) <= (Q2R err))%R.
 Proof.
   induction e;
     try (intros E1 E2 fVars dVars absenv nR nF err P elo ehi;
-    intros approxCEnv eval_real eval_float valid_error valid_intv valid_dVars absenv_eq).
+    intros approxCEnv eval_real eval_float valid_error valid_intv valid_dVars P_valid absenv_eq).
   - eapply validErrorboundCorrectVariable; eauto.
-  - pose proof (validIntervalbounds_sound (Const v) absenv dVars valid_intv valid_dVars eval_real).
+  - pose proof (validIntervalbounds_sound (Const v) absenv P dVars (vR:=nR) valid_intv valid_dVars).
     eapply validErrorboundCorrectConstant; eauto.
-    rewrite absenv_eq; auto.
+    rewrite absenv_eq in *; simpl in *.
+    apply H; try auto. admit.
   - unfold validErrorbound in valid_error.
     rewrite absenv_eq in valid_error.
     andb_to_prop valid_error.
@@ -1941,16 +1950,13 @@ Proof.
     inversion eval_real; subst.
     inversion eval_float; subst.
     simpl in *.
-    pose proof (validIntervalbounds_sound e1 absenv dVars L2 valid_dVars H4).
+    pose proof (validIntervalbounds_sound e1 absenv P dVars (vR:=v1) L2 valid_dVars).
     rewrite absenv_e1 in H.
-    pose proof (validIntervalbounds_sound e2 absenv dVars R2 valid_dVars H5).
+    pose proof (validIntervalbounds_sound e2 absenv P dVars (vR:=v2) R2 valid_dVars).
     rewrite absenv_e2 in H0;
       simpl in *.
     assert (eval_exp (Q2R machineEpsilon) (updEnv 2 v3 (updEnv 1 v0 emptyEnv))
-         (fun n : nat => if n =? 1 then (ivlo1 - err1, ivhi1 + err1) else (ivlo2 - err2, ivhi2 + err2))
-         (Binop b (Var Rdefinitions.R 1) (Var Rdefinitions.R 2)) (perturb (evalBinop b v0 v3) delta0)).
-    eapply (binary_unfolding (E1:=E1) (E2:=E2) (P:=P)); eauto.
-    apply mEps_geq_zero.
+                     (Binop b (Var Rdefinitions.R 1) (Var Rdefinitions.R 2)) (perturb (evalBinop b v0 v3) delta0)) by admit.
     destruct b.
     + eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
       unfold validErrorbound.
@@ -1965,6 +1971,8 @@ Proof.
         apply L1.
         apply R.
         apply Is_true_eq_left; apply R0.
+      * admit.
+      * admit.
     + eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto.
       unfold validErrorbound.
       rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
@@ -1978,6 +1986,8 @@ Proof.
         apply L1.
         apply R.
         apply Is_true_eq_left; apply R0.
+      * admit.
+      * admit.
     + eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto.
       unfold validErrorbound.
       rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
@@ -1991,6 +2001,8 @@ Proof.
         apply L1.
         apply R.
         apply Is_true_eq_left; apply R0.
+      * admit.
+      * admit.
     + eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto.
       unfold validErrorbound.
       rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
@@ -2004,9 +2016,11 @@ Proof.