Add Fixed-Point checking to FloVer in Coq.

Refactor error computation in semantics into separate function/Proposition
to be able to differentiate between truncation and rounding-to-nearest error.

coq/Environments.v

 (**
 Environment library.
-Defines the environment type for the Flover framework and a simulation relation between environments.
+Defines the environment type for the Flover framework and a simulation relation
+between environments.
  **)
-Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
-Require Import Flover.Infra.ExpressionAbbrevs Flover.Infra.RationalSimps Flover.Commands.
+From Coq
+     Require Import Reals.Reals micromega.Psatz QArith.Qreals.
+
+From Flover
+     Require Import Infra.ExpressionAbbrevs Infra.RationalSimps Commands.
 
 (**
 Define an approximation relation between two environments.
@@ -12,20 +16,25 @@ It is necessary to have this relation, since two evaluations of the very same
 exprression may yield different values for different machine epsilons
 (or environments that already only approximate each other)
  **)
-Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
+Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
+                      -> NatSet.t -> env -> Prop :=
 |approxRefl defVars A:
    approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
 |approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
    approxEnv E1 defVars A fVars dVars E2 ->
-   (Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R ->
+   (Rabs (v1 - v2) <= computeErrorR v1 m)%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
+   approxEnv (updEnv x v1 E1)
+             (updDefVars x m defVars) A (NatSet.add x fVars) dVars
+             (updEnv x v2 E2)
 |approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
    approxEnv E1 defVars A fVars dVars E2 ->
    FloverMap.find (Var Q x) A = Some (iv, err) ->
    (Rabs (v1 - v2) <= Q2R err)%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
+   approxEnv (updEnv x v1 E1)
+             (updDefVars x m defVars) A fVars (NatSet.add x dVars)
+             (updEnv x v2 E2).
 
 Section RelationProperties.
 
@@ -68,7 +77,7 @@ Section RelationProperties.
     E2 x = Some v2 ->
     NatSet.In x fVars ->
     Gamma x = Some m ->
-    (Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
+    (Rabs (v - v2) <= computeErrorR v m)%R.
   Proof.
     induction approxEnvs;
       intros E1_def E2_def x_free x_typed.

coq/ErrorBounds.v

@@ -7,25 +7,28 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
 Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
 Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
 
-
 Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
   eval_expr E1 (toRMap defVars) (Const M0 n) nR M0 ->
   eval_expr E2 defVars (Const m n) nF m ->
-  (Rabs (nR - nF) <= Rabs n * (Q2R (mTypeToQ m)))%R.
+  (Rabs (nR - nF) <= computeErrorR n m)%R.
 Proof.
   intros eval_real eval_float.
   inversion eval_real; subst.
   rewrite delta_0_deterministic; auto.
   inversion eval_float; subst.
   unfold perturb; simpl.
-  rewrite Rabs_err_simpl, Rabs_mult.
-  apply Rmult_le_compat_l; [apply Rabs_pos | auto].
-  simpl (mTypeToQ M0) in *.
-  apply (Rle_trans _ (Q2R 0) _); try auto.
-  rewrite Q2R0_is_0; lra.
+  unfold computeErrorR.
+  destruct m.
+  { unfold Rminus. rewrite Rplus_opp_r. rewrite Rabs_R0; lra. }
+  all: try rewrite Rabs_err_simpl, Rabs_mult.
+  all: try apply Rmult_le_compat_l; try auto using Rabs_pos.
+  unfold Rminus.
+  rewrite Ropp_plus_distr.
+  rewrite <- Rplus_assoc.
+  rewrite Rplus_opp_r, Rplus_0_l.
+  rewrite Rabs_Ropp; auto.
 Qed.
 
-
 Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
       (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
   eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
@@ -38,16 +41,16 @@ Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
            (Binop Plus (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
-  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%R.
+  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F + e2F) m)%R.
 Proof.
   intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion plus_real; subst.
   assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
   assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
-  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in plus_real; auto.
-  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
+  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join M0 M0) delta); auto.
   unfold evalBinop in *; simpl in *.
   clear delta H3.
   rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
@@ -68,27 +71,32 @@ Proof.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
-  repeat rewrite Ropp_plus_distr.
-  rewrite plus_bounds_simplify.
+  unfold computeErrorR.
   pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
-  rewrite Rplus_assoc.
-  eapply Rle_trans.
-  apply H.
-  pose proof (Rabs_triang (e2R + - e2F) (- ((e1F + e2F) * delta))).
-  pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H1).
-  eapply Rle_trans.
-  apply H4.
-  rewrite <- Rplus_assoc.
-  repeat rewrite <- Rsub_eq_Ropp_Rplus.
-  rewrite Rabs_Ropp.
-  eapply Rplus_le_compat.
-  - eapply Rplus_le_compat; auto.
-  - rewrite Rabs_mult.
+  destruct (join m0 m3);
+    repeat rewrite Ropp_plus_distr; try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
+  { repeat rewrite <- Rplus_assoc.
+    assert (e1R + e2R + - e1F + - e2F = e1R + - e1F + e2R + - e2F)%R by lra.
+    rewrite H1; clear H1.
+    rewrite Rplus_assoc.
+    eapply Rle_trans.
+    apply Rabs_triang; apply Rplus_le_compat; try auto.
+    rewrite Rplus_0_r.
+    apply Rplus_le_compat; try auto. }
+  Focus 4.
     eapply Rle_trans.
-    eapply Rmult_le_compat_l.
-    apply Rabs_pos.
-    apply H3.
-    apply Req_le; auto.
+    apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
+    apply Rplus_le_compat; try auto.
+    eapply Rle_trans.
+    apply Rabs_triang.
+    rewrite Rabs_Ropp. apply Rplus_le_compat; auto.
+  all: eapply Rle_trans; try eapply H.
+  all: setoid_rewrite Rplus_assoc at 2.
+  all: eapply Rplus_le_compat; try auto.
+  all: eapply Rle_trans; try eapply Rabs_triang.
+  all: eapply Rplus_le_compat; try auto.
+  all: rewrite Rabs_Ropp, Rabs_mult.
+  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
 Qed.
 
 (**
@@ -106,14 +114,14 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
            (Binop Sub (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
-  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (mTypeToQ m))))%R.
+  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F - e2F) m)%R.
 Proof.
   intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion sub_real; subst;
   assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
   assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
-  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in sub_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -138,22 +146,38 @@ Proof.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
   repeat rewrite Ropp_plus_distr.
-  rewrite plus_bounds_simplify.
-  rewrite Ropp_involutive.
-  rewrite Rplus_assoc.
-  eapply Rle_trans.
-  apply Rabs_triang.
-  eapply Rle_trans.
-  eapply Rplus_le_compat_l.
-  apply Rabs_triang.
-  rewrite <- Rplus_assoc.
-  setoid_rewrite Rplus_comm at 4.
-  repeat rewrite <- Rsub_eq_Ropp_Rplus.
-  rewrite Rabs_Ropp.
-  rewrite Rabs_minus_sym in bound_e2.
-  apply Rplus_le_compat; [apply Rplus_le_compat; auto | ].
-  rewrite Rabs_mult.
-  eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
+  unfold computeErrorR.
+  pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
+  destruct (join m0 m3);
+    repeat rewrite Ropp_plus_distr; try rewrite Ropp_involutive;
+      try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
+  { repeat rewrite <- Rplus_assoc.
+    assert (e1R + - e2R + - e1F + e2F = e1R + - e1F + - e2R + e2F)%R by lra.
+    rewrite H0; clear H0.
+    rewrite Rplus_assoc.
+    eapply Rle_trans.
+    apply Rabs_triang; apply Rplus_le_compat; try auto.
+    rewrite Rplus_0_r.
+    apply Rplus_le_compat; try auto.
+    rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
+    auto. }
+  Focus 4.
+    eapply Rle_trans.
+    apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
+    apply Rplus_le_compat; try auto.
+    eapply Rle_trans.
+    apply Rabs_triang.
+    rewrite Rabs_Ropp. apply Rplus_le_compat; try auto.
+    rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
+    auto.
+  all: eapply Rle_trans; try eapply Rabs_triang.
+  all: setoid_rewrite Rplus_assoc at 2.
+  all: eapply Rplus_le_compat; try auto.
+  all: eapply Rle_trans; try eapply Rabs_triang.
+  all: eapply Rplus_le_compat.
+  all: try (rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym; auto; fail).
+  all: rewrite Rabs_Ropp, Rabs_mult, <- Rsub_eq_Ropp_Rplus.
+  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
 Qed.
 
 Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
@@ -166,14 +190,14 @@ Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (Binop Mult (Var R 1) (Var R 2)) vF m ->
-  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (mTypeToQ m)))%R.
+  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
 Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion mult_real; subst;
   assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
   assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
-  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in mult_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -195,17 +219,14 @@ Proof.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
-  rewrite Ropp_plus_distr.
-  rewrite <- Rplus_assoc.
-  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
-  eapply Rle_trans.
-  eapply Rabs_triang.
-  eapply Rplus_le_compat_l.
-  rewrite Rabs_Ropp.
-  repeat rewrite Rabs_mult.
-  eapply Rmult_le_compat_l; auto.
-  rewrite <- Rabs_mult.
-  apply Rabs_pos.
+  unfold computeErrorR.
+  destruct (join m0 m3).
+  all: try rewrite Ropp_plus_distr, <- Rplus_assoc.
+  { rewrite Rplus_0_r. rewrite <- Rsub_eq_Ropp_Rplus; lra. }
+  all: eapply Rle_trans; try apply Rabs_triang.
+  all: try rewrite <- Rsub_eq_Ropp_Rplus, Rabs_Ropp; try rewrite Rabs_mult.
+  all: eapply Rplus_le_compat_l; try auto.
+  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
 Qed.
 
 Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
@@ -218,14 +239,14 @@ Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (Binop Div (Var R 1) (Var R 2)) vF m ->
-  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (mTypeToQ m)))%R.
+  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
 Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion div_real; subst;
   assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
   assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
-  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in div_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -246,16 +267,14 @@ Proof.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
-  rewrite Ropp_plus_distr.
-  rewrite <- Rplus_assoc.
-  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
-  eapply Rle_trans.
-  eapply Rabs_triang.
-  eapply Rplus_le_compat_l.
-  rewrite Rabs_Ropp.
-  repeat rewrite Rabs_mult.
-  eapply Rmult_le_compat_l; auto.
-  apply Rabs_pos.
+  unfold computeErrorR.
+  destruct (join m0 m3).
+  all: try rewrite Ropp_plus_distr, <- Rplus_assoc.
+  { rewrite Rplus_0_r. rewrite <- Rsub_eq_Ropp_Rplus; lra. }
+  all: eapply Rle_trans; try apply Rabs_triang.
+  all: try rewrite <- Rsub_eq_Ropp_Rplus, Rabs_Ropp; try rewrite Rabs_mult.
+  all: eapply Rplus_le_compat_l; try auto.
+  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
 Qed.
 
 Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
@@ -271,14 +290,14 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
   eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
            (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
            (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
-  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R.
+  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
 Proof.
   intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
   inversion fma_real; subst;
   assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
   assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
   assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
-  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in fma_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalFma in *; simpl in *.
@@ -300,32 +319,62 @@ Proof.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
-  rewrite Ropp_plus_distr.
-  rewrite <- Rplus_assoc.
-  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
-  rewrite Rsub_eq_Ropp_Rplus.
-  rewrite Rsub_eq_Ropp_Rplus.
-  rewrite Rsub_eq_Ropp_Rplus.
-  rewrite <- Rplus_assoc.
-  setoid_rewrite Rplus_comm at 8.
-  rewrite <- Rplus_assoc.
-  setoid_rewrite Rplus_comm at 9.
-  rewrite Rplus_assoc.
-  setoid_rewrite Rplus_assoc at 2.
-  rewrite <- Rplus_assoc.
-  rewrite <- Rsub_eq_Ropp_Rplus.
-  rewrite <- Rsub_eq_Ropp_Rplus.
-  rewrite <- Ropp_plus_distr.
-  rewrite <- Rsub_eq_Ropp_Rplus.
-  eapply Rle_trans.
-  eapply Rabs_triang.
-  eapply Rplus_le_compat_l.
-  rewrite Rabs_Ropp.
-  repeat rewrite Rabs_mult.
-  eapply Rmult_le_compat_l; auto.
-  apply Rabs_pos.
+  unfold computeErrorR.
+  destruct (join3 m0 m4 m5); rewrite Ropp_plus_distr.
+  { rewrite Rplus_0_r; hnf; right; f_equal; lra. }
+  Focus 4.
+    rewrite <- Rplus_assoc.
+    eapply Rle_trans.
+    eapply Rabs_triang.
+    rewrite Rabs_Ropp.
+    eapply Rplus_le_compat; try auto.
+    hnf; right; f_equal; lra.
+  all: repeat rewrite <- Rplus_assoc.
+  all: setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
+  all: repeat rewrite Rsub_eq_Ropp_Rplus.
+  all: rewrite <- Rplus_assoc.
+  all: setoid_rewrite Rplus_comm at 8.
+  all: try rewrite <- Rplus_assoc.
+  all: try setoid_rewrite Rplus_comm at 9.
+  all: eapply Rle_trans; try eapply Rabs_triang.
+  all: rewrite Rabs_Ropp.
+  all: repeat rewrite Rplus_assoc.
+  all: try rewrite <- Ropp_plus_distr.
+  all: apply Rplus_le_compat_l.
+  all: rewrite Rabs_mult; apply Rmult_le_compat_l; auto using Rabs_pos.
 Qed.
 
+Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (mEps m:mType) defVars:
+  eval_expr E1 (toRMap defVars) (toREval e) nR M0 ->
+  eval_expr E2 defVars e nF1 m ->
+  eval_expr (updEnv 1 nF1 emptyEnv)
+           (updDefVars 1 m defVars)
+           (toRExp (Downcast mEps (Var Q 1))) nF mEps->
+  (Rabs (nR - nF1) <= err)%R ->
+  (Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%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 H0; subst.
+    unfold perturb; simpl.
+    unfold updEnv in H3; simpl in H3; inversion H3; subst.
+    unfold computeErrorR.
+    destruct mEps.
+    { unfold Rminus. rewrite Rplus_opp_r, Rabs_R0; lra. }
+    all: replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra.
+    all: replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp).
+    all: try rewrite Rabs_mult; try apply Rmult_le_compat_l; auto using Rabs_pos.
+    unfold Rminus.
+    rewrite Ropp_plus_distr, <- Rplus_assoc.
+    rewrite Rplus_opp_r, Rplus_0_l, Rabs_Ropp; auto.
+Qed.
 
 Lemma err_prop_inversion_pos_real nF nR err elo ehi
       (float_iv_pos : (0 < elo - err)%R)
@@ -504,32 +553,3 @@ Proof.
   apply valid_bounds_e.
   auto.
 Qed.
-
-Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval e) nR M0 ->
-  eval_expr E2 defVars e nF1 m ->
-  eval_expr (updEnv 1 nF1 emptyEnv)
-           (updDefVars 1 m defVars)
-           (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
-  (Rabs (nR - nF1) <= err)%R ->
-  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (mTypeToQ 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 H0; subst.
-    unfold perturb; simpl.
-    unfold updEnv in H3; simpl in H3; inversion H3; subst.
-    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,6 +9,7 @@
 From Coq
      Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
      micromega.Psatz Reals.Reals.
+
 From Flover
      Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
      Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
@@ -23,13 +24,13 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
   | Some (intv, err), Some m =>
     if (Qleb 0 err) (* encoding soundness: errors are positive *)
     then
-      match e with (* case analysis for the exprression *)
+      match e with (* case analysis for the expression *)
       |Var _ v =>
        if (NatSet.mem v dVars)
        then true (* defined variables are checked at definition point *)
-       else (Qleb (maxAbs intv * (mTypeToQ m)) err)
-      |Const _ n =>
-       Qleb (maxAbs intv * (mTypeToQ m)) err
+       else Qleb (computeErrorQ (maxAbs intv) m) err
+      |Const m n =>
+       Qleb (computeErrorQ (maxAbs intv) m) err
       |Unop Neg e1 =>
        if (validErrorbound e1 typeMap A dVars)
        then
@@ -51,11 +52,15 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
            let upperBoundE2 := maxAbs ive2 in
            match b with
            | Plus =>
-             Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
+             let mAbs := (maxAbs (addIntv errIve1 errIve2)) in
+             Qleb (err1 + err2 + computeErrorQ mAbs m) err
            | Sub =>
-             Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
+             let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
+             Qleb (err1 + err2 + computeErrorQ mAbs m) err
            | Mult =>
-             Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
+             let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
+             let eProp := (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) in
+             Qleb (eProp + computeErrorQ mAbs m) err
            | Div =>
              if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
                  ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
@@ -63,7 +68,9 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
                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)) * (mTypeToQ m)) err
+               let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
+               let eProp := (upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) in
+               Qleb (eProp + computeErrorQ mAbs m) err
              else false
            end
          | _, _ => false
@@ -84,7 +91,8 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
             let upperBoundE3 := maxAbs ive3 in
             let errIntv_prod := multIntv errIve2 errIve3 in
             let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
-            Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIve1 errIntv_prod)) * (mTypeToQ m)) err
+            let mAbs := (maxAbs (addIntv errIve1 errIntv_prod)) in
+            Qleb (err1 + mult_error_bound + computeErrorQ mAbs m) err
           | _, _, _ => false
           end
         else false
@@ -94,7 +102,8 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
          match FloverMap.find e1 A with
          | Some (ive1, err1) =>
           let errIve1 := widenIntv ive1 err1 in
-          (Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
+          let mAbs := maxAbs errIve1 in
+          Qleb (err1 + computeErrorQ mAbs m1) err
          | None => false
          end
        else
@@ -140,18 +149,6 @@ Proof.
       auto.
 Qed.
 
-Ltac destruct_ex H pat :=
-  match type of H with
-  | exists v, ?H' =>
-               let vFresh:=fresh v in
-               let fN := fresh "ex" in
-               destruct H as [vFresh fN];
-               destruct_ex fN pat
-  | _ => destruct H as pat
-  end.
-
-Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
-
 Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P fVars
       dVars Gamma exprTypes:
     eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
@@ -217,17 +214,15 @@ Proof.
     apply not_in_not_mem in v_fVar.
     assert (v ∈ fVars) as v_in_fVars by set_tac.
     pose proof (approxEnv_fVar_bounded approxCEnv E1_v H6 v_in_fVars H5).
-    eapply Rle_trans.
-    apply H.
+    eapply Rle_trans; eauto.
     canonize_hyps.
-    rewrite Q2R_mult in error_valid.
     repeat destr_factorize.
-    rewrite <- maxAbs_impl_RmaxAbs in error_valid.
+    rewrite computeErrorQ_computeErrorR in error_valid.
     eapply Rle_trans; eauto.
-    eapply Rmult_le_compat_r.
-    + apply mTypeToQ_pos_R.
-    + destruct bounds_valid as [valid_lo valid_hi].
-      apply RmaxAbs; eauto.
+    rewrite <- maxAbs_impl_RmaxAbs.
+    apply computeErrorR_up.
+    apply contained_leq_maxAbs.
+    simpl in *; auto.
 Qed.
 
 Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR  Gamma:
@@ -237,11 +232,9 @@ Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR  Gamma:
 Proof.
   intros eval_real .
   repeat eexists.
-  econstructor.
-  rewrite Rabs_eq_Qabs.
-  apply Qle_Rle.
-  rewrite Qabs_pos; try lra.
-  apply mTypeToQ_pos_Q. lra.
+  eapply Const_dist'; eauto.
+  instantiate (1:= 0%R).
+  rewrite Rabs_R0. auto using mTypeToR_pos_R.
 Qed.
 
 Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars:
@@ -259,17 +252,13 @@ Proof.
   eapply const_abs_err_bounded; eauto.
   rename R into error_valid.
   inversion eval_real; subst.
-  simpl in *; rewrite Q2R0_is_0 in *.
-  rewrite delta_0_deterministic in intv_valid; auto.
-  apply Qle_bool_iff in error_valid.
-  apply Qle_Rle in error_valid.
-  destruct intv_valid.
-  eapply Rle_trans.
-  - eapply Rmult_le_compat_r.
-    apply mTypeToQ_pos_R.
-    apply RmaxAbs; eauto.
-  - rewrite Q2R_mult in error_valid.
-    rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
+  canonize_hyps.
+  eapply Rle_trans; eauto.
+  rewrite computeErrorQ_computeErrorR.
+  rewrite <- maxAbs_impl_RmaxAbs.
+  apply computeErrorR_up.
+  apply contained_leq_maxAbs.
+  simpl in *; auto.
 Qed.
 
 Lemma validErrorboundCorrectAddition E1 E2 A
@@ -309,27 +298,12 @@ Proof.
   rename R0 into valid_error.
   eapply Rle_trans.