Commit 8768d1b7 authored by Raphaël Monat's avatar Raphaël Monat

ErrorBounds translated to setting with mixed precision

parent 85fe6a93
......@@ -7,10 +7,10 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
eval_exp 0%R E1 (Const n) nR ->
eval_exp (Q2R machineEpsilon) E2 (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType):
eval_exp E1 (Const n) nR M0 ->
eval_exp E2 (Const n) nF M0 ->
(Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
Proof.
intros eval_real eval_float.
inversion eval_real; subst.
......@@ -19,6 +19,10 @@ Proof.
unfold perturb; simpl.
rewrite Rabs_err_simpl, Rabs_mult.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
simpl (meps M0) in *.
apply (Rle_trans _ (Q2R 0) _); try auto.
apply Qle_Rle; apply inj_eps_pos.
simpl (meps M0) in H0; rewrite Q2R0_is_0 in H0; auto.
Qed.
(*
......@@ -42,39 +46,42 @@ Qed.
*)
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q):
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Plus (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var R 1) (Var R 2)) vF ->
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m ->
eval_exp E1 (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Plus (Var R m 1) (Var R m 2)) vF m->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%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 *)
inversion plus_real; subst.
inversion plus_real; subst;
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in plus_real.
rewrite (meps_0_deterministic H5 e2_real) in plus_real.
clear H4 H5 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in plus_real.
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in plus_real.
clear H6 H7 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion plus_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
inversion H7; subst; inversion H8; subst.
unfold updEnv; simpl.
unfold updEnv in H0,H1; simpl in *.
symmetry in H0, H1.
inversion H0; inversion H1; subst.
unfold updEnv in H9,H11; simpl in *.
symmetry in H9, H11.
inversion H9; inversion H11; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
clear plus_float H7 H8 plus_real e1_real e1_float e2_real e2_float H9 H11.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -87,7 +94,7 @@ Proof.
pose proof (Rabs_triang (e2R + - e2F) (- ((e1F + e2F) * delta))).
pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
eapply Rle_trans.
apply H1.
apply H6.
rewrite <- Rplus_assoc.
repeat rewrite <- Rsub_eq_Ropp_Rplus.
rewrite Rabs_Ropp.
......@@ -97,7 +104,7 @@ Proof.
eapply Rle_trans.
eapply Rmult_le_compat_l.
apply Rabs_pos.
apply H2.
apply H4.
apply Req_le; auto.
Qed.
......@@ -105,39 +112,42 @@ Qed.
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2:
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Sub (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m ->
eval_exp E1 (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Sub (Var R m 1) (Var R m 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%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 *)
inversion sub_real; subst.
inversion sub_real; subst;
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in sub_real.
rewrite (meps_0_deterministic H5 e2_real) in sub_real.
clear H4 H5 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in sub_real.
clear H6 H7 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion sub_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
inversion H7; subst; inversion H8; subst.
unfold updEnv; simpl.
symmetry in H0, H1.
unfold updEnv in H0, H1; simpl in H0, H1.
inversion H0; inversion H1; subst.
symmetry in H9, H11.
unfold updEnv in H9, H11; simpl in H9, H11.
inversion H9; inversion H11; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H9 H11.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -161,36 +171,39 @@ Proof.
Qed.
Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env):
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Mult (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
(vR:R) (vF:R) (E1 E2:env) (m:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m ->
eval_exp E1 (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Mult (Var R m 1) (Var R m 2)) vF m->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%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 *)
inversion mult_real; subst.
inversion mult_real; subst;
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in mult_real.
rewrite (meps_0_deterministic H5 e2_real) in mult_real.
clear H4 H5 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in mult_real.
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in mult_real.
clear H6 H7 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion mult_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
symmetry in H0, H1;
inversion H7; subst; inversion H8; subst.
symmetry in H9, H11;
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
inversion H9; inversion H11; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H9 H11.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -208,36 +221,39 @@ Proof.
Qed.
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env):
eval_exp 0%R E1 (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F ->
eval_exp 0%R E1 (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F ->
eval_exp 0%R E1 (Binop Div (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
(vR:R) (vF:R) (E1 E2:env) (m:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m ->
eval_exp E1 (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Div (Var R m 1) (Var R m 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%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 *)
inversion div_real; subst.
inversion div_real; subst;
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in div_real.
rewrite (meps_0_deterministic H5 e2_real) in div_real.
clear H4 H5 v1 v2.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in div_real.
rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in div_real.
clear H6 H7 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion div_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
symmetry in H0, H1;
inversion H7; subst; inversion H8; subst.
symmetry in H9, H11;
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
inversion H9; inversion H11; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H9 H11.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......
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