Shorten some coq proofs

coq/ErrorValidation.v

@@ -92,12 +92,13 @@ Lemma validErrorboundCorrectConstant:
 Proof.
   intros cenv absenv n nR nF e nlo nhi P eval_real eval_float error_valid intv_valid absenv_const.
   unfold validErrorbound in error_valid.
-  rewrite absenv_const in error_valid.
   inversion eval_real; subst.
   rewrite delta_0_deterministic in eval_real; auto.
   rewrite delta_0_deterministic; auto.
   clear delta H0.
   inversion eval_float; subst.
+  pose proof (validIntervalbounds_sound (Const n) absenv P cenv (Q2R n) intv_valid eval_real) as iv_valid.
+  rewrite absenv_const in *;  simpl in *.
   unfold perturb in *; simpl in *.
   rewrite Rabs_err_simpl.
   unfold Qleb in error_valid.
@@ -106,27 +107,17 @@ Proof.
   apply Qle_bool_iff in error_valid.
   apply Qle_Rle in error_valid.
   eapply Rle_trans.
-  rewrite Rabs_mult.
-  eapply Rmult_le_compat_l; [ apply Rabs_pos | ].
-  apply H0.
-  rewrite Rabs_eq_Qabs.
-  rewrite Q2R_mult in error_valid.
-  eapply Rle_trans.
-  eapply Rmult_le_compat_r.
-  rewrite <- Q2R0_is_0.
-  apply Qle_Rle.
-  unfold machineEpsilon.
-  assert (Qle_bool 0 (1 # (2^53)) = true) by (unfold Qle_bool; auto).
-  rewrite <- Qle_bool_iff; auto.
-  rewrite absenv_const in intv_valid.
-  simpl in intv_valid.
-  andb_to_prop intv_valid.
-  Focus 2.
-  apply error_valid.
-  rewrite <- Rabs_eq_Qabs.
-  rewrite <- maxAbs_impl_RmaxAbs.
-  apply RmaxAbs; simpl; apply Qle_Rle; rewrite <- Qle_bool_iff; unfold Qleb in *; simpl in *;
-    [destruct (Qle_bool nlo n); auto | destruct (Qle_bool n nhi); auto].
+  - rewrite Rabs_mult.
+    eapply Rmult_le_compat_l; [ apply Rabs_pos | eauto ].
+  - rewrite Q2R_mult in error_valid.
+    eapply Rle_trans.
+    + eapply Rmult_le_compat_r.
+      apply mEps_geq_zero.
+      destruct iv_valid.
+      apply RmaxAbs; eauto.
+    + rewrite <- maxAbs_impl_RmaxAbs in error_valid.
+      unfold RmaxAbsFun in error_valid.
+      auto.
 Qed.
 
 Lemma validErrorboundCorrectParam:
@@ -179,6 +170,7 @@ Proof.
   rewrite <- H8;unfold RmaxAbsFun;simpl;auto.
 Qed.
 
+(* TODO: Maybe extract subproof for ivbounds of operands into main lemma *)
 Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
   eval_exp 0%R cenv P (toRExp e1) nR1 ->
   eval_exp 0%R cenv P (toRExp e2) nR2 ->
@@ -196,17 +188,10 @@ Lemma validErrorboundCorrectAddition cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 n
   (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
   intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded.
-  pose proof (ivbounds_approximatesPrecond_sound (Binop Plus e1 e2) absenv P valid_intv) as env_approx_p.
   eapply Rle_trans.
-  eapply add_abs_err_bounded.
-  apply e1_real.
-  apply e1_float.
-  apply e2_real.
-  apply e2_float.
-  apply eval_real.
-  apply eval_float.
-  apply err1_bounded.
-  apply err2_bounded.
+  apply
+    (add_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv P (Q2R err1) (Q2R err2));
+    try auto.
   unfold validErrorbound in valid_error at 1.
   rewrite absenv_add, absenv_e1, absenv_e2 in valid_error.
   andb_to_prop valid_error.
@@ -277,7 +262,6 @@ Proof.
   intros e1_real e2_real eval_real e1_float e2_float eval_float
          valid_error valid_intv absenv_e1 absenv_e2 absenv_sub
          err1_bounded err2_bounded.
-  pose proof (ivbounds_approximatesPrecond_sound (Binop Sub e1 e2) absenv P valid_intv) as env_approx_p.
   eapply Rle_trans.
   eapply subtract_abs_err_bounded.
   apply e1_real.
@@ -363,7 +347,6 @@ Proof.
   intros e1_real e2_real eval_real e1_float e2_float eval_float
          valid_error valid_intv absenv_e1 absenv_e2 absenv_mult
          err1_bounded err2_bounded.
-  pose proof (ivbounds_approximatesPrecond_sound (Binop Mult e1 e2) absenv P valid_intv) as env_approx_p.
   eapply Rle_trans.
   eapply (mult_abs_err_bounded (toRExp e1) _ _ (toRExp e2)); eauto.
   unfold validErrorbound in valid_error at 1.
@@ -936,7 +919,6 @@ Proof.
   intros e1_real e2_real eval_real e1_float e2_float eval_float
          valid_error valid_intv absenv_e1 absenv_e2 absenv_div
          err1_bounded err2_bounded.
-  pose proof (ivbounds_approximatesPrecond_sound (Binop Div e1 e2) absenv P valid_intv) as env_approx_p.
   eapply Rle_trans.
   apply (div_abs_err_bounded (toRExp e1) nR1 nF1 (toRExp e2) nR2 nF2 nR nF cenv P); auto.
   unfold validErrorbound in valid_error at 1;
@@ -983,7 +965,7 @@ Proof.
     apply Rplus_le_compat.
     (* Error Propagation proof *)
     + clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float
-            e1_real e2_float e2_real env_approx_p absenv_div
+            e1_real e2_float e2_real absenv_div
             valid_err_e1 valid_err_e2 cenv absenv alo ahi nR nF e1 e2 e P.
       unfold IntervalArith.contained, widenInterval in *.
       simpl in *.