Commit 349fbc0f authored by Heiko Becker's avatar Heiko Becker
Browse files

SimpleDoppler test working by hand

parent 706c08f3
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.ErrorBounds
Daisy.Infra.RealConstruction Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
Require Import Coq.QArith.QArith.
Require Import Daisy.ErrorValidation Daisy.Infra.RationalConstruction Daisy.Infra.ExpressionAbbrevs.
(*
TODO: update according to:
[ Info ]
......@@ -24,31 +21,9 @@ TODO: update according to:
[ Info ] Finished info phase
[ Info ] time:
[ Info ] info: 7 ms, rangeError: 67 ms, analysis: 11 ms, frontend: 2171 ms,
[ Info ]
[ Info ] Starting specs preprocessing phase
[ Info ] Finished specs preprocessing phase
[ Info ]
[ Info ]
[ Info ] Starting range-error phase
[ Info ] Machine epsilon 1.1102230246251565E-16
[ Info ] 331.4: [331.4, 331.4],7.358558207215537e-14
[ Info ] u: [-100.0, 100.0],2.220446049250313e-14
[ Info ] (331.4 + u): [231.4, 431.4],1.9158008512931703e-13
[ Info ] Finished range-error phase
[ Info ]
[ Info ] Starting info phase
[ Info ] doppler
[ Info ] abs-error: 1.9158008512931703e-13, range: [231.4, 431.4],
[ Info ] rel-error: 8.279173946815775E-16
[ Info ] Finished info phase
[ Info ] time:
[ Info ] info: 9 ms, rangeError: 149 ms, analysis: 15 ms, frontend: 2709 ms,
*)
(** TODO MOVE TO FILE
Ltac prove_constant := unfold realFromNum, negativePower; interval.
Ltac rw_asm H Lem := rewrite Lem; rewrite Lem in H.
......@@ -79,23 +54,35 @@ Proof.
rewrite <- Rsub_eq_Ropp_Rplus.
rewrite Rplus_minus; auto.
Qed.
**)
Definition u:nat := 1.
(** 1655/5 = 331; 0,4 = 2/5 **)
Definition cst1:R := 1657 / 5.
Definition cst1:Q := 1657 # 5.
(** Define abbreviations **)
Definition varU:exp R := Param R u.
Definition valCst:exp R := Const cst1.
Definition valCstAddVarU:exp R := Binop Plus valCst varU.
Definition varU:exp Q := Param Q u.
Definition valCst:exp Q := Const cst1.
Definition valCstAddVarU:exp Q := Binop Plus valCst varU.
(** Error values **)
Definition errCst1 := realFromNum 7358558207215537 15 14.
Definition errVaru := realFromNum 2220446049250313 15 14.
Definition lowerBoundAddUCst:R := 1157 / 5.
Definition upperBoundAddUCst:R := 2157 / 5.
Definition errAddUCst := realFromNum 19158008512931703 16 13.
Definition errCst1 := rationalFromNum (36792791036077685#1) 16 14.
Definition errVaru := rationalFromNum (11102230246251565#1) 16 14.
Definition lowerBoundAddUCst:Q := 1157 # 5.
Definition upperBoundAddUCst:Q := 2157 # 5.
Definition errAddUCst := rationalFromNum (9579004256465851#1) 15 14.
Definition absEnv : analysisResult :=
fun (e:exp Q) =>
match e with
|Const n => (cst1,cst1,errCst1)
|Param v => (-(100#1),(100#1),errVaru)
|Binop _ _ _ => (lowerBoundAddUCst,upperBoundAddUCst,errAddUCst)
| _ => (0,0,0) end.
Eval compute in validErrorbound valCstAddVarU absEnv.
(* UNUSED STUFF BEGINS HERE
(** The added assertion becomes the precondition for us **)
Definition precondition := fun env:nat -> R => (- 100 <= env u)%R /\ (env u <= 100)%R.
......@@ -393,4 +380,5 @@ Qed.
apply H22.
unfold cst1, errAddUCst, machineEpsilon; prove_constant.
}
Qed. *)
\ No newline at end of file
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