Commit d3c80dca authored by Heiko Becker's avatar Heiko Becker

Fix dependencies

parent 953cceba
......@@ -3,7 +3,7 @@ Proofs of general bounds on the error of arithmetic expressions.
This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Expressions.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
......
......@@ -14,8 +14,8 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (intv, err) := (env e) in
let errPos := Qleb 0 err in
match e with
|Var v => false
|Param v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Var _ v => false
|Param _ v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
......@@ -996,36 +996,36 @@ Proof.
lra.
}
- 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.
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.
(**
......@@ -1102,7 +1102,7 @@ Proof.
apply andb_prop_intro; split; try auto.
{ apply andb_prop_intro.
split; apply Is_true_eq_left; auto. }
* apply Is_true_eq_left; auto.
{ apply Is_true_eq_left; auto. }
+ eapply (validErrorboundCorrectSubtraction cenv absenv e1 e2); eauto.
simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
......
......@@ -8,8 +8,8 @@ Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions D
Fixpoint toRExp (e:exp Q) :=
match e with
|Var v => Var R v
|Param v => Param R v
|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.
......
......@@ -11,16 +11,16 @@ Import Lists.List.ListNotations.
Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
match e with
|Const n => []
|Var v => []
|Param v => [v]
|Var _ v => []
|Param _ v => [v]
|Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
end.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
let (intv, _) := absenv e in
match e with
| Var v => false
| Param v =>
| Var _ v => false
| Param _ v =>
isSupersetIntv (P v) intv
| Const n =>
isSupersetIntv (n,n) intv
......
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