Fix some annoying definitions

coq/abs_err.v

@@ -11,7 +11,7 @@ Definition abs_env:Type := exp R -> interval -> err -> Prop.
   First define when given an interval and an error, when another error is sound overapproximation of the absolute error
 **)
 Definition isSoundErr (error:err) (iv:intv) (propagatedErr:err) :=
-  (error >= machineEpsilon * Rmax (Rabs (IVlo(iv) - propagatedErr)) (Rabs (IVhi(iv) + propagatedErr)))%R.
+  (error >= machineEpsilon * Rmax (Rabs (IVlo iv)) (Rabs (IVhi iv)))%R.
 
 Definition maxAbs (IV:intv) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)).
 

coq/exps.v

@@ -31,8 +31,9 @@ Inductive exp (V:Type): Type :=
 (**
   Define the machine epsilon for floating point operations.
   FIXME: Currently set to 1.0 instead of the concrete value!
-**)
-Definition machineEpsilon:R := realFromNum 11102230246251565 16 16.
+ **)
+Definition machineEpsilon:R := realFromNum 1 1 53.
+(* Definition machineEpsilon:R := realFromNum 11102230246251565 16 16. *)
 (**
   Define a perturbation function to ease writing of basic definitions
 **)

coq/simple_doppler.v

@@ -2,26 +2,27 @@ Require Import Coq.Reals.Reals Interval.Interval_tactic Coq.micromega.Psatz.
 Require Import Daisy.abs_err Daisy.daisy_lang Daisy.newIntervalArith Daisy.exps Daisy.realConversion.
 
 (*
-[  Info   ]
-[  Info   ] Starting specs preprocessing phase
-[  Info   ] Finished specs preprocessing phase
-[  Info   ]
-[  Info   ]
-[  Info   ] Starting range-error phase
-[  Info   ] Machine epsilon 2.220446049250313E-16
-[  Info   ] 331.4: [331.4, 331.4],7.358558207215537e-14
-[  Info   ] u: [-100.0, 100.0],2.220446049250313e-14
-[  Info   ] (331.4 + u): [231.4, 431.4],1.9158008512931703e-13
-[  Info   ] Finished range-error phase
-[  Info   ]
-[  Info   ] Starting info phase
-[  Info   ] doppler
-[  Info   ] abs-error: 1.9158008512931703e-13, range: [231.4, 431.4],
-[  Info   ] rel-error: 8.279173946815775E-16
-[  Info   ] Finished info phase
-[  Info   ] time:
-[  Info   ] info:      7 ms, rangeError:     58 ms, analysis:      8 ms, frontend:   2167 ms,
+[  Info  ]
+[  Info  ] Starting specs preprocessing phase
+[  Info  ] Finished specs preprocessing phase
+[  Info  ]
+[  Info  ]
+[  Info  ] Starting range-error phase
+[  Info  ] Machine epsilon 1.1102230246251565E-16
+[  Info  ] 331.4: [331.4, 331.4],7.358558207215537e-14
+[  Info  ] u: [-100.0, 100.0],2.220446049250313e-14
+[  Info  ] (331.4 + u): [231.4, 431.4],1.9158008512931703e-13
+[  Info  ] Finished range-error phase
+[  Info  ]
+[  Info  ] Starting info phase
+[  Info  ] doppler
+[  Info  ] abs-error: 1.9158008512931703e-13, range: [231.4, 431.4],
+[  Info  ] rel-error: 8.279173946815775E-16
+[  Info  ] Finished info phase
+[  Info  ] time:
+[  Info  ] info:      9 ms, rangeError:    149 ms, analysis:     15 ms, frontend:   2709 ms,
  *)
+
 Definition u:nat := 1.
 (** 1655/5 = 331; 0,4 = 2/5 **)
 Definition cst1:R := 1657 / 5.
@@ -68,10 +69,27 @@ Proof.
       apply (AbsErrConst cst1 (mkInterval cst1 cst1) errCst1); [constructor | ].
       unfold isSoundErr; simpl.
       unfold errCst1, cst1, machineEpsilon.
-      assert (Rabs (1657 / 5) <= (Rabs (1657 / 5)))%R by (apply Req_le; auto).
-      erewrite Rmax_left; auto.
-      unfold realFromNum.
-      unfold negPow.
+      assert (1657 / 5 >= 0)%R by (unfold realFromNum, negPow; interval).
+      unfold Rabs;
+      destruct Rcase_abs as [lt_plus | ge_plus];
+      [ exfalso; apply Rlt_not_le in lt_plus; apply lt_plus; apply Rge_le in H; auto | ].
+      rewrite Rmax_left; [ | apply Req_le; auto].
+      unfold realFromNum, negPow.
+      field_simplify.
+      interval.
+      assert (1657 / 5 - realFromNum 11102230246251565 16 16 >= 0)%R by (unfold realFromNum, negPow; interval).
+      assert (1657 / 5 + realFromNum 11102230246251565 16 16 >= 0)%R by (unfold realFromNum, negPow; interval).
+      unfold Rabs. destruct Rcase_abs.
+      * exfalso.
+        apply Rlt_not_le in r.
+        apply r; apply Rge_le in H; auto.
+      * destruct Rcase_abs as [lt_plus | ge_plus];
+          [ exfalso; apply Rlt_not_le in lt_plus; apply lt_plus; apply Rge_le in H0; auto | ].
+        assert ((1657 / 5 + realFromNum 11102230246251565 16 16) > (1657 / 5 - realFromNum 11102230246251565 16 16))%R by (unfold realFromNum, negPow; interval).
+        erewrite Rmax_left; auto.
+        unfold realFromNum.
+        unfold negPow.
+        interval.
       unfold Rabs.
       assert (1657 / 5 >= 0)%R by interval.
       destruct Rcase_abs.