Merge branch 'fixed_point_checking' into 'master'

Add fixed-point checking to FloVer's coq development

See merge request AVA/FloVer!1

coq/CertificateChecker.v

@@ -38,7 +38,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
     CertificateChecker e absenv P defVars = true ->
     exists iv err vR vF m,
       FloverMap.find e absenv = Some (iv, err) /\
-      eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
+      eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
       eval_expr E2 defVars (toRExp e) vF m /\
       (forall vF m,
           eval_expr E2 defVars (toRExp e) vF m ->
@@ -93,7 +93,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
     CertificateCheckerCmd f absenv P defVars = true ->
     exists iv err vR vF m,
       FloverMap.find  (getRetExp f) absenv = Some (iv,err) /\
-    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
     bstep (toRCmd f) E2 defVars vF m /\
     (forall vF m,
         bstep (toRCmd f) E2 defVars vF m ->

coq/Commands.v

@@ -29,7 +29,7 @@ Fixpoint toRCmd (f:cmd Q) :=
 
 Fixpoint toREvalCmd (f:cmd R) :=
   match f with
-  |Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
+  |Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
   |Ret e => Ret (toREval e)
   end.
 

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,47 +7,50 @@ 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 E1 (toRMap defVars) (Const REAL n) nR REAL ->
   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 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
   eval_expr E2 defVars (toRExp e1) e1F m1->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
   eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (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.
+  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  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 REAL REAL) 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))).
+  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 H.
-  pose proof (Rabs_triang (e2R + - e2F) (- ((e1F + e2F) * delta))).
-  pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H1).
+    apply Rabs_triang; apply Rplus_le_compat; try auto.
+    rewrite Rplus_0_r.
+    apply Rplus_le_compat; try auto. }
+  Focus 4.
     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.
+    apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
+    apply Rplus_le_compat; try auto.
     eapply Rle_trans.
-    eapply Rmult_le_compat_l.
-    apply Rabs_pos.
-    apply H3.
-    apply Req_le; auto.
+    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.
 
 (**
@@ -96,24 +104,24 @@ Qed.
 **)
 Lemma subtract_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 (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
   eval_expr E2 defVars (toRExp e1) e1F m1 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
   eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (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.
+  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in sub_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -138,42 +146,58 @@ Proof.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
   repeat rewrite Ropp_plus_distr.
-  rewrite plus_bounds_simplify.
-  rewrite Ropp_involutive.
+  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 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.
-  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].
+    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)
       (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
   eval_expr E2 defVars (toRExp e1) e1F m1 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
   eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
   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.
+  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in mult_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -195,37 +219,34 @@ 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)
       (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
   eval_expr E2 defVars (toRExp e1) e1F m1 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
   eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
   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.
+  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  subst; simpl in H3; auto.
   rewrite delta_0_deterministic in div_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
@@ -246,39 +267,37 @@ 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)
       (e3:expr Q) (e3R:R) (e3F:R)
       (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
   eval_expr E2 defVars (toRExp e1) e1F m1->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
   eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R REAL ->
   eval_expr E2 defVars (toRExp e3) e3F m3->
-  eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
+  eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
   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.
+  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
+  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.
+  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.
-  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.
+    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 REAL ->
+  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/Expressions.v

 (**
   Formalization of the base exprression language for the flover framework
  **)
-From Coq
-Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals
-Structures.Orders.
-Require Import Flover.Infra.RealRationalProps Flover.Infra.RationalSimps
-               Flover.Infra.Ltacs.
-Require Export Flover.Infra.Abbrevs Flover.Infra.RealSimps Flover.Infra.NatSet
-        Flover.IntervalArithQ Flover.IntervalArith Flover.Infra.MachineType.
+From Flover
+     Require Import Infra.RealRationalProps Infra.Ltacs.
+
+From Flover
+     Require Export Infra.Abbrevs Infra.NatSet Infra.MachineType.
 
 (**
   Expressions will use binary operators.
@@ -113,90 +111,6 @@ Inductive expr (V:Type): Type :=
 | Fma: expr V -> expr V -> expr V -> expr V
 | Downcast: mType -> expr V -> expr V.
 
-(**
-  Boolean equality function on exprressions.
-  Used in certificates to define the analysis result as function
-**)
-Fixpoint exprEq (e1:expr Q) (e2:expr Q) :=
-  match e1, e2 with
-  | Var _ v1, Var _ v2 => (v1 =? v2)
-  | Const m1 n1, Const m2 n2 =>
-    (mTypeEq m1 m2) && (Qeq_bool n1 n2)
-  | Unop o1 e11, Unop o2 e22 =>
-    (unopEq o1 o2) && (exprEq e11 e22)
-  | Binop o1 e11 e12, Binop o2 e21 e22 =>
-    (binopEq o1 o2) && (exprEq e11 e21) && (exprEq e12 e22)
-  | Fma e11 e12 e13, Fma e21 e22 e23 =>
-    (exprEq e11 e21) && (exprEq e12 e22) && (exprEq e13 e23)
-  | Downcast m1 f1, Downcast m2 f2 =>
-    (mTypeEq m1 m2) && (exprEq f1 f2)
-  | _, _ => false
-  end.
-
-Lemma exprEq_refl e:
-  exprEq e e = true.
-Proof.
-  induction e; try (apply andb_true_iff; split); simpl in *; auto .
-  - symmetry; apply beq_nat_refl.
-  - apply mTypeEq_refl.
-  - apply Qeq_bool_iff; lra.
-  - case u; auto.
-  - case b; auto.
-  - firstorder.
-  - apply mTypeEq_refl.
-Qed.