Commit 71a45a2f authored by Joachim Bard's avatar Joachim Bard
Browse files

WIP: better error computation

parent 703be8b5
......@@ -11,6 +11,48 @@ From Flover
Infra.RealRationalProps Environments Infra.ExpressionAbbrevs
ExpressionSemantics.
Lemma split_error delta m vR vF :
(Rabs delta <= mTypeToR m)%R ->
(Rabs (perturb vF m delta - vR) <= Rabs (vF - vR) + computeErrorR (vR + (vF - vR)) m)%R.
Proof.
intros Hdelta. rewrite Rplus_minus. rewrite Rplus_comm.
destruct m; unfold perturb, computeErrorR.
- cbn. lra.
- rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rplus_comm.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rplus_assoc.
eapply Rle_trans; [apply Rabs_triang |].
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rabs_mult. apply Rplus_le_compat; try lra.
apply Rmult_le_compat_l; auto using Rabs_pos.
- rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rplus_comm.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rplus_assoc.
eapply Rle_trans; [apply Rabs_triang |].
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rabs_mult. apply Rplus_le_compat; try lra.
apply Rmult_le_compat_l; auto using Rabs_pos.
- rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rplus_comm.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rplus_assoc.
eapply Rle_trans; [apply Rabs_triang |].
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rabs_mult. apply Rplus_le_compat; try lra.
apply Rmult_le_compat_l; auto using Rabs_pos.
- rewrite Rplus_comm.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Rplus_assoc.
eapply Rle_trans; [apply Rabs_triang |].
rewrite Rsub_eq_Ropp_Rplus.
apply Rplus_le_compat; lra.
Qed.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars DeltaMap:
eval_expr E1 (toRTMap defVars) DeltaMapR (Const REAL n) nR REAL ->
eval_expr E2 defVars DeltaMap (Const m n) nF m ->
......
......@@ -52,15 +52,17 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
let upperBoundE2 := maxAbs ive2 in
match b with
| Plus =>
let mAbs := (maxAbs (addIntv errIve1 errIve2)) in
Qleb (err1 + err2 + computeErrorQ mAbs m) err
let propErr := err1 + err2 in
let mAbs := (maxAbs intv) + propErr in
Qleb (propErr + computeErrorQ mAbs m) err
| Sub =>
let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
Qleb (err1 + err2 + computeErrorQ mAbs m) err
let propErr := err1 + err2 in
let mAbs := (maxAbs intv) + propErr in
Qleb (propErr + computeErrorQ mAbs m) err
| Mult =>
let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
let eProp := (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) in
Qleb (eProp + computeErrorQ mAbs m) err
let propErr := (maxAbs ive1) * err2 + (maxAbs ive2) * err1 + err1 * err2 in
let mAbs := (maxAbs intv) + propErr in
Qleb (propErr + computeErrorQ mAbs m) err
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
......
......@@ -107,6 +107,7 @@ Proof.
assert (m = mF) by congruence; subst.
rewrite <- maxAbs_impl_RmaxAbs.
apply computeErrorR_up.
unfold RmaxAbsFun. rewrite <- RmaxAbs_peel_Rabs.
apply contained_leq_maxAbs.
simpl in *; auto.
Qed.
......@@ -147,18 +148,17 @@ Proof.
rewrite computeErrorQ_computeErrorR.
rewrite <- maxAbs_impl_RmaxAbs.
apply computeErrorR_up.
unfold RmaxAbsFun. rewrite <- RmaxAbs_peel_Rabs.
apply contained_leq_maxAbs.
simpl in *; auto.
Qed.
Lemma validErrorboundCorrectAddition E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma DeltaMap:
eval_Real E1 Gamma e1 nR1 ->
eval_Real E1 Gamma e2 nR2 ->
(e1:expr Q) (e2:expr Q) (nR nF :R) (err err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m Gamma DeltaMap:
eval_Real E1 Gamma (Binop Plus e1 e2) nR ->
eval_Fin E2 Gamma DeltaMap e1 nF1 m1 ->
eval_Fin E2 Gamma DeltaMap e2 nF2 m2 ->
eval_Fin E2 Gamma DeltaMap (Binop Plus e1 e2) nF m ->
(*
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars (Binop Plus (Var R 1) (Var R 2)) m
(updDefVars (Var Rdefinitions.R 2) m2
......@@ -167,16 +167,58 @@ Lemma validErrorboundCorrectAddition E1 E2 A
then DeltaMap (evalBinop Plus nF1 nF2) m
else None)
(toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
*)
validErrorbound (Binop Plus e1 e2) Gamma A dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
FloverMap.find e1 A = Some ((e1lo,e1hi),err1) ->
FloverMap.find e2 A = Some ((e2lo, e2hi),err2) ->
FloverMap.find (Binop Plus e1 e2) A = Some ((alo,ahi),e)->
FloverMap.find (Binop Plus e1 e2) A = Some ((alo,ahi),err)->
FloverMap.find (Binop Plus e1 e2) Gamma = Some m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
(forall nR1 nF1 m, eval_Real E1 Gamma e1 nR1 ->
eval_Fin E2 Gamma DeltaMap e1 nF1 m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R) ->
(forall nR2 nF2 m, eval_Real E1 Gamma e2 nR2 ->
eval_Fin E2 Gamma DeltaMap e2 nF2 m ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R) ->
(Q2R alo <= nR <= Q2R ahi)%R ->
(Rabs (nR - nF) <= (Q2R err))%R.
Proof.
intros eval_real eval_float
valid_error A_e1 A_e2 A_add
Gamma_Plus err1_bounded err2_bounded valid_range.
inversion eval_float; subst.
cbn in valid_error. rewrite A_add, Gamma_Plus in valid_error.
rewrite A_e1, A_e2 in valid_error. Flover_compute.
rename R0 into valid_error.
canonize_hyps.
rewrite Rabs_minus_sym.
eapply Rle_trans; [now apply split_error | cbn].
assert (Rabs (v1 + v2 - nR) <= Q2R (err1 + err2))%R as Hprop.
{ inversion eval_real; subst. cbn.
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
rewrite Q2R_plus. rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr.
rewrite <- Rplus_assoc. rewrite (Rplus_assoc v1). rewrite (Rplus_comm v2). rewrite <- Rplus_assoc.
rewrite (Rplus_assoc _ v2). rewrite <- !Rsub_eq_Ropp_Rplus.
eapply Rle_trans; [apply Rabs_triang |].
apply Rplus_le_compat; rewrite Rabs_minus_sym; eauto. }
eapply Rle_trans; [| exact valid_error].
rewrite Q2R_plus, computeErrorQ_computeErrorR.
apply Rplus_le_compat; auto.
apply computeErrorR_up.
rewrite Q2R_plus.
eapply Rle_trans; [apply Rabs_triang |].
rewrite <- maxAbs_impl_RmaxAbs.
rewrite (Rabs_pos_eq (_ + _)).
- apply Rplus_le_compat; auto.
inversion eval_real; subst.
now apply contained_leq_maxAbs.
- rewrite Q2R_plus. unfold RmaxAbsFun. rewrite RmaxAbs_peel_Rabs.
apply Rplus_le_le_0_compat; auto using Rabs_pos.
apply Rplus_le_le_0_compat; eauto using err_always_positive.
Qed.
(*
Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
......@@ -212,15 +254,14 @@ Proof.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; lra.
Qed.
*)
Lemma validErrorboundCorrectSubtraction E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma DeltaMap:
eval_Real E1 Gamma e1 nR1 ->
eval_Real E1 Gamma e2 nR2 ->
(e1:expr Q) (e2:expr Q) (nR nF :R) (err err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m Gamma DeltaMap:
eval_Real E1 Gamma (Binop Sub e1 e2) nR ->
eval_Fin E2 Gamma DeltaMap e1 nF1 m1->
eval_Fin E2 Gamma DeltaMap e2 nF2 m2 ->
eval_Fin E2 Gamma DeltaMap (Binop Sub e1 e2) nF m ->
(*
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars (Binop Sub (Var R 1) (Var R 2)) m
(updDefVars (Var Rdefinitions.R 2) m2
......@@ -229,16 +270,60 @@ Lemma validErrorboundCorrectSubtraction E1 E2 A
then DeltaMap (evalBinop Sub nF1 nF2) m
else None)
(toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
*)
validErrorbound (Binop Sub e1 e2) Gamma A dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
FloverMap.find e1 A = Some ((e1lo,e1hi),err1) ->
FloverMap.find e2 A = Some ((e2lo, e2hi),err2) ->
FloverMap.find (Binop Sub e1 e2) A = Some ((alo,ahi),e)->
FloverMap.find (Binop Sub e1 e2) A = Some ((alo,ahi),err)->
FloverMap.find (Binop Sub e1 e2) Gamma = Some m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
(forall nR1 nF1 m, eval_Real E1 Gamma e1 nR1 ->
eval_Fin E2 Gamma DeltaMap e1 nF1 m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R) ->
(forall nR2 nF2 m, eval_Real E1 Gamma e2 nR2 ->
eval_Fin E2 Gamma DeltaMap e2 nF2 m ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R) ->
(Q2R alo <= nR <= Q2R ahi)%R ->
(Rabs (nR - nF) <= (Q2R err))%R.
Proof.
intros eval_real eval_float
valid_error A_e1 A_e2 A_add
Gamma_Plus err1_bounded err2_bounded valid_range.
inversion eval_float; subst.
cbn in valid_error. rewrite A_add, Gamma_Plus in valid_error.
rewrite A_e1, A_e2 in valid_error. Flover_compute.
rename R0 into valid_error.
canonize_hyps.
rewrite Rabs_minus_sym.
eapply Rle_trans; [now apply split_error | cbn].
assert (Rabs (v1 - v2 - nR) <= Q2R (err1 + err2))%R as Hprop.
{ inversion eval_real; subst. cbn.
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
rewrite Q2R_plus. rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_minus_distr.
rewrite (Rsub_eq_Ropp_Rplus v3). rewrite Rsub_eq_Ropp_Rplus.
rewrite <- Rplus_assoc. rewrite (Rplus_assoc v1). rewrite (Rplus_comm _ v3). rewrite Rplus_assoc.
rewrite (Rplus_comm _ (- v0)).
rewrite <- (Rplus_assoc). rewrite <- !Rsub_eq_Ropp_Rplus.
eapply Rle_trans; [apply Rabs_triang |].
apply Rplus_le_compat; eauto. rewrite Rabs_minus_sym; eauto. }
eapply Rle_trans; [| exact valid_error].
rewrite Q2R_plus, computeErrorQ_computeErrorR.
apply Rplus_le_compat; auto.
apply computeErrorR_up.
rewrite Q2R_plus.
eapply Rle_trans; [apply Rabs_triang |].
rewrite <- maxAbs_impl_RmaxAbs.
rewrite (Rabs_pos_eq (_ + _)).
- apply Rplus_le_compat; auto.
inversion eval_real; subst.
now apply contained_leq_maxAbs.
- rewrite Q2R_plus. unfold RmaxAbsFun. rewrite RmaxAbs_peel_Rabs.
apply Rplus_le_le_0_compat; auto using Rabs_pos.
apply Rplus_le_le_0_compat; eauto using err_always_positive.
Qed.
(*
Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub Gamma_sub
......@@ -278,6 +363,7 @@ Proof.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; lra.
Qed.
*)
Lemma multiplicationErrorBounded e1lo e1hi e2lo e2hi nR1 nF1 nR2 nF2 err1 err2 :
(Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
......@@ -745,6 +831,7 @@ Proof.
}
Qed.
(*
Lemma validErrorboundCorrectMult E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma DeltaMap:
......@@ -812,7 +899,9 @@ Proof.
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; lra.
Qed.
*)
(*
Lemma validErrorboundCorrectDiv E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma DeltaMap:
......@@ -1725,6 +1814,7 @@ Proof.
- rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H3.
rewrite (Qmult_inj_r) in H3; auto. }
Qed.
*)
Lemma validErrorboundCorrectFma E1 E2 A
(e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R)
......@@ -1794,6 +1884,7 @@ Proof.
pose proof (IntervalArith.interval_addition_valid _ _ valid_err_mult valid_err3).
rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
apply computeErrorR_up.
unfold RmaxAbsFun. rewrite <- RmaxAbs_peel_Rabs.
apply contained_leq_maxAbs.
simpl in *; split.
+ rewrite Q2R_min4.
......@@ -1858,10 +1949,11 @@ Proof.
apply Rplus_le_compat_l.
rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
apply computeErrorR_up.
unfold RmaxAbsFun. rewrite <- RmaxAbs_peel_Rabs.
apply contained_leq_maxAbs.
simpl in *; split; try rewrite Q2R_plus in *;
try rewrite Q2R_minus in *;
lra.
Qed.
End soundnessProofs.
\ No newline at end of file
End soundnessProofs.
......@@ -179,14 +179,49 @@ Proof.
+ intros * eval_float.
clear eval_float1 eval_float2.
inversion eval_float; subst.
destruct b.
{ destruct iv1, iv2. eapply (validErrorboundCorrectAddition (e1:=e1) A); eauto.
- cbn. instantiate (1:=dVars); Flover_compute.
rewrite L, L1, R; simpl; auto.
- eapply toRExpMap_find_map; eauto.
- intros. assert (nR1 = v1) by (eapply meps_0_deterministic; eauto).
subst. eapply valid_bounds_e1. eauto.
- intros. assert (nR2 = v2) by (eapply meps_0_deterministic; eauto).
subst. eapply valid_bounds_e2. eauto.
- cbn.
(* TODO *)
eapply (binary_unfolding H26 H21 H19 H22 H25) in eval_float; try auto.
destruct b.
* rewrite Rabs_minus_sym. eapply Rle_trans ; [now apply split_error |].
cbn. unfold error in Heqo. assert (e = err) by congruence; subst.
assert (Rabs (v0 + v3 - (v1 + v2)) <= Q2R (err1 + err2))%R as Hprop.
{ rewrite Q2R_plus. rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr.
rewrite <- Rplus_assoc. rewrite (Rplus_assoc v0). rewrite (Rplus_comm v3). rewrite <- Rplus_assoc.
rewrite (Rplus_assoc _ v3). rewrite <- !Rsub_eq_Ropp_Rplus.
eapply Rle_trans; [apply Rabs_triang |].
apply Rplus_le_compat; rewrite Rabs_minus_sym; eauto. }
rewrite Rplus_comm. eapply Rle_trans. apply Rplus_le_compat; [exact Hprop |].
2: { canonize_hyps. rewrite Q2R_plus in R0. exact R0. }
{ rewrite computeErrorQ_computeErrorR.
assert (m = m__FP).
{ eapply toRExpMap_some in Heqo0.
2: cbn; reflexivity.
congruence. }
subst.
apply computeErrorR_mono. rewrite Q2R_plus.
rewrite <- (Rplus_minus (v1 + v2) (v0 + v3)).
eapply Rle_trans; [apply Rabs_triang |].
rewrite (Rabs_pos_eq (Q2R _ + _)).
- apply Rplus_le_compat; auto. admit.
- rewrite Q2R_plus. admit. }
(*
* eapply (validErrorboundCorrectAddition (e1:=e1) A); eauto.
{ cbn. instantiate (1:=dVars); Flover_compute.
rewrite L, L1, R; simpl; auto. }
{ destruct iv1; auto. }
{ destruct iv2; auto. }
{ eapply toRExpMap_find_map; eauto. }
*)
* eapply (validErrorboundCorrectSubtraction (e1:=e1) A); eauto.
{ cbn; instantiate (1:=dVars); Flover_compute.
rewrite L, L1, R; simpl; auto. }
......@@ -497,4 +532,4 @@ Proof.
eapply validErrorBoundsRec_single in H1; eauto.
destruct H1. eapply H2; eauto.
(* - cbn in *. Flover_compute; congruence. *)
Qed.
\ No newline at end of file
Admitted.
\ No newline at end of file
......@@ -150,16 +150,13 @@ Proof.
apply pow_lt; lra.
Qed.
Lemma computeErrorR_up (v a b:R) m:
Rabs v <= RmaxAbsFun (a,b) ->
computeErrorR v m <= computeErrorR (RmaxAbsFun (a,b)) m.
Lemma computeErrorR_up (v1 v2: R) m:
Rabs v1 <= Rabs v2 ->
computeErrorR v1 m <= computeErrorR v2 m.
Proof.
intros.
intros H.
unfold computeErrorR; destruct m; try lra.
all:apply Rmult_le_compat_r; try auto using mTypeToR_pos_R.
all:unfold RmaxAbsFun in *.
all:setoid_rewrite Rabs_right at 2; try auto.
all:apply Rle_ge; rewrite Rmax_Rle; auto using Rabs_pos.
all: apply Rmult_le_compat_r; auto using mTypeToR_pos_R.
Qed.
Close Scope R_scope.
......
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