Commit e892d8de authored by Heiko Becker's avatar Heiko Becker
Browse files

Add type abbrev for environments

parent 6144c6f9
......@@ -37,12 +37,16 @@ Definition m_eps:R := 1.
**)
Definition perturb (r:R) (e:R) :=
Rmult r (Rplus 1 e).
(**
Abbreviation for the type of an environment
**)
Definition env_ty := nat -> R.
(**
Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation
of the real valued computation by (1 + d)
**)
Inductive eval_exp (eps:R) (env:nat -> R) : (exp R) -> R -> Prop :=
Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps env (Var R x) (env x)
| Const_dist n delta:
Rle (Rabs delta) eps ->
......@@ -55,7 +59,7 @@ Inductive eval_exp (eps:R) (env:nat -> R) : (exp R) -> R -> Prop :=
(**
Define real evaluation as stated above:
**)
Definition is_real_value (e:exp R) (env:nat -> R) (v:R) := eval_exp R0 env e v.
Definition is_real_value (e:exp R) (env:env_ty) (v:R) := eval_exp R0 env e v.
(**
Prove that using eps = 0 makes the evaluation deterministic
**)
......@@ -71,7 +75,7 @@ Proof.
apply Rsqr_0_uniq in Rabs_eq; assumption.
Qed.
Lemma eval_det (e:exp R) (env:nat -> R):
Lemma eval_det (e:exp R) (env:env_ty):
forall v1 v2,
eval_exp R0 env e v1 ->
eval_exp R0 env e v2 ->
......@@ -97,7 +101,7 @@ Inductive bexp (V:Type) : Type :=
(**
Define evaluation of booleans for reals
**)
Inductive bval (eps:R) (env:nat -> R) : (bexp R) -> Prop -> Prop :=
Inductive bval (eps:R) (env:env_ty) : (bexp R) -> Prop -> Prop :=
leq_eval (e1:exp R) (e2:exp R) (v1:R) (v2:R):
eval_exp eps env e1 v1 ->
eval_exp eps env e2 v2 ->
......
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