Addition correct apart from correctness hole for IV checker

coq/ErrorValidation.v

@@ -8,6 +8,32 @@ Section ComputableErrors.
 
   Definition machineEpsilon := (1#(2^53)).
 
+  Lemma mEps_eq_Rmeps:
+    Q2R machineEpsilon = Expressions.machineEpsilon.
+  Proof.
+    unfold Q2R, machineEpsilon, Expressions.machineEpsilon.
+    unfold RealConstruction.realFromNum, RealConstruction.negativePower.
+    unfold Qden.
+    assert (/ (IZR (' (2 ^ 53))) = 1 / (2^53))%R.
+    - assert (2^53 = ' (2^53))%Z by auto.
+      assert ( 1 / (2^53) = / 2^53)%R by lra.
+      rewrite H0.
+      f_equal. unfold IZR. rewrite <- Fcore_Raux.P2R_INR.
+      unfold Fcore_Raux.P2R. simpl; lra.
+    - rewrite H.
+      f_equal. simpl; lra.
+  Qed.
+
+  Lemma mEps_geq_zero:
+    (0 <= Q2R machineEpsilon)%R.
+  Proof.
+    rewrite <- Q2R0_is_0.
+    apply Qle_Rle.
+    unfold machineEpsilon.
+    apply Qle_bool_iff.
+    unfold Qle_bool; auto.
+  Qed.
+
   Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
     let (intv, err) := (env e) in
       match e with
@@ -181,14 +207,15 @@ Section ComputableErrors.
     apply error_valid.
   Qed.
 
-  Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) :
+  Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
       eval_exp 0%R cenv (toRExp e1) nR1 ->
       eval_exp 0%R cenv (toRExp e2) nR2 ->
       eval_exp 0%R cenv (toRExp (Binop Plus e1 e2)) nR ->
       eval_exp (Q2R machineEpsilon) cenv (toRExp e1) nF1 ->
       eval_exp (Q2R machineEpsilon) cenv (toRExp e2) nF2 ->
-      eval_exp (Q2R machineEpsilon) (updEnv 1 nF1 (updEnv 2 nF2 cenv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
+      eval_exp (Q2R machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
       validErrorbound (Binop Plus e1 e2) absenv = true ->
+      validIntervalbounds (Binop Plus e1 e2) absenv P = true ->
       absenv e1 = ((e1lo,e1hi),err1) ->
       absenv e2 = ((e2lo, e2hi),err2) ->
       absenv (Binop Plus e1 e2) = ((alo,ahi),e)->
@@ -196,18 +223,20 @@ Section ComputableErrors.
       (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
       (Rabs (nR - nF) <= (Q2R e))%R.
   Proof.
-    intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
+    intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
     eapply Rle_trans.
     eapply add_abs_err_bounded.
     apply e1_real.
-    admit.
+    rewrite <- mEps_eq_Rmeps.
+    apply e1_float.
     apply e2_real.
-    admit.
-    (* TODO: Fix machine epsilons *)
+    rewrite <- mEps_eq_Rmeps.
+    apply e2_float.
     apply eval_real.
-    admit.
+    rewrite <- mEps_eq_Rmeps; apply eval_float.
     apply err1_bounded.
     apply err2_bounded.
+    rewrite <- mEps_eq_Rmeps.
     unfold validErrorbound in valid_error at 1.
     rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
     apply Is_true_eq_left in valid_error.
@@ -228,16 +257,31 @@ Section ComputableErrors.
     repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
     eapply Rle_trans.
     apply Rplus_le_compat_l.
-    eapply Rmult_le_compat. (* FIXME: Make compat_r when machineEpsilons are fixed *)
-    apply Rabs_pos.
-    admit.
-    Focus 3.
-    apply valid_error.
+    eapply Rmult_le_compat_r.
+    apply mEps_geq_zero.
     Focus 2.
-    admit.
+    apply valid_error.
     eapply Rle_trans.
     eapply Rabs_triang.
     eapply Rplus_le_compat.
+    clear valid_e1 valid_e2.
+    (* TODO: MAke this a lemma *)
+    rewrite Rabs_minus_sym in err1_bounded.
+    assert (Rabs nF1 - Rabs nR1 <= Q2R err1)%R.
+    - eapply Rle_trans; [apply Rabs_triang_inv | auto].
+    - assert (Rabs nF1 <= Rabs nR1 + Q2R err1)%R by lra.
+      (* TODO: Make this a lemma too. This looks lika a coprrectness lemma for IV arithmetic checker*)
+      assert (Rabs nR1 <= RmaxAbsFun (e1lo, e1hi))%R.
+      + unfold validIntervalbounds in valid_intv; simpl in valid_intv.
+        rewrite absenv_e1, absenv_e2, absenv_add in valid_intv.
+        admit.
+      + assert (Rabs nR1 + Q2R err1 <= RmaxAbsFun (e1lo, e1hi) + Q2R err1)%R by (apply Rplus_le_compat_r; auto).
+        eapply Rle_trans.
+        apply H0.
+        eapply Rle_trans.
+        apply H2.
+        apply Rle_abs.
+    - (* similar by lemma *) admit.
   Admitted.
 
   Lemma validErrorboundCorrect (e:exp Q):

coq/Expressions.v

@@ -36,7 +36,7 @@ Inductive exp (V:Type): Type :=
   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.
 (**
   Define a perturbation function to ease writing of basic definitions
 **)