Commit 87e74ade authored by Heiko Becker's avatar Heiko Becker

Show stronger soundness in Error validator

parent 604e29ed
......@@ -1976,7 +1976,7 @@ Qed.
Proof is by induction on the expression e.
Each case requires the application of one of the soundness lemmata proven before
**)
Theorem validErrorbound_gives_eval (e:exp Q):
Theorem validErrorbound_sound (e:exp Q):
forall E1 E2 fVars dVars absenv nR err P elo ehi Gamma defVars,
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars absenv fVars dVars E2 ->
......@@ -1993,20 +1993,25 @@ Theorem validErrorbound_gives_eval (e:exp Q):
(forall v1 : NatSet.elt, (v1) mem (fVars dVars) = true ->
exists m0 : mType, defVars v1 = Some m0) ->
absenv e = ((elo,ehi),err) ->
exists nF m,
eval_exp E2 defVars (toRExp e) nF m.
(exists nF m,
eval_exp E2 defVars (toRExp e) nF m) /\
(forall nF m,
eval_exp E2 defVars (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%R).
Proof.
revert e; induction e;
intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_intv
valid_dVars P_valid vars_wellTyped absenv_eq.
- inversion typing_ok; subst.
edestruct (validErrorboundCorrectVariable); eauto.
destruct H as [m [eval_var _]]; eauto.
split.
+ eapply validErrorboundCorrectVariable_eval; eauto.
+ intros * eval_float. eapply validErrorboundCorrectVariable; eauto.
- inversion typing_ok; subst.
case_eq (Gamma (Const m v)); intros; rewrite H in H0; [ | inversion H0 ].
apply mTypeEq_compat_eq in H0; subst.
edestruct (validErrorboundCorrectConstant); eauto.
+ simpl in valid_intv.
assert (Q2R elo <= nR <= Q2R ehi)%R.
{
simpl in valid_intv.
rewrite absenv_eq in valid_intv.
simpl in eval_real; inversion eval_real; subst.
simpl in *; rewrite Q2R0_is_0 in H3.
......@@ -2014,242 +2019,28 @@ Proof.
unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv.
canonize_hyps.
simpl in H0,H1.
split; auto.
+ edestruct H0 as [m [eval_const _]]; eauto.
- unfold validErrorbound in valid_error.
split; auto. }
split.
+ eapply validErrorboundCorrectConstant_eval; eauto.
+ intros * eval_float.
pose proof (typingSoundnessExp _ _ typing_ok eval_float).
rewrite H in H1.
inversion H1; subst.
eapply validErrorboundCorrectConstant; eauto.
- simpl in *.
rewrite absenv_eq in valid_error.
case_eq (Gamma (Unop u e)); intros * type_unop;
rewrite type_unop in valid_error; [ | inversion valid_error ].
andb_to_prop valid_error.
destruct u; try congruence.
env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
rename R into valid_error.
andb_to_prop valid_error.
apply Qeq_bool_iff in R.
apply Qeq_eqR in R.
rewrite R.
destruct iv as [e_lo e_hi].
inversion eval_real; subst.
destruct (IHe E1 E2 fVars dVars absenv v1 err_e P e_lo e_hi Gamma defVars) as [nF [mF [eval_float valid_bounds_e]]];
eauto.
+ simpl in typing_ok.
rewrite type_unop in typing_ok.
case_eq (Gamma e); intros * type_e; rewrite type_e in typing_ok; [ | inversion typing_ok ].
andb_to_prop typing_ok; auto.
+ simpl in valid_intv.
rewrite absenv_eq in valid_intv; andb_to_prop valid_intv.
auto.
+ exists (evalUnop Neg nF); exists mF.
simpl.
split; try eauto.
apply bound_flip_sub.
rewrite absenv_e; auto.
- pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
simpl in valid_error.
env_assert absenv e1 absenv_e1.
env_assert absenv e2 absenv_e2.
destruct absenv_e1 as [iv1 [err1 absenv_e1]].
destruct absenv_e2 as [iv2 [err2 absenv_e2]].
iv_assert iv1 iv_e1.
destruct iv_e1 as [ivlo1 [ivhi1 iv_e1]].
rewrite iv_e1 in absenv_e1.
iv_assert iv2 iv_e2.
destruct iv_e2 as [ivlo2 [ivhi2 iv_e2]].
rewrite iv_e2 in absenv_e2.
subst; simpl in *.
rewrite absenv_eq, absenv_e1, absenv_e2 in *.
case_eq (Gamma (Binop b e1 e2));
intros * type_b; rewrite type_b in valid_error; [ | inversion valid_error ].
rewrite type_b in typing_ok; simpl in typing_ok.
case_eq (Gamma e1);
intros * type_e1; rewrite type_e1 in typing_ok; [ | inversion typing_ok ].
case_eq (Gamma e2);
intros * type_e2; rewrite type_e2 in typing_ok; [ | inversion typing_ok ].
andb_to_prop typing_ok.
apply mTypeEq_compat_eq in L0; subst.
andb_to_prop valid_error.
simpl in valid_intv.
andb_to_prop valid_intv.
inversion eval_real; subst.
apply M0_join_is_M0 in H2.
destruct H2; subst.
destruct (IHe1 E1 E2 fVars dVars absenv 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)
as [vF2 [mF2 [eval_float_e2 bounded_e2]]];
try auto; set_tac.
destruct (validIntervalbounds_sound _ _ _ E1 defVars L2 (fVars := fVars) (dVars:=dVars))
as [v1' [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 R4 (fVars:= fVars) (dVars:=dVars))
as [v2' [eval_real_e2 bounds_e2]];
try auto; set_tac.
rewrite absenv_e2 in bounds_e2; simpl in *.
pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6.
assert (b = Div -> ~ (vF2 = 0)%R) as no_div_zero.
{ intros; subst; simpl in *.
andb_to_prop R2.
apply le_neq_bool_to_lt_prop in L0.
assert (contained vF1 (widenInterval (Q2R ivlo1, Q2R ivhi1) (Q2R err1)))
as bounds_float_e1.
{ eapply distance_gives_iv; simpl;
try eauto. }
assert (contained vF2 (widenInterval (Q2R ivlo2, Q2R ivhi2) (Q2R err2)))
as bounds_float_e2.
{ eapply distance_gives_iv; simpl;
try eauto. }
simpl in *.
hnf; intro; subst.
rewrite <- Q2R0_is_0 in bounds_float_e2.
destruct L0 as [nodivzero | nodivzero]; apply Qlt_Rlt in nodivzero; try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; try lra.
}
assert (eval_exp E2 defVars (Binop b (toRExp e1) (toRExp e2)) (perturb (evalBinop b vF1 vF2) (Q2R (mTypeToQ (join mF1 mF2)))) (join mF1 mF2))
as eval_float.
{ econstructor; eauto.
rewrite Rabs_right; try lra.
apply Rle_ge.
apply mTypeToQ_pos_R.
}
exists (perturb (evalBinop b vF1 vF2) (Q2R (mTypeToQ (join mF1 mF2))));
exists (join mF1 mF2); split; [auto | ].
apply binary_unfolding in eval_float; try auto.
destruct b.
+ eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
* simpl.
rewrite type_b.
rewrite type_e1.
rewrite type_e2.
rewrite mTypeEq_refl, R0, R; auto.
* simpl.
rewrite absenv_eq.
rewrite type_b.
rewrite L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2.
auto.
+ eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto.
* simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto.
* simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2; auto.
+ eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto.
* simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto.
* simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2; auto.
+ eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto.
* simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto.
* simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2; auto.
* andb_to_prop R3; auto.
- env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
iv_assert iv iv_e.
destruct iv_e as [ivlo_e [ivhi_e iv_e]].
rewrite iv_e in absenv_e.
subst; simpl in *.
rewrite absenv_eq, absenv_e in *.
case_eq (Gamma (Downcast m e));
intros * type_b; rewrite type_b in valid_error; [ | inversion valid_error ].
rewrite type_b in typing_ok; simpl in typing_ok.
case_eq (Gamma e);
intros * type_e; rewrite type_e in typing_ok; [ | inversion typing_ok ].
andb_to_prop typing_ok.
apply mTypeEq_compat_eq in L0; subst.
andb_to_prop valid_error.
simpl in valid_intv.
andb_to_prop valid_intv.
inversion eval_real; subst.
apply M0_least_precision in H1.
subst.
destruct (IHe E1 E2 fVars dVars absenv v1 err_e P ivlo_e ivhi_e Gamma defVars)
as [vF [mF [eval_float_e bounded_e]]];
try auto; set_tac.
pose proof (typingSoundnessExp _ _ R eval_float_e).
rewrite H in type_e; inversion type_e; subst.
destruct (validIntervalbounds_sound _ _ _ E1 defVars L1 (fVars := fVars) (dVars:=dVars))
as [v1' [eval_real_e bounds_e]];
try auto; set_tac.
rewrite absenv_e in bounds_e.
pose proof (meps_0_deterministic _ eval_real_e H4); subst. clear H4.
exists (perturb vF (Q2R (mTypeToQ m0)));
exists m0.
split; [econstructor; eauto |].
+ rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
+ rewrite Q2R0_is_0 in *. rewrite (delta_0_deterministic _ delta) in *; try auto.
eapply validErrorboundCorrectRounding; eauto.
* econstructor; eauto.
rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
* simpl. rewrite type_b, H.
rewrite mTypeEq_refl, R0, R; auto.
* simpl. rewrite absenv_eq, absenv_e, type_b, L; simpl.
rewrite L0; auto.
Qed.
(**
Soundness theorem for the error bound validator.
Proof is by induction on the expression e.
Each case requires the application of one of the soundness lemmata proven before
**)
Theorem validErrorbound_sound (e:exp Q):
forall E1 E2 fVars dVars absenv nR err P elo ehi Gamma defVars,
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars absenv fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
validErrorbound e Gamma absenv dVars = true ->
validIntervalbounds e absenv P dVars = true ->
(forall v1, NatSet.mem v1 dVars = true ->
exists vr, E1 v1 = Some vr /\
(Q2R (fst (fst (absenv (Var Q v1)))) <= vr <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
(forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v1 : NatSet.elt, (v1) mem (fVars dVars) = true ->
exists m0 : mType, defVars v1 = Some m0) ->
absenv e = ((elo,ehi),err) ->
exists nF m,
eval_exp E2 defVars (toRExp e) nF m /\
(Rabs (nR - nF) <= (Q2R err))%R.
Proof.
revert e; induction e;
intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_intv
valid_dVars P_valid vars_wellTyped absenv_eq.
- inversion typing_ok; subst.
eapply validErrorboundCorrectVariable; eauto.
- inversion typing_ok; subst.
case_eq (Gamma (Const m v)); intros; rewrite H in H0; [ | inversion H0 ].
apply mTypeEq_compat_eq in H0; subst.
eapply validErrorboundCorrectConstant; eauto.
simpl in valid_intv.
rewrite absenv_eq in valid_intv.
simpl in eval_real; inversion eval_real; subst.
simpl in *; rewrite Q2R0_is_0 in H3.
rewrite delta_0_deterministic; auto.
unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv.
destruct (absenv e) as [[e_lo e_hi] err_e] eqn:absenv_e.
repeat
match goal with
| [H: _ = true |- _] => andb_to_prop H
end.
canonize_hyps.
simpl in H0,H1.
split; auto.
- unfold validErrorbound in valid_error.
rewrite absenv_eq in valid_error.
case_eq (Gamma (Unop u e)); intros * type_unop;
rewrite type_unop in valid_error; [ | inversion valid_error ].
andb_to_prop valid_error.
destruct u; try congruence.
env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
rename R into valid_error.
andb_to_prop valid_error.
apply Qeq_bool_iff in R.
apply Qeq_eqR in R.
rewrite R.
destruct iv as [e_lo e_hi].
inversion eval_real; subst.
destruct (IHe E1 E2 fVars dVars absenv v1 err_e P e_lo e_hi Gamma defVars) as [nF [mF [eval_float valid_bounds_e]]];
destruct (IHe E1 E2 fVars dVars absenv v1 err_e P e_lo e_hi Gamma defVars) as [[nF [mF eval_float]] valid_bounds_e];
eauto.
+ simpl in typing_ok.
rewrite type_unop in typing_ok.
......@@ -2258,52 +2049,47 @@ Proof.
+ simpl in valid_intv.
rewrite absenv_eq in valid_intv; andb_to_prop valid_intv.
auto.
+ exists (evalUnop Neg nF); exists mF.
simpl.
split; try eauto.
apply bound_flip_sub.
rewrite absenv_e; auto.
+ split.
* exists (evalUnop Neg nF); exists mF.
simpl; eauto.
* intros * eval_float_op.
inversion eval_float_op; subst; simpl.
apply bound_flip_sub.
rewrite Qeq_bool_iff in R0.
apply Qeq_eqR in R0; rewrite R0.
simpl.
eapply valid_bounds_e; eauto.
- pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
simpl in valid_error.
env_assert absenv e1 absenv_e1.
env_assert absenv e2 absenv_e2.
destruct absenv_e1 as [iv1 [err1 absenv_e1]].
destruct absenv_e2 as [iv2 [err2 absenv_e2]].
iv_assert iv1 iv_e1.
destruct iv_e1 as [ivlo1 [ivhi1 iv_e1]].
rewrite iv_e1 in absenv_e1.
iv_assert iv2 iv_e2.
destruct iv_e2 as [ivlo2 [ivhi2 iv_e2]].
rewrite iv_e2 in absenv_e2.
destruct (absenv e1) as [[ivlo1 ivhi1] err1] eqn:absenv_e1;
destruct (absenv e2) as [[ivlo2 ivhi2] err2] eqn:absenv_e2.
subst; simpl in *.
rewrite absenv_eq, absenv_e1, absenv_e2 in *.
case_eq (Gamma (Binop b e1 e2));
intros * type_b; rewrite type_b in valid_error; [ | inversion valid_error ].
rewrite type_b in typing_ok; simpl in typing_ok.
intros * type_b; rewrite type_b in *; [ | inversion valid_error ].
case_eq (Gamma e1);
intros * type_e1; rewrite type_e1 in typing_ok; [ | inversion typing_ok ].
case_eq (Gamma e2);
intros * type_e2; rewrite type_e2 in typing_ok; [ | inversion typing_ok ].
andb_to_prop typing_ok.
apply mTypeEq_compat_eq in L0; subst.
andb_to_prop valid_error.
simpl in valid_intv.
andb_to_prop valid_intv.
repeat match goal with
| [H: _ = true |- _] => andb_to_prop H
end.
type_conv.
inversion eval_real; subst.
apply M0_join_is_M0 in H2.
destruct H2; subst.
destruct (IHe1 E1 E2 fVars dVars absenv v1 err1 P ivlo1 ivhi1 Gamma defVars)
as [vF1 [mF1 [eval_float_e1 bounded_e1]]];
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)
as [vF2 [mF2 [eval_float_e2 bounded_e2]]];
as [[vF2 [mF2 eval_float_e2]] bounded_e2];
try auto; set_tac.
destruct (validIntervalbounds_sound _ _ _ E1 defVars L2 (fVars := fVars) (dVars:=dVars))
destruct (validIntervalbounds_sound _ _ _ E1 defVars L0 (fVars := fVars) (dVars:=dVars))
as [v1' [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 R4 (fVars:= fVars) (dVars:=dVars))
destruct (validIntervalbounds_sound _ _ _ E1 defVars R0 (fVars:= fVars) (dVars:=dVars))
as [v2' [eval_real_e2 bounds_e2]];
try auto; set_tac.
rewrite absenv_e2 in bounds_e2; simpl in *.
......@@ -2311,7 +2097,7 @@ Proof.
assert (b = Div -> ~ (vF2 = 0)%R) as no_div_zero.
{ intros; subst; simpl in *.
andb_to_prop R2.
apply le_neq_bool_to_lt_prop in L0.
apply le_neq_bool_to_lt_prop in L1.
assert (contained vF1 (widenInterval (Q2R ivlo1, Q2R ivhi1) (Q2R err1)))
as bounds_float_e1.
{ eapply distance_gives_iv; simpl;
......@@ -2321,51 +2107,50 @@ Proof.
{ eapply distance_gives_iv; simpl;
try eauto. }
simpl in *.
hnf; intro; subst.
intro; subst.
rewrite <- Q2R0_is_0 in bounds_float_e2.
destruct L0 as [nodivzero | nodivzero]; apply Qlt_Rlt in nodivzero; try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; try lra.
destruct L1 as [nodivzero | nodivzero];
apply Qlt_Rlt in nodivzero;
try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; lra.
}
assert (eval_exp E2 defVars (Binop b (toRExp e1) (toRExp e2)) (perturb (evalBinop b vF1 vF2) (Q2R (mTypeToQ (join mF1 mF2)))) (join mF1 mF2))
as eval_float.
{ econstructor; eauto.
split.
+ repeat eexists; econstructor; eauto.
rewrite Rabs_right; try lra.
apply Rle_ge.
instantiate (1 := 0%R).
apply mTypeToQ_pos_R.
}
exists (perturb (evalBinop b vF1 vF2) (Q2R (mTypeToQ (join mF1 mF2))));
exists (join mF1 mF2); split; [auto | ].
apply binary_unfolding in eval_float; try auto.
destruct b.
+ eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
* simpl.
rewrite type_b.
rewrite type_e1.
rewrite type_e2.
rewrite mTypeEq_refl, R0, R; auto.
* simpl.
rewrite absenv_eq.
rewrite type_b.
rewrite L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2.
auto.
+ eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto.
* simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto.
* simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2; auto.
+ eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto.
* simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto.
* simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2; auto.
+ eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto.
* simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto.
* simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl.
rewrite absenv_e1, absenv_e2; auto.
* andb_to_prop R3; auto.
- env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
iv_assert iv iv_e.
destruct iv_e as [ivlo_e [ivhi_e iv_e]].
rewrite iv_e in absenv_e.
apply Rle_ge.
hnf; right. reflexivity.
+ intros * eval_float.
clear eval_float_e1 eval_float_e2.
inversion eval_float; subst.
eapply (binary_unfolding _ H2 H4 H8) in eval_float; try auto.
destruct b.
* eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
{ simpl.
rewrite type_b.
rewrite type_e1.
rewrite type_e2.
rewrite mTypeEq_refl, R3, R4; auto. }
{ simpl.
rewrite absenv_eq.
rewrite type_b.
rewrite L, L2, R1; simpl.
rewrite absenv_e1, absenv_e2.
auto. }
* eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto.
{ simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R3, R4; auto. }
{ simpl; rewrite absenv_eq, type_b, L, L2, R1; simpl.
rewrite absenv_e1, absenv_e2; auto. }
* eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto.
{ simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R3, R4; auto. }
{ simpl; rewrite absenv_eq, type_b, L, L2, R1; simpl.
rewrite absenv_e1, absenv_e2; auto. }
* eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto.
{ simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R3, R4; auto. }
{ simpl; rewrite absenv_eq, type_b, L, L2, R1; simpl.
rewrite absenv_e1, absenv_e2; auto. }
{ andb_to_prop R; auto. }
- destruct (absenv e) as [[ivlo_e ivhi_e] err_e] eqn: absenv_e.
subst; simpl in *.
rewrite absenv_eq, absenv_e in *.
case_eq (Gamma (Downcast m e));
......@@ -2382,7 +2167,7 @@ Proof.
apply M0_least_precision in H1.
subst.
destruct (IHe E1 E2 fVars dVars absenv v1 err_e P ivlo_e ivhi_e Gamma defVars)
as [vF [mF [eval_float_e bounded_e]]];
as [[vF [mF eval_float_e]] bounded_e];
try auto; set_tac.
pose proof (typingSoundnessExp _ _ R eval_float_e).
rewrite H in type_e; inversion type_e; subst.
......@@ -2391,20 +2176,26 @@ Proof.
try auto; set_tac.
rewrite absenv_e in bounds_e.
pose proof (meps_0_deterministic _ eval_real_e H4); subst. clear H4.
exists (perturb vF (Q2R (mTypeToQ m0)));
exists m0.
split; [econstructor; eauto |].
+ rewrite Rabs_right; try lra.
split.
+ exists (perturb vF (Q2R (mTypeToQ m0)));
exists m0.
econstructor; eauto.
rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
+ rewrite Q2R0_is_0 in *. rewrite (delta_0_deterministic _ delta) in *; try auto.
intros * eval_float.
clear eval_float_e.
inversion eval_float; subst.
eapply validErrorboundCorrectRounding; eauto.
* econstructor; eauto.
rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
* simpl. eapply Downcast_dist'; eauto.
constructor. unfold updDefVars. rewrite Nat.eqb_refl; auto.
unfold updEnv; simpl; auto.
* simpl. rewrite type_b, H.
rewrite mTypeEq_refl, R0, R; auto.
* simpl. rewrite absenv_eq, absenv_e, type_b, L; simpl.
rewrite L0; auto.
Unshelve.
intros. auto.
Qed.
Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
......@@ -2451,7 +2242,7 @@ Proof.
| [H : validErrorbound _ _ _ _ = true |- _] =>
eapply validErrorbound_sound
with (err := err_e) (elo := ivlo_e) (ehi:= ivhi_e) in H; eauto;
destruct H as [vF [ mF [eval_float_e bounded_e]]]
destruct H as [[vF [ mF eval_float_e]] bounded_e]
end.
repeat
match goal with
......@@ -2462,7 +2253,8 @@ Proof.
(NatSet.add n dVars) (updEnv n vF E2)).
+ eapply approxUpdBound; try auto.
simpl in *.
apply Rle_trans with (r2:= Q2R err_e); lra.
apply Rle_trans with (r2:= Q2R err_e); try lra.
eapply bounded_e; eauto.
+ rename R into valid_rec.
rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *;
simpl in *.
......@@ -2531,7 +2323,7 @@ Proof.
unfold updEnv; simpl.
unfold validErrorboundCmd in valid_bounds.
simpl in *.
edestruct validErrorbound_sound as [vF [mF [eval_e bounded_e]]]; eauto.
edestruct validErrorbound_sound as [[vF [mF eval_e]] bounded_e]; eauto.
exists vF; exists mF; econstructor; eauto.
Qed.
......@@ -2581,254 +2373,82 @@ Proof.
| [H : validErrorbound _ _ _ _ = true |- _] =>
eapply validErrorbound_sound
with (err := err_e) (elo := ivlo_e) (ehi:= ivhi_e) in H; eauto;
destruct H as [vFe [mFe [eval_float_e bounded_e]]]
destruct H as [[vFe [mFe eval_float_e]] bounded_e]
end.
repeat
match goal with
| [H : Qeq_bool _ _ = true |- _] => rewrite Qeq_bool_iff in H
| [H : _ == _ |- _ ] => apply Qeq_eqR in H
end.
assert (approxEnv (updEnv n v E1) (updDefVars n mF defVars) absenv fVars
(NatSet.add n dVars) (updEnv n vFe E2)).
+ eapply approxUpdBound; try auto.
rename R into valid_rec.
rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *;
simpl in *.
apply Rle_trans with (r2:= Q2R err_e); lra.
+ rename R into valid_rec.
rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *;
simpl in *.
match goal with
| [ H: _ && _ = true |- _] => andb_to_prop H
end.
type_conv.
apply (IHf absenv (updEnv n v E1) (updEnv n vF E2) outVars fVars
(NatSet.add n dVars) vR vF mF elo ehi err P Gamma
(updDefVars n m defVars));
eauto.
{ eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
- rewrite NatSet.add_spec, NatSet.union_spec;
rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto.
- rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ hnf. intros a in_diff.
rewrite NatSet.diff_spec, NatSet.add_spec in in_diff.
destruct in_diff as [ in_freeVars no_dVar].
apply freeVars_subset.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet