WIP: Porting the different validators to mixed-precision.

/!\ Does not compile

coq/ErrorBounds.v

@@ -8,8 +8,8 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSim
 Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
 Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType):
-  eval_exp E1 (Const n) nR M0 ->
-  eval_exp E2 (Const n) nF M0 ->
+  eval_exp E1 (Const m n) nR M0 ->
+  eval_exp E2 (Const m n) nF m ->
   (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
 Proof.
   intros eval_real eval_float.
@@ -21,8 +21,7 @@ Proof.
   apply Rmult_le_compat_l; [apply Rabs_pos | auto].
   simpl (meps M0) in *.
   apply (Rle_trans _ (Q2R 0) _); try auto.
-  apply Qle_Rle; apply inj_eps_pos.
-  simpl (meps M0) in H0; rewrite Q2R0_is_0 in H0; auto.
+  rewrite Q2R0_is_0; lra.
 Qed.
 
 (*
@@ -77,11 +76,11 @@ Proof.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
   unfold updEnv; simpl.
-  unfold updEnv in H9,H11; simpl in *.
-  symmetry in H9, H11.
-  inversion H9; inversion H11; subst.
+  unfold updEnv in H9,H6; simpl in *.
+  symmetry in H9, H6.
+  inversion H9; inversion H6; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear plus_float H7 H8 plus_real e1_real e1_float e2_real e2_float H9 H11.
+  clear plus_float H7 H8 plus_real e1_real e1_float e2_real e2_float H9 H6.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -94,7 +93,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 H6.
+  apply H1.
   rewrite <- Rplus_assoc.
   repeat rewrite <- Rsub_eq_Ropp_Rplus.
   rewrite Rabs_Ropp.
@@ -143,11 +142,11 @@ Proof.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
   unfold updEnv; simpl.
-  symmetry in H9, H11.
-  unfold updEnv in H9, H11; simpl in H9, H11.
-  inversion H9; inversion H11; subst.
+  symmetry in H9, H6.
+  unfold updEnv in H9, H6; simpl in H9, H6.
+  inversion H9; inversion H6; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H9 H11.
+  clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H9 H6.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -199,11 +198,11 @@ Proof.
   inversion mult_float; subst.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
-  symmetry in H9, H11;
+  symmetry in H9, H6;
     unfold updEnv in *; simpl in *.
-  inversion H9; inversion H11; subst.
+  inversion H9; inversion H6; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H9 H11.
+  clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H9 H6.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -249,11 +248,11 @@ Proof.
   inversion div_float; subst.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
-  symmetry in H9, H11;
+  symmetry in H9, H6;
     unfold updEnv in *; simpl in *.
-  inversion H9; inversion H11; subst.
+  inversion H9; inversion H6; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H9 H11.
+  clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H9 H6.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -447,3 +446,29 @@ Proof.
   auto.
   rewrite Q2R0_is_0; auto.
 Qed.
+
+Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E: env) (err:R) (machineEpsilon m:mType):
+  eval_exp E (toREval e) nR M0 ->
+  eval_exp E e nF1 m ->
+  eval_exp (updEnv 1 m nF1 E) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon->
+  (Rabs (nR - nF1) <= err)%R ->
+  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
+Proof.
+  intros eval_real eval_float eval_float_rnd err_bounded.
+  replace (nR - nF)%R with ((nR - nF1) + (nF1 - nF))%R by lra.
+  eapply Rle_trans.
+  apply (Rabs_triang (nR - nF1) (nF1 - nF)).
+  apply (Rle_trans _ (err + Rabs (nF1 - nF))  _).
+  - apply Rplus_le_compat_r; assumption.
+  - apply Rplus_le_compat_l.
+    inversion eval_float_rnd; subst.
+    inversion H5; subst.
+    inversion H7.
+    unfold perturb; simpl.
+    replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra.
+    replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp).
+    rewrite Rabs_mult.
+    apply Rmult_le_compat_l.
+    + apply Rabs_pos.
+    + auto. 
+Qed.

coq/ErrorValidation.v

@@ -9,59 +9,70 @@
 Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
 Require Import Coq.micromega.Psatz Coq.Reals.Reals.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps Daisy.Infra.Ltacs.
-Require Import Daisy.Environments Daisy.IntervalValidation Daisy.ErrorBounds.
+Require Import Daisy.Environments Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
 
 (** Error bound validator **)
-Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) (dVars:NatSet.t):=
+Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analysisResult) (dVars:NatSet.t):=
   let (intv, err) := (absenv e) in
-  if (Qleb 0 err)
-  then
-    match e with
-    |Var _ v =>
-     if (NatSet.mem v dVars)
-     then true
-     else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
-    |Const n =>
-     Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
-    |Unop _ _ => false
-    |Binop b e1 e2 =>
-     if ((validErrorbound e1 absenv dVars) && (validErrorbound e2 absenv dVars))
-     then
-          let (ive1, err1) := absenv e1 in
-          let (ive2, err2) := absenv e2 in
-          let errIve1 := widenIntv ive1 err1 in
-          let errIve2 := widenIntv ive2 err2 in
-          let upperBoundE1 := maxAbs ive1 in
-          let upperBoundE2 := maxAbs ive2 in
-          match b with
-          | Plus =>
-            Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * machineEpsilon) err
-          | Sub =>
-            Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * machineEpsilon) err
-          | Mult =>
-            Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * machineEpsilon) err
-          | Div =>
-            if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
-                 ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
-                then
-                  let upperBoundInvE2 := maxAbs (invertIntv ive2) in
-                  let minAbsIve2 := minAbs (errIve2) in
-                  let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
-                  Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * machineEpsilon) err
-                else false
-          end
-     else false
-    end
-  else false.
+  let mopt := typeMap e in
+  match mopt with
+  | None => false
+  | Some m =>
+    if (Qleb 0 err)
+    then
+      match e with
+      |Var _ _ v =>
+       if (NatSet.mem v dVars)
+       then true
+       else (Qleb (maxAbs intv * (meps m)) err)
+      |Const _ n =>
+       Qleb (maxAbs intv * (meps m)) err
+      |Unop _ _ => false
+      |Binop b e1 e2 =>
+       if ((validErrorbound e1 typeMap absenv dVars) && (validErrorbound e2 typeMap absenv dVars))
+       then
+         let (ive1, err1) := absenv e1 in
+         let (ive2, err2) := absenv e2 in
+         let errIve1 := widenIntv ive1 err1 in
+         let errIve2 := widenIntv ive2 err2 in
+         let upperBoundE1 := maxAbs ive1 in
+         let upperBoundE2 := maxAbs ive2 in
+         match b with
+         | Plus =>
+           Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (meps m)) err
+         | Sub =>
+           Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (meps m)) err
+         | Mult =>
+           Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (meps m)) err
+         | Div =>
+           if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
+               ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
+           then
+             let upperBoundInvE2 := maxAbs (invertIntv ive2) in
+             let minAbsIve2 := minAbs (errIve2) in
+             let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
+             Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (meps m)) err
+           else false
+         end
+       else false
+      |Downcast m1 e1 =>
+       let (ive1, err1) := absenv e1 in
+       let rec := validErrorbound e1 typeMap absenv dVars in
+       let errIve1 := widenIntv ive1 err1 in
+       andb rec (Qleb (err1 + maxAbs errIve1 * (meps m1)) err)
+      end
+    else false
+  end.
 
 (** Error bound command validator **)
 Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool :=
   match f with
-  |Let x e g =>
-   if ((validErrorbound e env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))))
+  |Let m x e g =>
+   let tmap := typeExpression e in
+   if ((validErrorbound e tmap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q m x)))))
    then validErrorboundCmd g env (NatSet.add x dVars)
    else false
-  |Ret e => validErrorbound e env dVars
+  |Ret e => validErrorbound e (typeExpression e) env dVars
   end.
 
 (**
@@ -69,46 +80,65 @@ Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) (dVars:NatSet.t) {str
     This lemma enables us to deduce from each run of the validator the invariant
     that when it succeeds, the errors must be positive.
 **)
-Lemma err_always_positive e (absenv:analysisResult) iv err dVars:
-  validErrorbound e absenv dVars = true ->
+Lemma err_always_positive e tmap (absenv:analysisResult) iv err dVars:
+  validErrorbound e tmap absenv dVars = true ->
   (iv,err) = absenv e ->
   (0 <= Q2R err)%R.
 Proof.
-  destruct e;intros validErrorbound_e absenv_e;
+  destruct e; intros validErrorbound_e absenv_e;
     unfold validErrorbound in validErrorbound_e;
-    rewrite <- absenv_e in validErrorbound_e; simpl in *;
-      andb_to_prop validErrorbound_e.
-  - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
-  - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
-  - inversion R.
-  - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
+    rewrite <- absenv_e in validErrorbound_e; simpl in *.
+  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+    + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+    + destruct (tmap (Var Q m n)); inversion validErrorbound_e.
+  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+    + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+    + destruct (tmap (Const m q)); inversion validErrorbound_e.
+  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+    + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+    + destruct (tmap (Unop u e)); inversion validErrorbound_e.
+  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+    + apply Qle_bool_iff, Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+    + destruct (tmap (Binop b e1 e2));inversion validErrorbound_e.
+  - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+    + apply Qle_bool_iff, Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+    + destruct (tmap (Downcast m e));inversion validErrorbound_e.
 Qed.
 
 Lemma validErrorboundCorrectVariable:
-  forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars,
+  forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m,
     approxEnv E1 absenv fVars dVars E2 ->
-    eval_exp 0%R E1 (toRExp (Var Q v)) nR ->
-    eval_exp (Q2R machineEpsilon) E2 (toRExp (Var Q v)) nF ->
-    validIntervalbounds (Var Q v) absenv P dVars = true ->
-    validErrorbound (Var Q v) absenv dVars = true ->
+    eval_exp E1 (toREval (toRExp (Var Q m v))) nR M0 ->
+    eval_exp E2 (toRExp (Var Q m v)) nF m ->
+    validIntervalbounds (erasure (Var Q m v)) absenv P dVars = true ->
+    validErrorbound (Var Q m v) (typeExpression (Var Q m v)) absenv dVars = true ->
     (forall v,
         NatSet.mem v dVars = true ->
         exists r : R,
-          E1 v = Some r /\
-          (Q2R (fst (fst (absenv (Var Q v)))) <= r <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
+          E1 v = Some (r, M0) /\
+          (Q2R (fst (fst (absenv (Var Q m v)))) <= r <= Q2R (snd (fst (absenv (Var Q m v)))))%R) ->
     (forall v, NatSet.mem v fVars= true ->
-          exists r, E1 v = Some r /\
+          exists r, E1 v = Some (r, M0) /\
                 (Q2R (fst (P v)) <= r <= Q2R (snd (P v)))%R) ->
-    absenv (Var Q v) = ((nlo, nhi), e) ->
+    absenv (Var Q m 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 error_valid dVars_sound P_valid absenv_var.
-  inversion eval_real; inversion eval_float; subst.
-  rename H0 into E1_v;
-    rename H3 into E2_v.
+  intros * approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
+  simpl in eval_real; inversion eval_real; inversion eval_float; subst.
+  rename H2 into E1_v;
+    rename H7 into E2_v.
+  (* assert ((typeExpression (Var Q m v)) (Var Q m v) = Some m) as tEv. *)
+  (* unfold typeExpression. unfold expEqBool. *)
+  (* case_eq (mTypeEqBool m m && (v =? v)); intros; auto. *)
+  (* apply andb_false_iff in H. destruct H. assert (mTypeEqBool m m = true) by (apply EquivEqBoolEq; auto). *)
+  (* congruence. *)
+  (* assert (v =? v = true) by (apply beq_nat_true_iff; auto). *)
+  (* congruence. *)
   simpl in error_valid.
   rewrite absenv_var in error_valid; simpl in error_valid.
+  assert (mTypeEqBool m m && (v =? v) = true).
+  apply andb_true_iff; split; [ rewrite EquivEqBoolEq | apply beq_nat_true_iff ]; auto.
+  rewrite H in error_valid.
   rewrite <- andb_lazy_alt in error_valid.
   andb_to_prop error_valid.
   rename L into error_pos.
@@ -131,19 +161,18 @@ Proof.
         rewrite x_in_union in *.
         congruence.
       * rewrite x_not_bound in error_valid.
-        inversion E1_v; inversion E2_v;
-          subst.
+        inversion E1_v; inversion E2_v; subst.
         eapply Rle_trans; try eauto.
         apply Qle_bool_iff in error_valid.
         apply Qle_Rle in error_valid.
         eapply Rle_trans; eauto.
         rewrite Q2R_mult.
         apply Rmult_le_compat_r.
-        { apply mEps_geq_zero. }
+        { apply inj_eps_posR. } 
         { rewrite <- maxAbs_impl_RmaxAbs.
           apply contained_leq_maxAbs.
           unfold contained; simpl.
-          pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
+          pose proof (validIntervalbounds_sound (erasure (Var Q m x)) A P (E:=fun y : nat => if y =? x then Some (nR, M0) else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
           rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
           apply valid_bounds_prf; try auto.
           intros v v_mem_diff.
@@ -263,7 +292,7 @@ Proof.
   destruct intv_valid.
   eapply Rle_trans.
   - eapply Rmult_le_compat_r.
-    apply mEps_geq_zero.
+    apply inj_eps_posR.
     apply RmaxAbs; eauto.
   - rewrite Q2R_mult in error_valid.
     rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
@@ -324,7 +353,7 @@ Proof.
   rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   apply Rmult_le_compat_r;try (apply Rabs_pos).
-  apply mEps_geq_zero.
+  apply inj_eps_posR.
   rewrite <- maxAbs_impl_RmaxAbs.
   destruct intv_valid.
   eapply RmaxAbs; auto.
@@ -363,7 +392,7 @@ Proof.
   eapply Rle_trans.
   apply Rplus_le_compat_l.
   eapply Rmult_le_compat_r.
-  apply mEps_geq_zero.
+  apply inj_eps_posR.
   Focus 2.
   rewrite Qle_bool_iff in valid_error.
   apply Qle_Rle in valid_error.
@@ -447,7 +476,7 @@ Proof.
   eapply Rle_trans.
   apply Rplus_le_compat_l.
   eapply Rmult_le_compat_r.
-  apply mEps_geq_zero.
+  apply inj_eps_posR.
   Focus 2.
   apply valid_error.
   remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
@@ -995,7 +1024,7 @@ Proof.
     destruct H3.
     unfold RmaxAbsFun.
     apply Rmult_le_compat_r.
-    apply mEps_geq_zero.
+    apply inj_eps_posR.
     apply RmaxAbs; subst; simpl in *.
     + rewrite Q2R_min4.
       repeat rewrite Q2R_mult;
@@ -1885,7 +1914,7 @@ Proof.
         { destruct valid_div_float.
           unfold RmaxAbsFun.
           apply Rmult_le_compat_r.
-          apply mEps_geq_zero.
+          apply inj_eps_posR.
           rewrite <- maxAbs_impl_RmaxAbs.
           unfold RmaxAbsFun.
           apply RmaxAbs; subst; simpl in *.

coq/ssaPrgs.v

@@ -49,7 +49,7 @@ Proof.
     assert (NatSet.In n (NatSet.singleton n)) as in_n by (rewrite NatSet.singleton_spec; auto).
     specialize (fVars_live n in_n).
     destruct fVars_live as [vR E_def].
-    exists vR; constructor; auto.
+    exists vR; econstructor; eauto.
   - exists (perturb (Q2R v) 0); constructor.
     simpl (meps M0); rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
   - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0)
@@ -207,13 +207,12 @@ Proof.
   induction e; intros v' E1 E2 agree_on_vars.
   - split; intros eval_Var.
     + inversion eval_Var; subst.
-      rewrite agree_on_vars in H4.
-      apply (Var_load _ _ _ H1).
-      auto.
+      (*assert (m1 = M0) by (apply ifisMorePreciseM0; auto); subst.*)
+      rewrite agree_on_vars in H2.
+      apply Var_load; auto.
     + inversion eval_Var; subst.
-      rewrite <- agree_on_vars in H4.
-      apply (Var_load _ _ _ H1).
-      auto.
+      rewrite <- agree_on_vars in H2.
+      apply Var_load; auto.
   - split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
   - split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
     + erewrite IHe; eauto.
@@ -238,16 +237,16 @@ Proof.
 revert E1 E2 vR.
   induction f; intros E1 E2 vR agree_on_vars.
   - split; intros bstep_Let; inversion bstep_Let; subst.
-    + erewrite shadowing_free_rewriting_exp in H7; auto.
+    + erewrite shadowing_free_rewriting_exp in H5; auto.
       econstructor; eauto.
       rewrite <- IHf.
-      apply H8.
+      apply H6.
       intros n'; unfold updEnv.
       case_eq (n' =? n); auto.
-    + erewrite <- shadowing_free_rewriting_exp in H7; auto.
+    + erewrite <- shadowing_free_rewriting_exp in H5; auto.
       econstructor; eauto.
       rewrite IHf.
-      apply H8.
+      apply H6.
       intros n'; unfold updEnv.
       case_eq (n' =? n); auto.
   - split; intros bstep_Ret; inversion bstep_Ret; subst.
@@ -281,7 +280,7 @@ Proof.
       rewrite valid_vars in *; congruence.
     + econstructor.
       auto.
-      rewrite H; auto.
+      rewrite H; auto. 
   - inversion eval_e; subst; constructor; auto.
   - inversion eval_e; subst; econstructor; eauto.
   - simpl in valid_vars.
@@ -322,10 +321,10 @@ Proof.
     + unfold updEnv in eval_upd. simpl in *.
       inversion eval_upd; subst.
       case_eq (n =? x); intros; try auto.
-      * unfold toREvalEnv in H4. rewrite H in H4.
-        inversion H4; subst; auto.
-      * unfold toREvalEnv in H4; rewrite H in H4.
+      * rewrite H in H2.
+        inversion H2; subst; auto.