Commit 473b51a3 authored by Heiko Becker's avatar Heiko Becker

Remove the double definition of the machine epsilon

parent ebec7fd3
......@@ -5,7 +5,7 @@
as shown in the soundness theorem.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation.
Require Export Coq.QArith.QArith.
......@@ -25,7 +25,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (cenv:env_ty) (vR:R) (vF:R),
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) vR ->
eval_exp machineEpsilon cenv (toRExp e) vF ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e) vF ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
......@@ -46,5 +46,4 @@ Proof.
destruct H as [ivlo [ ivhi iv_eq]].
subst; rewrite absenv_eq in *; simpl in *.
eapply (validErrorbound_sound e cenv absenv vR vF err P); eauto.
rewrite mEps_eq_Rmeps; auto.
Qed.
\ No newline at end of file
......@@ -4,13 +4,13 @@ This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
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.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps Daisy.Expressions.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
forall cenv:nat -> R,
eval_exp 0%R cenv (Const n) nR ->
eval_exp machineEpsilon cenv (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * machineEpsilon)%R.
eval_exp (Q2R machineEpsilon) cenv (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
Proof.
intros cenv eval_real eval_float.
inversion eval_real; subst.
......@@ -24,8 +24,8 @@ Qed.
Lemma param_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R):
eval_exp 0%R cenv (Param R n) nR ->
eval_exp machineEpsilon cenv (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (cenv n) * machineEpsilon)%R.
eval_exp (Q2R machineEpsilon) cenv (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (cenv n) * (Q2R machineEpsilon))%R.
Proof.
intros eval_real eval_float.
inversion eval_real; subst.
......@@ -39,14 +39,14 @@ Qed.
Lemma add_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 (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Plus e1 e2) vR ->
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Plus (Var R 1) (Var R 2)) vF ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Plus (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 + e2F) * (Q2R machineEpsilon)))%R.
Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
......@@ -98,14 +98,14 @@ Qed.
**)
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 (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Sub e1 e2) vR ->
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
eval_exp (Q2R 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 - e2F)) * (Q2R 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 *)
......@@ -150,12 +150,12 @@ Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env_ty) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp machineEpsilon cenv e1 e1F ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Mult e1 e2) vR ->
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * machineEpsilon)%R.
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
......@@ -194,12 +194,12 @@ Qed.
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env_ty) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp machineEpsilon cenv e1 e1F ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp (Q2R machineEpsilon) cenv e2 e2F ->
eval_exp 0%R cenv (Binop Div e1 e2) vR ->
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * machineEpsilon)%R.
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
......
(**
This file contains the coq implementation of the error bound validator as well
as its soundness proof. The function validErrorbound is the Error bound
......@@ -199,16 +198,13 @@ Proof.
eapply Rle_trans.
eapply add_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 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.
andb_to_prop valid_error.
......@@ -284,16 +280,13 @@ Proof.
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 eval_float.
apply err1_bounded.
apply err2_bounded.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_sub, absenv_e1, absenv_e2 in valid_error.
andb_to_prop valid_error.
......@@ -373,13 +366,6 @@ Proof.
pose proof (ivbounds_approximatesPrecond_sound (Binop Mult e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
eapply (mult_abs_err_bounded (toRExp e1) _ _ (toRExp e2)); eauto.
rewrite <- mEps_eq_Rmeps.
apply e1_float.
rewrite <- mEps_eq_Rmeps.
apply e2_float.
rewrite <- mEps_eq_Rmeps.
apply eval_float.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_mult, absenv_e1, absenv_e2 in valid_error.
andb_to_prop valid_error.
......@@ -952,7 +938,6 @@ Proof.
valid_error valid_intv absenv_e1 absenv_e2 absenv_div
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Div e1 e2) absenv P valid_intv) as env_approx_p.
rewrite mEps_eq_Rmeps in e1_float, e2_float, eval_float.
eapply Rle_trans.
apply (div_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv); auto.
unfold validErrorbound in valid_error at 1;
......@@ -1807,7 +1792,6 @@ Proof.
apply Rle_Qle in H3. lra. }
{ destruct valid_div_float.
unfold RmaxAbsFun.
rewrite <- mEps_eq_Rmeps.
apply Rmult_le_compat_r.
apply mEps_geq_zero.
rewrite <- maxAbs_impl_RmaxAbs.
......
......@@ -147,30 +147,6 @@ Proof.
unfold Q2RP; destruct iv; apply minAbs_impl_RminAbs.
Qed.
Lemma mEps_eq_Rmeps:
Q2R RationalSimps.machineEpsilon = RealSimps.machineEpsilon.
Proof.
unfold Q2R, RationalSimps.machineEpsilon, RealSimps.machineEpsilon.
unfold Qden.
unfold Rdiv.
f_equal.
- f_equal.
assert (2^53 = ' (2^53))%Z by auto.
rewrite <- H.
unfold Z.pow.
rewrite (Zpower_pos_is_exp 52 1).
rewrite mult_IZR.
rewrite (Zpower_pos_is_exp 26 26).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 13 13).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 12 1).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 6 6).
repeat rewrite (Zpower_pos_is_exp 3 3).
repeat rewrite mult_IZR. simpl. lra.
Qed.
Lemma mEps_geq_zero:
(0 <= Q2R RationalSimps.machineEpsilon)%R.
Proof.
......@@ -181,54 +157,6 @@ Proof.
unfold Qle_bool; auto.
Qed.
Lemma positive_inversion_error_prop v err:
(0 <= err)%R ->
(0 < v)%R ->
(0 < (v - err))%R ->
( /(v - err) - (/v) <= (/ ((v - err) * (v - err))) * err)%R.
Proof.
intros err_pos v_neq_0 verr_neq_0.
assert (v - err <= v)%R as verr_lt_v by lra.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
rewrite <- Rsub_eq_Ropp_Rplus.
assert (v - err - v = - err)%R as v_simp by lra.
rewrite v_simp.
assert (0 < (v - err) * v)%R by (apply Rmult_0_lt_preserving; auto).
assert (0 < (v - err) * (v - err))%R by (apply Rmult_0_lt_preserving; auto).
unfold Rdiv.
rewrite Rmult_comm.
repeat rewrite <- (Ropp_mult_distr_r).
rewrite <- Ropp_inv_permute; try lra.
rewrite <- (Ropp_mult_distr_l).
rewrite Ropp_involutive.
apply Rmult_le_compat_r; try lra.
apply Rinv_le_contravar; try lra.
apply Rmult_le_compat_l; lra.
Qed.
Lemma negative_inversion_error_prop v err:
(0 <= err)%R ->
(v < 0)%R ->
((v + err) < 0)%R ->
( / v - (/ (v + err)) <= (/ ((v + err) * (v + err))) * err)%R.
Proof.
intros err_pos v_neq_0 verr_neq_0.
assert (0 < - v)%R as opp_v by lra.
assert (0 < - v - err)%R as opp_verr by lra.
pose proof (positive_inversion_error_prop (- v) err err_pos opp_v opp_verr) as the_goal.
assert (/ (- v - err) - / - v = / v - / (v + err))%R as eq.
- setoid_rewrite Rsub_eq_Ropp_Rplus at 2; rewrite <- Ropp_plus_distr.
repeat (rewrite <- Ropp_inv_permute; try lra).
- rewrite eq in the_goal.
assert (- v - err = - (v + err))%R as v_err_opp by lra.
repeat rewrite v_err_opp in the_goal.
rewrite <- Ropp_mult_distr_r, <- Ropp_mult_distr_l in the_goal.
rewrite Ropp_involutive in the_goal.
assumption.
Qed.
Lemma minAbs_positive_iv_is_lo a b:
(0 < a)%R ->
(a <= b)%R ->
......
......@@ -76,11 +76,6 @@ Proof.
rewrite Rsqr_0 in Rabs_eq.
apply Rsqr_0_uniq in Rabs_eq; assumption.
Qed.
(**
Define the machine epsilon for floating point operations.
Current value: 2^(-53)
**)
Definition machineEpsilon:R := (1/2^53).
Lemma RmaxAbs_peel_Rabs a b:
Rmax (Rabs a) (Rabs b) = Rabs (Rmax (Rabs a) (Rabs b)).
......
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