Add documentation to Expressions.v, rename some lemmas

coq/ErrorBounds.v

@@ -14,7 +14,7 @@ Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
 Proof.
   intros cenv eval_real eval_float.
   inversion eval_real; subst.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic; auto.
   inversion eval_float; subst.
   unfold perturb; simpl.
   rewrite Rabs_err_simpl.
@@ -29,7 +29,7 @@ Lemma param_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R):
 Proof.
   intros eval_real eval_float.
   inversion eval_real; subst.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic; auto.
   inversion eval_float; subst.
   unfold perturb; simpl.
   rewrite Rabs_err_simpl.
@@ -51,14 +51,14 @@ Proof.
   intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion plus_real; subst.
-  rewrite perturb_0_val in plus_real; auto.
-  rewrite (perturb_0_val (eval_binop Plus v1 v2) delta); auto.
+  rewrite delta_0_deterministic in plus_real; auto.
+  rewrite (delta_0_deterministic (eval_binop Plus v1 v2) delta); auto.
   unfold eval_binop in *; simpl in *.
   clear delta H2.
-  rewrite (eval_0_det H4 e1_real);
-    rewrite (eval_0_det H5 e2_real).
-  rewrite (eval_0_det H4 e1_real) in plus_real.
-  rewrite (eval_0_det H5 e2_real) in plus_real.
+  rewrite (meps_0_deterministic H4 e1_real);
+    rewrite (meps_0_deterministic H5 e2_real).
+  rewrite (meps_0_deterministic H4 e1_real) in plus_real.
+  rewrite (meps_0_deterministic H5 e2_real) in plus_real.
   clear H4 H5 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion plus_float; subst.
@@ -110,14 +110,14 @@ Proof.
   intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion sub_real; subst.
-  rewrite perturb_0_val in sub_real; auto.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic in sub_real; auto.
+  rewrite delta_0_deterministic; auto.
   unfold eval_binop in *; simpl in *.
   clear delta H2.
-  rewrite (eval_0_det H4 e1_real);
-    rewrite (eval_0_det H5 e2_real).
-  rewrite (eval_0_det H4 e1_real) in sub_real.
-  rewrite (eval_0_det H5 e2_real) in sub_real.
+  rewrite (meps_0_deterministic H4 e1_real);
+    rewrite (meps_0_deterministic H5 e2_real).
+  rewrite (meps_0_deterministic H4 e1_real) in sub_real.
+  rewrite (meps_0_deterministic H5 e2_real) in sub_real.
   clear H4 H5 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion sub_float; subst.
@@ -160,14 +160,14 @@ Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion mult_real; subst.
-  rewrite perturb_0_val in mult_real; auto.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic in mult_real; auto.
+  rewrite delta_0_deterministic; auto.
   unfold eval_binop in *; simpl in *.
   clear delta H2.
-  rewrite (eval_0_det H4 e1_real);
-    rewrite (eval_0_det H5 e2_real).
-  rewrite (eval_0_det H4 e1_real) in mult_real.
-  rewrite (eval_0_det H5 e2_real) in mult_real.
+  rewrite (meps_0_deterministic H4 e1_real);
+    rewrite (meps_0_deterministic H5 e2_real).
+  rewrite (meps_0_deterministic H4 e1_real) in mult_real.
+  rewrite (meps_0_deterministic H5 e2_real) in mult_real.
   clear H4 H5 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion mult_float; subst.
@@ -204,14 +204,14 @@ Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion div_real; subst.
-  rewrite perturb_0_val in div_real; auto.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic in div_real; auto.
+  rewrite delta_0_deterministic; auto.
   unfold eval_binop in *; simpl in *.
   clear delta H2.
-  rewrite (eval_0_det H4 e1_real);
-    rewrite (eval_0_det H5 e2_real).
-  rewrite (eval_0_det H4 e1_real) in div_real.
-  rewrite (eval_0_det H5 e2_real) in div_real.
+  rewrite (meps_0_deterministic H4 e1_real);
+    rewrite (meps_0_deterministic H5 e2_real).
+  rewrite (meps_0_deterministic H4 e1_real) in div_real.
+  rewrite (meps_0_deterministic H5 e2_real) in div_real.
   clear H4 H5 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion div_float; subst.

coq/ErrorValidation.v

@@ -95,8 +95,8 @@ Proof.
   unfold validErrorbound in error_valid.
   rewrite absenv_const in error_valid.
   inversion eval_real; subst.
-  rewrite perturb_0_val in eval_real; auto.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic in eval_real; auto.
+  rewrite delta_0_deterministic; auto.
   clear delta H0.
   inversion eval_float; subst.
   unfold perturb in *; simpl in *.
@@ -148,8 +148,8 @@ Proof.
   unfold validErrorbound in error_valid.
   rewrite absenv_param in error_valid.
   inversion eval_real; subst.
-  rewrite perturb_0_val in eval_real; auto.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic in eval_real; auto.
+  rewrite delta_0_deterministic; auto.
   inversion eval_float; subst.
   unfold precondValidForExec in cenv_approx_p.
   specialize (absenv_approx_p v).
@@ -1288,7 +1288,7 @@ Proof.
       apply Is_true_eq_true in valid_intv_e2.
     apply Is_true_eq_true in valid_intv.
     inversion eval_real; subst.
-    apply existential_rewriting_binary in eval_float.
+    apply binary_unfolding in eval_float.
     destruct eval_float as [v1F [v2F [eval_e1_float [eval_e2_float eval_float]]]].
     destruct b.
     + eapply (validErrorboundCorrectAddition cenv absenv e1 e2); eauto.

coq/Expressions.v

@@ -11,7 +11,7 @@ Set Implicit Arguments.
 **)
 Inductive binop : Type := Plus | Sub | Mult | Div.
 
-Definition binop_eq_bool (b1:binop) (b2:binop) :=
+Definition binopEqBool (b1:binop) (b2:binop) :=
   match b1 with
     Plus => match b2 with Plus => true |_ => false end
   | Sub => match b2 with Sub => true |_ => false end
@@ -23,7 +23,7 @@ Definition binop_eq_bool (b1:binop) (b2:binop) :=
   Next define an evaluation function for binary operators on reals.
   Errors are added on the expression evaluation level later.
  **)
-Definition eval_binop (o:binop) (v1:R) (v2:R) :=
+Definition evalBinop (o:binop) (v1:R) (v2:R) :=
   match o with
   | Plus => Rplus v1 v2
   | Sub => Rminus v1 v2
@@ -37,7 +37,7 @@ Definition eval_binop (o:binop) (v1:R) (v2:R) :=
  **)
 Inductive unop: Type := Neg | Inv.
 
-Definition unop_eq_bool (o1:unop) (o2:unop) :=
+Definition unopEqBool (o1:unop) (o2:unop) :=
   match o1 with
   |Neg => match o2 with |Neg => true |_=> false end
   |Inv => match o2 with |Inv => true |_ => false end
@@ -47,7 +47,7 @@ Definition unop_eq_bool (o1:unop) (o2:unop) :=
    Define evaluation for unary operators on reals.
    Errors are added on the expression evaluation level later.
  **)
-Definition eval_unop (o:unop) (v:R):=
+Definition evalUnop (o:unop) (v:R):=
   match o with
   |Neg => (- v)%R
   |Inv => (/ v)%R
@@ -68,7 +68,7 @@ Inductive exp (V:Type): Type :=
 | Binop: binop -> exp V -> exp V -> exp V.
 
 
-Fixpoint exp_eq_bool (e1:exp Q) (e2:exp Q) :=
+Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
   match e1 with
   |Var _ v1 =>
    match e2 with
@@ -87,12 +87,12 @@ Fixpoint exp_eq_bool (e1:exp Q) (e2:exp Q) :=
    end
   |Unop o1 e11 =>
    match e2 with
-   |Unop o2 e22 => andb (unop_eq_bool o1 o2) (exp_eq_bool e11 e22)
+   |Unop o2 e22 => andb (unopEqBool o1 o2) (expEqBool e11 e22)
    |_ => false
    end
   |Binop o1 e11 e12 =>
    match e2 with
-   |Binop o2 e21 e22 => andb (binop_eq_bool o1 o2) (andb (exp_eq_bool e11 e21) (exp_eq_bool e12 e22))
+   |Binop o2 e21 e22 => andb (binopEqBool o1 o2) (andb (expEqBool e11 e21) (expEqBool e12 e22))
    |_ => false
    end
   end.
@@ -109,6 +109,7 @@ of the real valued computation by (1 + delta), where |delta| <= machine epsilon.
 
 It is important that variables are not perturbed when loading from an environment.
 This is the case, since loading a float value should not increase an additional error.
+Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
 **)
 Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
   Var_load x: eval_exp eps env (Var R x) (env x)
@@ -118,21 +119,20 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
 | Const_dist n delta:
     Rle (Rabs delta) eps ->
     eval_exp eps env (Const n) (perturb n delta)
-(** Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit **)
-| Unop_neg e1 v1: eval_exp eps env e1 v1 -> eval_exp eps env (Unop Neg e1) (eval_unop Neg v1)
+| Unop_neg e1 v1: eval_exp eps env e1 v1 -> eval_exp eps env (Unop Neg e1) (evalUnop Neg v1)
 | Unop_inv e1 v1 delta: Rle (Rabs delta) eps ->
                         eval_exp eps env e1 v1 ->
-                        eval_exp eps env (Unop Inv e1) (perturb (eval_unop Inv v1) delta)
+                        eval_exp eps env (Unop Inv e1) (perturb (evalUnop Inv v1) delta)
 | Binop_dist op e1 e2 v1 v2 delta:
     Rle (Rabs delta) eps ->
                 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).
+                eval_exp eps env (Binop op e1 e2) (perturb (evalBinop op v1 v2) delta).
 
 (**
-If |delta| <= 0 then perturb v delta is exactly v
+If |delta| <= 0 then perturb v delta is exactly v.
 **)
-Lemma perturb_0_val (v:R) (delta:R):
+Lemma delta_0_deterministic (v:R) (delta:R):
   (Rabs delta <= 0)%R ->
   perturb v delta = v.
 Proof.
@@ -145,9 +145,9 @@ Proof.
 Qed.
 
 (**
-Evaluation with 0 as epsilon is deterministic
+Evaluation with 0 as machine epsilon is deterministic
 **)
-Lemma eval_0_det (e:exp R) (env:env_ty):
+Lemma meps_0_deterministic (e:exp R) (env:env_ty):
   forall v1 v2,
   eval_exp R0 env e v1 ->
   eval_exp R0 env e v2 ->
@@ -155,7 +155,7 @@ Lemma eval_0_det (e:exp R) (env:env_ty):
 Proof.
   induction e; intros v1 v2 eval_v1 eval_v2;
     inversion eval_v1; inversion eval_v2; [ auto | | | | | | | ];
-      repeat try rewrite perturb_0_val; subst; auto.
+      repeat try rewrite delta_0_deterministic; subst; auto.
   - rewrite (IHe v0 v3); auto.
   - inversion H3.
   - inversion H4.
@@ -169,9 +169,9 @@ Helping lemma. Needed in soundness proof.
 For each evaluation of using an arbitrary epsilon, we can replace it by
 evaluating the subexpressions and then binding the result values to different
 variables in the environment.
-This needs the property that variables are not perturbed as opposed to parameters
+This relies on the property that variables are not perturbed as opposed to parameters
 **)
-Lemma existential_rewriting_binary (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
+Lemma binary_unfolding (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
   (eval_exp eps cenv (Binop b e1 e2) v <->
    exists v1 v2,
      eval_exp eps cenv e1 v1 /\
@@ -194,8 +194,10 @@ Proof.
     constructor; auto.
 Qed.
 
-
-Lemma existential_rewriting_unary (e:exp R) (eps:R) (cenv:env_ty) (v:R):
+(**
+Analogous lemma for unary expressions.
+**)
+Lemma unary_unfolding (e:exp R) (eps:R) (cenv:env_ty) (v:R):
   (eval_exp eps cenv (Unop Inv e) v <->
    exists v1,
      eval_exp eps cenv e v1 /\

coq/IntervalValidation.v

@@ -170,7 +170,7 @@ Proof.
     rewrite p_n, absenv_n in env_approx_p.
     specialize (precond_valid n); rewrite p_n in precond_valid.
     inversion eval_f; subst.
-    rewrite perturb_0_val; auto.
+    rewrite delta_0_deterministic; auto.
     destruct intv as [abslo abshi]; simpl in *.
     apply andb_prop_elim in env_approx_p.
     destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
@@ -194,7 +194,7 @@ Proof.
     apply andb_prop_elim in valid_bounds.
     destruct valid_bounds as [valid_lo valid_hi].
     inversion eval_f; subst.
-    rewrite perturb_0_val; auto.
+    rewrite delta_0_deterministic; auto.
     unfold contained; simpl.
     split.
     + apply Is_true_eq_true in valid_lo.
@@ -256,7 +256,7 @@ Proof.
          unfold contained, invertInterval in inv_valid; simpl in *.
          apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
          destruct IHf.
-         rewrite perturb_0_val; auto.
+         rewrite delta_0_deterministic; auto.
          unfold eval_unop, perturb; split.
          { eapply Rle_trans. apply valid_lo.
            destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
@@ -306,8 +306,8 @@ Proof.
          }
   - intros vR valid_precond valid_bounds eval_f; inversion eval_f; subst.
     pose proof (ivbounds_approximatesPrecond_sound (Binop b f1 f2) absenv P valid_bounds) as env_approx_p.
-    rewrite perturb_0_val in eval_f; auto.
-    rewrite perturb_0_val; auto.
+    rewrite delta_0_deterministic in eval_f; auto.
+    rewrite delta_0_deterministic; auto.
     simpl in valid_bounds.
     case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin.
     case_eq (absenv f1); intros iv1 err1 absenv_f1.

coq/attic/ModuleExpressions.v

@@ -75,7 +75,7 @@ Inductive eval_exp (eps:V) (env:env_ty) : (exp V) -> V -> Prop :=
 
 End Expression.
 
-Lemma perturb_0_val (v:R) (delta:R):
+Lemma delta_0_deterministic (v:R) (delta:R):
   (Rabs delta <= 0)%R ->
   perturb v delta = v.
 Proof.
@@ -95,7 +95,7 @@ Lemma eval_det (e:exp R) (env:env_ty):
 Proof.
   induction e; intros v1 v2 eval_v1 eval_v2;
     inversion eval_v1; inversion eval_v2; [ auto | | | ];
-      repeat try rewrite perturb_0_val; auto.
+      repeat try rewrite delta_0_deterministic; auto.
   subst.
   rewrite (IHe1 v0 v4); auto.
   rewrite (IHe2 v3 v5); auto.

coq/attic/SimpleDoppler.v

@@ -163,12 +163,12 @@ Proof.
   - inversion eval_real as
         [ | | | op e1 e2 v1 v2 delta delta_leq_0 eval_cst1 eval_param_u [op_eq e1_eq e2_eq] vR_eq];
       subst.
-    rewrite perturb_0_val in eval_real; auto.
+    rewrite delta_0_deterministic in eval_real; auto.
     inversion eval_cst1; subst.
-    rewrite perturb_0_val in eval_real; auto.
+    rewrite delta_0_deterministic in eval_real; auto.
     inversion eval_param_u; subst.
-    repeat rewrite perturb_0_val; auto.
-    rewrite perturb_0_val in eval_real , eval_param_u, eval_cst1; auto.
+    repeat rewrite delta_0_deterministic; auto.
+    rewrite delta_0_deterministic in eval_real , eval_param_u, eval_cst1; auto.
     clear delta delta0 delta1 delta_leq_0 H0 H1.
     inversion eval_float; subst.
     inversion H4; subst.

coq/attic/SimpleMultiplication.v

@@ -166,12 +166,12 @@ Proof.
   - inversion eval_real as
         [ | | | op e1 e2 v1 v2 delta delta_leq_0 eval_cst1 eval_param_u [op_eq e1_eq e2_eq] vR_eq];
       subst.
-    rewrite perturb_0_val in eval_real; auto.
+    rewrite delta_0_deterministic in eval_real; auto.
     inversion eval_cst1; subst.
-    rewrite perturb_0_val in eval_real; auto.
+    rewrite delta_0_deterministic in eval_real; auto.
     inversion eval_param_u; subst.
-    repeat rewrite perturb_0_val; auto.
-    rewrite perturb_0_val in eval_real , eval_param_u, eval_cst1; auto.
+    repeat rewrite delta_0_deterministic; auto.
+    rewrite delta_0_deterministic in eval_real , eval_param_u, eval_cst1; auto.
     clear delta delta0 delta1 delta_leq_0 H0 H1.
     inversion eval_float; subst.
     inversion H4; subst.

coq/attic/mult_abs

@@ -12,8 +12,8 @@ Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion mult_real; subst.
-  rewrite perturb_0_val in mult_real; auto.
-  rewrite perturb_0_val; auto.
+  rewrite delta_0_deterministic in mult_real; auto.
+  rewrite delta_0_deterministic; auto.
   unfold eval_binop in *; simpl in *.
   clear delta H2.
   rewrite (eval_det H4 e1_real);