Commit f4d01b0d authored by Heiko Becker's avatar Heiko Becker

Prove errorbound for exact inversion on rationals

parent 139f71f7
......@@ -3,8 +3,8 @@ Proofs of general bounds on the error of arithmetic expressions.
This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Expressions.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps Daisy.Expressions.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
forall cenv:nat -> R,
......@@ -233,4 +233,281 @@ Proof.
repeat rewrite Rabs_mult.
eapply Rmult_le_compat_l; auto.
apply Rabs_pos.
Qed.
Lemma err_prop_inversion_pos nF2 nR2 err2 (e2lo e2hi:Q)
(float_iv_pos : (Q2R 0 < Q2R (e2lo - err2))%R)
(real_iv_pos : (Q2R 0 < Q2R e2lo)%R)
(err2_bounded : (Rabs (nR2 - nF2) <= Q2R err2)%R)
(valid_bounds_e2 : (Q2R e2lo <= nR2 <= Q2R e2hi)%R)
(valid_bounds_e2_err : (Q2R e2lo - Q2R err2 <= nF2 <= Q2R e2hi + Q2R err2)%R)
(err2_pos : (0 <= Q2R err2)%R):
(Rabs (/nR2 - / nF2) <= Q2R err2 * / ((Q2R e2lo- Q2R err2) * (Q2R e2lo- Q2R err2)))%R.
Proof.
unfold Rabs in err2_bounded.
destruct Rcase_abs in err2_bounded.
- rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr in err2_bounded.
rewrite Ropp_involutive in err2_bounded.
assert (nF2 <= nR2 + Q2R err2)%R by lra.
assert (nR2 - Q2R err2 <= nF2)%R by lra.
assert (0 < nR2 - Q2R err2)%R.
+ rewrite <- Q2R0_is_0.
eapply Rlt_le_trans.
apply float_iv_pos.
rewrite Q2R_minus; lra.
+ assert (0 < nF2)%R by (rewrite <- Q2R0_is_0; lra).
apply Rinv_le_contravar in H; try auto.
apply Rinv_le_contravar in H0; try auto.
assert (nR2 < nF2)%R by lra.
apply Rinv_lt_contravar in H3.
* assert (0 < /nR2 - /nF2)%R by lra.
rewrite Rabs_right; try lra.
repeat rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Ropp_le_contravar.
apply H.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (nR2 + - (nR2 + Q2R err2) = - Q2R err2)%R by lra.
rewrite H5.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
{ rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
- rewrite <- Rsub_eq_Ropp_Rplus.
apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra.
- eapply Rmult_le_compat; try lra;
rewrite <- Rsub_eq_Ropp_Rplus;
rewrite <- Q2R_minus, <- Q2R0_is_0; lra. }
{ assert (0 < (nR2 + Q2R err2) * nR2)%R by (apply Rmult_0_lt_preserving; lra); lra. }
* apply Rmult_0_lt_preserving; lra.
- assert (nF2 <= Q2R err2 + nR2)%R by lra.
assert (nR2 - Q2R err2 <= nF2)%R by lra.
assert (0 < nR2 - Q2R err2)%R.
+ rewrite <- Q2R0_is_0.
eapply Rlt_le_trans.
apply float_iv_pos.
rewrite Q2R_minus; lra.
+ assert (0 < nF2)%R.
* rewrite <- Q2R0_is_0.
eapply Rlt_le_trans.
apply float_iv_pos. rewrite Q2R_minus. lra.
* apply Rinv_le_contravar in H; try auto.
apply Rinv_le_contravar in H0; try auto.
assert (nF2 <= nR2)%R by lra.
apply Rinv_le_contravar in H3; try lra.
hnf in H3.
destruct H3.
{ assert (0 < /nF2 - /nR2)%R by lra.
rewrite Rabs_left; try lra.
repeat rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
rewrite Ropp_involutive.
eapply Rle_trans.
eapply Rplus_le_compat_l.
apply H0.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (- nR2 + (nR2 -Q2R err2) = - Q2R err2)%R by lra.
rewrite H5.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_l.
rewrite <- Ropp_inv_permute.
- rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
+ rewrite <- Rsub_eq_Ropp_Rplus.
apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra.
+ eapply Rmult_le_compat; try lra;
rewrite <- Rsub_eq_Ropp_Rplus;
rewrite <- Q2R_minus, <- Q2R0_is_0; lra.
- assert (0 < (nR2 - Q2R err2) * nR2)%R by (apply Rmult_0_lt_preserving; lra); lra. }
{ rewrite Rabs_right; try lra.
repeat rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Ropp_le_contravar.
apply H.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (nR2 + - (Q2R err2 + nR2) = - Q2R err2)%R by lra.
rewrite H4.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
- rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
+ rewrite <- Rsub_eq_Ropp_Rplus.
apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra.
+ eapply Rmult_le_compat; try lra;
rewrite <- Rsub_eq_Ropp_Rplus;
rewrite <- Q2R_minus, <- Q2R0_is_0; lra.
- assert (0 < nR2 * (Q2R err2 + nR2))%R by (apply Rmult_0_lt_preserving; lra); lra. }
Qed.
Lemma err_prop_inversion_neg nF2 nR2 err2 (e2lo e2hi:Q)
(float_iv_neg : (Q2R (e2hi + err2) < Q2R 0)%R)
(real_iv_neg : (Q2R e2hi < Q2R 0)%R)
(err2_bounded : (Rabs (nR2 - nF2) <= Q2R err2)%R)
(valid_bounds_e2 : (Q2R e2lo <= nR2 <= Q2R e2hi)%R)
(valid_bounds_e2_err : (Q2R e2lo - Q2R err2 <= nF2 <= Q2R e2hi + Q2R err2)%R)
(err2_pos : (0 <= Q2R err2)%R):
(Rabs (/nR2 - / nF2) <= Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R.
Proof.
unfold Rabs in err2_bounded.
destruct Rcase_abs in err2_bounded.
- rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr in err2_bounded.
rewrite Ropp_involutive in err2_bounded.
assert (nF2 <= nR2 + Q2R err2)%R by lra.
assert (nR2 - Q2R err2 <= nF2)%R by lra.
assert (nR2 + Q2R err2 < 0)%R.
+ rewrite <- Q2R0_is_0.
eapply Rle_lt_trans.
Focus 2.
apply float_iv_neg.
rewrite Q2R_plus; lra.
+ assert (0 < - (nR2 + Q2R err2))%R by lra.
assert (nF2 < 0)%R.
* rewrite <- Q2R0_is_0; eapply Rle_lt_trans.
apply H.
eapply Rle_lt_trans.
Focus 2.
apply float_iv_neg.
rewrite Q2R_plus; lra.
* assert (0 < - nF2)%R by lra.
apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H.
apply Rinv_le_contravar in H0; try auto.
apply Rinv_le_contravar in H; try auto.
repeat (rewrite <- Ropp_inv_permute in H0; try lra).
repeat (rewrite <- Ropp_inv_permute in H; try lra).
apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H.
repeat (rewrite Ropp_involutive in H, H0).
assert (nR2 < nF2)%R by lra.
apply Ropp_lt_contravar in H5.
apply Rinv_lt_contravar in H5.
{ rewrite <- Ropp_inv_permute in H5; try lra.
rewrite <- Ropp_inv_permute in H5; try lra.
apply Ropp_lt_contravar in H5.
assert (0 < /nR2 - /nF2)%R by lra.
rewrite Rabs_right; try lra.
repeat rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Ropp_le_contravar.
apply H.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (nR2 + - (nR2 + Q2R err2) = - Q2R err2)%R by lra.
rewrite H7.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
- rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
+ apply Rmult_lt_0_inverting; rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; try lra.
+ destruct valid_bounds_e2_err, valid_bounds_e2.
eapply Rle_trans.
eapply Rmult_le_compat_neg_l.
rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; hnf; left; auto.
eapply Rle_trans.
apply H11. lra.
setoid_rewrite Rmult_comm at 1.
eapply Rmult_le_compat_neg_l. hnf; left; lra.
lra.
- assert (0 < (nR2 + Q2R err2) * nR2)%R by (apply Rmult_lt_0_inverting; lra); lra. }
{ rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive.
apply Rmult_lt_0_inverting; lra. }
- assert (nF2 <= Q2R err2 + nR2)%R by lra.
assert (nR2 - Q2R err2 <= nF2)%R by lra.
assert (nR2 + Q2R err2 < 0)%R.
+ rewrite <- Q2R0_is_0.
eapply Rle_lt_trans.
Focus 2.
apply float_iv_neg.
rewrite Q2R_plus; lra.
+ assert (0 < - (Q2R err2 + nR2))%R by lra.
assert (nF2 < 0)%R.
* rewrite <- Q2R0_is_0; eapply Rle_lt_trans.
apply H.
eapply Rle_lt_trans.
Focus 2.
apply float_iv_neg.
rewrite Q2R_plus; lra.
* assert (0 < - nF2)%R by lra.
apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H.
apply Rinv_le_contravar in H0; try auto.
apply Rinv_le_contravar in H; try auto.
repeat (rewrite <- Ropp_inv_permute in H0; try lra).
repeat (rewrite <- Ropp_inv_permute in H; try lra).
apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H.
repeat (rewrite Ropp_involutive in H, H0).
assert (nF2 <= nR2)%R by lra.
apply Ropp_le_contravar in H5.
apply Rinv_le_contravar in H5; try lra.
repeat (rewrite <- Ropp_inv_permute in H5; try lra).
apply Ropp_le_contravar in H5.
repeat rewrite Ropp_involutive in H5.
hnf in H5.
destruct H5.
{ assert (0 < /nF2 - /nR2)%R by lra.
rewrite Rabs_left; try lra.
repeat rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
rewrite Ropp_involutive.
eapply Rle_trans.
eapply Rplus_le_compat_l.
apply H0.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (- nR2 + (nR2 - Q2R err2) = - Q2R err2)%R by lra.
rewrite H7.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_l.
rewrite <- Ropp_inv_permute.
- rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
+ apply Rmult_lt_0_inverting; rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; try lra.
+ destruct valid_bounds_e2_err, valid_bounds_e2.
eapply Rle_trans.
eapply Rmult_le_compat_neg_l.
rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; hnf; left; auto.
eapply Rle_trans.
apply H11. lra.
setoid_rewrite Rmult_comm at 1.
eapply Rmult_le_compat_neg_l. hnf; left; lra.
lra.
- assert (0 < nR2 * (nR2 - Q2R err2))%R by (apply Rmult_lt_0_inverting; lra); lra. }
{ rewrite Rabs_right; try lra.
repeat rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Ropp_le_contravar.
apply H.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (nR2 + - (Q2R err2 + nR2) = - Q2R err2)%R by lra.
rewrite H6.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
- rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
+ apply Rmult_lt_0_inverting; rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; try lra.
+ destruct valid_bounds_e2_err, valid_bounds_e2.
eapply Rle_trans.
eapply Rmult_le_compat_neg_l.
rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; hnf; left; auto.
eapply Rle_trans.
apply H10. lra.
setoid_rewrite Rmult_comm at 1.
eapply Rmult_le_compat_neg_l. hnf; left; lra.
lra.
- assert (0 < (nR2 + Q2R err2) * nR2)%R by (apply Rmult_lt_0_inverting; lra); lra. }
Qed.
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment