Commit 868479ee authored by Heiko Becker's avatar Heiko Becker
Browse files

Add draft state of checker

parent c8a22163
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.ZArith.ZArith Coq.Reals.Reals Coq.QArith.Qreals.
(*Coq.QArith.Qcanon.*)
Require Import Coq.micromega.Psatz.
Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps Daisy.IntervalArith.
Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps Daisy.IntervalArith Daisy.ErrorBounds Daisy.Infra.Abbrevs.
Section ComputableErrors.
......@@ -82,13 +82,17 @@ Section ComputableErrors.
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let e1F := upperBoundE1 + (upperBoundE1 * machineEpsilon) in
let e2F := upperBoundE2 + (upperBoundE2 * machineEpsilon) in
(* WAS:
let e1F := upperBoundE1 + (upperBoundE1 * err1) in
let e2F := upperBoundE2 + (upperBoundE2 * err2) in *)
let e1F := upperBoundE1 + err1 in
let e2F := upperBoundE2 + err2 in
let theVal :=
match b with
| Plus => Qleb (err1 + err2 + (Qabs (e1F + e2F) * machineEpsilon)) err
| Sub => false
| Mult => false
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * machineEpsilon) err
(* TODO:Validity of next two computations *)
| Sub => Qleb (err1 + err2 + (Qabs (e1F - e2F) * machineEpsilon)) err
| Mult => Qleb ((upperBoundE1 * upperBoundE2) + (e1F * e2F) + (e1F * e2F * err1) + (e1F * e2F * err2) + (e1F * e2F * err1 * err2) + (((e1F * e2F) + (e1F * e2F * err1) + (e1F * e2F * err2) + (e1F * e2F * err1 * err2))*machineEpsilon)) err
| Div => false
end
in andb rec theVal
......@@ -290,14 +294,88 @@ Section ComputableErrors.
apply error_valid.
Qed.
Fixpoint toRExp (e:exp Q) :=
match e with
|Var v => Var R v
|Param v => Param R v
|Const n => Const (Q2R n)
|Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
end.
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) :
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 1 nF1 (updEnv 2 nF2 cenv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Plus e1 e2) absenv = 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 absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
eapply Rle_trans.
eapply add_abs_err_bounded.
apply e1_real.
admit.
apply e2_real.
admit.
(* TODO: Fix machine epsilons *)
apply eval_real.
admit.
apply err1_bounded.
apply err2_bounded.
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 Q2R_mult in valid_error.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite Q2R_mult in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans.
apply Rplus_le_compat_l.
eapply Rmult_le_compat. (* FIXME: Make compat_r when machineEpsilons are fixed *)
apply Rabs_pos.
admit.
Focus 3.
apply valid_error.
Focus 2.
admit.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat.
rewrite Q2R_mult in error_valid.
apply error_valid.
apply
instantiate (1 := Q2R err1).
instantiate (2 := nF1).
inversion eval_real; subst.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
unfold eval_binop; simpl.
Lemma validErrorboundCorrect:
forall cenv (n:Q),
eval_exp 0%R cenv (Const n%R) nR ->
eval_exp machineEpsilon%R cenv (Const n%R) ->
validErrorbound (Const n) (fun x => ( (n,n),n * machineEpsilon)) = true
Eval compute in validErrorbound (Var Q 1) (fun x => ((1567#5,1567#5),(2^53#1))).
Eval compute in validErrorbound (Const (1567#5)) (fun x => ((1567#5,1567#5),(2^53#1))).
End ComputableErrors.
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