Commit 75e8cdab authored by Heiko Becker's avatar Heiko Becker

Fix formalization flaw in Coq checker and prepare gitignore for testing

parent f295fc40
......@@ -3,6 +3,7 @@ target/
.DS_Store
src/test/resources/range_regression_today.txt
hol/.ocamlinit
hol/output/*
dmtcp*
ckpt*
hol/run_hol.sh
......@@ -16,9 +17,10 @@ coq/Makefile
coq/*/*.glob
coq/*/.*
coq/*/*.vo
coq/output/*
daisy
rawdata/*
.ensime*
/daisy
last.log
output/*.scala
output/*
......@@ -104,7 +104,7 @@ Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Sub (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= err1 + err2 + ((Rabs e1F + Rabs e2F) * machineEpsilon))%R.
(Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * machineEpsilon))%R.
Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
......@@ -130,37 +130,21 @@ Proof.
repeat rewrite Rsub_eq_Ropp_Rplus.
repeat rewrite Ropp_plus_distr.
rewrite plus_bounds_simplify.
pose proof (Rabs_triang (e1R + - e1F) ((- e2R + - - e2F) + - ((e1F + - e2F) * delta))).
rewrite Ropp_involutive.
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).
apply Rabs_triang.
eapply Rle_trans.
apply H1.
eapply Rplus_le_compat_l.
apply Rabs_triang.
rewrite <- Rplus_assoc.
setoid_rewrite Rplus_comm at 4.
repeat rewrite <- Rsub_eq_Ropp_Rplus.
rewrite Rabs_Ropp.
assert (Rabs (- e2R - - e2F)%R = Rabs (e2R - e2F)).
- rewrite Rsub_eq_Ropp_Rplus.
rewrite <- Ropp_plus_distr.
rewrite Rabs_Ropp.
rewrite <- Rsub_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 Rsub_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.
rewrite Rabs_minus_sym in bound_e2.
apply Rplus_le_compat; [apply Rplus_le_compat; auto | ].
rewrite Rabs_mult.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
......
......@@ -19,20 +19,38 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (ive1, err1) := env e1 in
let (ive2, err2) := env e2 in
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 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
| Plus => Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Sub => Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Div => false
end
in andb (andb rec errPos) theVal
end.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma Qred_eq_frac:
forall q1 q2,
Is_true (Qleb q1 q2) <-> Is_true (Qleb (Qred q1) q2).
Proof.
intros; split; intros.
- apply Is_true_eq_left. apply Is_true_eq_true in H.
unfold Qleb in *; apply Qle_bool_iff. apply Qle_bool_iff in H.
rewrite Qred_correct; auto.
- apply Is_true_eq_left. apply Is_true_eq_true in H. unfold Qleb in *.
rewrite Qle_bool_iff.
rewrite Qle_bool_iff in H.
rewrite Qred_correct in H.
auto.
Qed.
(** Since errors are intervals with 0 as center, we track them as single value since this eases proving upper bounds **)
Lemma err_always_positive e (absenv:analysisResult) iv err:
validErrorbound e absenv = true ->
......@@ -218,21 +236,29 @@ Proof.
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_rec err_pos].
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.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat_r.
apply mEps_geq_zero.
Focus 2.
apply Rle_Qle in valid_error.
rewrite <- Qle_bool_iff in valid_error.
apply Is_true_eq_left in valid_error.
apply Is_true_eq_true in valid_error.
rewrite 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.
......@@ -243,15 +269,33 @@ Proof.
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.
- pose proof (validIntervalbounds_sound _ _ _ _ _ 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.
- pose proof (validIntervalbounds_sound _ _ _ _ _ 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.
remember (addIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.additionIsValid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
subst; simpl in *.
apply RmaxAbs; simpl.
- rewrite Q2R_min4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
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 :
......@@ -318,13 +362,39 @@ Proof.
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.
- pose proof (validIntervalbounds_sound _ _ _ _ _ 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.
- pose proof (validIntervalbounds_sound _ _ _ _ _ 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.
remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.subtractionIsValid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
subst; simpl in *.
apply RmaxAbs; simpl.
- rewrite Q2R_min4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_opp;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_opp;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; auto.
Qed.
Lemma validErrorboundCorrectMult 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 :
......@@ -932,21 +1002,39 @@ Proof.
rewrite H1.
lra.
}
- apply Rmult_le_compat; [ apply Rabs_pos | apply mEps_geq_zero | | apply Req_le; auto ].
rewrite Q2R_mult; repeat rewrite Q2R_plus.
repeat rewrite <- maxAbs_impl_RmaxAbs.
repeat rewrite Rabs_mult.
apply Rmult_le_compat; [apply Rabs_pos | apply Rabs_pos | | ].
+ apply (Rabs_error_bounded_maxAbs nR1); try auto.
rewrite absenv_e1 in valid_e1; simpl in *; unfold contained; auto.
+ apply (Rabs_error_bounded_maxAbs nR2); try auto.
rewrite absenv_e2 in valid_e2; simpl in *; unfold contained; auto.
- remember (multIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.interval_multiplication_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
unfold RmaxAbsFun.
apply Rmult_le_compat_r.
apply mEps_geq_zero.
apply RmaxAbs; subst; simpl in *.
- rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
Qed.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
precondValidForExec P cenv ->
......
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