Commit 59976fa6 authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files

Fix merge errors in ErrorValidation

parent 9489c9c8
......@@ -74,18 +74,19 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
&& (validErrorbound e2 typeMap A dVars)
&& (validErrorbound e3 typeMap A dVars))
then
let (ive1, err1) := A e1 in
let (ive2, err2) := A e2 in
let (ive3, err3) := A e3 in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let errIve3 := widenIntv ive3 err3 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let upperBoundE3 := maxAbs ive3 in
let errIntv_prod := multIntv errIve2 errIve3 in
let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIve1 errIntv_prod)) * (mTypeToQ m)) err
match DaisyMap.find e1 A, DaisyMap.find e2 A, DaisyMap.find e3 A with
| Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let errIve3 := widenIntv ive3 err3 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let upperBoundE3 := maxAbs ive3 in
let errIntv_prod := multIntv errIve2 errIve3 in
let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIve1 errIntv_prod)) * (mTypeToQ m)) err
| _, _, _ => false
end
else false
|Downcast m1 e1 =>
if validErrorbound e1 typeMap A dVars
......@@ -1893,7 +1894,7 @@ Proof.
rewrite (Qmult_inj_r) in H3; auto. }
Qed.
Lemma validErrorboundCorrectFma E1 E2 absenv
Lemma validErrorboundCorrectFma E1 E2 A
(e1:exp Q) (e2:exp Q) (e3: exp Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error)
(alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars (m m1 m2 m3:mType) Gamma defVars:
m = join3 m1 m2 m3 ->
......@@ -1908,45 +1909,34 @@ Lemma validErrorboundCorrectFma E1 E2 absenv
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(toRExp (Fma (Var Q 1) (Var Q 2) (Var Q 3))) nF m ->
typeCheck (Fma e1 e2 e3) defVars Gamma = true ->
validErrorbound (Fma e1 e2 e3) Gamma absenv dVars = true ->
validErrorbound (Fma e1 e2 e3) Gamma A dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
(Q2R e3lo <= nR3 <= Q2R e3hi)%R ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv e3 = ((e3lo, e3hi),err3) ->
absenv (Fma e1 e2 e3) = ((alo,ahi),e)->
DaisyMap.find e1 A = Some ((e1lo,e1hi),err1) ->
DaisyMap.find e2 A = Some ((e2lo, e2hi),err2) ->
DaisyMap.find e3 A = Some ((e3lo, e3hi),err3) ->
DaisyMap.find (Fma e1 e2 e3) A = Some ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR3 - nF3) <= (Q2R err3))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float
subexpr_ok valid_error valid_e1 valid_e2 valid_e3 absenv_e1 absenv_e2 absenv_e3 absenv_fma
subexpr_ok valid_error valid_e1 valid_e2 valid_e3 A_e1 A_e2 A_e3 A_fma
err1_bounded err2_bounded err3_bounded.
Daisy_compute; try congruence; type_conv; subst.
cbn in *; Daisy_compute; type_conv; subst.
eapply Rle_trans.
eapply (fma_abs_err_bounded e1 e2 e3); eauto.
unfold validErrorbound in valid_error.
rewrite absenv_fma, absenv_e1, absenv_e2, absenv_e3 in valid_error.
case_eq (Gamma (Fma e1 e2 e3)); intros; rewrite H in valid_error; [ | inversion valid_error ].
simpl in subexpr_ok; rewrite H in subexpr_ok.
case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ].
case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ].
case_eq (Gamma e3); intros; rewrite H2 in subexpr_ok; [ | inversion subexpr_ok ].
andb_to_prop subexpr_ok.
apply mTypeEq_compat_eq in L; subst.
pose proof (typingSoundnessExp _ _ R1 e1_float).
pose proof (typingSoundnessExp _ _ R0 e2_float).
pose proof (typingSoundnessExp _ _ R e3_float).
rewrite H0 in H3; rewrite H1 in H4; rewrite H2 in H5; inversion H3; inversion H4; inversion H5; subst.
clear H0 H1 H2 H3 H4 H5.
andb_to_prop valid_error.
rename R3 into valid_error.
assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv dVars); eauto).
assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv dVars); eauto).
assert (0 <= Q2R err3)%R as err3_pos by (eapply (err_always_positive e3 Gamma absenv dVars); eauto).
clear R2 R4 L0.
pose proof (typingSoundnessExp _ _ R4 e1_float).
pose proof (typingSoundnessExp _ _ R3 e2_float).
pose proof (typingSoundnessExp _ _ R2 e3_float).
rewrite H in Heqo0; rewrite H0 in Heqo1; rewrite H1 in Heqo2;
inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
rename R0 into valid_error.
assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma A dVars); eauto).
assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma A dVars); eauto).
assert (0 <= Q2R err3)%R as err3_pos by (eapply (err_always_positive e3 Gamma A dVars); eauto).
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
repeat rewrite Q2R_plus in valid_error.
......@@ -1956,8 +1946,6 @@ Proof.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans; eauto.
clear absenv_e1 absenv_e2 absenv_e3 valid_error e e1 e2 e3 absenv_fma
H L R1 R0 R e1_real e2_real e3_real e1_float e2_float e3_float eval_real eval_float.
apply Rplus_le_compat.
- eauto using Rle_trans, Rabs_triang, Rplus_le_compat, multiplicationErrorBounded.
- apply Rmult_le_compat_r; auto using mTypeToQ_pos_R.
......@@ -1969,17 +1957,16 @@ Proof.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv_sum = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv_sum = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
(* rewrite <- H, <- H0. *)
assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded).
assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded).
assert (contained nR3 (Q2R e3lo, Q2R e3hi)) as contained_intv3 by auto.
pose proof (distance_gives_iv (a:=nR3) _ _ contained_intv3 err3_bounded).
pose proof (IntervalArith.interval_multiplication_valid _ _ H2 H3).
pose proof (IntervalArith.interval_addition_valid _ _ H1 H4).
(* simpl in *. *)
destruct H5, H4.
pose proof (IntervalArith.interval_multiplication_valid _ _ H5 H6).
pose proof (IntervalArith.interval_addition_valid _ _ H4 H7).
destruct H8.
unfold RmaxAbsFun.
subst.
apply RmaxAbs; subst; simpl in *.
......@@ -2185,7 +2172,7 @@ Proof.
{ cbn; instantiate (1:=dVars); Daisy_compute.
rewrite L, L2,L4, R1; simpl; auto. }
{ andb_to_prop R; auto. }
- simpl in valid_error.
(*- simpl in valid_error.
destruct (absenv e1) as [[ivlo1 ivhi1] err1] eqn:absenv_e1;
destruct (absenv e2) as [[ivlo2 ivhi2] err2] eqn:absenv_e2;
destruct (absenv e3) as [[ivlo3 ivhi3] err3] eqn:absenv_e3.
......@@ -2202,32 +2189,36 @@ Proof.
repeat match goal with
| [H: _ = true |- _] => andb_to_prop H
end.
type_conv.
type_conv.*)
- cbn in *. rewrite A_eq in *.
Daisy_compute; try congruence; type_conv; subst; simpl in *.
inversion eval_real; subst.
assert (m3 = M0 /\ m4 = M0 /\ m5 = M0) as [? [? ?]] by (split; try split; eapply toRMap_eval_M0; eauto); subst.
destruct (IHe1 E1 E2 fVars dVars absenv v1 err1 P ivlo1 ivhi1 Gamma defVars)
assert (m0 = M0 /\ m4 = M0 /\ m5 = M0) as [? [? ?]] by (split; try split; eapply toRMap_eval_M0; eauto); subst.
destruct i as [ivlo1 ivhi1]; destruct i2 as [ivlo2 ivhi2]; destruct i1 as [ivlo3 ivhi3];
rename e into err1; rename e5 into err2; rename e4 into err3.
destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars)
as [[vF1 [mF1 eval_float_e1]] bounded_e1];
try auto; set_tac.
destruct (IHe2 E1 E2 fVars dVars absenv v2 err2 P ivlo2 ivhi2 Gamma defVars)
destruct (IHe2 E1 E2 fVars dVars A v2 err2 P ivlo2 ivhi2 Gamma defVars)
as [[vF2 [mF2 eval_float_e2]] bounded_e2];
try auto; set_tac.
destruct (IHe3 E1 E2 fVars dVars absenv v3 err3 P ivlo3 ivhi3 Gamma defVars)
destruct (IHe3 E1 E2 fVars dVars A v3 err3 P ivlo3 ivhi3 Gamma defVars)
as [[vF3 [mF3 eval_float_e3]] bounded_e3];
try auto; set_tac.
destruct (validIntervalbounds_sound _ _ _ E1 defVars L (fVars := fVars) (dVars:=dVars))
as [v1' [eval_real_e1 bounds_e1]];
destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) L (fVars := fVars) (dVars:=dVars))
as [iv1' [ err1' [v1' [map_e1 [eval_real_e1 bounds_e1]]]]];
try auto; set_tac.
rewrite absenv_e1 in bounds_e1.
pose proof (meps_0_deterministic _ eval_real_e1 H5); subst. clear H5.
destruct (validIntervalbounds_sound _ _ _ E1 defVars R1 (fVars:= fVars) (dVars:=dVars))
as [v2' [eval_real_e2 bounds_e2]];
rewrite map_e1 in Heqo; inversion Heqo; subst.
pose proof (meps_0_deterministic _ eval_real_e1 H5); subst; clear H5.
destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) R1 (fVars:= fVars) (dVars:=dVars))
as [iv2' [err2' [v2' [map_e2 [eval_real_e2 bounds_e2]]]]];
try auto; set_tac.
rewrite absenv_e2 in bounds_e2; simpl in *.
rewrite map_e2 in Heqo2; inversion Heqo2; subst.
pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6.
destruct (validIntervalbounds_sound _ _ _ E1 defVars R0 (fVars:= fVars) (dVars:=dVars))
as [v3' [eval_real_e3 bounds_e3]];
destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) R0 (fVars:= fVars) (dVars:=dVars))
as [iv3' [err3' [v3' [map_e3 [eval_real_e3 bounds_e3]]]]];
try auto; set_tac.
rewrite absenv_e3 in bounds_e3; simpl in *.
rewrite map_e3 in Heqo5; inversion Heqo5; subst.
pose proof (meps_0_deterministic _ eval_real_e3 H7); subst; clear H7.
split.
+ repeat eexists; econstructor; eauto.
......@@ -2235,23 +2226,25 @@ Proof.
instantiate (1 := 0%R).
apply mTypeToQ_pos_R.
apply Rle_ge.
hnf; right. reflexivity.
hnf; right; reflexivity.
+ intros * eval_float.
clear eval_float_e1 eval_float_e2 eval_float_e3.
inversion eval_float; subst.
eapply (fma_unfolding H4 H5 H8 H9) in eval_float; try auto.
eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) absenv); eauto.
eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) A); eauto.
{ simpl.
rewrite type_fma.
rewrite type_e1.
rewrite type_e2.
rewrite type_e3.
rewrite Heqo0.
rewrite Heqo4.
rewrite Heqo6.
rewrite Heqo7.
rewrite mTypeEq_refl, R5, R6, R7; auto. }
{ simpl.
rewrite absenv_eq.
rewrite type_fma.
rewrite A_eq.
rewrite Heqo0.
rewrite R, L1, L2, R4; simpl.
rewrite absenv_e1, absenv_e2, absenv_e3.
rewrite map_e1, map_e2, map_e3.
inversion Heqo1.
rewrite <- H0.
auto. }
- cbn in *; Daisy_compute; try congruence; type_conv; subst.
inversion eval_real; subst.
......
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