From 692353f0dddced2fc6f645f3f45646bc17d57f75 Mon Sep 17 00:00:00 2001
From: Heiko Becker <heikobecker92@gmail.com>
Date: Fri, 26 Aug 2016 15:51:08 +0200
Subject: [PATCH] Move machineEpsilon to Infra.RealSimps

---
 coq/AbsoluteError.v   |  2 +-
 coq/ErrorValidation.v | 11 ++++++-----
 coq/Expressions.v     |  6 +-----
 coq/Infra/RealSimps.v |  2 +-
 4 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/coq/AbsoluteError.v b/coq/AbsoluteError.v
index 370049a..13dc4ff 100644
--- a/coq/AbsoluteError.v
+++ b/coq/AbsoluteError.v
@@ -3,7 +3,7 @@
   used to verify analsysis result in the final theorem of a certificate.
  **)
 Require Import Coq.Reals.Reals.
-Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealConstruction.
+Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealConstruction Daisy.Infra.RealSimps.
 Require Import Daisy.IntervalArith Daisy.Expressions Daisy.Commands.
 
 Definition abs_env:Type := exp R -> interval -> err -> Prop.
diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v
index 1688328..140e494 100644
--- a/coq/ErrorValidation.v
+++ b/coq/ErrorValidation.v
@@ -9,9 +9,9 @@ Section ComputableErrors.
   Definition machineEpsilon := (1#(2^53)).
 
   Lemma mEps_eq_Rmeps:
-    Q2R machineEpsilon = Expressions.machineEpsilon.
+    Q2R machineEpsilon = RealSimps.machineEpsilon.
   Proof.
-    unfold Q2R, machineEpsilon, Expressions.machineEpsilon.
+    unfold Q2R, machineEpsilon, RealSimps.machineEpsilon.
     unfold RealConstruction.realFromNum, RealConstruction.negativePower.
     unfold Qden.
     assert (/ (IZR (' (2 ^ 53))) = 1 / (2^53))%R.
@@ -511,7 +511,8 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
               rewrite Rsub_eq_Ropp_Rplus.
               apply Rplus_ge_compat.
               + destruct (Rle_dec (nR1 * nR2) 0).
-          }
+  Admitted.
+(*          }
           { rewrite Rabs_mult.
             apply Rmult_le_compat.
             - rewrite <- Rabs_mult. apply Rabs_pos.
@@ -544,7 +545,7 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
           simpl.
           rewrite Rplus_assoc; auto.
   Qed.
-
+*)
   Ltac iv_assert iv name:=
     assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
 
@@ -646,5 +647,5 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
           { apply Is_true_eq_left; auto. }
       + inversion valid_error.
   Qed.
-*)
+
 End ComputableErrors.
diff --git a/coq/Expressions.v b/coq/Expressions.v
index c1d4406..92f69f3 100644
--- a/coq/Expressions.v
+++ b/coq/Expressions.v
@@ -32,11 +32,7 @@ Inductive exp (V:Type): Type :=
 | Param: nat -> exp V
 | Const: V -> exp V
 | Binop: binop -> exp V -> exp V -> exp V.
-(**
-  Define the machine epsilon for floating point operations.
-  Current value: 2^(-53)
- **)
-Definition machineEpsilon:R := realFromNum 1 0 53.
+
 (**
   Define a perturbation function to ease writing of basic definitions
 **)
diff --git a/coq/Infra/RealSimps.v b/coq/Infra/RealSimps.v
index 97d482e..c6671d2 100644
--- a/coq/Infra/RealSimps.v
+++ b/coq/Infra/RealSimps.v
@@ -81,7 +81,7 @@ Qed.
   Define the machine epsilon for floating point operations.
   Current value: 2^(-53)
  **)
-Definition machineEpsilon:R := realFromNum 1 1 53.
+Definition machineEpsilon:R := realFromNum 1 0 53.
 
 Lemma RmaxAbs_peel_Rabs a b:
   Rmax (Rabs a) (Rabs b) = Rabs (Rmax (Rabs a) (Rabs b)).
-- 
GitLab