Environments.v 1.53 KB
Newer Older
1
2
3
4
(**
Environment library.
Defines the environment type for the Daisy framework and a simulation relation between environments.
 **)
5
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
6
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RationalSimps Daisy.Commands.
7
8
9
10
11
12
13
14

(**
Define an approximation relation between two environments.
We use this relation for the soundness proofs.
It is necessary to have this relation, since two evaluations of the very same
expression may yield different values for different machine epsilons
(or environments that already only approximate each other)
 **)
15
16
17
Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
|approxRefl A:
   approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
18
|approxUpdFree E1 E2 A v1 v2 x fVars dVars m:
19
   approxEnv E1 A fVars dVars E2 ->
20
   (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R ->
21
   NatSet.mem x (NatSet.union fVars dVars) = false ->
22
   approxEnv (updEnv x M0 v1 E1) A (NatSet.add x fVars) dVars (updEnv x m v2 E2)
23
|approxUpdBound E1 E2 A v1 v2 x fVars dVars m:
24
   approxEnv E1 A fVars dVars E2 ->
25
   (Rabs (v1 - v2) <= Q2R (snd (A (Var Q m x))))%R ->
26
   NatSet.mem x (NatSet.union fVars dVars) = false ->
27
   approxEnv (updEnv x M0 v1 E1) A fVars (NatSet.add x dVars) (updEnv x m v2 E2).
28

29
30
31
32
33
34
Inductive approxParams :env -> env -> Prop :=
|approxParamRefl:
   approxParams emptyEnv emptyEnv
|approxParamUpd E1 E2 m x v1 v2 :
   approxParams E1 E2 ->
   (Rabs (v1 - v2) <= Q2R (meps m))%R ->
35
   approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2).