Commit 19760c41 authored by Heiko Becker's avatar Heiko Becker
Browse files

Improvements adn fix broken toy example

parent 903bfabb
......@@ -11,10 +11,10 @@ Definition abs_env:Type := exp R -> interval -> err -> Prop.
(**
First define when given an interval and an error, when another error is sound overapproximation of the absolute error
**)
Definition isSoundErr (error:err) (iv:intv) (propagatedErr:err) :=
Definition isSoundErr (error:err) (iv:interval) (propagatedErr:err) :=
(error >= machineEpsilon * Rmax (Rabs (IVlo iv)) (Rabs (IVhi iv)))%R.
Definition maxAbs (IV:intv) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)).
Definition maxAbs (IV:interval) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)).
Definition mult_err (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) :=
(maxAbs
......
......@@ -2,13 +2,20 @@ Require Import Coq.Reals.Reals.
(**
Some type abbreviations, to ease writing
**)
(**
Intervals are a type, consisting of a pair of two real numbers
Additionally add some constructing and destructing definitions for encapsulation and
define them to automatically unfold upon simplification.
**)
Definition interval:Type := R * R.
Definition intv:Type := R * R.
Definition err:Type := R.
Definition ann:Type := intv * err.
Definition IVlo (iv:intv) := fst iv.
Definition IVhi (iv:intv) := snd iv.
Definition ann:Type := interval * err.
Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
Definition IVlo (intv:interval) := fst intv.
Definition IVhi (intv:interval) := snd intv.
Arguments mkInterval _ _/.
Arguments IVlo _ /.
Arguments IVhi _ /.
......
......@@ -4,20 +4,6 @@
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions.
(**
Intervals are a type, consisting of a pair of two real numbers
Additionally add some constructing and destructing definitions for encapsulation and
define them to automatically unfold upon simplification.
**)
Definition interval:Type := R * R.
Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
Definition IVlo (intv:interval) := fst intv.
Definition IVhi (intv:interval) := snd intv.
Arguments mkInterval _ _/.
Arguments IVlo _ /.
Arguments IVhi _ /.
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
......@@ -28,7 +14,7 @@ Definition valid (intv:interval) :Prop :=
Definition contained (x:R) (intv:interval) :=
(IVlo intv <= x <= IVhi intv)%R.
Lemma containedImpliesValid (x:R) (intv:interval) :
Lemma contained_implies_valid (x:R) (intv:interval) :
contained x intv ->
valid intv.
Proof.
......@@ -43,7 +29,7 @@ Definition isSupersetInterval (iv1:interval) (iv2:interval) :=
Definition pointInterval (x:R) := mkInterval x x.
Lemma containedImpliesSubset (x:R) (intv:interval):
Lemma contained_implies_subset (x:R) (intv:interval):
contained x intv ->
isSupersetInterval (pointInterval x) intv.
Proof.
......@@ -146,13 +132,15 @@ Definition widenInterval (Iv:interval) (v:R) := mkInterval (IVlo Iv - v) (IVhi I
Definition negateInterval (intv:interval) := mkInterval (- IVhi intv) (- IVlo intv).
Lemma negationIsValid (intv:interval) (a:R) :
Lemma interval_negation_valid (intv:interval) (a:R) :
contained a intv-> contained (- a) (negateInterval intv).
Proof.
unfold contained; destruct intv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi].
split; apply Ropp_ge_le_contravar; apply Rle_ge; auto.
Qed.
Definition invertInterval (intv:interval) := mkInterval (/ IVhi intv) (/ IVlo intv).
Definition addInterval (iv1:interval) (iv2:interval) :=
absIntvUpd Rplus iv1 iv2.
......@@ -187,13 +175,13 @@ Proof.
intros contained_1 contained_I2.
rewrite Rsub_eq_Ropp_Rplus.
apply additionIsValid; auto.
apply negationIsValid; auto.
apply interval_negation_valid; auto.
Qed.
(*
FIXME: This needs to be beautified
*)
Definition interval_mult_err (I1:interval) (e1:err) (I2:intv) (e2:err) :=
Definition interval_mult_err (I1:interval) (e1:err) (I2:interval) (e2:err) :=
addInterval
(addInterval
(addInterval
......@@ -210,7 +198,7 @@ Definition multInterval (iv1:interval) (iv2:interval) :=
Prove is structurally the same as the proof done Jourdan et al. in Verasco, in FloatIntervalsForward.v
TODO: Credit
**)
Lemma multiplicationIsValid (I1:interval) (I2:interval) (a:R) (b:R) :
Lemma interval_multiplication_valid (I1:interval) (I2:interval) (a:R) (b:R) :
contained a I1 ->
contained b I2 ->
contained (a * b) (multInterval I1 I2).
......@@ -283,6 +271,18 @@ Proof.
rewrite Rmult_comm; auto.
Qed.
Definition divideInterval (I1:interval) (I2:interval) :=
multInterval I1 (mkInterval (/ (IVhi I2)) (/ (IVlo I2))).
(*
Corollary interval_divisision_valid (I1:interval) (I2:interval) :
validIntervalDiv I1 I2 (divideInterval I1 I2).
Proof.
unfold validIntervalDiv.
intros a b contained_a contained_b; unfold divideInterval.
apply interval_multiplication_valid; auto.
unfold contained in *; simpl.
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
Require Import Coq.Reals.Reals Interval.Interval_tactic Coq.micromega.Psatz.
Require Import Coq.Setoids.Setoid.
Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith Daisy.Expressions Daisy.Infra.RealConstruction.
Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith Daisy.Expressions Daisy.Infra.RealConstruction Daisy.Infra.Abbrevs.
(*
[ Info ]
......@@ -149,21 +149,18 @@ Proof.
- inversion eval_real as
[ | | | op e1 e2 v1 v2 delta delta_leq_0 eval_cst1 eval_param_u [op_eq e1_eq e2_eq] vR_eq];
subst.
rewrite perturb_0_val; auto.
rewrite perturb_0_val in eval_real; auto.
clear H2 delta.
inversion eval_cst1; subst.
rewrite perturb_0_val in eval_real; auto.
inversion eval_param_u; subst.
repeat rewrite perturb_0_val; auto.
rewrite perturb_0_val in eval_real , eval_param_u, eval_cst1; auto.
clear delta delta0 delta1 delta_leq_0 H0 H1.
inversion eval_float; subst.
inversion H4; subst.
inversion H5; subst.
rewrite (perturb_0_val _ delta0) in H4, eval_real; auto.
rewrite (perturb_0_val _ delta0); auto.
rewrite (perturb_0_val _ delta1) in H5, eval_real; auto.
rewrite (perturb_0_val _ delta1); auto.
clear H0 H1 delta0 delta1.
inversion H6; subst.
inversion H7; subst.
pose proof (const_abs_err_bounded H4 H6).
pose proof (param_abs_err_bounded H5 H7).
pose proof (const_abs_err_bounded eval_cst1 H4).
pose proof (param_abs_err_bounded eval_param_u H5).
unfold eval_binop.
unfold perturb in *; simpl in *.
rewrite Rabs_err_simpl in *.
......@@ -203,9 +200,9 @@ Proof.
}
* eapply Rplus_le_compat; [auto | apply Req_le; auto].
+ eapply Rplus_le_compat; [auto | apply Req_le; auto].
repeat rewrite Rabs_Ropp in H8; auto.
repeat rewrite Rabs_Ropp in H6; auto.
rewrite Rabs_Ropp; auto.
+ eapply Rle_trans. apply H8.
+ eapply Rle_trans. apply H6.
repeat rewrite Rplus_assoc.
eapply Rle_trans.
apply Rplus_le_compat. apply H.
......@@ -233,14 +230,13 @@ Proof.
destruct uContained, cst1Contained, containedAdd.
assert (Rabs cst1 = cst1) by (assert (0 <= cst1)%R by (unfold cst1; interval); rewrite Rabs_pos_eq; auto).
repeat rewrite Rabs_mult.
repeat rewrite H17.
repeat rewrite H15.
assert (Rabs (cenv u) <= Rmax (Rabs (-100)) (Rabs (100)))%R by (apply RmaxAbs; auto).
assert (Rabs (-100) = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
assert (Rabs 100 = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H19, H20 in H18.
rewrite Rmax_left in H18; [ | lra].
clear H19 H20.
assert (forall eps:R, 0 <= eps -> Rabs (cenv u) * eps <= 100 * eps)%R. by (intros; apply Rmult_le_compat_r; auto).
rewrite H17, H18 in H16.
rewrite Rmax_left in H16; [ | lra].
assert (forall eps:R, 0 <= eps -> Rabs (cenv u) * eps <= 100 * eps)%R by (intros; apply Rmult_le_compat_r; auto).
assert (cst1 * Rabs delta0 * Rabs delta <= cst1 * machineEpsilon * machineEpsilon)%R.
* assert (cst1 * Rabs delta0 <= cst1 * machineEpsilon)%R by (apply Rmult_le_compat_l; [unfold cst1, realFromNum, negativePower; interval | auto]).
repeat rewrite Rmult_assoc.
......@@ -274,7 +270,7 @@ Proof.
apply H20.
eapply Rplus_le_compat.
eapply Rmult_le_compat; try auto using Rabs_pos.
apply H18.
apply H16.
apply H2.
apply H22.
unfold cst1, errAddUCst, machineEpsilon; prove_constant.
......
(*
Some type abbreviations, to ease writing.
Additionally define getter functions to make stuff more portable if we change the infrastructure later.
*)
new_type_abbrev ("interval", `:real#real`);;
new_type_abbrev ("err", `:real`);;
new_type_abbrev ("ann", `:intverval#err`);;
let mkInterval = define `mkInterval (a:real) (b:real) = (a,b)`;;
let IVhi = define `IVhi (iv:interval) = SND (iv)`;;
let IVlo = define `IVlo (iv:interval) = FST (iv)`;;
let getErr = define `getErr (val:ann) = SND (val)`;;
let getIntv = define `getIntv (val:ann) = FST (val)`;;
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