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

Prove holes in validation of errors, which required validity of interval checker

parent 5166f958
......@@ -99,18 +99,6 @@ Section ComputableErrors.
|Const _ => (((-100) # 1,100 # 1),errVaru)
|_ => ((lowerBoundAddUCst,upperBoundAddUCst),errAddUCst) end).
Definition envApproximatesPrecond (P:nat -> intv) (absenv:analysisResult) :=
forall u:nat,
let (ivlo,ivhi) := P u in
let (absIv,err) := absenv (Param Q u) in
let (abslo,abshi) := absIv in
(abslo <= ivlo /\ ivhi <= abshi)%Q.
Definition precondValidForExec (P:nat->intv) (cenv:nat->R) :=
forall v:nat,
let (ivlo,ivhi) := P v in
(Q2R ivlo <= cenv v <= Q2R ivhi)%R.
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
eval_exp 0%R cenv (Const (Q2R n)) nR ->
......@@ -208,22 +196,24 @@ Section ComputableErrors.
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 :
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 machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R 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.
envApproximatesPrecond P absenv ->
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 machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R 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 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.
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.
......@@ -260,6 +250,14 @@ Section ComputableErrors.
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.
......@@ -270,36 +268,54 @@ Section ComputableErrors.
- assert (Rabs nF1 <= Rabs nR1 + Q2R err1)%R by lra.
(* TODO: Make this a lemma too. This looks lika a coprrectness lemma for IV arithmetic checker*)
assert (Rabs nR1 <= RmaxAbsFun (e1lo, e1hi))%R.
+ unfold validIntervalbounds in valid_intv; simpl in valid_intv.
rewrite absenv_e1, absenv_e2, absenv_add in valid_intv.
admit.
+ pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e1 e1_real).
unfold RmaxAbsFun.
rewrite absenv_e1 in H1; simpl in H1; destruct H1.
eapply RmaxAbs; auto.
+ assert (Rabs nR1 + Q2R err1 <= RmaxAbsFun (e1lo, e1hi) + Q2R err1)%R by (apply Rplus_le_compat_r; auto).
eapply Rle_trans.
apply H0.
eapply Rle_trans.
apply H2.
apply Rle_abs.
- (* similar by lemma *) admit.
Admitted.
- rewrite Rabs_minus_sym in err2_bounded.
assert (Rabs nF2 - Rabs nR2 <= Q2R err2)%R.
+ eapply Rle_trans; [apply Rabs_triang_inv | auto].
+ assert (Rabs nF2 <= Rabs nR2 + Q2R err2)%R by lra.
(* TODO: Make this a lemma too. This looks lika a coprrectness lemma for IV arithmetic checker*)
assert (Rabs nR2 <= RmaxAbsFun (e2lo, e2hi))%R.
* pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e2 e2_real).
unfold RmaxAbsFun.
rewrite absenv_e2 in H1; simpl in H1; destruct H1.
eapply RmaxAbs; auto.
* assert (Rabs nR2 + Q2R err2 <= RmaxAbsFun (e2lo, e2hi) + Q2R err2)%R by (apply Rplus_le_compat_r; auto).
eapply Rle_trans.
apply H0.
eapply Rle_trans.
apply H2.
apply Rle_abs.
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 :
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 machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R 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.
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 :
envApproximatesPrecond P absenv ->
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 machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R 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 e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_add
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.
......@@ -315,7 +331,7 @@ Section ComputableErrors.
apply err2_bounded.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
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].
......@@ -335,6 +351,14 @@ Section ComputableErrors.
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.
......@@ -345,17 +369,33 @@ Section ComputableErrors.
- assert (Rabs nF1 <= Rabs nR1 + Q2R err1)%R by lra.
(* TODO: Make this a lemma too. This looks lika a coprrectness lemma for IV arithmetic checker*)
assert (Rabs nR1 <= RmaxAbsFun (e1lo, e1hi))%R.
+ unfold validIntervalbounds in valid_intv; simpl in valid_intv.
rewrite absenv_e1, absenv_e2, absenv_add in valid_intv.
admit.
+ pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e1 e1_real).
unfold RmaxAbsFun.
rewrite absenv_e1 in H1; simpl in H1; destruct H1.
eapply RmaxAbs; auto.
+ assert (Rabs nR1 + Q2R err1 <= RmaxAbsFun (e1lo, e1hi) + Q2R err1)%R by (apply Rplus_le_compat_r; auto).
eapply Rle_trans.
apply H0.
eapply Rle_trans.
apply H2.
apply Rle_abs.
- (* similar by lemma *) admit.
Admitted.
- rewrite Rabs_minus_sym in err2_bounded.
assert (Rabs nF2 - Rabs nR2 <= Q2R err2)%R.
+ eapply Rle_trans; [apply Rabs_triang_inv | auto].
+ assert (Rabs nF2 <= Rabs nR2 + Q2R err2)%R by lra.
(* TODO: Make this a lemma too. This looks lika a coprrectness lemma for IV arithmetic checker*)
assert (Rabs nR2 <= RmaxAbsFun (e2lo, e2hi))%R.
* pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p p_valid valid_iv_e2 e2_real).
unfold RmaxAbsFun.
rewrite absenv_e2 in H1; simpl in H1; destruct H1.
eapply RmaxAbs; auto.
* assert (Rabs nR2 + Q2R err2 <= RmaxAbsFun (e2lo, e2hi) + Q2R err2)%R by (apply Rplus_le_compat_r; auto).
eapply Rle_trans.
apply H0.
eapply Rle_trans.
apply H2.
apply Rle_abs.
Qed.
Lemma validErrorboundCorrect (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
......
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