general lemma about constants

coq/exps.v

 (**
 Formalization of the base expression language for the daisy framework
  **)
-Require Import Coq.Reals.Reals.
+Require Import Coq.Reals.Reals Interval.Interval_tactic.
 Require Import Daisy.realConversion.
 Set Implicit Arguments.
 (**
@@ -94,6 +94,59 @@ Proof.
     rewrite (IHe1 v0 v4); auto.
     rewrite (IHe2 v3 v5); auto.
 Qed.
+
+Lemma perturb_0_val (v:R) (delta:R):
+  (Rabs delta <= 0)%R ->
+  perturb v delta = v.
+Proof.
+  intros abs_0; apply Rabs_0_impl_eq in abs_0; subst.
+  unfold perturb.
+  rewrite Rmult_plus_distr_l.
+  rewrite Rmult_0_r.
+  rewrite Rmult_1_r.
+  rewrite Rplus_0_r; auto.
+Qed.
+
+Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) :
+  (a - b = a + (- b))%R.
+Proof.
+  field_simplify; reflexivity.
+Qed.
+
+Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
+  forall cenv:nat -> R,
+  eval_exp 0%R cenv (Const n) nR ->
+  eval_exp machineEpsilon cenv (Const n) nF ->
+  (Rabs (nR - nF) <= Rabs (n * machineEpsilon))%R.
+Proof.
+  intros cenv eval_real eval_float.
+  inversion eval_real; subst.
+  rewrite perturb_0_val; auto.
+  inversion eval_float; subst.
+  unfold perturb; simpl.
+  rewrite Rmult_plus_distr_l.
+  rewrite Rmult_1_r.
+  rewrite Rsub_eq_Ropp_Rplus.
+  rewrite Ropp_plus_distr.
+  assert (-n + (- (n * delta0)) = ( -(n * delta0) + - n))%R by (rewrite Rplus_comm; auto).
+  rewrite H.
+  rewrite <- Rsub_eq_Ropp_Rplus.
+  rewrite Rplus_minus.
+  rewrite Rabs_Ropp.
+  repeat rewrite Rabs_mult.
+  apply Rmult_le_compat_l.
+  - apply Rabs_pos.
+  - assert (Rabs machineEpsilon = machineEpsilon).
+    + unfold machineEpsilon.
+      unfold realFromNum, negPow.
+      unfold Rabs.
+      destruct Rcase_abs; auto.
+      exfalso.
+      apply (Rlt_not_ge _ _ r).
+      interval.
+    + rewrite H2; auto.
+Qed.
+
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)