Skip to content

GitLab

Commit c056a2d9 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Rename Lemma in ExpressionsSemantics and fix assumptions for abstract bound lemmas

parent ebc6d460
Show whitespace changes
Inline Side-by-side
Showing with 65 additions and 62 deletions
coq/ErrorBounds.v
View file @ c056a2d9
......@@ -3,12 +3,16 @@ Proofs of general bounds on the error of arithmetic exprressions.
This shortens soundness proofs later.
Bounds are exprlained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs Flover.ExpressionSemantics.
From Coq
Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals.
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealSimps
Infra.RealRationalProps Environments Infra.ExpressionAbbrevs
ExpressionSemantics.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
eval_expr E1 (toRTMap defVars) (Const REAL n) nR REAL ->
eval_expr E2 defVars (Const m n) nF m ->
(Rabs (nR - nF) <= computeErrorR n m)%R.
Proof.
......@@ -31,13 +35,14 @@ Qed.
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr E1 (toRTMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))
(updDefVars (Binop Plus (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(Binop Plus (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
......@@ -46,8 +51,8 @@ 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.
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) REAL delta); auto.
......@@ -86,7 +91,6 @@ Proof.
eapply Rle_trans; [ apply Rabs_triang |].
apply Rplus_le_compat; try auto.
rewrite Rabs_Ropp; simpl. auto.
all: eapply Rle_trans; try eapply H.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -101,42 +105,39 @@ Qed.
**)
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr E1 (toRTMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))
(updDefVars (Binop Sub (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(Binop Sub (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F - e2F) m)%R.
Proof.
admit.
Admitted.
(*
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.
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite (delta_0_deterministic (evalBinop Sub v1 v2) REAL delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H8 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e2) H8 e2_real) in sub_real.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion sub_float; subst.
unfold perturb; simpl.
inversion H6; subst; inversion H7; subst.
unfold updEnv in H1,H12; simpl in *.
symmetry in H1,H12.
inversion H1; inversion H12; subst.
inversion H11; subst; inversion H14; subst.
unfold updEnv in H1,H13; simpl in *.
symmetry in H1,H13.
inversion H1; inversion H13; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H6 H1.
repeat rewrite Rmult_plus_distr_l.
......@@ -176,17 +177,17 @@ Admitted.
all: rewrite Rabs_Ropp, Rabs_mult, <- Rsub_eq_Ropp_Rplus.
all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
Qed.
*)
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr E1 (toRTMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))
(updDefVars (Binop Mult (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(Binop Mult (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
Proof.
......@@ -196,8 +197,8 @@ Admitted.
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;
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -232,13 +233,14 @@ Qed.
Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr E1 (toRTMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))
(updDefVars (Binop Div (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(Binop Div (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
Proof.
......@@ -248,8 +250,8 @@ Admitted.
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;
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -285,15 +287,16 @@ Qed.
Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(e3:expr Q) (e3R:R) (e3F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R REAL ->
eval_expr E1 (toRTMap defVars) (toREval (toRExp e3)) e3R REAL ->
eval_expr E2 defVars (toRExp e3) e3F m3->
eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
eval_expr E1 (toRTMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
(updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m
(updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))))
(Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
(Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
Proof.
......@@ -302,9 +305,9 @@ Admitted.
(*
intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
inversion fma_real; subst;
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in fma_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -356,7 +359,7 @@ Qed.
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
(mEps m:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval e) nR REAL ->
eval_expr E1 (toRTMap defVars) (toREval e) nR REAL ->
eval_expr E2 defVars e nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars (Var R 1) m defVars)
......
coq/ExpressionSemantics.v
View file @ c056a2d9
......@@ -184,7 +184,7 @@ Proof.
auto.
Qed.
Lemma toRMap_eval_REAL f:
Lemma toRTMap_eval_REAL f:
forall v E Gamma m, eval_expr E (toRTMap Gamma) (toREval f) v m -> m = REAL.
Proof.
induction f; intros * eval_f; inversion eval_f; subst.
......@@ -247,20 +247,20 @@ Proof.
+ cbn in *. Flover_compute; rewrite (IHf v0 v3); [auto | | ];
destruct m, m0; cbn in *; congruence.
- inversion ev1; inversion ev2; subst.
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v4); try auto.
rewrite (IHf2 v3 v5); try auto.
- inversion ev1; inversion ev2; subst.
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v5); try auto.
rewrite (IHf2 v3 v6); try auto.
......
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