Fix issues notes in comments to #10

coq/AffineValidation.v

@@ -587,8 +587,8 @@ Proof.
           try (field_simplify in Hlt; assert (h = l) as Hz by lra; apply eqR_Qeq in Hz; lra).
       - rewrite Rdiv_abs_le_bounds; try lra.
         assert (0 < h - l)%R as H1 by lra.
-        Rrewrite (vR - h / 2 - l /2 = vR - (h + l) / 2)%R.
-        Rrewrite (1 * (h / 2 + l / 2 - l) = (h - l) / 2)%R.
+        field_rewrite (vR - h / 2 - l /2 = vR - (h + l) / 2)%R.
+        field_rewrite (1 * (h / 2 + l / 2 - l) = (h - l) / 2)%R.
         apply Rabs_Rle_condition; lra.
     }
     pose (noise := exist (fun x => -(1) <= x <= 1)%R noise_expression Hnoise).
@@ -625,8 +625,8 @@ Proof.
           try (field_simplify in Hlt; assert (h = l) as Hz by lra; apply eqR_Qeq in Hz; lra).
       - rewrite Rdiv_abs_le_bounds; try lra.
         assert (0 < h - l)%R as H1 by lra.
-        Rrewrite (vR - h / 2 - l /2 = vR - (h + l) / 2)%R.
-        Rrewrite (1 * (h / 2 + l / 2 - l) = (h - l) / 2)%R.
+        field_rewrite (vR - h / 2 - l /2 = vR - (h + l) / 2)%R.
+        field_rewrite (1 * (h / 2 + l / 2 - l) = (h - l) / 2)%R.
         apply Rabs_Rle_condition; lra.
     }
     pose (noise := exist (fun x => -(1) <= x <= 1)%R noise_expression Hnoise).
@@ -890,9 +890,9 @@ Proof.
     simpl.
     rewrite Qeq_bool_refl.
     apply andb_true_intro.
-    split; rewrite Qle_bool_iff; simpl; field_simplify; Qrewrite ((2#1) * v * / (2#1) == v).
-    * now Qrewrite (fst i / 1 == fst i).
-    * now Qrewrite (snd i / 1 == snd i).
+    split; rewrite Qle_bool_iff; simpl; field_simplify; field_rewrite ((2#1) * v * / (2#1) == v).
+    * now field_rewrite (fst i / 1 == fst i).
+    * now field_rewrite (snd i / 1 == snd i).
   }
   assert (fresh noise (fromIntv (v, v) noise))
     by (unfold fromIntv; simpl ivlo; simpl ivhi; rewrite Qeq_bool_refl;
@@ -906,7 +906,7 @@ Proof.
     simpl.
     rewrite Q2R_plus.
     rewrite Q2R_div; try lra.
-    unfold af_evals, Ropt_eq; simpl.
+    unfold af_evals; simpl.
     lra.
   }
   assert (FloverMap.find (elt:=affine_form Q) (Const m v) (FloverMap.add (Const m v) (fromIntv (v, v) noise) iexpmap) = Some (fromIntv (v, v) noise))

coq/Infra/Ltacs.v

@@ -186,7 +186,10 @@ Ltac telling_rewrite pat hyp :=
 Tactic Notation "unify asm" open_constr(pat) hyp(H):=
   telling_rewrite pat H.
 
-Ltac Qrewrite H :=
+(* Takes a field-structure equality expression, tries to rewrite the *)
+(* the left side in the goal with right if the equality holds        *)
+Ltac field_rewrite H :=
+  let tmp := fresh "tmp" in
   assert H as tmp by (try field; try lra); rewrite tmp; clear tmp.
 
 Ltac destruct_ex H pat :=

coq/Infra/RationalSimps.v

@@ -252,3 +252,15 @@ Proof.
   rewrite Qabs_Qle_condition in abs_leq_0.
   lra.
 Qed.
+
+Lemma Qabs_bounded (x y: Q):
+  -(1) <= x <= 1 ->
+  Qabs(x*y) <= Qabs y.
+Proof.
+  intros.
+  rewrite Qabs_Qmult.
+  assert (Qabs y == 1 * Qabs y) as tmp by lra; rewrite tmp at 2; clear tmp.
+  eapply Qmult_le_compat_r.
+  - apply Qabs_Qle_condition; auto.
+  - apply Qabs_nonneg.
+Qed.

coq/Infra/RealSimps.v

@@ -88,6 +88,16 @@ Proof.
   apply Rsqr_0_uniq in Rabs_eq; assumption.
 Qed.
 
+Lemma Rabs_bounded (x y: R):
+  (-1 <= x <= 1)%R ->
+  (Rabs(x*y) <= Rabs y)%R.
+Proof.
+  intros.
+  rewrite Rabs_mult.
+  assert (Rabs y = 1 * Rabs y)%R as tmp by lra; rewrite tmp at 2; clear tmp.
+  eapply Rmult_le_compat_r; eauto using Rabs_pos, Rabs_le.
+Qed.
+
 Lemma RmaxAbs_peel_Rabs a b:
   Rmax (Rabs a) (Rabs b) = Rabs (Rmax (Rabs a) (Rabs b)).
 Proof.