AbsoluteError.v 3.45 KB
 Heiko Becker committed Jul 13, 2016 1 2 3 4 5 ``````(** Definition of the computation of the absolute error. used to verify analsysis result in the final theorem of a certificate. **) Require Import Coq.Reals.Reals. `````` Heiko Becker committed Aug 26, 2016 6 ``````Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealConstruction Daisy.Infra.RealSimps. `````` Heiko Becker committed Aug 15, 2016 7 ``````Require Import Daisy.IntervalArith Daisy.Expressions Daisy.Commands. `````` 8 `````` `````` Heiko Becker committed Aug 09, 2016 9 ``````Definition abs_env:Type := exp R -> interval -> err -> Prop. `````` Heiko Becker committed Jul 31, 2016 10 `````` `````` Heiko Becker committed Jul 13, 2016 11 ``````(** `````` 12 13 `````` First define when given an interval and an error, when another error is sound overapproximation of the absolute error **) `````` Heiko Becker committed Aug 17, 2016 14 ``````Definition isSoundErr (error:err) (iv:interval) (propagatedErr:err) := `````` Heiko Becker committed Aug 12, 2016 15 `````` (error >= machineEpsilon * Rmax (Rabs (IVlo iv)) (Rabs (IVhi iv)))%R. `````` Heiko Becker committed Jul 26, 2016 16 `````` `````` Heiko Becker committed Aug 17, 2016 17 ``````Definition maxAbs (IV:interval) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)). `````` Heiko Becker committed Jul 26, 2016 18 `````` `````` Heiko Becker committed Aug 03, 2016 19 ``````Definition mult_err (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) := `````` Heiko Becker committed Jul 29, 2016 20 `````` (maxAbs `````` 21 22 23 `````` (addInterval (addInterval (multInterval `````` Heiko Becker committed Jul 29, 2016 24 25 `````` (getIntv val_e1) (getErr val_e2, getErr val_e2)) `````` 26 `````` (multInterval `````` Heiko Becker committed Jul 29, 2016 27 28 `````` (getIntv val_e2) (getErr val_e1, getErr val_e1))) `````` 29 30 31 `````` (multInterval (multInterval (multInterval `````` Heiko Becker committed Jul 29, 2016 32 33 34 35 `````` (getIntv val_e1) (getIntv val_e2)) (getErr val_e1, getErr val_e1)) (getErr val_e2, getErr val_e1)))). `````` Heiko Becker committed Jul 26, 2016 36 `````` `````` Heiko Becker committed Aug 03, 2016 37 ``````Definition isSoundErrBin (op:binop) (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) (val:ann):= `````` Heiko Becker committed Jul 26, 2016 38 `````` match op with `````` Heiko Becker committed Jul 29, 2016 39 `````` Plus `````` Heiko Becker committed Aug 12, 2016 40 41 `````` => isSupersetInterval (getIntv val) (addInterval (getIntv val_e1) (getIntv val_e2)) /\ isSoundErr (getErr val) (getIntv val) (getErr val_e1 + getErr val_e2)%R `````` Heiko Becker committed Jul 29, 2016 42 `````` |Sub `````` Heiko Becker committed Sep 07, 2016 43 `````` => isSupersetInterval (getIntv val) (subtractInterval (getIntv val_e1) (getIntv val_e2)) /\ `````` Heiko Becker committed Aug 12, 2016 44 `````` isSoundErr (getErr val) (getIntv val) (getErr val_e1 - getErr val_e2)%R `````` Heiko Becker committed Jul 29, 2016 45 `````` |Mult `````` Heiko Becker committed Aug 12, 2016 46 47 `````` => isSupersetInterval (getIntv val) (multInterval (getIntv val_e1) (getIntv val_e2)) /\ isSoundErr (getErr val) (getIntv val) (mult_err e1 val_e1 e2 val_e2) `````` Heiko Becker committed Jul 29, 2016 48 `````` |Div `````` Heiko Becker committed Aug 12, 2016 49 `````` (** FIXME!! **) `````` 50 `````` => (isSupersetInterval (getIntv val) (intv_div_err (getIntv val_e1) (getErr val_e1) (getIntv val_e2) (getErr val_e2)) /\ `````` Heiko Becker committed Aug 03, 2016 51 `````` isSoundErr (getErr val) (getIntv val) (mult_err e1 val_e1 e2 (((/ IVlo (getIntv val_e2))%R, (/ IVhi (getIntv val_e2))%R), getErr val_e2))) `````` Heiko Becker committed Jul 29, 2016 52 ``````end. `````` 53 54 `````` Inductive AbsErrExp : exp R -> abs_env -> err -> Prop := `````` Heiko Becker committed Aug 09, 2016 55 `````` AbsErrConst n iv e (env:abs_env): `````` Heiko Becker committed Aug 05, 2016 56 `````` env (Const n) (iv) e -> `````` Heiko Becker committed Aug 10, 2016 57 `````` isSoundErr e iv machineEpsilon -> `````` Heiko Becker committed Aug 05, 2016 58 `````` AbsErrExp (Const n) env e `````` Heiko Becker committed Aug 09, 2016 59 ``````|AbsErrVar v iv e (env:abs_env): `````` Heiko Becker committed Aug 05, 2016 60 `````` env (Var R v) iv e -> `````` Heiko Becker committed Aug 10, 2016 61 `````` isSoundErr e iv machineEpsilon -> `````` Heiko Becker committed Aug 05, 2016 62 `````` AbsErrExp (Var R v) env e `````` Heiko Becker committed Aug 16, 2016 63 64 65 66 ``````|AbsErrParam v iv e (env:abs_env): env (Param R v) iv e -> isSoundErr e iv machineEpsilon -> AbsErrExp (Param R v) env e `````` Heiko Becker committed Aug 05, 2016 67 68 69 70 71 72 73 74 ``````|AbsErrBinop op e1 iv1 er1 e2 iv2 er2 iv eabs (env:abs_env): env e1 iv1 er1 -> env e2 iv2 er2 -> env (Binop op e1 e2) iv eabs -> AbsErrExp e1 env er1 -> AbsErrExp e2 env er2 -> isSoundErrBin op e1 (iv1,er1) e2 (iv2,er2) (iv,eabs) -> AbsErrExp (Binop op e1 e2) env eabs. `````` 75 `````` `````` Heiko Becker committed Jul 26, 2016 76 ``````Definition AbsErrBExp (c: bexp R) (err:intv*err) := True. `````` 77 78 `````` Inductive AbsErrPrg : cmd R -> abs_env -> err -> Prop := `````` Heiko Becker committed Aug 05, 2016 79 80 81 82 `````` AbsErrLet (x:nat) e s iv er (env:abs_env) err: env e iv er -> AbsErrExp e env er -> (env (Var R x) iv er) -> `````` 83 84 85 86 87 88 89 `````` AbsErrPrg s env err -> AbsErrPrg (Let R x e s) env err |AbsErrIte c s t env err: (* AbsErrBExp c (env c) -> *) AbsErrPrg s env err -> AbsErrPrg t env err -> AbsErrPrg (Ite R c s t) env err `````` Heiko Becker committed Aug 05, 2016 90 91 92 93 ``````|AbsErrRet e iv er (env:abs_env) : env e iv er -> AbsErrExp e env er -> AbsErrPrg (Ret R e) env er.``````