Commit 8f121ce2 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add draft of error computing function

parent 69f42541
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.ZArith.ZArith Coq.Reals.Reals.
Require Import Daisy.Expressions.
Section ComputableErrors.
Definition test (frac:Q) :=
match frac with
|a#b => (a+1)#(b-1)
Definition interval :Type := Q * Q.
Definition error :Type := Q.
Definition analysisResult :Type := exp Q -> interval * error.
Definition Qleb :=Qle_bool.
Definition maxAbs (iv:interval) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Definition machineEpsilon := (1#(2^53)).
Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
match e with
|Var v => false
|Param v => false
(* A constant will be a point interval. Take maxAbs never the less *)
|Const n => let (intv,err) := env (Const n) in
Qleb (maxAbs intv * machineEpsilon) err
|Binop b e1 e2 =>
let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in
match b with
Plus => false
|Sub => false
|Mult => false
|Div => false
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