Certificate checking now with division in Coq

coq/ErrorValidation.v

@@ -30,7 +30,15 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
        | Plus => Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
        | Sub => Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
        | Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
-       | Div => Qleb ((maxAbs (subtractIntv (divideIntv ive1 ive2) (divideIntv errIve1 errIve2))) + (maxAbs (divideIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
+       | Div => let nodiv0_fl := orb
+                            (andb (Qleb (ivhi errIve2) 0) (negb (Qeq_bool (ivhi errIve2) 0)))
+                            (andb (Qleb 0 (ivlo errIve2)) (negb (Qeq_bool (ivlo errIve2) 0))) in
+               if nodiv0_fl
+               then Qleb
+                      ((maxAbs (subtractIntv (divideIntv ive1 ive2) (divideIntv errIve1 errIve2)))
+                       + (maxAbs (divideIntv errIve1 errIve2)) * RationalSimps.machineEpsilon)
+                      err
+               else false
        end
    in andb (andb rec errPos) theVal
   end.
@@ -1028,7 +1036,6 @@ Proof.
         repeat rewrite Q2R_plus; auto.
 Qed.
 
-<<<<<<< HEAD
 Lemma validErrorboundCorrectDiv 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 :
   precondValidForExec P cenv ->
   eval_exp 0%R cenv (toRExp e1) nR1 ->
@@ -1074,72 +1081,155 @@ Proof.
   assert (0 <= Q2R err1)%R as err1_pos by (apply (err_always_positive e1 absenv (e1lo,e1hi) err1); auto).
   assert (0 <= Q2R err2)%R as err2_pos by (apply (err_always_positive e2 absenv (e2lo,e2hi) err2); auto).
   clear valid_err1 valid_err2.
-  apply Qle_bool_iff in valid_error.
-  apply Qle_Rle in valid_error.
-  rewrite Q2R_plus, Q2R_mult in valid_error.
-  eapply Rle_trans.
-  Focus 2.
-  apply valid_error.
-  eapply Rplus_le_compat.
-  - (* Similar to other goal *)
-    remember
-      (subtractIntv (divideIntv (e1lo, e1hi) (e2lo, e2hi))
-                    (divideIntv (widenIntv (e1lo, e1hi) err1)
-                                (widenIntv (e2lo, e2hi) err2))) as iv.
-    iv_assert iv iv_unf.
-    destruct iv_unf as [ivl [ivh iv_unf]].
-    rewrite iv_unf.
-    rewrite <- maxAbs_impl_RmaxAbs.
-    assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
-    assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
-    rewrite <- H, <- H0.
-    admit. (* By validity of IV, monotonicity *)
-  - apply Rmult_le_compat_r.
-    + apply mEps_geq_zero.
-    + remember (divideIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
-  iv_assert iv iv_unf.
-  destruct iv_unf as [ivl [ivh iv_unf]].
-  rewrite iv_unf.
-  rewrite <- maxAbs_impl_RmaxAbs.
-  assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
-  assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
-  rewrite <- H, <- H0.
-  admit. (*
-  assert (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1 by admit.
-  rewrite absenv_e1 in valid_bounds_e1.
-  simpl in valid_bounds_e1.
-  pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
-  pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
-  rewrite absenv_e2 in valid_bounds_e2.
-  simpl in valid_bounds_e2.
-  pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
-  pose proof (IntervalArith.interval_multiplication_valid _ _ _ _ H1 H2).
-  unfold IntervalArith.contained in H3.
-  destruct H3.
-  unfold RmaxAbsFun.
-  apply Rmult_le_compat_r.
-  apply mEps_geq_zero.
-  apply RmaxAbs; subst; simpl in *.
-  - rewrite Q2R_min4.
-    repeat rewrite Q2R_mult;
-      repeat rewrite Q2R_minus;
-      repeat rewrite Q2R_plus; auto.
-  - rewrite Q2R_max4.
-    repeat rewrite Q2R_mult;
-      repeat rewrite Q2R_minus;
-      repeat rewrite Q2R_plus; auto.
-Qed. *)
-Admitted.
+  assert (Qleb (ivhi (widenIntv (e2lo, e2hi) err2)) 0 && negb (Qeq_bool (ivhi (widenIntv (e2lo, e2hi) err2)) 0)
+          || Qleb 0 (ivlo (widenIntv (e2lo, e2hi) err2)) && negb (Qeq_bool (ivlo (widenIntv (e2lo, e2hi) err2)) 0)
+          = true) as nodiv0_fl.
+  - case_eq (Qleb (ivhi (widenIntv (e2lo, e2hi) err2)) 0 && negb (Qeq_bool (ivhi (widenIntv (e2lo, e2hi) err2)) 0)
+          || Qleb 0 (ivlo (widenIntv (e2lo, e2hi) err2)) && negb (Qeq_bool (ivlo (widenIntv (e2lo, e2hi) err2)) 0));
+      intros cond_val; rewrite cond_val in valid_error; auto.
+  - rewrite nodiv0_fl in valid_error.
+    pose proof (le_neq_bool_to_lt_prop _ _ nodiv0_fl) as nodiv0_fl_lt.
+    apply Qle_bool_iff in valid_error.
+    apply Qle_Rle in valid_error.
+    rewrite Q2R_plus, Q2R_mult in valid_error.
+    pose proof (validBoundsDiv_uneq_zero e1 e2 absenv P e2lo e2hi err2 absenv_e2 valid_intv) as nodiv0_rl.
+    unfold validIntervalbounds in valid_intv.
+    apply Is_true_eq_left in valid_intv.
+    rewrite absenv_div, absenv_e1, absenv_e2 in valid_intv.
+    apply andb_prop_elim in valid_intv.
+    destruct valid_intv as [valid_rec valid_div].
+    apply andb_prop_elim in valid_rec; apply andb_prop_elim in valid_div.
+    destruct valid_div as [valid_div _].
+    destruct valid_rec as [valid_e1 valid_e2];
+      apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
+    pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_e1 e1_real) as valid_bounds_e1.
+    rewrite absenv_e1 in valid_bounds_e1.
+    simpl in valid_bounds_e1.
+    pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_e2 e2_real) as valid_bounds_e2.
+    rewrite absenv_e2 in valid_bounds_e2.
+    simpl in valid_bounds_e2.
+    clear valid_e1 valid_e2 nodiv0_fl.
+    pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded) as nF1_bounded.
+    pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded) as nF2_bounded.
+    assert (IntervalArith.contained (nR1 / nR2)%R (divideInterval (Q2R e1lo, Q2R e1hi) (Q2R e2lo, Q2R e2hi))) as real_div_contained.
+    + apply IntervalArith.divisionIsValid; simpl; try auto.
+      destruct nodiv0_rl as [A | A]; apply Qlt_Rlt in A; rewrite <- Q2R0_is_0; auto.
+    + assert (IntervalArith.contained (nF1 / nF2)%R (divideInterval (widenInterval (Q2R e1lo, Q2R e1hi) (Q2R err1)) (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))) as float_div_contained.
+      * apply IntervalArith.divisionIsValid; simpl; try auto.
+        unfold widenIntv in nodiv0_fl_lt; simpl in nodiv0_fl_lt.
+        destruct nodiv0_fl_lt as [A | A];
+          apply Qlt_Rlt in A; rewrite <- Q2R0_is_0; rewrite <- Q2R_plus;
+            rewrite <- Q2R_minus; auto.
+      * pose proof (IntervalArith.subtractionIsValid _ _ (nR1 / nR2)%R _ real_div_contained float_div_contained) as contained_prop_error.
+    eapply Rle_trans.
+    Focus 2.
+    apply valid_error.
+    eapply Rplus_le_compat.
+    { (* Similar to other goal *)
+      apply contained_leq_maxAbs in contained_prop_error.
+      rewrite <- maxAbs_impl_RmaxAbs_iv.
+      assert (Q2RP
+         (subtractIntv (divideIntv (e1lo, e1hi) (e2lo, e2hi))
+                       (divideIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2))) =
+              subtractInterval (divideInterval (Q2R e1lo, Q2R e1hi) (Q2R e2lo, Q2R e2hi))
+                               (divideInterval (widenInterval (Q2R e1lo, Q2R e1hi) (Q2R err1))
+                                               (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))).
+      - unfold widenIntv in nodiv0_fl_lt; simpl in nodiv0_fl_lt.
+        unfold IntervalArith.widenInterval, IntervalArith.contained in nF2_bounded; simpl in nF2_bounded.
+        unfold subtractInterval, divideInterval, widenInterval, addInterval, multInterval, absIntvUpd; simpl.
+        rewrite Q2R_min4, Q2R_max4.
+        repeat rewrite Q2R_plus.
+        repeat rewrite Q2R_opp.
+        repeat rewrite Q2R_min4.
+        repeat rewrite Q2R_max4.
+        repeat rewrite Q2R_mult.
+        repeat rewrite Q2R_inv; try hnf; intros.
+        repeat rewrite Q2R_plus, Q2R_minus.
+        auto.
+        + destruct nodiv0_fl_lt.
+          * apply Qlt_Rlt in H0.
+            rewrite <- Q2R_minus in nF2_bounded.
+            rewrite <- Q2R_plus in nF2_bounded.
+            assert (Q2R (e2lo- err2) <= Q2R (e2hi + err2))%R by lra.
+            apply Rle_Qle in H1.
+            rewrite H in H1.
+            apply Qle_Rle in H1.
+            lra.
+          * rewrite H in H0; lra.
+        + destruct nodiv0_fl_lt.
+          * rewrite H in H0; lra.
+          * apply Qlt_Rlt in H0.
+            rewrite <- Q2R_minus in nF2_bounded.
+            rewrite <- Q2R_plus in nF2_bounded.
+            assert (Q2R (e2lo- err2) <= Q2R (e2hi + err2))%R by lra.
+            apply Rle_Qle in H1.
+            rewrite H in H1.
+            apply Qle_Rle in H1.
+            lra.
+        + destruct nodiv0_rl.
+          * apply Qlt_Rlt in H0.
+            rewrite <- Q2R_minus in nF2_bounded.
+            rewrite <- Q2R_plus in nF2_bounded.
+            assert (Q2R e2lo <= Q2R e2hi)%R by lra.
+            apply Rle_Qle in H1.
+            rewrite H in H1.
+            apply Qle_Rle in H1.
+            lra.
+          * rewrite H in H0; lra.
+        + destruct nodiv0_rl.
+          * rewrite H in H0; lra.
+          * apply Qlt_Rlt in H0.
+            rewrite <- Q2R_minus in nF2_bounded.
+            rewrite <- Q2R_plus in nF2_bounded.
+            assert (Q2R e2lo <= Q2R e2hi)%R by lra.
+            apply Rle_Qle in H1.
+            rewrite H in H1.
+            apply Qle_Rle in H1.
+            lra.
+      - rewrite H; auto. }
+    { apply Rmult_le_compat_r.
+      - apply mEps_geq_zero.
+      - apply contained_leq_maxAbs in float_div_contained.
+        rewrite <- maxAbs_impl_RmaxAbs_iv.
+        assert (Q2RP (divideIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) =
+                divideInterval (widenInterval (Q2R e1lo, Q2R e1hi) (Q2R err1))
+                               (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2))).
+        + unfold widenIntv in nodiv0_fl_lt; simpl in nodiv0_fl_lt.
+          unfold IntervalArith.widenInterval, IntervalArith.contained in nF2_bounded; simpl in nF2_bounded.
+          unfold subtractInterval, divideInterval, widenInterval, addInterval, multInterval, absIntvUpd; simpl.
+          rewrite Q2R_min4, Q2R_max4.
+          repeat rewrite Q2R_mult.
+          repeat rewrite Q2R_inv; try hnf; intros.
+          repeat rewrite Q2R_minus, Q2R_plus; auto.
+          * destruct nodiv0_fl_lt.
+            { apply Qlt_Rlt in H0.
+            rewrite <- Q2R_minus in nF2_bounded.
+            rewrite <- Q2R_plus in nF2_bounded.
+            assert (Q2R (e2lo- err2) <= Q2R (e2hi + err2))%R by lra.
+            apply Rle_Qle in H1.
+            rewrite H in H1.
+            apply Qle_Rle in H1.
+            lra. }
+            { rewrite H in H0; lra. }
+          * destruct nodiv0_fl_lt.
+            { rewrite H in H0; lra. }
+            { apply Qlt_Rlt in H0.
+            rewrite <- Q2R_minus in nF2_bounded.
+            rewrite <- Q2R_plus in nF2_bounded.
+            assert (Q2R (e2lo- err2) <= Q2R (e2hi + err2))%R by lra.
+            apply Rle_Qle in H1.
+            rewrite H in H1.
+            apply Qle_Rle in H1.
+            lra. }
+        + rewrite H; auto. }
+Qed.
 
-Lemma validErrorbound_sound (e:exp Q):
-=======
 (**
    Soundness theorem for the error bound validator.
    Proof is by induction on the expression e.
    Each case requires the application of one of the soundness lemmata proven before
 **)
 Theorem validErrorbound_sound (e:exp Q):
->>>>>>> certification
   forall cenv absenv nR nF err P elo ehi,
     precondValidForExec P cenv ->
     eval_exp 0%R cenv (toRExp e) nR ->

coq/Infra/RationalSimps.v

@@ -39,3 +39,19 @@ Proof.
   setoid_rewrite Qmult_comm at 1 2.
   apply Qmult_le_compat_r; auto.
 Qed.
+
+Lemma le_neq_bool_to_lt_prop a b:
+  (Qleb a 0 && negb (Qeq_bool a 0) || Qleb 0 b && negb (Qeq_bool b 0)) = true ->
+  a < 0 \/ 0 < b.
+Proof.
+  intros le_neq_bool.
+  apply Is_true_eq_left in le_neq_bool.
+  apply orb_prop_elim in le_neq_bool.
+  destruct le_neq_bool as [lt_0 | lt_0];
+    apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0];
+      apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0;
+        apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0;
+          rewrite Qle_bool_iff in le_0;
+          rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0];
+            [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
+Qed.
\ No newline at end of file

coq/IntervalArith.v

@@ -155,7 +155,7 @@ Proof.
     + apply Ropp_le_ge_contravar in H0;
         repeat rewrite Ropp_involutive in H0; lra.
   - assert (- / ivlo <= - / a)%R.
-    +  repeat rewrite Ropp_inv_permute; try lra.
+    + repeat rewrite Ropp_inv_permute; try lra.
        eapply RIneq.Rinv_le_contravar; try lra.
     + apply Ropp_le_ge_contravar in H0;
         repeat rewrite Ropp_involutive in H0; lra.

coq/IntervalValidation.v

@@ -110,14 +110,8 @@ Proof.
   apply andb_prop_elim in validBounds.
   destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
   destruct validBounds as [_ nodiv0].
-  apply orb_prop_elim in nodiv0.
-  destruct nodiv0 as [lt_0 | lt_0];
-    apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0];
-      apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0;
-        apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0;
-          rewrite Qle_bool_iff in le_0;
-          rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0];
-            [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
+  apply Is_true_eq_true in nodiv0.
+  apply le_neq_bool_to_lt_prop; auto.
 Qed.
 
 Theorem validIntervalbounds_sound (e:exp Q):