Add lemma about parameters, fix flaw that parameters had no error bound

coq/Expressions.v

 (**
 Formalization of the base expression language for the daisy framework
  **)
-Require Import Coq.Reals.Reals Interval.Interval_tactic.
+Require Import Coq.Reals.Reals.
 Require Import Daisy.Infra.RealConstruction.
 Set Implicit Arguments.
 (**
@@ -20,20 +20,23 @@ Fixpoint eval_binop (o:binop) (v1:R) (v2:R) :=
   | Mult => Rmult v1 v2
   | Div => Rdiv v1 v2
   end.
-(*
+(**
   Define expressions parametric over some value type V.
   Will ease reasoning about different instantiations later.
-*)
+  Note that we differentiate between wether we use a variable from the environment or a parameter.
+  Parameters do not have error bounds in the invariants, so they must be perturbed, but variables from the
+  program will be perturbed upon binding, so we do not need to perturb them.
+**)
 Inductive exp (V:Type): Type :=
   Var: nat -> exp V
+| Param: nat -> exp V
 | Const: V -> exp V
 | Binop: binop -> exp V -> exp V -> exp V.
 (**
   Define the machine epsilon for floating point operations.
-  FIXME: Currently set to 1.0 instead of the concrete value!
+  Current value: 2^(-53)
  **)
 Definition machineEpsilon:R := realFromNum 1 1 53.
-(* Definition machineEpsilon:R := realFromNum 11102230246251565 16 16. *)
 (**
   Define a perturbation function to ease writing of basic definitions
 **)
@@ -50,6 +53,7 @@ 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)
 | Const_dist n delta:
     Rle (Rabs delta) eps ->
     eval_exp eps env (Const n) (perturb n delta)
@@ -77,24 +81,6 @@ Proof.
   apply Rsqr_0_uniq in Rabs_eq; assumption.
 Qed.
 
-Lemma eval_det (e:exp R) (env:env_ty):
-  forall v1 v2,
-  eval_exp R0 env e v1 ->
-  eval_exp R0 env e v2 ->
-  v1 = v2.
-Proof.
-  induction e; intros v1 v2 eval_v1 eval_v2; inversion eval_v1; inversion eval_v2; try auto.
-  - apply Rabs_0_impl_eq in H0;
-      apply Rabs_0_impl_eq in H3.
-    rewrite H0, H3; reflexivity.
-  - apply Rabs_0_impl_eq in H2;
-      apply Rabs_0_impl_eq in H9.
-    rewrite H2, H9.
-    subst.
-    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.
@@ -107,17 +93,34 @@ Proof.
   rewrite Rplus_0_r; auto.
 Qed.
 
+Lemma eval_det (e:exp R) (env:env_ty):
+  forall v1 v2,
+  eval_exp R0 env e v1 ->
+  eval_exp R0 env e v2 ->
+  v1 = v2.
+Proof.
+  induction e; intros v1 v2 eval_v1 eval_v2;
+    inversion eval_v1; inversion eval_v2; [ auto | | | ];
+      repeat try rewrite perturb_0_val; auto.
+  subst.
+  rewrite (IHe1 v0 v4); auto.
+  rewrite (IHe2 v3 v5); auto.
+Qed.
+
 Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) :
   (a - b = a + (- b))%R.
 Proof.
   field_simplify; reflexivity.
 Qed.
 
+(**
+  TODO: Check wether we need Rabs (n * machineEpsilon) instead
+**)
 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.
+  (Rabs (nR - nF) <= Rabs n * machineEpsilon)%R.
 Proof.
   intros cenv eval_real eval_float.
   inversion eval_real; subst.
@@ -134,29 +137,35 @@ Proof.
   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, negativePower.
-      unfold Rabs.
-      destruct Rcase_abs; auto.
-      exfalso.
-      apply (Rlt_not_ge _ _ r).
-      interval.
-    + rewrite H2; auto.
+  apply Rmult_le_compat_l; [apply Rabs_pos | auto].
 Qed.
 
+(**
+  TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
+  (nlo <= cenv n <= nhi)%R ->   (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
+**)
 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.
+  eval_exp 0%R cenv (Param R n) nR ->
+  eval_exp machineEpsilon cenv (Param R n) nF ->
+  (Rabs (nR - nF) <= Rabs (cenv n) * machineEpsilon)%R.
 Proof.
-  intros [lo_le_env env_le_hi] eval_real eval_float.
+  intros eval_real eval_float.
   inversion eval_real; subst.
-  (* rewrite perturb_0_val. *)
-Admitted.
+  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 (- cenv n + - (cenv n * delta0) = - (cenv n * delta0) + - cenv 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 | auto].
+Qed.
 
 (**
   Using the parametric expressions, define boolean expressions for conditionals