Rework expression and cmd semantics for removing parameters distinction

coq/Commands.v

@@ -2,7 +2,8 @@
  Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
  **)
 Require Import Coq.Reals.Reals Coq.QArith.QArith.
-Require Export Daisy.Infra.ExpressionAbbrevs.
+Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
+
 (**
   Next define what a program is.
   Currently no loops, only conditionals and assignments
@@ -10,65 +11,41 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
 **)
 Inductive cmd (V:Type) :Type :=
 Let: nat -> exp V -> cmd V -> cmd V
-| Ret: exp V -> cmd V
-| Nop: cmd V.
+| Ret: exp V -> cmd V.
+(*| Nop: cmd V. *)
 
-(**
+(*
+UNUSED!
    Small Step semantics for Daisy language
-**)
-Inductive sstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
-  let_s x e s VarEnv ParamEnv P v eps:
-    eval_exp eps VarEnv ParamEnv P e v ->
-    sstep (Let R x e s) VarEnv ParamEnv P eps s (updEnv x v VarEnv)
- |ret_s e VarEnv ParamEnv P v eps:
-    eval_exp eps VarEnv ParamEnv P  e v ->
-    sstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
+Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
+  let_s x e s E v eps:
+    eval_exp eps E e v ->
+    sstep (Let x e s) E eps s (updEnv x v E)
+ |ret_s e E v eps:
+    eval_exp eps E e v ->
+    sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
+ *)
 
 (**
   Analogously define Big Step semantics for the Daisy language
  **)
-Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> R -> Prop :=
-  let_b x e s s' VarEnv ParamEnv P v eps res:
-    eval_exp eps VarEnv ParamEnv P e v ->
-    bstep s (updEnv x v VarEnv) ParamEnv P eps s' res ->
-    bstep (Let R x e s) VarEnv ParamEnv P eps s' res
- |ret_b e VarEnv ParamEnv P v eps:
-    eval_exp eps VarEnv ParamEnv P e v ->
-    bstep (Ret R e) VarEnv ParamEnv P eps (Nop R) v.
-
-Fixpoint substitute_exp (v:nat) (e:exp Q) (e_old:exp Q) :=
-  match e_old with
-  |Var _ v_old => if (v =? v_old) then e else Var Q v_old
-  |Unop op e' => Unop op (substitute_exp v e e')
-  |Binop op e1 e2 => Binop op (substitute_exp v e e1) (substitute_exp v e e2)
-  |e => e
-  end.
+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.
 
-Fixpoint substitute (v:nat) (e:exp Q) (f:cmd Q) :=
+Fixpoint freeVars (f:cmd Q) :NatSet.t :=
   match f with
-  |Let _ x e_x g =>
-   let new_e  := substitute_exp v e e_x in
-   Let Q x new_e (substitute v e g)
-  |Ret _ e_ret => Ret Q (substitute_exp v e e_ret)
-  |Nop _ => Nop Q
+  | Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
+  | Ret e => Expressions.freeVars e
   end.
 
-Fixpoint expand_lets (f:cmd Q) (fuel:nat) :option (cmd Q):=
-  match fuel with
-  |0%nat => Some f
-  |S fuel' =>
-   match f with
-   |Let _ x e g =>
-    (expand_lets (substitute x e g) fuel')
-   |Ret _ e => Some (Ret Q e)
-   |Nop _ => None
-   end
-  end.
-
-Fixpoint count_lets (f:cmd Q) :nat :=
+Fixpoint definedVars (f:cmd Q) :NatSet.t :=
   match f with
-  |Let _ x e g => S (count_lets g)
-  | _ => 0%nat
-  end.
-
-Definition expand (f:cmd Q) := expand_lets f (count_lets f).
\ No newline at end of file
+  | Let x _ g => NatSet.add x (definedVars g)
+  | Ret _ => NatSet.empty
+  end.
\ No newline at end of file

coq/Environments.v

 (**
 Environment library.
 Defines the environment type for the Daisy framework and a simulation relation between environments.
-FIXME: Would it make sense to differenciate between a parameter environment and a variable environment?
  **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
-Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
+Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RationalSimps Daisy.Commands.
 
 (**
 Define an approximation relation between two environments.
@@ -13,8 +12,24 @@ It is necessary to have this relation, since two evaluations of the very same
 expression may yield different values for different machine epsilons
 (or environments that already only approximate each other)
  **)
-Inductive approxEnv : env -> analysisResult -> env -> Prop :=
-|approxRefl E A: approxEnv E A E
-|approxUpd E1 E2 A v1 v2 x: approxEnv E1 A E2 ->
-			    (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
-                            approxEnv (updEnv x v1 E1) A (updEnv x v2 E2).
\ No newline at end of file
+Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
+|approxRefl A:
+   approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
+|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
+   approxEnv E1 A fVars dVars E2 ->
+   (Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%R ->
+   NatSet.mem x dVars = false ->
+   approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
+|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
+   approxEnv E1 A fVars dVars E2 ->
+   (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
+   NatSet.mem x fVars = false ->
+   approxEnv (updEnv x v1 E1) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
+
+Inductive approxParams :env -> R -> env -> Prop :=
+|approxParamRefl eps:
+   approxParams emptyEnv eps emptyEnv
+|approxParamUpd E1 E2 eps x v1 v2 :
+   approxParams E1 eps E2 ->
+   (Rabs (v1 - v2) <= eps)%R ->
+   approxParams (updEnv x v1 E1) eps (updEnv x v2 E2).

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) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
-  eval_exp 0%R VarEnv1 ParamEnv P (Const n) nR ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Const n) nF ->
+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 ->
   (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
 Proof.
   intros eval_real eval_float.
@@ -21,30 +21,34 @@ Proof.
   apply Rmult_le_compat_l; [apply Rabs_pos | auto].
 Qed.
 
-Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
-  eval_exp 0%R VarEnv1 ParamEnv P (Param R n) nR ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Param R n) nF ->
-  (Rabs (nR - nF) <= Rabs (ParamEnv n) * (Q2R machineEpsilon))%R.
+(*
+Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
+  eval_exp 0%R E1 P (Param R n) nR ->
+  eval_exp (Q2R machineEpsilon) E2 P (Param R n) nF ->
+  (Rabs (nR - nF) <=  * (Q2R machineEpsilon))%R.
 Proof.
   intros eval_real eval_float.
   inversion eval_real; subst.
   rewrite delta_0_deterministic; auto.
   inversion eval_float; subst.
   unfold perturb; simpl.
+  exists v; split; try auto.
+
+  rewrite H3 in H8; inversion H8.
   rewrite Rabs_err_simpl.
   repeat rewrite Rabs_mult.
   apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
 Qed.
+*)
 
 Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond)
-      (err1 err2 :Q):
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (Binop Plus (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var R 1) (Var R 2)) vF ->
+      (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 ->
   (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.
@@ -66,8 +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.
   (* 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.
+  clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H7.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -80,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 H1.
+  apply H4.
   rewrite <- Rplus_assoc.
   repeat rewrite <- Rsub_eq_Ropp_Rplus.
   rewrite Rabs_Ropp.
@@ -98,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) (VarEnv1 VarEnv2 ParamEnv:nat->R) P err1 err2:
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (Binop Sub (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var R 1) (Var R 2)) vF ->
+      (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 ->
   (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.
@@ -126,8 +133,11 @@ 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.
   (* 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.
+  clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -151,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) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (Binop Mult (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF ->
+      (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 ->
   (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.
@@ -176,9 +186,11 @@ Proof.
   inversion mult_float; subst.
   unfold perturb; simpl.
   inversion H4; subst; inversion H5; subst.
-  unfold updEnv; simpl.
+  symmetry in H0, H7;
+    unfold updEnv in *; simpl in *.
+  inversion H0; inversion H7; 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.
+  clear mult_float H4 H5 mult_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.
@@ -196,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) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
-  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
-  eval_exp 0%R VarEnv1 ParamEnv P (Binop Div (toRExp e1) (toRExp e2)) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF ->
+      (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 ->
   (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.
@@ -221,9 +233,11 @@ Proof.
   inversion div_float; subst.
   unfold perturb; simpl.
   inversion H4; subst; inversion H5; subst.
-  unfold updEnv; simpl.
+  symmetry in H0, H7;
+    unfold updEnv in *; simpl in *.
+  inversion H0; inversion H7; 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.
+  clear div_float H4 H5 div_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.

coq/Expressions.v

@@ -3,8 +3,8 @@ Formalization of the base expression language for the daisy framework
 Required in all files, since we will always reason about expressions.
  **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
-Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
-Set Implicit Arguments.
+Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith.
+
 (**
   Expressions will use binary operators.
   Define them first
@@ -56,13 +56,9 @@ Definition evalUnop (o:unop) (v:R):=
 (**
   Define expressions parametric over some value type V.
   Will ease reasoning about different instantiations later.
-  Note that we differentiate between wether we use a variable from the environment or a parameter.
-  Parameters do not have error bounds in the invariants, so they must be perturbed, but variables from the
-  program will be perturbed upon binding, so we do not need to perturb them.
 **)
 Inductive exp (V:Type): Type :=
   Var: nat -> exp V
-| Param: nat -> exp V
 | Const: V -> exp V
 | Unop: unop -> exp V -> exp V
 | Binop: binop -> exp V -> exp V -> exp V.
@@ -78,11 +74,6 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
    |Var _ v2 => v1 =? v2
    | _=> false
    end
-  |Param _ v1 =>
-   match e2 with
-   |Param _ v2 => v1 =? v2
-   | _=> false
-   end
   |Const n1 =>
    match e2 with
    |Const n2 => Qeq_bool n1 n2
@@ -115,29 +106,36 @@ It is important that variables are not perturbed when loading from an environmen
 This is the case, since loading a float value should not increase an additional error.
 Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
 **)
-Inductive eval_exp (eps:R) (VarEnv:env) (ParamEnv:env) (P:precond) : (exp R) -> R -> Prop :=
-  Var_load x: eval_exp eps VarEnv ParamEnv P (Var R x) (VarEnv x)
-| Param_acc x delta delta_lo delta_hi:
-    ((Rabs delta) <= eps)%R ->
-    ((Rabs delta_lo) <= eps)%R ->
-    ((Rabs delta_hi) <= eps)%R ->
-    ((perturb (Q2R (fst (P x))) delta_lo) <= perturb (ParamEnv x) delta <= (perturb (Q2R (snd (P x))) delta_hi))%R ->
-    eval_exp eps VarEnv ParamEnv P (Param R x) (perturb (ParamEnv x) delta)
+Inductive eval_exp (eps:R) (E:env) (P:precond) :(exp R) -> R -> Prop :=
+| Var_load x v delta_lo delta_hi:
+    E x = Some v ->
+    (Rabs delta_lo <= eps)%R ->
+    (Rabs delta_hi <= eps)%R ->
+    (perturb (Q2R (ivlo (P x))) delta_lo <= v <= perturb (Q2R (ivhi (P x))) delta_hi)%R ->
+    eval_exp eps E P (Var R x) v
 | Const_dist n delta:
     Rle (Rabs delta) eps ->
-    eval_exp eps VarEnv ParamEnv P (Const n) (perturb n delta)
+    eval_exp eps E P (Const n) (perturb n delta)
 | Unop_neg f1 v1:
-    eval_exp eps VarEnv ParamEnv P f1 v1 ->
-    eval_exp eps VarEnv ParamEnv P (Unop Neg f1) (evalUnop Neg v1)
+    eval_exp eps E P f1 v1 ->
+    eval_exp eps E P (Unop Neg f1) (evalUnop Neg v1)
 | Unop_inv f1 v1 delta:
     Rle (Rabs delta) eps ->
-    eval_exp eps VarEnv ParamEnv P f1 v1 ->
-    eval_exp eps VarEnv ParamEnv P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
+    eval_exp eps E P f1 v1 ->
+    eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
 | Binop_dist op f1 f2 v1 v2 delta:
     Rle (Rabs delta) eps ->
-                eval_exp eps VarEnv ParamEnv P f1 v1 ->
-                eval_exp eps VarEnv ParamEnv P f2 v2 ->
-                eval_exp eps VarEnv ParamEnv P (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
+    eval_exp eps E P f1 v1 ->
+    eval_exp eps E P f2 v2 ->
+    eval_exp eps E P (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
+
+Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
+  match e with
+  | Var _ x => NatSet.singleton x
+  | Unop u e1 => freeVars e1
+  | Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2)
+  | _ => NatSet.empty
+  end.
 
 (**
 If |delta| <= 0 then perturb v delta is exactly v.
@@ -154,15 +152,17 @@ Qed.
 (**
 Evaluation with 0 as machine epsilon is deterministic
 **)
-Lemma meps_0_deterministic (f:exp R) (VarEnv ParamEnv:env) (P:precond):
+Lemma meps_0_deterministic (f:exp R) (E:env) (P:precond):
   forall v1 v2,
-  eval_exp R0 VarEnv ParamEnv P f v1 ->
-  eval_exp R0 VarEnv ParamEnv P f v2 ->
+  eval_exp 0 E P f v1 ->
+  eval_exp 0 E P f v2 ->
   v1 = v2.
 Proof.
   induction f; intros v1 v2 eval_v1 eval_v2;
     inversion eval_v1; inversion eval_v2;
       repeat try rewrite delta_0_deterministic; subst; auto.
+  - rewrite H6 in H0; inversion H0;
+      subst; auto.
   - rewrite (IHf v0 v3); auto.
   - inversion H3.
   - inversion H4.
@@ -178,36 +178,273 @@ evaluating the subexpressions and then binding the result values to different
 variables in the Eironment.
 This relies on the property that variables are not perturbed as opposed to parameters
 **)
-Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (VarEnv ParamEnv:env) (P:precond) (v:R):
-  (eval_exp eps VarEnv ParamEnv P (Binop b f1 f2) v <->
-   exists v1 v2,
-     eval_exp eps VarEnv ParamEnv P f1 v1 /\
-     eval_exp eps VarEnv ParamEnv P f2 v2 /\
-     eval_exp eps (updEnv 2 v2 (updEnv 1 v1 VarEnv)) ParamEnv P (Binop b (Var R 1) (Var R 2)) v).
+Lemma binary_unfolding b f1 f2 eps E1 E2 P vF1 vF2 vR1 vR2 f1_lo f1_hi f2_lo f2_hi err1 err2 delta:
+  eval_exp eps E2 P (Binop b f1 f2) (perturb (evalBinop b vF1 vF2) delta) ->
+  eval_exp eps E2 P f1 vF1 ->
+  eval_exp eps E2 P f2 vF2 ->
+  eval_exp 0%R E1 P f1 vR1 ->
+  eval_exp 0%R E1 P f2 vR2 ->
+  contained vR1 (Q2R f1_lo, Q2R f1_hi) ->
+  contained vR2 (Q2R f2_lo, Q2R f2_hi) ->
+  (0 <= eps)%R ->
+  (Rabs delta <= eps)%R ->
+  (Rabs (vR1 - vF1) <= Q2R err1)%R ->
+  (Rabs (vR2 - vF2) <= Q2R err2)%R ->
+  eval_exp eps (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv))
+           (fun n => if n =? 1 then (f1_lo - err1, f1_hi + err1) else (f2_lo - err2, f2_hi + err2))
+           (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b vF1 vF2) delta).
 Proof.
-  split.
-  - intros eval_bin.
-    inversion eval_bin; subst.
-    exists v1, v2.
-    repeat split; try auto.
-    constructor; try auto;
-    constructor; auto.
-  - intros exists_val.
-    destruct exists_val as [v1 [v2 [eval_f1 [eval_f2 eval_e_E]]]].
-    inversion eval_e_E; subst.
-    inversion H4; inversion H5; subst.
-    unfold updEnv in *; simpl in *.
-    constructor; auto.
+  intros eval_float eval_f1_float eval_f2_float eval_f1_real eval_f2_real
+         vR1_contained vR2_contained err_pos delta_valid err1_bound err2_bound.
+  pose proof (distance_gives_iv vF1 vR1_contained err1_bound) as vF1_err_iv.
+  pose proof (distance_gives_iv vF2 vR2_contained err2_bound) as vF2_err_iv.
+  assert (Rabs eps <= eps)%R as eps_valid by (rewrite Rabs_right; lra).
+  assert (Rabs (-eps) <= eps)%R as neg_eps_valid.
+  - hnf in err_pos.
+    destruct err_pos.
+    + rewrite Rabs_left; lra.
+    + rewrite Rabs_right; lra.
+  - constructor; try auto.
+    + destruct (Rlt_le_dec (Q2R f1_lo - Q2R err1) 0) as [lo_lt_0 | lo_geq_0];
+      destruct (Rlt_le_dec (Q2R f1_hi + Q2R err1) 0) as [hi_lt_0 | hi_geq_0].
+      * econstructor; try auto.
+        apply eps_valid.
+        apply neg_eps_valid.
+        simpl.
+        unfold perturb.
+        unfold contained in vF1_err_iv.
+        simpl in *.
+        destruct vF1_err_iv as [vF1_err_lo vF1_err_hi].
+        split;
+          rewrite Rmult_plus_distr_l;
+          rewrite Rmult_1_r.
+        { rewrite Q2R_minus.
+          eapply Rle_trans.
+          Focus 2.
+          apply vF1_err_lo.
+          setoid_rewrite <- (Rplus_0_r (Q2R f1_lo - Q2R err1)) at 3.
+          apply Rplus_le_compat; try lra.
+          rewrite <- (Rmult_0_r 0).
+          eapply Rle_trans.
+          apply Rmult_le_compat_r; try lra.
+          hnf. left; apply lo_lt_0.
+          repeat (rewrite Rmult_0_l); lra. }
+        { rewrite Q2R_plus.
+          eapply Rle_trans.
+          apply vF1_err_hi.
+          setoid_rewrite <- (Rplus_0_r (Q2R f1_hi + Q2R err1)) at 1.
+          apply Rplus_le_compat; try lra.
+          hnf in err_pos.
+          destruct err_pos.
+          - hnf; left; apply Rmult_lt_0_inverting; lra.
+          - subst. lra. }
+      * econstructor; try auto.
+        apply eps_valid.
+        apply eps_valid.
+        simpl.
+        unfold perturb.
+        unfold contained in vF1_err_iv.
+        simpl in *.
+        destruct vF1_err_iv as [vF1_err_lo vF1_err_hi].
+        split;
+          rewrite Rmult_plus_distr_l;
+          rewrite Rmult_1_r.
+        { rewrite Q2R_minus.
+          eapply Rle_trans.
+          Focus 2.
+          apply vF1_err_lo.
+          setoid_rewrite <- (Rplus_0_r (Q2R f1_lo - Q2R err1)) at 3.
+          apply Rplus_le_compat; try lra.
+          rewrite <- (Rmult_0_r 0).
+          eapply Rle_trans.
+          apply Rmult_le_compat_r; try lra.
+          hnf. left; apply lo_lt_0.
+          repeat (rewrite Rmult_0_l); lra. }
+        { rewrite Q2R_plus.
+          eapply Rle_trans.
+          apply vF1_err_hi.
+          setoid_rewrite <- (Rplus_0_r (Q2R f1_hi + Q2R err1)) at 1.
+          apply Rplus_le_compat; try lra.
+          rewrite <- (Rmult_0_r 0).
+          apply Rmult_le_compat; lra. }
+      * econstructor; try auto.
+        apply neg_eps_valid.
+        apply neg_eps_valid.
+        simpl.
+        unfold perturb.
+        unfold contained in vF1_err_iv.
+        simpl in *.
+        destruct vF1_err_iv as [vF1_err_lo vF1_err_hi].
+        split;
+          rewrite Rmult_plus_distr_l;
+          rewrite Rmult_1_r.
+        { rewrite Q2R_minus.
+          eapply Rle_trans.
+          Focus 2.
+          apply vF1_err_lo.
+          setoid_rewrite <- (Rplus_0_r (Q2R f1_lo - Q2R err1)) at 3.
+          apply Rplus_le_compat; try lra. }
+        { rewrite Q2R_plus.