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

Draft lemma on variables

parent 9259e089
......@@ -147,6 +147,15 @@ Proof.
+ rewrite H2; auto.
Lemma var_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R) (nlo:R) (nhi:R):
(nlo <= cenv n <= nhi)%R ->
eval_exp 0%R cenv (Var R n) nR ->
eval_exp machineEpsilon cenv (Var R n) nF ->
(Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
intros [lo_le_env env_le_hi] eval_real eval_float.
inversion eval_real; subst.
rewrite perturb_0_val.
Using the parametric expressions, define boolean expressions for conditionals
Supports Markdown
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