Commit 372a1de9 authored by Heiko Becker's avatar Heiko Becker

Simplify Coq proof

parent 4864dbb0
......@@ -53,7 +53,9 @@ Definition env_ty := nat -> R.
**)
Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps env (Var R x) (env x)
| Param_acc x delta: ((Rabs delta) <= eps)%R -> eval_exp eps env (Param R x) (perturb (env x) delta)
| Param_acc x delta:
((Rabs delta) <= eps)%R ->
eval_exp eps env (Param R x) (perturb (env x) delta)
| Const_dist n delta:
Rle (Rabs delta) eps ->
eval_exp eps env (Const n) (perturb n delta)
......@@ -62,10 +64,6 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
eval_exp eps env e1 v1 ->
eval_exp eps env e2 v2 ->
eval_exp eps env (Binop op e1 e2) (perturb (eval_binop op v1 v2) delta).
(**
Define real evaluation as stated above:
**)
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
**)
......@@ -144,7 +142,7 @@ Proof.
inversion eval_float; subst.
unfold perturb; simpl.
rewrite Rabs_err_simpl.
repeat rewrite Rabs_mult.
rewrite Rabs_mult.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
......
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