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

Move around some definitions for dependency cleanup and prove small lemma to...

Move around some definitions for dependency cleanup and prove small lemma to simplify bound proofs in ErrorValidation.v
parent 7ddb9f2d
......@@ -6,34 +6,6 @@ Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.ErrorBoun
Section ComputableErrors.
Definition machineEpsilon := (1#(2^53)).
Lemma mEps_eq_Rmeps:
Q2R machineEpsilon = RealSimps.machineEpsilon.
Proof.
unfold Q2R, machineEpsilon, RealSimps.machineEpsilon.
unfold RealConstruction.realFromNum, RealConstruction.negativePower.
unfold Qden.
assert (/ (IZR (' (2 ^ 53))) = 1 / (2^53))%R.
- assert (2^53 = ' (2^53))%Z by auto.
assert ( 1 / (2^53) = / 2^53)%R by lra.
rewrite H0.
f_equal. unfold IZR. rewrite <- Fcore_Raux.P2R_INR.
unfold Fcore_Raux.P2R. simpl; lra.
- rewrite H.
f_equal. simpl; lra.
Qed.
Lemma mEps_geq_zero:
(0 <= Q2R machineEpsilon)%R.
Proof.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
unfold machineEpsilon.
apply Qle_bool_iff.
unfold Qle_bool; auto.
Qed.
(*
Multiplication :
let eterm := (Rabs (e1R * err2) + Rabs(e2R * err1) + Rabs (err1 * err2) +
......@@ -51,9 +23,9 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
let (intv, err) := (env e) in
match e with
|Var v => false
|Param v => Qleb (maxAbs intv * machineEpsilon) err
|Param v => Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
(* A constant will be a point intv. Take maxAbs never the less *)
|Const n => Qleb (maxAbs intv * machineEpsilon) err
|Const n => Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
let (ive2, err2) := env e2 in
......@@ -67,10 +39,10 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
let e2F := upperBoundE2 + err2 in
let theVal :=
match b with
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * machineEpsilon) err
| Plus => Qleb (err1 + err2 + (Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon) err
(* TODO:Validity of next two computations *)
| Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * machineEpsilon)) err
| Mult => Qleb (Qabs (upperBoundE1 * upperBoundE2 - (e1F * e2F)) + Qabs(e1F * e2F) * machineEpsilon) err
| Sub => Qleb (err1 + err2 + ((Qabs e1F + Qabs e2F) * RationalSimps.machineEpsilon)) err
| Mult => Qleb (Qabs (upperBoundE1 * upperBoundE2 - (e1F * e2F)) + Qabs(e1F * e2F) * RationalSimps.machineEpsilon) err
| Div => false
end
in andb rec theVal
......@@ -82,7 +54,7 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
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 machineEpsilon) cenv (Const (Q2R n)) nF ->
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) ->
......@@ -130,7 +102,7 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
envApproximatesPrecond P absenv ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (Param R v) nR ->
eval_exp (Q2R machineEpsilon) cenv (Param R v) nF ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (Param R v) nF ->
validErrorbound (Param Q v) absenv = true ->
validIntervalbounds (Param Q v) absenv P = true ->
absenv (Param Q v) = ((plo,phi),e) ->
......@@ -181,9 +153,9 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
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 ->
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) ->
......@@ -241,39 +213,12 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat.
(* TODO: MAke this a lemma *)
rewrite Rabs_minus_sym in err1_bounded.
assert (Rabs nF1 - Rabs nR1 <= Q2R err1)%R.
- eapply Rle_trans; [apply Rabs_triang_inv | auto].
- 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.
+ 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.
- 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.
- pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p 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_correct _ _ _ _ _ env_approx_p 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 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 :
......@@ -282,9 +227,9 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
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 ->
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) ->
......@@ -316,7 +261,6 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
apply andb_prop_elim in valid_error.
destruct valid_error as [valid_rec valid_error].
apply andb_prop_elim in valid_rec.
(** FIXME: Remove if trouble ahead *)
clear valid_rec.
apply Is_true_eq_true in valid_error.
apply Qle_bool_iff in valid_error.
......@@ -342,50 +286,24 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
Focus 2.
apply valid_error.
eapply Rplus_le_compat.
(* TODO: MAke this a lemma *)
rewrite Rabs_minus_sym in err1_bounded.
assert (Rabs nF1 - Rabs nR1 <= Q2R err1)%R.
- eapply Rle_trans; [apply Rabs_triang_inv | auto].
- 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.
+ 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.
- 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.
- pose proof (validIntervalbounds_correct _ _ _ _ _ env_approx_p 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_correct _ _ _ _ _ env_approx_p 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 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 :
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 Mult 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 Mult (Var Q 1) (Var Q 2))) nF ->
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 Mult (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Mult e1 e2) absenv = true ->
validIntervalbounds (Binop Mult e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
......@@ -521,7 +439,7 @@ Qabs (upperBoundE1 * err2) + Qabs(upperBoundE2 * err1) + Qabs (err1 * err2) +
envApproximatesPrecond P absenv ->
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) nR ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e) nF ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e) nF ->
validErrorbound e absenv = true ->
validIntervalbounds e absenv P = true ->
absenv e = ((elo,ehi),err) ->
......
......@@ -3,6 +3,9 @@ Require Import Daisy.Infra.Abbrevs.
Definition Qleb :=Qle_bool.
Definition Qeqb := Qeq_bool.
Definition machineEpsilon := (1#(2^53)).
(*
Definition Qc2Q (q:Qc) :Q := match q with
Qcmake a P => a end.
......
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
Fixpoint toRExp (e:exp Q) :=
match e with
......@@ -10,9 +10,6 @@ Fixpoint toRExp (e:exp Q) :=
|Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
end.
Definition RmaxAbsFun (iv:intv) :=
Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
Lemma Q2R0_is_0:
Q2R 0 = 0%R.
Proof.
......@@ -140,4 +137,30 @@ Proof.
- intros less. apply Qle_Rle in less.
assert (Rmin (Q2R a) (Q2R b) = Q2R b) by (apply Rmin_right; auto).
rewrite H; auto.
Qed.
Lemma mEps_eq_Rmeps:
Q2R machineEpsilon = RealSimps.machineEpsilon.
Proof.
unfold Q2R, machineEpsilon, RealSimps.machineEpsilon.
unfold RealConstruction.realFromNum, RealConstruction.negativePower.
unfold Qden.
assert (/ (IZR (' (2 ^ 53))) = 1 / (2^53))%R.
- assert (2^53 = ' (2^53))%Z by auto.
assert ( 1 / (2^53) = / 2^53)%R by lra.
rewrite H0.
f_equal. unfold IZR. rewrite <- Fcore_Raux.P2R_INR.
unfold Fcore_Raux.P2R. simpl; lra.
- rewrite H.
f_equal. simpl; lra.
Qed.
Lemma mEps_geq_zero:
(0 <= Q2R machineEpsilon)%R.
Proof.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
unfold machineEpsilon.
apply Qle_bool_iff.
unfold Qle_bool; auto.
Qed.
\ No newline at end of file
......@@ -2,7 +2,7 @@
Formalization of real valued interval arithmetic
TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
......@@ -285,4 +285,34 @@ Proof.
split. *)
Definition intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err) :=
interval_mult_err I1 e1 ( (/ IVlo (I2))%R, (/ IVhi (I2))%R) e2.
\ No newline at end of file
interval_mult_err I1 e1 ( (/ IVlo (I2))%R, (/ IVhi (I2))%R) e2.
Definition RmaxAbsFun (iv:intv) :=
Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
Lemma contained_leq_maxAbs a ivlo ivhi:
contained a (Q2R ivlo, Q2R ivhi) ->
(Rabs a <= RmaxAbsFun (ivlo, ivhi))%R.
Proof.
intros contained_a.
unfold RmaxAbsFun.
unfold contained in contained_a; simpl in contained_a; destruct contained_a.
eapply RmaxAbs; auto.
Qed.
Lemma Rabs_error_bounded_maxAbs a b eps ivlo ivhi:
(Rabs (a - b) <= eps)%R ->
contained a (Q2R ivlo, Q2R ivhi) ->
(Rabs b <= Rabs (RmaxAbsFun (ivlo, ivhi) + eps))%R.
Proof.
intros Rabs_le_eps contained_a.
pose proof (contained_leq_maxAbs _ _ _ contained_a).
rewrite Rabs_minus_sym in Rabs_le_eps.
assert (Rabs b - Rabs a <= eps)%R.
- eapply Rle_trans; [apply Rabs_triang_inv | auto].
- assert (Rabs b <= Rabs a + eps)%R by lra.
assert (Rabs a + eps <= RmaxAbsFun (ivlo, ivhi) + eps)%R by (apply Rplus_le_compat_r; auto).
eapply Rle_trans; eauto.
eapply Rle_trans; eauto.
apply Rle_abs.
Qed.
\ No newline at end of file
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