Skip to content

GitLab

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

Test multiplication, fix flaw

parent 6ee8f753
Hide whitespace changes
Inline Side-by-side
Showing with 93 additions and 75 deletions
coq/ErrorBounds.v
View file @ d17de1b5
......@@ -174,7 +174,7 @@ Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R)
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= Rabs e1R * Rabs e2R + (Rabs e1F * Rabs e2F + Rabs e1F * Rabs e2F * machineEpsilon))%R.
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * machineEpsilon)%R.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
......@@ -199,52 +199,14 @@ Proof.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
rewrite <- Rplus_assoc.
setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rabs_triang.
repeat rewrite Rabs_Ropp.
rewrite Rabs_Ropp.
repeat rewrite Rabs_mult.
eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_l.
eapply Rmult_le_compat_l; auto.
rewrite <- Rabs_mult.
apply Rabs_pos.
apply H2.
apply Req_le; auto.
Qed.
(*
pose proof (Rabs_triang (e1R + - e1F) ((- e2R + - - e2F) + - ((e1F + - e2F) * delta))).
rewrite Rplus_assoc.
eapply Rle_trans.
apply H.
pose proof (Rabs_triang (- e2R + - - e2F) (- ((e1F + - e2F) * delta))).
pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
eapply Rle_trans.
apply H1.
rewrite <- Rplus_assoc.
repeat rewrite <- Rmult_eq_Ropp_Rplus.
rewrite Rabs_Ropp.
assert (Rabs (- e2R - - e2F)%R = Rabs (e2R - e2F)).
- rewrite Rmult_eq_Ropp_Rplus.
rewrite <- Ropp_plus_distr.
rewrite Rabs_Ropp.
rewrite <- Rmult_eq_Ropp_Rplus; auto.
- rewrite H3.
eapply Rplus_le_compat.
+ eapply Rplus_le_compat; auto.
+ rewrite Rabs_mult.
eapply Rle_trans.
eapply Rmult_le_compat_l.
apply Rabs_pos.
apply H2.
rewrite Rmult_eq_Ropp_Rplus.
eapply Rle_trans.
eapply Rmult_le_compat_r.
unfold machineEpsilon, RealConstruction.realFromNum, RealConstruction.negativePower; interval.
apply Rabs_triang.
rewrite Rabs_Ropp.
apply Req_le; auto.
*)
\ No newline at end of file
Qed.
\ No newline at end of file
coq/ErrorValidation.v
View file @ d17de1b5
......@@ -70,7 +70,7 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * machineEpsilon) err
(* TODO:Validity of next two computations *)
| Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * machineEpsilon)) err
| Mult => Qleb (Qabs upperBoundE1 * Qabs upperBoundE2 + (Qabs e1F * Qabs e2F + Qabs e1F * Qabs e2F * machineEpsilon)) err
| Mult => Qleb (Qabs (upperBoundE1 * upperBoundE2 - (e1F * e2F)) + Qabs(e1F * e2F) * machineEpsilon) err
| Div => false
end
in andb rec theVal
......@@ -491,6 +491,37 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
assert (Rabs nF2 <= RmaxAbsFun (e2lo, e2hi) + Q2R err2)%R by (eapply Rle_trans; [ apply H2 | eapply Rplus_le_compat_r; auto]).
assert (Rabs nF2 <= Rabs (RmaxAbsFun (e2lo, e2hi) + Q2R err2))%R by (eapply Rle_trans; [apply H3 | apply Rle_abs]).
clear H1 H2 H3.
apply Rplus_le_compat.
{ apply Fcore_Raux.Rabs_le_inv in H. apply Fcore_Raux.Rabs_le_inv in H0.
apply Fcore_Raux.Rabs_le_inv in H4. apply Fcore_Raux.Rabs_le_inv in H5.
apply Fcore_Raux.Rabs_le.
split.
- rewrite Q2R_minus, Q2R_mult.
rewrite Q2R_mult.
repeat rewrite Q2R_plus.
repeat rewrite <- maxAbs_impl_RmaxAbs.
repeat rewrite Rsub_eq_Ropp_Rplus.
rewrite <- (Ropp_involutive (nR1 * nR2)).
setoid_rewrite Rplus_comm at 2.
rewrite <- Ropp_plus_distr.
apply Ropp_ge_le_contravar.
eapply Rge_trans.
apply Rle_ge.
apply Rabs_triang_inv.
rewrite Rsub_eq_Ropp_Rplus.
apply Rplus_ge_compat.
+ destruct (Rle_dec (nR1 * nR2) 0).
}
{ rewrite Rabs_mult.
apply Rmult_le_compat.
- rewrite <- Rabs_mult. apply Rabs_pos.
- apply mEps_geq_zero.
- repeat rewrite Q2R_mult; repeat rewrite Q2R_plus.
rewrite Rabs_mult. repeat rewrite <- maxAbs_impl_RmaxAbs.
apply Rmult_le_compat; [apply Rabs_pos| apply Rabs_pos |apply H4 | apply H5].
- apply Req_le; auto.
}
rewrite <- Rplus_assoc.
eapply Rle_trans.
eapply Rplus_le_compat.
......@@ -615,5 +646,5 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
{ apply Is_true_eq_left; auto. }
+ inversion valid_error.
Qed.
*)
End ComputableErrors.
coq/Infra/RationalConstruction.v
View file @ d17de1b5
......@@ -5,4 +5,4 @@ Require Import Coq.QArith.QArith.
Definition negativePower base exp :Q := 1 # base^exp.
Definition rationalFromNum n unitsBehindColon exp :Q :=
(n * (negativePower (10) unitsBehindColon) * (negativePower (2) exp))%Q.
\ No newline at end of file
(n * (negativePower (10) unitsBehindColon) * (negativePower (10) exp))%Q.
\ No newline at end of file
coq/VerificationTests/SimpleMultiplication.v
View file @ d17de1b5
Require Import Coq.Reals.Reals Interval.Interval_tactic Coq.micromega.Psatz.
Require Import Coq.Setoids.Setoid.
Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith
Daisy.Expressions Daisy.ErrorBounds
Daisy.Infra.RealConstruction Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
Require Import Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qminmax.
Require Import Daisy.ErrorValidation Daisy.Infra.RationalConstruction Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RationalSimps Daisy.IntervalValidation.
(*
[ Info ]
......@@ -12,21 +9,18 @@ Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith
[ Info ]
[ Info ] Starting range-error phase
[ Info ] Machine epsilon 1.1102230246251565E-16
[ Info ] 100.: [100.0, 100.0],0.
[ Info ] u: [-100.0, 100.0],2.220446049250313e-14
[ Info ] (100. * u): [-10000.0, 10000.0],4.440892098500627e-12
[ Info ] (1657)/(5): [331.4, 331.4],(1657)/(45035996273704960)
[ Info ] u: [-100.0, 100.0],(25)/(2251799813685248)
[ Info ] ((1657)/(5) * u).propagatedError = [-7.358558207215538E-12, 7.358558207215538E-12]
[ Info ] ((1657)/(5) * u): [-33140.0, 33140.0],(2016477162795049297422773199443075165)/(182687704666362864775460604089535377456991567872)
[ Info ] Finished range-error phase
[ Info ]
[ Info ] Starting info phase
[ Info ] doppler
[ Info ] abs-error: 4.440892098500627e-12, range: [-10000.0, 10000.0],
[ Info ] rel-error: NaN
[ Info ] Finished info phase
[ Info ] time:
[ Info ] info: 6 ms, rangeError: 77 ms, analysis: 13 ms, frontend: 2400 ms,
[ Info ] abs-error: (2016477162795049297422773199443075165)/(182687704666362864775460604089535377456991567872), range: [-33140.0, 33140.0],
*)
(** TODO MOVE TO FILE
Ltac prove_constant := unfold realFromNum, negativePower; interval.
Ltac rw_asm H Lem := rewrite Lem; rewrite Lem in H.
......@@ -57,21 +51,52 @@ Proof.
rewrite Rplus_minus; auto.
Qed.
**)
Definition u:nat := 1.
(** 1655/5 = 331; 0,4 = 2/5 **)
Definition cst1:R := 100.
Definition cst1:Q := 1657 # 5.
(** Define abbreviations **)
Definition varU:exp R := Param R u.
Definition valCst:exp R := Const cst1.
Definition valCstMultVarU:exp R := Binop Mult valCst varU.
Definition varU:exp Q := Param Q u.
Definition valCst:exp Q := Const cst1.
Definition valCstAddVarU:exp Q := Binop Mult valCst varU.
(** Error values **)
Definition errCst1 := realFromNum 0 1 1.
Definition errVaru := realFromNum 2220446049250313 15 14.
Definition lowerBoundMultUCst:R := - realFromNum 10000 0 0.
Definition upperBoundMultUCst:R := realFromNum 10000 0 0.
Definition errMultUCst := realFromNum 4440892098500627 15 12.
Definition errCst1 := (1657)#(45035996273704960).
Definition errVaru := (25)#(2251799813685248).
Definition lowerBoundMultUCst:Q := - (33140#1).
Definition upperBoundMultUCst:Q := (33140#1).
Definition errMultUCst :=(2016477162795049297422773199443075165)#(182687704666362864775460604089535377456991567872).
Definition absEnv : analysisResult :=
fun (e:exp Q) =>
match e with
|Const n => (cst1,cst1,errCst1)
|Param v => (-(100#1),(100#1),errVaru)
|Binop _ _ _ => (lowerBoundMultUCst,upperBoundMultUCst,errMultUCst)
| _ => (0,0,0) end.
Definition precondition :precond := fun _ => (-(100#1),(100#1)).
Definition machineEpsilon := (1#(2^53)).
Definition l := Eval compute in (maxAbs (cst1,cst1) * machineEpsilon).
Definition r := Eval compute in (Qred errCst1).
Eval compute in (Qleb l r).
Eval compute in validErrorbound valCst absEnv.
Eval compute in validErrorbound varU absEnv.
Eval compute in validErrorbound valCstAddVarU absEnv.
Definition tmp := Eval compute in (let (iv,err) := absEnv valCstAddVarU in
let (ive1, err1) := absEnv valCst in
let (ive2, err2) := absEnv varU in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let e1F := upperBoundE1 + err1 in
let e2F := upperBoundE2 + err2 in
Qleb (Qabs (upperBoundE1 * upperBoundE2 - ( e1F * e2F)) + Qabs(e1F * e2F * machineEpsilon)) err).
Eval compute in Qleb tmp errMultUCst.
(** The added assertion becomes the precondition for us **)
Definition precondition := fun env:nat -> R => (- 100 <= env u)%R /\ (env u <= 100)%R.
......@@ -106,7 +131,7 @@ Proof.
apply (AbsErrConst cst1 (mkInterval cst1 cst1) errCst1); [constructor | ].
unfold isSoundErr; simpl.
unfold errCst1, cst1, machineEpsilon.
unfold realFromNum, negativePower.
unfold rationalFromNum, negativePower.
rewrite Rmax_left; [ |apply Req_le; auto].
assert (Rabs 100 = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H.
......@@ -114,7 +139,7 @@ Proof.
+ apply (AbsErrParam u (mkInterval (- 100) (100)) errVaru); [constructor | ].
unfold isSoundErr; simpl.
unfold Expressions.machineEpsilon, errVaru.
unfold realFromNum.
unfold rationalFromNum.
unfold negativePower.
assert (Rabs (-100) = 100%R) by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H.
......@@ -141,8 +166,8 @@ Proof.
* unfold isSoundErr; simpl.
unfold lowerBoundMultUCst, upperBoundMultUCst, errMultUCst.
unfold Expressions.machineEpsilon.
assert (- realFromNum 10000 0 0 <= 0)%R by prove_constant.
assert (0 <= realFromNum 10000 0 0) %R by prove_constant.
assert (- rationalFromNum 10000 0 0 <= 0)%R by prove_constant.
assert (0 <= rationalFromNum 10000 0 0) %R by prove_constant.
rewrite Rabs_left1; auto.
rewrite Rabs_pos_eq; auto.
rewrite Ropp_involutive.
......@@ -258,7 +283,7 @@ Proof.
rewrite Rmax_left in H16; [ | lra].
assert (forall eps:R, 0 <= eps -> Rabs (cenv u) * eps <= 100 * eps)%R by (intros; apply Rmult_le_compat_r; auto).
assert (cst1 * Rabs delta0 * Rabs delta <= cst1 * machineEpsilon * machineEpsilon)%R.
* assert (cst1 * Rabs delta0 <= cst1 * machineEpsilon)%R by (apply Rmult_le_compat_l; [unfold cst1, realFromNum, negativePower; interval | auto]).
* assert (cst1 * Rabs delta0 <= cst1 * machineEpsilon)%R by (apply Rmult_le_compat_l; [unfold cst1, rationalFromNum, negativePower; interval | auto]).
repeat rewrite Rmult_assoc.
apply Rmult_le_compat_l; [unfold cst1; prove_constant | ].
apply Rmult_le_compat; auto using Rabs_pos.
......
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