Prove subtraction correct for error bound validation

coq/ErrorBounds.v

@@ -97,7 +97,7 @@ Qed.
 (**
   Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
 **)
-Lemma substract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
+Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
   eval_exp 0%R cenv e1 e1R ->
   eval_exp machineEpsilon cenv e1 e1F ->
   eval_exp 0%R cenv e2 e2R ->
@@ -106,7 +106,7 @@ Lemma substract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e
   eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv))  (Binop Sub (Var R 1) (Var R 2)) vF ->
   (Rabs (e1R - e1F) <= err1)%R ->
   (Rabs (e2R - e2F) <= err2)%R ->
-  (Rabs (vR - vF) <= err1 + err2 + (Rabs (e1F - e2F) * machineEpsilon))%R.
+  (Rabs (vR - vF) <= err1 + err2 + ((Rabs e1F + Rabs e2F) * machineEpsilon))%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 *)
@@ -156,5 +156,11 @@ Proof.
        eapply Rmult_le_compat_l.
        apply Rabs_pos.
        apply H2.
+       rewrite Rsub_eq_Ropp_Rplus.
+       eapply Rle_trans.
+       eapply Rmult_le_compat_r.
+       unfold machineEpsilon, RealConstruction.realFromNum, RealConstruction.negativePower; interval.
+       apply Rabs_triang.
+       rewrite Rabs_Ropp.
        apply Req_le; auto.
 Qed.
\ No newline at end of file

coq/ErrorValidation.v

@@ -56,7 +56,7 @@ Section ComputableErrors.
             match b with
             | Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * machineEpsilon) err
             (* TODO:Validity of next two computations *)
-            | Sub => Qleb (err1 + err2 + (Qabs (e1F - e2F) * machineEpsilon)) err
+            | Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * machineEpsilon)) err
             | Mult => Qleb ((upperBoundE1 * upperBoundE2) + (e1F * e2F) + (e1F * e2F * err1) + (e1F * e2F * err2) + (e1F * e2F * err1 * err2) + (((e1F * e2F) + (e1F * e2F * err1) + (e1F * e2F * err2) + (e1F * e2F * err1 * err2))*machineEpsilon)) err
             | Div => false
             end
@@ -250,10 +250,8 @@ Section ComputableErrors.
     repeat rewrite Q2R_plus in valid_error.
     repeat rewrite Q2R_mult in valid_error.
     repeat rewrite Q2R_plus in valid_error.
-    repeat rewrite Q2R_mult in valid_error.
     repeat rewrite <- Rabs_eq_Qabs in valid_error.
     repeat rewrite Q2R_plus in valid_error.
-    repeat rewrite Q2R_mult in valid_error.
     repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
     eapply Rle_trans.
     apply Rplus_le_compat_l.
@@ -261,10 +259,85 @@ Section ComputableErrors.
     apply mEps_geq_zero.
     Focus 2.
     apply valid_error.
+    clear valid_e1 valid_e2.
     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 validErrorboundCorrectSubtraction 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 Sub e1 e2)) nR ->
+      eval_exp (Q2R machineEpsilon) cenv (toRExp e1) nF1 ->
+      eval_exp (Q2R machineEpsilon) cenv (toRExp e2) nF2 ->
+      eval_exp (Q2R machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
+      validErrorbound (Binop Sub e1 e2) absenv = true ->
+      validIntervalbounds (Binop Sub e1 e2) absenv P = true ->
+      absenv e1 = ((e1lo,e1hi),err1) ->
+      absenv e2 = ((e2lo, e2hi),err2) ->
+      absenv (Binop Sub e1 e2) = ((alo,ahi),e)->
+      (Rabs (nR1 - nF1) <= (Q2R err1))%R ->
+      (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 valid_intv absenv_e1 absenv_e2 absenv_add
+           err1_bounded err2_bounded.
+    eapply Rle_trans.
+    eapply subtract_abs_err_bounded.
+    apply e1_real.
+    rewrite <- mEps_eq_Rmeps.
+    apply e1_float.
+    apply e2_real.
+    rewrite <- mEps_eq_Rmeps.
+    apply e2_float.
+    apply eval_real.
+    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.
+    apply andb_prop_elim in valid_error.
+    destruct valid_error as [valid_rec valid_error].
+    apply andb_prop_elim in valid_rec.
+    (** FIXME: Remove if trouble ahead *)
+    clear valid_rec.
+    apply Is_true_eq_true in valid_error.
+    apply Qle_bool_iff in valid_error.
+    apply Qle_Rle in valid_error.
+    repeat rewrite Q2R_plus in valid_error.
+    repeat rewrite Q2R_mult in valid_error.
+    repeat rewrite Q2R_plus in valid_error.
+    repeat rewrite <- Rabs_eq_Qabs in valid_error.
+    repeat rewrite Q2R_plus in valid_error.
+    repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
+    eapply Rle_trans.
+    apply Rplus_le_compat_l.
+    eapply Rmult_le_compat_r.
+    apply mEps_geq_zero.
+    Focus 2.
+    apply valid_error.
+    eapply Rplus_le_compat.
     (* TODO: MAke this a lemma *)
     rewrite Rabs_minus_sym in err1_bounded.
     assert (Rabs nF1 - Rabs nR1 <= Q2R err1)%R.
@@ -291,14 +364,41 @@ Section ComputableErrors.
       eval_exp 0%R cenv (toRExp e) nR ->
       eval_exp (Q2R machineEpsilon) cenv (toRExp e) nF ->
       validErrorbound e absenv = true ->
+      validIntervalbounds e absenv P = true ->
       absenv e = ((elo,ehi),err) ->
       (Rabs (nR - nF) <= (Q2R err))%R.
   Proof.
     induction e.
     - intros; simpl in *.
-      rewrite H4 in H3; inversion H3.
+      rewrite H5 in H3; rewrite H5 in H4; inversion H3.
     - intros; eapply validErrorboundCorrectParam; eauto.
     - intros; eapply validErrorboundCorrectConstant; eauto.
+    - intros. destruct b.
+      + inversion H1; subst.
+        apply existential_rewriting in H2.
+        destruct H2.
+        destruct H2.
+        destruct H2.
+        destruct H6.
+        eapply (validErrorboundCorrectAddition cenv absenv e1 e2); eauto.
+        destruct (absenv e1) as [iv1 err1]; destruct iv1; admit.
+        destruct (absenv e2) as [iv2 err2]; destruct iv2; admit.
+        eapply IHe1; auto.
+        apply H. apply H0. apply H11. apply H2. admit.
+        admit. admit.
+        eapply IHe2; auto.
+        apply H. apply H0.
+        apply H12. apply H6.
+        admit. admit. admit.
+      + admit.
+      + admit.
+      + simpl in H3.
+        rewrite H5 in H3.
+        apply Is_true_eq_left in H3.
+        destruct (absenv e1); destruct (absenv e2).
+        apply andb_prop_elim in H3.
+        destruct H3.
+        simpl in H6; contradiction.
   Admitted.
 
 End ComputableErrors.