Commit 88c19995 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'coq_fixes'

parents d6ede076 2ed096b1
......@@ -19,6 +19,11 @@ coq/*/.*
coq/*/*.vo
coq/output/*
coq/*.time
hol4/*Theory*
hol4/*.ui
hol4/*.uo
hol4/.*
hol4/heap
daisy
rawdata/*
.ensime*
......
......@@ -17,8 +17,7 @@ Proof.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
unfold perturb; simpl.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
rewrite Rabs_err_simpl, Rabs_mult.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
......@@ -235,279 +234,181 @@ Proof.
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.
Lemma err_prop_inversion_pos_real nF nR err elo ehi
(float_iv_pos : (0 < elo - err)%R)
(real_iv_pos : (0 < elo)%R)
(err_bounded : (Rabs (nR - nF) <= err)%R)
(valid_bounds_e2 : (elo <= nR <= ehi)%R)
(valid_bounds_e2_err : (elo - err <= nF <= ehi + err)%R)
(err_pos : (0 <= err)%R):
(Rabs (/nR - / nF) <= err * / ((elo - err) * (elo- err)))%R.
Proof.
rewrite Rabs_case_inverted in err_bounded.
assert (0 < nF)%R as nF_pos by lra.
destruct err_bounded as [ [diff_pos err_bounded] | [diff_neg err_bounded]].
- cut (0 < /nF - / nR)%R.
+ intros abs_neg.
rewrite Rabs_left; try lra.
rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive.
rewrite Ropp_inv_permute; try lra.
apply (Rle_trans _ (/ - nR + / (nR - err))).
* apply Rplus_le_compat_l.
apply Rinv_le_contravar; lra.
* rewrite equal_naming_inv; try lra.
assert (- nR + (nR - err) = - err)%R as simplify_up by lra.
rewrite simplify_up.
unfold Rdiv.
repeat(rewrite <- Ropp_mult_distr_l); rewrite <- Ropp_inv_permute.
{
rewrite <- Ropp_mult_distr_r, Ropp_involutive.
apply Rmult_le_compat_l; try lra.
apply Rinv_le_contravar.
- apply Rmult_0_lt_preserving; lra.
- apply Rmult_le_compat; lra.
}
{ assert (0 < nR * (nR - err))%R by (apply Rmult_0_lt_preserving; lra); lra. }
+ cut (/ nR < /nF)%R.
* intros; lra.
* apply Rinv_lt_contravar; try lra.
apply Rmult_0_lt_preserving; lra.
- cut (0 <= /nR - /nF)%R.
+ intros abs_pos.
rewrite Rabs_right; try lra.
rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive in err_bounded.
rewrite Rsub_eq_Ropp_Rplus.
apply (Rle_trans _ (/nR - / (nR + err))).
* apply Rplus_le_compat_l.
apply Ropp_le_contravar.
apply Rinv_le_contravar; lra.
* rewrite Rsub_eq_Ropp_Rplus, Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
rewrite simpl_up.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
{ rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
- apply Rmult_0_lt_preserving; lra.
- apply Rmult_le_compat; lra.
}
{ assert (0 < nR * (nR + err))%R by (apply Rmult_0_lt_preserving; lra); lra. }
+ cut (/nF <= /nR)%R.
* intros; lra.
* apply Rinv_le_contravar; try lra.
Qed.
Lemma err_prop_inversion_pos nF nR err (elo ehi:Q)
(float_iv_pos : (Q2R 0 < Q2R (elo - err))%R)
(real_iv_pos : (Q2R 0 < Q2R elo)%R)
(err_bounded : (Rabs (nR - nF) <= Q2R err)%R)
(valid_bounds_e2 : (Q2R elo <= nR <= Q2R ehi)%R)
(valid_bounds_e2_err : (Q2R elo - Q2R err <= nF <= Q2R ehi + Q2R err)%R)
(err_pos : (0 <= Q2R err)%R):
(Rabs (/nR - / nF) <= Q2R err * / ((Q2R elo- Q2R err) * (Q2R elo- Q2R err)))%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.
eapply err_prop_inversion_pos_real; try rewrite <- Q2R0_is_0; eauto.
rewrite <- Q2R_minus; auto.
rewrite Q2R0_is_0; auto.
Qed.
Lemma err_prop_inversion_neg_real nF nR err elo ehi
(float_iv_neg : (ehi + err < 0)%R)
(real_iv_neg : (ehi < 0)%R)
(err_bounded : (Rabs (nR - nF) <= err)%R)
(valid_bounds_e : (elo <= nR <= ehi)%R)
(valid_bounds_e_err : (elo - err <= nF <= ehi + err)%R)
(err_pos : (0 <= err)%R):
(Rabs (/nR - / nF) <= err * / ((ehi + err) * (ehi + err)))%R.
Proof.
rewrite Rabs_case_inverted in err_bounded.
assert (nF < 0)%R as nF_neg by lra.
destruct err_bounded as [ [diff_pos err_bounded] | [diff_neg err_bounded]].
- cut (0 < /nF - / nR)%R.
+ intros abs_neg.
rewrite Rabs_left; try lra.
rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive.
rewrite Ropp_inv_permute; try lra.
apply (Rle_trans _ (/ - nR + / (nR - err))).
* apply Rplus_le_compat_l.
assert (0 < - nF)%R by lra.
assert (0 < - (nR - err))%R by lra.
assert (nR - err <= nF)%R as nR_lower by lra.
apply Ropp_le_contravar in nR_lower.
apply Rinv_le_contravar in nR_lower; try lra.
repeat (rewrite <- Ropp_inv_permute in nR_lower; try lra).
* rewrite equal_naming_inv; try lra.
assert (- nR + (nR - err) = - err)%R as simplify_up by lra.
rewrite simplify_up.
unfold Rdiv.
repeat(rewrite <- Ropp_mult_distr_l); rewrite <- Ropp_inv_permute.
{
rewrite <- Ropp_mult_distr_r, Ropp_involutive.
apply Rmult_le_compat_l; try lra.
apply Rinv_le_contravar.
- apply Rmult_lt_0_inverting; lra.
- eapply Rle_trans.
eapply Rmult_le_compat_neg_l; try lra.
instantiate (1 := (nR - err)%R); try lra.
setoid_rewrite Rmult_comm.
eapply Rmult_le_compat_neg_l; lra.
}
{ assert (0 < nR * (nR - err))%R by (apply Rmult_lt_0_inverting; lra); lra. }
+ cut (/ nR < /nF)%R.
* intros; lra.
* apply Rinv_lt_contravar; try lra.
apply Rmult_lt_0_inverting; lra.
- cut (0 <= /nR - /nF)%R.
+ intros abs_pos.
rewrite Rabs_right; try lra.
rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive in err_bounded.
rewrite Rsub_eq_Ropp_Rplus.
apply (Rle_trans _ (/nR - / (nR + err))).
* apply Rplus_le_compat_l.
apply Ropp_le_contravar.
assert (0 < - nF)%R by lra.
assert (0 < - (nR + err))%R by lra.
assert (nF <= nR + err)%R as nR_upper by lra.
apply Ropp_le_contravar in nR_upper.
apply Rinv_le_contravar in nR_upper; try lra.
repeat (rewrite <- Ropp_inv_permute in nR_upper; try lra).
* rewrite Rsub_eq_Ropp_Rplus, Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (nR2 + - (nR2 + Q2R err2) = - Q2R err2)%R by lra.
rewrite H5.
assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
rewrite simpl_up.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- 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. }
- apply Rmult_lt_0_inverting; lra.
- eapply Rle_trans.
eapply Rmult_le_compat_neg_l; try lra.
instantiate (1:= (nR + err)%R); try lra.
setoid_rewrite Rmult_comm.
eapply Rmult_le_compat_neg_l; lra.
}
{ assert (0 < nR * (nR + err))%R by (apply Rmult_lt_0_inverting; lra); lra. }
+ cut (/nF <= /nR)%R.
* intros; lra.
* assert (nR <= nF)%R by lra.
assert (- nF <= - nR)%R as le_inv by lra.
apply Rinv_le_contravar in le_inv; try lra.
repeat (rewrite <- Ropp_inv_permute in le_inv; try 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.
Lemma err_prop_inversion_neg nF nR err (elo ehi:Q)
(float_iv_neg : (Q2R (ehi + err) < Q2R 0)%R)
(real_iv_neg : (Q2R ehi < Q2R 0)%R)
(err_bounded : (Rabs (nR - nF) <= Q2R err)%R)
(valid_bounds_e : (Q2R elo <= nR <= Q2R ehi)%R)
(valid_bounds_e_err : (Q2R elo - Q2R err <= nF <= Q2R ehi + Q2R err)%R)
(err_pos : (0 <= Q2R err)%R):
(Rabs (/nR - / nF) <= Q2R err * / ((Q2R ehi + Q2R err) * (Q2R ehi + Q2R err)))%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
eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra.
rewrite <- Q2R_plus ; auto.
apply valid_bounds_e.
auto.
rewrite Q2R0_is_0; auto.
Qed.
......@@ -14,8 +14,8 @@ Require Import Daisy.IntervalArith Daisy.IntervalArithQ Daisy.ErrorBounds Daisy.
Require Import Daisy.Environments.
(** Error bound validator **)
Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (intv, err) := (env e) in
Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) :=
let (intv, err) := (absenv e) in
let errPos := Qleb 0 err in
match e with
|Var _ v => false
......@@ -23,9 +23,9 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Unop _ _ => false
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
let (ive2, err2) := env e2 in
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
let (ive1, err1) := absenv e1 in
let (ive2, err2) := absenv e2 in
let rec := andb (validErrorbound e1 absenv) (validErrorbound e2 absenv) in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
......@@ -171,6 +171,7 @@ Proof.
rewrite Rabs_mult.
eapply Rle_trans;[ | apply error_valid].
apply Rmult_le_compat;try (apply Rabs_pos);[ | apply H2].
rewrite (delta_0_deterministic (cenv v) delta) in *; auto.
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo H1).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) H4 ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H5 H6).
......@@ -244,7 +245,7 @@ Proof.
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.additionIsValid _ _ _ _ H1 H2).
pose proof (IntervalArith.interval_addition_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
subst; simpl in *.
......@@ -324,7 +325,7 @@ Proof.
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.subtractionIsValid _ _ _ _ H1 H2).
pose proof (IntervalArith.interval_subtraction_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
subst; simpl in *.
......@@ -1774,7 +1775,7 @@ Proof.
assert (IVhi (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)) < 0 \/ 0 < IVlo (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))%R
as no_div_zero_widen
by (unfold widenInterval in *; simpl in *; rewrite Q2R_plus, Q2R_minus in no_div_zero_float; auto).
pose proof (IntervalArith.divisionIsValid _ _ _ _ no_div_zero_widen valid_bounds_e1_err valid_bounds_e2_err) as valid_div_float.
pose proof (IntervalArith.interval_division_valid _ _ _ _ no_div_zero_widen valid_bounds_e1_err valid_bounds_e2_err) as valid_div_float.
unfold IntervalArith.contained, widenInterval in *; simpl in *.
assert (e2lo - err2 == 0 -> False).
* hnf; intros.
......
......@@ -45,7 +45,7 @@ Definition unopEqBool (o1:unop) (o2:unop) :=
(**
Define evaluation for unary operators on reals.
Errors are added on the expression evaluation level later.
Errors are added in the expression evaluation level later.
**)
Definition evalUnop (o:unop) (v:R):=
match o with
......@@ -104,7 +104,7 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
Define a perturbation function to ease writing of basic definitions
**)
Definition perturb (r:R) (e:R) :=
Rmult r (Rplus 1 e).
(r * (1 + e))%R.
(**
Define expression evaluation relation parametric by an "error" epsilon.
......@@ -119,7 +119,7 @@ Inductive eval_exp (eps:R) (E:env) (P:precond) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps E P (Var R x) (E x)
| Param_acc x delta:
((Rabs delta) <= eps)%R ->
((Q2R (fst (P x))) <= E x <= (Q2R (snd (P x))))%R ->
((Q2R (fst (P x))) <= perturb (E x) delta <= (Q2R (snd (P x))))%R ->
eval_exp eps E P (Param R x) (perturb (E x) delta)
| Const_dist n delta:
Rle (Rabs delta) eps ->
......
......@@ -55,17 +55,3 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :R :=
if y =? x
then v
else E y.
(**
In the final proof we will assume that the given environment under which the
expression is executed agrees with the precondition.
Define this as meaning that for a given variable, the environments value must be
contained in the preconditions interval for it.
This definition suffices since Daisys expressions are immutable, hence no
variable can be written twice.
This means that a free variable will never be defined in the program text
**)
Definition precondValidForExec (P:nat->intv) (cenv:env) :=
forall v:nat,
let (ivlo,ivhi) := P v in
(Q2R ivlo <= cenv v <= Q2R ivhi)%R.
\ No newline at end of file
......@@ -22,7 +22,6 @@ Proof.
destruct Rcase_abs; lra.
Qed.
Lemma bound_flip_sub:
forall a b e,
(Rabs (a - b) <= e ->
...