Minor lemma fixes

coq/Expressions.v

@@ -98,7 +98,7 @@ Lemma existential_rewriting (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty
    exists v1 v2,
      eval_exp eps cenv e1 v1 /\
      eval_exp eps cenv e2 v2 /\
-     eval_exp eps (updEnv 1 v1 (updEnv 2 v2 cenv)) (Binop b (Var R 1) (Var R 2)) v).
+     eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cenv)) (Binop b (Var R 1) (Var R 2)) v).
 Proof.
   split.
   - intros eval_bin.
@@ -116,6 +116,33 @@ Proof.
     constructor; auto.
 Qed.
 
+Lemma sub_to_plus eps cenv e1 e2 v v2 v1:
+  eval_exp eps cenv e1 v1 ->
+  eval_exp eps cenv e2 v2 ->
+  eval_exp eps (updEnv 1 v1 (updEnv 2 (- v2) cenv)) (Binop Plus (Var R 1) (Var R 2)) v <->
+  eval_exp eps (updEnv 1 v1 (updEnv 2 v2 cenv)) (Binop Sub (Var R 1) (Var R 2)) v.
+Proof.
+  intros eval_e2.
+  split.
+  - intros.
+    inversion H0; subst.
+    inversion H7; subst.
+    unfold eval_binop; simpl. unfold updEnv at 3; unfold updEnv at 3; simpl.
+    rewrite <- Rsub_eq_Ropp_Rplus.
+    constructor; auto.
+    + inversion H6; subst. unfold updEnv at 3; unfold updEnv at 3; simpl. apply Var_load.
+    + unfold updEnv at 3 in H7; unfold updEnv at 3 in H7; simpl in H7.
+      apply Var_load.
+  - intros.
+    inversion H0; subst.
+    inversion H7; subst.
+    unfold eval_binop; simpl. unfold updEnv at 3; unfold updEnv at 3; simpl.
+    rewrite Rsub_eq_Ropp_Rplus.
+    constructor; auto.
+    + inversion H6; subst. unfold updEnv in *; simpl in *; apply Var_load.
+    + unfold updEnv in *; simpl in *. apply Var_load.
+Qed.
+
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)

coq/SimpleDoppler.v

@@ -125,7 +125,7 @@ Proof.
     + unfold valCst.
       apply (AbsErrConst cst1 (mkInterval cst1 cst1) errCst1); [constructor | ].
       unfold isSoundErr; simpl.
-      unfold errCst1, cst1, machineEpsilon.
+      unfold errCst1, cst1, Expressions.machineEpsilon.
       assert (1657 / 5 >= 0)%R by prove_constant.
       unfold Rabs;
       destruct Rcase_abs as [lt_plus | ge_plus];
@@ -135,7 +135,7 @@ Proof.
       interval.
     + apply (AbsErrParam u (mkInterval (- 100) (100)) errVaru); [constructor | ].
       unfold isSoundErr; simpl.
-      unfold machineEpsilon, errVaru.
+      unfold Expressions.machineEpsilon, errVaru.
       unfold realFromNum.
       unfold negativePower.
       assert (Rabs (-100) = 100%R) by (unfold Rabs; destruct Rcase_abs; lra).
@@ -163,7 +163,7 @@ Proof.
         apply Req_le; auto.
       * unfold isSoundErr; simpl.
         unfold lowerBoundAddUCst, upperBoundAddUCst, errAddUCst.
-        unfold machineEpsilon.
+        unfold Expressions.machineEpsilon.
         assert (0 <= (1157/5))%R by interval.
         assert (0 <= (2157/5))%R by interval.
         repeat rewrite Rabs_pos_eq; auto.
@@ -195,12 +195,12 @@ Proof.
     repeat rewrite Rmult_1_r.
     eapply Rle_trans.
     eapply Rplus_le_compat_l.
-    eapply Rmult_le_compat_r; [unfold machineEpsilon; prove_constant | ].
+    eapply Rmult_le_compat_r; [unfold Expressions.machineEpsilon; prove_constant | ].
     eapply Rabs_triang.
 
     eapply Rle_trans.
     eapply Rplus_le_compat_l.
-    eapply Rmult_le_compat_r;  [unfold machineEpsilon; prove_constant | ].
+    eapply Rmult_le_compat_r;  [unfold Expressions.machineEpsilon; prove_constant | ].
     eapply Rplus_le_compat.
     eapply Rabs_triang.
     eapply Rabs_triang.
@@ -229,9 +229,9 @@ Proof.
     eapply Rplus_le_compat.
     eapply Rplus_le_compat_l.
     eapply H20; auto.
-    unfold machineEpsilon; prove_constant.
+    unfold Expressions.machineEpsilon; prove_constant.
     eapply Rmult_le_compat_r.
-    unfold machineEpsilon; prove_constant.
+    unfold Expressions.machineEpsilon; prove_constant.
     eapply Rplus_le_compat.
     eapply Rplus_le_compat_l.
     eapply Rmult_le_compat_l; auto.
@@ -245,7 +245,7 @@ Proof.
     eapply Rmult_le_compat_l.
     prove_constant.
     apply H1.
-    unfold cst1, machineEpsilon, errAddUCst; prove_constant.
+    unfold cst1, Expressions.machineEpsilon, errAddUCst. unfold machineEpsilon. prove_constant.
 Admitted.
 
     (*

coq/SimpleMultiplication.v

@@ -113,7 +113,7 @@ Proof.
       (* TODO: What about vlaues that are actually floats ? *) admit.
     + apply (AbsErrParam u (mkInterval (- 100) (100)) errVaru); [constructor | ].
       unfold isSoundErr; simpl.
-      unfold machineEpsilon, errVaru.
+      unfold Expressions.machineEpsilon, errVaru.
       unfold realFromNum.
       unfold negativePower.
       assert (Rabs (-100) = 100%R) by (unfold Rabs; destruct Rcase_abs; lra).
@@ -140,7 +140,7 @@ Proof.
         prove_constant. (* And here too *)
       * unfold isSoundErr; simpl.
         unfold lowerBoundMultUCst, upperBoundMultUCst, errMultUCst.
-        unfold machineEpsilon.
+        unfold Expressions.machineEpsilon.
         assert (- realFromNum 10000 0 0 <= 0)%R by prove_constant.
         assert (0 <= realFromNum 10000 0 0) %R by prove_constant.
         rewrite Rabs_left1; auto.