Commit b0ff2319 authored by Heiko Becker's avatar Heiko Becker
Browse files

All unused files are now in the attic. Make some cleanups

parent 935df721
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
(*Coq.QArith.Qcanon.*)
Require Import Coq.micromega.Psatz Coq.Reals.Reals Interval.Interval_tactic.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.IntervalArithQ.
Require Import Daisy.ErrorBounds Daisy.IntervalValidation Daisy.PreconditionValidation.
Section ComputableErrors.
Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (intv, err) := (env e) in
let errPos := Qleb 0 err in
match e with
|Var v => false
|Param v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
(* A constant will be a point intv. Take maxAbs never the less *)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
let (ive2, err2) := env e2 in
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let e1F := upperBoundE1 + err1 in
let e2F := upperBoundE2 + err2 in
let theVal :=
match b with
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon) err
| Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon)) err
| Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + Qabs(e1F * e2F) * RationalSimps.machineEpsilon) err
| Div => false
end
in andb (andb rec errPos) theVal
end.
(*
Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (intv, err) := (env e) in
let errPos := Qleb 0 err in
match e with
|Var v => false
|Param v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
(* A constant will be a point intv. Take maxAbs never the less *)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
let (ive2, err2) := env e2 in
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let e1F := upperBoundE1 + err1 in
let e2F := upperBoundE2 + err2 in
let theVal :=
match b with
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon) err
| Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon)) err
| Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + Qabs(e1F * e2F) * RationalSimps.machineEpsilon) err
| Div => false
end
in andb (andb rec errPos) theVal
end.
(*
Functional Scheme validErrorbound_ind := Induction for validErrorbound Sort Prop.
*)
*)
Lemma err_always_positive e (absenv:analysisResult) iv err:
validErrorbound e absenv = true ->
(iv,err) = absenv e ->
(0 <= Q2R err)%R.
Proof.
destruct e;intros validErrorbound_e absenv_e;
unfold validErrorbound in validErrorbound_e;
rewrite <- absenv_e in validErrorbound_e; simpl in *.
- inversion validErrorbound_e.
- apply Is_true_eq_left in validErrorbound_e.
apply andb_prop_elim in validErrorbound_e.
destruct validErrorbound_e as [hyp _].
apply Is_true_eq_true in hyp.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
- apply Is_true_eq_left in validErrorbound_e.
apply andb_prop_elim in validErrorbound_e.
destruct validErrorbound_e as [hyp _].
apply Is_true_eq_true in hyp.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
- destruct (absenv e1). destruct (absenv e2).
apply Is_true_eq_left in validErrorbound_e.
apply andb_prop_elim in validErrorbound_e.
destruct validErrorbound_e as [hyp _].
apply andb_prop_elim in hyp.
destruct hyp as [ _ hyp].
apply Is_true_eq_true in hyp.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
Qed.
Lemma err_always_positive e (absenv:analysisResult) iv err:
validErrorbound e absenv = true ->
(iv,err) = absenv e ->
(0 <= Q2R err)%R.
Proof.
destruct e;intros validErrorbound_e absenv_e;
unfold validErrorbound in validErrorbound_e;
rewrite <- absenv_e in validErrorbound_e; simpl in *.
- inversion validErrorbound_e.
- apply Is_true_eq_left in validErrorbound_e.
apply andb_prop_elim in validErrorbound_e.
destruct validErrorbound_e as [hyp _].
apply Is_true_eq_true in hyp.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
- apply Is_true_eq_left in validErrorbound_e.
apply andb_prop_elim in validErrorbound_e.
destruct validErrorbound_e as [hyp _].
apply Is_true_eq_true in hyp.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
- destruct (absenv e1). destruct (absenv e2).
apply Is_true_eq_left in validErrorbound_e.
apply andb_prop_elim in validErrorbound_e.
destruct validErrorbound_e as [hyp _].
apply andb_prop_elim in hyp.
destruct hyp as [ _ hyp].
apply Is_true_eq_true in hyp.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
Qed.
Ltac math_hnf := repeat rewrite Rsub_eq_Ropp_Rplus;
repeat rewrite Ropp_plus_distr;
repeat rewrite Rmult_plus_distr_r;
repeat rewrite Rmult_plus_distr_l;
repeat rewrite Ropp_involutive;
repeat rewrite <- Rplus_assoc.
Ltac math_hnf := repeat rewrite Rsub_eq_Ropp_Rplus;
repeat rewrite Ropp_plus_distr;
repeat rewrite Rmult_plus_distr_r;
repeat rewrite Rmult_plus_distr_l;
repeat rewrite Ropp_involutive;
repeat rewrite <- Rplus_assoc.
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
eval_exp 0%R cenv (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) cenv (Const (Q2R n)) nF ->
validErrorbound (Const n) absenv = true ->
validIntervalbounds (Const n) absenv P = true ->
absenv (Const n) = ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv absenv n nR nF e nlo nhi P eval_real eval_float error_valid intv_valid absenv_const.
unfold validErrorbound in error_valid.
rewrite absenv_const in error_valid.
inversion eval_real; subst.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
clear delta H0.
inversion eval_float; subst.
unfold perturb in *; simpl in *.
rewrite Rabs_err_simpl.
unfold Qleb in error_valid.
apply Is_true_eq_left in error_valid.
apply andb_prop_elim in error_valid.
destruct error_valid as [_ error_valid].
apply Is_true_eq_true in error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
eapply Rle_trans.
rewrite Rabs_mult.
eapply Rmult_le_compat_l; [ apply Rabs_pos | ].
apply H0.
rewrite Rabs_eq_Qabs.
rewrite Q2R_mult in error_valid.
eapply Rle_trans.
eapply Rmult_le_compat_r.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
unfold machineEpsilon.
assert (Qle_bool 0 (1 # (2^53)) = true) by (unfold Qle_bool; auto).
rewrite <- Qle_bool_iff; auto.
rewrite absenv_const in intv_valid.
simpl in intv_valid.
apply Is_true_eq_left in intv_valid.
apply andb_prop_elim in intv_valid.
destruct intv_valid as [valid_lo valid_hi]; unfold Is_true in *.
Focus 2. apply error_valid.
rewrite <- Rabs_eq_Qabs.
rewrite <- maxAbs_impl_RmaxAbs.
apply RmaxAbs; simpl; apply Qle_Rle; rewrite <- Qle_bool_iff; unfold Qleb in *; simpl in *;
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
eval_exp 0%R cenv (Const (Q2R n)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) cenv (Const (Q2R n)) nF ->
validErrorbound (Const n) absenv = true ->
validIntervalbounds (Const n) absenv P = true ->
absenv (Const n) = ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv absenv n nR nF e nlo nhi P eval_real eval_float error_valid intv_valid absenv_const.
unfold validErrorbound in error_valid.
rewrite absenv_const in error_valid.
inversion eval_real; subst.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
clear delta H0.
inversion eval_float; subst.
unfold perturb in *; simpl in *.
rewrite Rabs_err_simpl.
unfold Qleb in error_valid.
apply Is_true_eq_left in error_valid.
apply andb_prop_elim in error_valid.
destruct error_valid as [_ error_valid].
apply Is_true_eq_true in error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
eapply Rle_trans.
rewrite Rabs_mult.
eapply Rmult_le_compat_l; [ apply Rabs_pos | ].
apply H0.
rewrite Rabs_eq_Qabs.
rewrite Q2R_mult in error_valid.
eapply Rle_trans.
eapply Rmult_le_compat_r.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
unfold machineEpsilon.
assert (Qle_bool 0 (1 # (2^53)) = true) by (unfold Qle_bool; auto).
rewrite <- Qle_bool_iff; auto.
rewrite absenv_const in intv_valid.
simpl in intv_valid.
apply Is_true_eq_left in intv_valid.
apply andb_prop_elim in intv_valid.
destruct intv_valid as [valid_lo valid_hi]; unfold Is_true in *.
Focus 2. apply error_valid.
rewrite <- Rabs_eq_Qabs.
rewrite <- maxAbs_impl_RmaxAbs.
apply RmaxAbs; simpl; apply Qle_Rle; rewrite <- Qle_bool_iff; unfold Qleb in *; simpl in *;
[destruct (Qle_bool nlo n); auto | destruct (Qle_bool n nhi); auto].
Qed.
Lemma validErrorboundCorrectParam:
forall cenv absenv (v:nat) nR nF e P plo phi,
(forall n, List.In n (freeVars Q (Param Q v)) ->
Is_true(isSupersetIntv (P n) (fst (absenv (Param Q n))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp (Param Q v)) nF ->
validErrorbound (Param Q v) absenv = true ->
validIntervalbounds (Param Q v) absenv P = true ->
absenv (Param Q v) = ((plo,phi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv absenv v nR nF e P plo phi absenv_approx_p cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param.
unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid.
inversion eval_real; subst.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
inversion eval_float; subst.
unfold precondValidForExec in cenv_approx_p.
specialize (absenv_approx_p v).
specialize (cenv_approx_p v).
assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists).
destruct H as [ivlo [ivhi P_eq]].
rewrite <- P_eq in absenv_approx_p, cenv_approx_p.
rewrite absenv_param in absenv_approx_p.
unfold freeVars in absenv_approx_p; simpl in absenv_approx_p.
assert (v = v \/ False) by auto.
specialize (absenv_approx_p H).
unfold isSupersetIntv in absenv_approx_p.
apply andb_prop_elim in absenv_approx_p.
destruct absenv_approx_p as [plo_le_ivlo ivhi_le_phi].
apply Is_true_eq_true, Qle_bool_iff in plo_le_ivlo.
apply Is_true_eq_true, Qle_bool_iff in ivhi_le_phi.
destruct cenv_approx_p as [ivlo_le_cenv cenv_le_ivhi].
apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi.
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo ivlo_le_cenv).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) cenv_le_ivhi ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H2 H3).
unfold perturb.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
eapply Rle_trans.
eapply Rmult_le_compat; [ apply Rabs_pos | apply Rabs_pos | | ].
apply H4.
apply H1.
pose proof (maxAbs_impl_RmaxAbs plo phi).
unfold RmaxAbsFun in H5.
simpl in H5.
rewrite H5.
apply Is_true_eq_left in error_valid.
apply andb_prop_elim in error_valid.
destruct error_valid as [_ error_valid].
apply Is_true_eq_true in error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
rewrite Q2R_mult in error_valid.
apply error_valid.
Qed.
Qed.
Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
(forall v, List.In v (freeVars Q (Binop Plus e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
Lemma validErrorboundCorrectParam:
forall cenv absenv (v:nat) nR nF e P plo phi,
(forall n, List.In n (freeVars Q (Param Q v)) ->
Is_true(isSupersetIntv (P n) (fst (absenv (Param Q n))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Plus e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Plus e1 e2) absenv = true ->
validIntervalbounds (Binop Plus e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Plus e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
eval_exp 0%R cenv (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp (Param Q v)) nF ->
validErrorbound (Param Q v) absenv = true ->
validIntervalbounds (Param Q v) absenv P = true ->
absenv (Param Q v) = ((plo,phi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
eapply Rle_trans.
eapply add_abs_err_bounded.
apply e1_real.
rewrite <- mEps_eq_Rmeps.
apply e1_float.
apply e2_real.
rewrite <- mEps_eq_Rmeps.
apply e2_float.
apply eval_real.
rewrite <- mEps_eq_Rmeps; apply eval_float.
apply err1_bounded.
apply err2_bounded.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
apply Is_true_eq_left in valid_error.
apply andb_prop_elim in valid_error.
destruct valid_error as [ valid_rec valid_error].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_error.
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite Q2R_mult in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
apply mEps_geq_zero.
Focus 2.
apply valid_error.
clear valid_e1 valid_e2.
simpl in valid_intv.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_intv.
apply Is_true_eq_left in valid_intv.
apply andb_prop_elim in valid_intv.
destruct valid_intv as [valid_rec valid_intv].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_iv_e1 valid_iv_e2].
apply Is_true_eq_true in valid_iv_e1; apply Is_true_eq_true in valid_iv_e2.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat.
- assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1.
+ intros v in_fV_e1.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
+ pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- assert (forall v : nat, List.In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e2.
+ intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e2 p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (Rabs_error_bounded_maxAbs nR2); try auto.
unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
Qed.
Proof.
intros cenv absenv v nR nF e P plo phi absenv_approx_p cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param.
unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid.
inversion eval_real; subst.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
inversion eval_float; subst.
unfold precondValidForExec in cenv_approx_p.
specialize (absenv_approx_p v).
specialize (cenv_approx_p v).
assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists).
destruct H as [ivlo [ivhi P_eq]].
rewrite <- P_eq in absenv_approx_p, cenv_approx_p.
rewrite absenv_param in absenv_approx_p.
unfold freeVars in absenv_approx_p; simpl in absenv_approx_p.
assert (v = v \/ False) by auto.
specialize (absenv_approx_p H).
unfold isSupersetIntv in absenv_approx_p.
apply andb_prop_elim in absenv_approx_p.
destruct absenv_approx_p as [plo_le_ivlo ivhi_le_phi].
apply Is_true_eq_true, Qle_bool_iff in plo_le_ivlo.
apply Is_true_eq_true, Qle_bool_iff in ivhi_le_phi.
destruct cenv_approx_p as [ivlo_le_cenv cenv_le_ivhi].
apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi.
pose proof (Rle_trans (Q2R plo) (Q2R ivlo) (cenv v) plo_le_ivlo ivlo_le_cenv).
pose proof (Rle_trans (cenv v) (Q2R ivhi) (Q2R phi) cenv_le_ivhi ivhi_le_phi).
pose proof (RmaxAbs (Q2R plo) (cenv v) (Q2R phi) H2 H3).
unfold perturb.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
eapply Rle_trans.
eapply Rmult_le_compat; [ apply Rabs_pos | apply Rabs_pos | | ].
apply H4.
apply H1.
pose proof (maxAbs_impl_RmaxAbs plo phi).
unfold RmaxAbsFun in H5.
simpl in H5.
rewrite H5.
apply Is_true_eq_left in error_valid.
apply andb_prop_elim in error_valid.
destruct error_valid as [_ error_valid].
apply Is_true_eq_true in error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
rewrite Q2R_mult in error_valid.
apply error_valid.
Qed.
Lemma validErrorboundCorrectSubtraction cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
(forall v, List.In v (freeVars Q (Binop Sub e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Sub e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Sub e1 e2) absenv = true ->
validIntervalbounds (Binop Sub e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Sub e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_sub
err1_bounded err2_bounded.
eapply Rle_trans.
eapply subtract_abs_err_bounded.
apply e1_real.
rewrite <- mEps_eq_Rmeps.
apply e1_float.
apply e2_real.
rewrite <- mEps_eq_Rmeps.
apply e2_float.
apply eval_real.
rewrite <- mEps_eq_Rmeps. apply eval_float.
apply err1_bounded.
apply err2_bounded.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_sub, absenv_e1, absenv_e2 in valid_error.
apply Is_true_eq_left in valid_error.
apply andb_prop_elim in valid_error.
destruct valid_error as [valid_rec valid_error].
apply andb_prop_elim in valid_rec.
clear valid_rec.
apply Is_true_eq_true in valid_error.
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite Q2R_mult in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
apply mEps_geq_zero.
simpl in valid_intv.
rewrite absenv_sub, absenv_e1, absenv_e2 in valid_intv.
apply Is_true_eq_left in valid_intv.
apply andb_prop_elim in valid_intv.
destruct valid_intv as [valid_rec valid_intv].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_iv_e1 valid_iv_e2].
apply Is_true_eq_true in valid_iv_e1; apply Is_true_eq_true in valid_iv_e2.
Focus 2.
apply valid_error.
eapply Rplus_le_compat.
- assert (forall v : nat, List.In v (freeVars Q e1 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e1.
+ intros v in_fV_e1.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
+ pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e1 p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
apply (Rabs_error_bounded_maxAbs nR1); try auto.
unfold contained; rewrite absenv_e1 in valid_bounds_e1; auto.
- assert (forall v : nat, List.In v (freeVars Q e2 ) -> Is_true (isSupersetIntv (P v) (fst (absenv (Param Q v)))))
as env_approx_e2.
+ intros v in_fV_e2.
assert (List.In v (freeVars Q (Binop Plus e1 e2))) by (unfold freeVars; apply in_or_app; auto).
apply (env_approx_p v H).
pose proof (validIntervalbounds_sound _ _ _ _ _ env_approx_e2 p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
apply (Rabs_error_bounded_maxAbs nR2); try auto.
unfold contained; rewrite absenv_e2 in valid_bounds_e2; auto.
Qed.
Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
(forall v, List.In v (freeVars Q (Binop Plus e1 e2)) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v))))) ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Plus e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Plus e1 e2) absenv = true ->
validIntervalbounds (Binop Plus e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Plus e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
eapply Rle_trans.
eapply add_abs_err_bounded.
apply e1_real.
rewrite <- mEps_eq_Rmeps.
apply e1_float.
apply e2_real.
rewrite <- mEps_eq_Rmeps.
apply e2_float.
apply eval_real.
rewrite <- mEps_eq_Rmeps; apply eval_float.
apply err1_bounded.
apply err2_bounded.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
apply Is_true_eq_left in valid_error.
apply andb_prop_elim in valid_error.
destruct valid_error as [ valid_rec valid_error].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_error.
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite Q2R_mult in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
apply mEps_geq_zero.
Focus 2.
apply valid_error.
clear valid_e1 valid_e2.
simpl in valid_intv.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_intv.