Commit 4ccb040c authored by Heiko Becker's avatar Heiko Becker

Fix remaining admits

parent 4d4ab82d
......@@ -191,9 +191,6 @@ Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:
(Binop Mult (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
Proof.
admit.
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;
......@@ -203,18 +200,17 @@ Admitted.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
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 mult_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in mult_real.
clear H3 H4.
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 mult_real.
rewrite (meps_0_deterministic (toRExp e2) H8 e2_real) in mult_real.
(* 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 H6; subst.
unfold updEnv in *; simpl in *.
inversion H1; inversion H11; subst.
cbn in *. inversion H0; inversion H10; 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 mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1.
repeat rewrite Rmult_plus_distr_l.
......@@ -229,7 +225,6 @@ Admitted.
all: eapply Rplus_le_compat_l; try auto.
all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
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:
......@@ -244,9 +239,6 @@ Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
(Binop Div (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
Proof.
admit.
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;
......@@ -256,18 +248,17 @@ Admitted.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
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 div_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in div_real.
clear H3 H4.
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 div_real.
rewrite (meps_0_deterministic (toRExp e2) H8 e2_real) in div_real.
(* 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 H6; subst.
unfold updEnv in *; simpl in *.
inversion H1; inversion H11; subst.
cbn in *. inversion H0; inversion H10; 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 div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
repeat rewrite Rmult_plus_distr_l.
......@@ -282,7 +273,6 @@ Admitted.
all: eapply Rplus_le_compat_l; try auto.
all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
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)
......@@ -300,9 +290,6 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
(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.
admit.
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 toRTMap_eval_REAL; eauto).
......@@ -312,20 +299,19 @@ Admitted.
rewrite delta_0_deterministic in fma_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalFma 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 e3) H5 e3_real).
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in fma_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in fma_real.
rewrite (meps_0_deterministic (toRExp e3) H5 e3_real) in fma_real.
clear H3 H4 H5 v1 v2 v3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H8 e2_real);
rewrite (meps_0_deterministic (toRExp e3) H9 e3_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in fma_real.
rewrite (meps_0_deterministic (toRExp e2) H8 e2_real) in fma_real.
rewrite (meps_0_deterministic (toRExp e3) H9 e3_real) in fma_real.
inversion fma_float; subst.
unfold evalFma in *.
unfold perturb; simpl.
inversion H3; subst; inversion H4; subst; inversion H5; subst.
inversion H11; subst; inversion H14; subst; inversion H15; subst.
cbn in *.
inversion H0; inversion H1; inversion H6; inversion H7; inversion H12; inversion H13; subst.
inversion H0; inversion H1; inversion H12; inversion H13; inversion H16;
inversion H17; subst.
clear fma_float H7 fma_real e1_real e1_float e2_real e2_float e3_real e3_float H6 H1 H5 H9 H3 H0 H4 H8.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
......@@ -355,7 +341,6 @@ Admitted.
all: apply Rplus_le_compat_l.
all: rewrite Rabs_mult; apply Rmult_le_compat_l; auto using Rabs_pos.
Qed.
*)
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
(mEps m:mType) defVars:
......@@ -368,10 +353,6 @@ Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
(Rabs (nR - nF1) <= err)%R ->
(Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%R.
Proof.
admit.
Admitted.
(*
intros eval_real eval_float eval_float_rnd err_bounded.
replace (nR - nF)%R with ((nR - nF1) + (nF1 - nF))%R by lra.
eapply Rle_trans.
......@@ -380,10 +361,10 @@ Admitted.
- apply Rplus_le_compat_r; assumption.
- apply Rplus_le_compat_l.
inversion eval_float_rnd; subst.
inversion H5; subst.
inversion H6; subst.
inversion H0; subst.
unfold perturb; simpl.
unfold updEnv in H3; simpl in H3; inversion H3; subst.
unfold updEnv in H4; simpl in H4; inversion H4; subst.
unfold computeErrorR.
destruct mEps.
{ unfold Rminus. rewrite Rplus_opp_r, Rabs_R0; lra. }
......@@ -394,7 +375,6 @@ Admitted.
rewrite Ropp_plus_distr, <- Rplus_assoc.
rewrite Rplus_opp_r, Rplus_0_l, Rabs_Ropp; auto.
Qed.
*)
Lemma err_prop_inversion_pos_real nF nR err elo ehi
(float_iv_pos : (0 < elo - err)%R)
......
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