diff --git a/coq/ErrorBounds.v b/coq/ErrorBounds.v index 8f3211afeb187c2f71676d1430024374be87fde0..68a0ed9f7e6cbb1210402fbe61240e432f1ba5d4 100644 --- a/coq/ErrorBounds.v +++ b/coq/ErrorBounds.v @@ -260,23 +260,70 @@ Qed. Lemma fma_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (e3:exp Q) (e3R:R) (e3F:R) - (vR:R) (vF:R) (E1 E2:env) (err1 err2 err3:Q) (m m1 m2:mType) defVars: + (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars: eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1-> eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 -> - eval_exp E2 defVars (toRExp e3) e3F m1-> + eval_exp E2 defVars (toRExp e3) e3F m3-> eval_exp E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 -> - eval_exp (upd Env 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) + eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars))) (Fma (Var R 1) (Var R 2) (Var R 3)) vF m -> - (Rabs (e1R - e1F) <= Q2R err1)%R -> - (Rabs (e2R - e2F) <= Q2R err2)%R -> - (Rabs (e3R - e3F) <= Q2R err3)%R -> - (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%R. - (Rabs (vR - vF) <= Rabs (err1 + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R. + (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R. Proof. + intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float. + inversion fma_real; subst; + assert (m0 = M0) by (eapply toRMap_eval_M0; eauto). + assert (m4 = M0) by (eapply toRMap_eval_M0; eauto). + assert (m5 = M0) by (eapply toRMap_eval_M0; eauto). + subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto. + rewrite delta_0_deterministic in fma_real; auto. + rewrite delta_0_deterministic; auto. + unfold evalFma in *; simpl in *. + clear delta H3. + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real); + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real); + rewrite (meps_0_deterministic (toRExp e3) H7 e3_real). + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in fma_real. + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in fma_real. + rewrite (meps_0_deterministic (toRExp e3) H7 e3_real) in fma_real. + clear H5 H6 v1 v2 v3 H7 H2. + inversion fma_float; subst. + unfold evalFma in *. + unfold perturb; simpl. + inversion H3; subst; inversion H6; subst; inversion H7; subst. + unfold updEnv in *; simpl in *. + inversion H5; inversion H1; inversion H9; subst. + clear fma_float H7 fma_real e1_real e1_float e2_real e2_float e3_real e3_float H6 H1 H5 H9 H3 H0 H4 H8. + repeat rewrite Rmult_plus_distr_l. + rewrite Rmult_1_r. + rewrite Rsub_eq_Ropp_Rplus. + rewrite Ropp_plus_distr. + rewrite <- Rplus_assoc. + setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2. + rewrite Rsub_eq_Ropp_Rplus. + rewrite Rsub_eq_Ropp_Rplus. + rewrite Rsub_eq_Ropp_Rplus. + rewrite <- Rplus_assoc. + setoid_rewrite Rplus_comm at 8. + rewrite <- Rplus_assoc. + setoid_rewrite Rplus_comm at 9. + rewrite Rplus_assoc. + setoid_rewrite Rplus_assoc at 2. + rewrite <- Rplus_assoc. + rewrite <- Rsub_eq_Ropp_Rplus. + rewrite <- Rsub_eq_Ropp_Rplus. + rewrite <- Ropp_plus_distr. + rewrite <- Rsub_eq_Ropp_Rplus. + eapply Rle_trans. + eapply Rabs_triang. + eapply Rplus_le_compat_l. + rewrite Rabs_Ropp. + repeat rewrite Rabs_mult. + eapply Rmult_le_compat_l; auto. + apply Rabs_pos. Qed. diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index 7d0d981e794d6030e1d427f20d91eae51977c9d0..e9f1126df197d2e18b8251bfe35eefa7734c2cb5 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -81,7 +81,7 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *) let upperBoundE3 := maxAbs ive3 in let errIntv_prod := multIntv errIve2 errIve3 in let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in - Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIntv_prod errIve1)) * (mTypeToQ m)) err + Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIve1 errIntv_prod)) * (mTypeToQ m)) err else false |Downcast m1 e1 => if validErrorbound e1 typeMap A dVars @@ -465,6 +465,472 @@ Proof. repeat rewrite Q2R_minus; auto. Qed. +Lemma multiplicationErrorBounded e1lo e1hi e2lo e2hi nR1 nF1 nR2 nF2 err1 err2 : + (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> + (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> + (Rabs (nR1 - nF1) <= Q2R err1)%R -> + (Rabs (nR2 - nF2) <= Q2R err2)%R -> + (0 <= Q2R err1)%R -> + (0 <= Q2R err2)%R -> + (Rabs (nR1 * nR2 - nF1 * nF2) <= + RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + + Q2R err1 * Q2R err2)%R. +Proof. + intros valid_e1 valid_e2 err1_bounded err2_bounded err1_pos err2_pos. + unfold Rabs in err1_bounded. + unfold Rabs in err2_bounded. + (* Before doing case distinction, prove bounds that will be used many times: *) + assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R + as upperBound_nR1 + by (apply contained_leq_maxAbs_val; auto). + assert (nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R + as upperBound_nR2 + by (apply contained_leq_maxAbs_val; auto). + assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R + as upperBound_Ropp_nR1 + by (apply contained_leq_maxAbs_neg_val; auto). + assert (- nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R + as upperBound_Ropp_nR2 + by (apply contained_leq_maxAbs_neg_val; auto). + assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R + as bound_nR1 by (apply Rmult_le_compat_r; auto). + assert (- nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R + as bound_neg_nR1 by (apply Rmult_le_compat_r; auto). + assert (nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R + as bound_nR2 by (apply Rmult_le_compat_r; auto). + assert (- nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R + as bound_neg_nR2 by (apply Rmult_le_compat_r; auto). + assert (- (Q2R err1 * Q2R err2) <= Q2R err1 * Q2R err2)%R as err_neg_bound + by (rewrite Ropp_mult_distr_l; apply Rmult_le_compat_r; lra). + assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R + as zero_up_nR1 by lra. + assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R + as nR1_to_sum by lra. + assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R + as sum_to_errsum by lra. + (* Large case distinction for + a) different cases of the value of Rabs (...) and + b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *) + destruct Rcase_abs in err1_bounded; destruct Rcase_abs in err2_bounded. + + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. + rewrite Ropp_plus_distr in err1_bounded, err2_bounded. + rewrite Ropp_involutive in err1_bounded, err2_bounded. + assert (nF1 <= Q2R err1 + nR1)%R by lra. + assert (nF2 <= Q2R err2 + nR2)%R by lra. + unfold Rabs. + destruct Rcase_abs. + * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. + rewrite Ropp_involutive. + destruct (Rle_lt_dec 0 nF1). + { (* Upper Bound ... *) + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. hnf. left; auto. + assert (nR1 <= nF1)%R by lra. + apply H1. + lra. + } + { + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR2 < nF2)%R by lra. + apply Rlt_le in H1; apply H1. + destruct (Rle_lt_dec 0 nR2). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR1 < nF1)%R by lra. + apply Rlt_le in H1; apply H1. + lra. + } + * rewrite Rsub_eq_Ropp_Rplus. + destruct (Rle_lt_dec 0 nF1). + { + rewrite Ropp_mult_distr_r. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + assert (- nF2 <= - nR2)%R by lra. + apply H1. + destruct (Rle_lt_dec 0 (- nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR1 < nF1)%R by lra. + apply Rlt_le in H1; apply H1. + lra. + } + { + rewrite Ropp_mult_distr_l. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l. + rewrite <- (Ropp_involutive 0). + apply Ropp_ge_le_contravar. + apply Rle_ge. + rewrite Ropp_0. + hnf. left; auto. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + assert (- nF1 <= -nR1)%R by lra. + apply H1. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + apply Ropp_le_ge_contravar in H. + apply Rge_le in H. + apply H. + lra. + } + + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. + rewrite Ropp_plus_distr in err1_bounded. + rewrite Ropp_involutive in err1_bounded. + assert (nF1 <= Q2R err1 + nR1)%R by lra. + assert (nF2 <= Q2R err2 + nR2)%R by lra. + unfold Rabs. + destruct Rcase_abs. + * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. + rewrite Ropp_involutive. + destruct (Rle_lt_dec 0 nF1). + { (* Upper Bound ... *) + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. hnf. left; auto. + assert (nR1 <= nF1)%R by lra. + apply H1. + lra. + } + { + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (- nF2 <= - (nR2 - Q2R err2))%R by lra. + apply Ropp_le_ge_contravar in H1. + repeat rewrite Ropp_involutive in H1. + apply Rge_le in H1. + apply H1. + destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR1 < nF1)%R by lra. + apply Rlt_le in H1; apply H1. + lra. + } + * rewrite Rsub_eq_Ropp_Rplus. + destruct (Rle_lt_dec 0 nF1). + { + rewrite Ropp_mult_distr_r. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + assert (- nF2 <= - nR2 + Q2R err2)%R by lra. + apply H1. + destruct (Rle_lt_dec 0 (- nR2 + Q2R err2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR1 < nF1)%R by lra. + apply Rlt_le in H1; apply H1. + lra. + } + { + rewrite Ropp_mult_distr_l. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l. + rewrite <- (Ropp_involutive 0). + apply Ropp_ge_le_contravar. + apply Rle_ge. + rewrite Ropp_0. + hnf. left; auto. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + assert (- nF1 <= -nR1)%R by lra. + apply H1. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + apply Ropp_le_ge_contravar in H. + apply Rge_le in H. + apply H. + lra. + } + + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. + rewrite Ropp_plus_distr in err2_bounded. + rewrite Ropp_involutive in err2_bounded. + assert (nF1 <= Q2R err1 + nR1)%R by lra. + assert (nF2 <= Q2R err2 + nR2)%R by lra. + unfold Rabs. + destruct Rcase_abs. + * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. + rewrite Ropp_involutive. + destruct (Rle_lt_dec 0 nF1). + { (* Upper Bound ... *) + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. hnf. left; auto. + assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. + apply Ropp_le_ge_contravar in H1. + repeat rewrite Ropp_involutive in H1. + apply Rge_le in H1. + apply H1. + lra. + } + { + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR2 < nF2)%R by lra. + apply Rlt_le in H1; apply H1. + destruct (Rle_lt_dec 0 nR2). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. + apply Ropp_le_ge_contravar in H1. + repeat rewrite Ropp_involutive in H1. + apply Rge_le in H1. + apply H1. + lra. + } + * rewrite Rsub_eq_Ropp_Rplus. + destruct (Rle_lt_dec 0 nF1). + { + rewrite Ropp_mult_distr_r. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + assert (- nF2 <= - nR2)%R by lra. + apply H1. + destruct (Rle_lt_dec 0 (- nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. + apply Ropp_le_ge_contravar in H1. + repeat rewrite Ropp_involutive in H1. + apply Rge_le in H1. + apply H1. + lra. + } + { + rewrite Ropp_mult_distr_l. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l. + lra. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. + apply H1. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l; try lra. + apply Ropp_le_ge_contravar in H. + apply Rge_le in H. + apply H. + lra. + } + (* All positive *) + + assert (nF1 <= Q2R err1 + nR1)%R by lra. + assert (nF2 <= Q2R err2 + nR2)%R by lra. + unfold Rabs. + destruct Rcase_abs. + * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. + rewrite Ropp_involutive. + destruct (Rle_lt_dec 0 nF1). + { (* Upper Bound ... *) + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. hnf. left; auto. + assert (nR1 - Q2R err1 <= nF1)%R by lra. + apply H1. + lra. + } + { + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_neg_l. + hnf. left; auto. + assert (nR2 - Q2R err2 <= nF2)%R by lra. + apply H1. + destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + lra. + assert (nR1 - Q2R err1 <= nF1)%R by lra. + apply H1. + lra. + } + * rewrite Rsub_eq_Ropp_Rplus. + destruct (Rle_lt_dec 0 nF1). + { + rewrite Ropp_mult_distr_r. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l; auto. + assert (- nF2 <= Q2R err2 - nR2)%R by lra. + apply H1. + destruct (Rle_lt_dec 0 (Q2R err2 - nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + apply H. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + lra. + assert (nR1 - Q2R err1 <= nF1)%R by lra. + apply H1. + lra. + } + { + rewrite Ropp_mult_distr_l. + eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_l. + rewrite <- (Ropp_involutive 0). + apply Ropp_ge_le_contravar. + apply Rle_ge. + rewrite Ropp_0. + lra. + apply H0. + destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). + - eapply Rle_trans. + eapply Rplus_le_compat_l. + eapply Rmult_le_compat_r; auto. + assert (- nF1 <= Q2R err1 - nR1)%R by lra. + apply H1. + lra. + - eapply Rle_trans. + eapply Rplus_le_compat_l. + rewrite Rmult_comm. + eapply Rmult_le_compat_neg_l. + lra. + apply Ropp_le_ge_contravar in H. + apply Rge_le in H. + apply H. + lra. + } +Qed. + Lemma validErrorboundCorrectMult E1 E2 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) dVars (m m1 m2:mType) Gamma defVars: @@ -522,460 +988,7 @@ Proof. Focus 2. apply valid_error. apply Rplus_le_compat. - - unfold Rabs in err1_bounded. - unfold Rabs in err2_bounded. - (* Before doing case distinction, prove bounds that will be used many times: *) - assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R - as upperBound_nR1 - by (apply contained_leq_maxAbs_val; auto). - assert (nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R - as upperBound_nR2 - by (apply contained_leq_maxAbs_val; auto). - assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R - as upperBound_Ropp_nR1 - by (apply contained_leq_maxAbs_neg_val; auto). - assert (- nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R - as upperBound_Ropp_nR2 - by (apply contained_leq_maxAbs_neg_val; auto). - assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R - as bound_nR1 by (apply Rmult_le_compat_r; auto). - assert (- nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R - as bound_neg_nR1 by (apply Rmult_le_compat_r; auto). - assert (nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R - as bound_nR2 by (apply Rmult_le_compat_r; auto). - assert (- nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R - as bound_neg_nR2 by (apply Rmult_le_compat_r; auto). - assert (- (Q2R err1 * Q2R err2) <= Q2R err1 * Q2R err2)%R as err_neg_bound - by (rewrite Ropp_mult_distr_l; apply Rmult_le_compat_r; lra). - assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R - as zero_up_nR1 by lra. - assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R - as nR1_to_sum by lra. - assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R - as sum_to_errsum by lra. - clear e1_real e1_float e2_real e2_float eval_real eval_float valid_error - absenv_e1 absenv_e2. - (* Large case distinction for - a) different cases of the value of Rabs (...) and - b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *) - destruct Rcase_abs in err1_bounded; destruct Rcase_abs in err2_bounded. - + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. - rewrite Ropp_plus_distr in err1_bounded, err2_bounded. - rewrite Ropp_involutive in err1_bounded, err2_bounded. - assert (nF1 <= Q2R err1 + nR1)%R by lra. - assert (nF2 <= Q2R err2 + nR2)%R by lra. - unfold Rabs. - destruct Rcase_abs. - * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - destruct (Rle_lt_dec 0 nF1). - { (* Upper Bound ... *) - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. hnf. left; auto. - assert (nR1 <= nF1)%R by lra. - apply H2. - lra. - } - { - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR2 < nF2)%R by lra. - apply Rlt_le in H2; apply H2. - destruct (Rle_lt_dec 0 nR2). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR1 < nF1)%R by lra. - apply Rlt_le in H2; apply H2. - lra. - } - * rewrite Rsub_eq_Ropp_Rplus. - destruct (Rle_lt_dec 0 nF1). - { - rewrite Ropp_mult_distr_r. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - assert (- nF2 <= - nR2)%R by lra. - apply H2. - destruct (Rle_lt_dec 0 (- nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR1 < nF1)%R by lra. - apply Rlt_le in H2; apply H2. - lra. - } - { - rewrite Ropp_mult_distr_l. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l. - rewrite <- (Ropp_involutive 0). - apply Ropp_ge_le_contravar. - apply Rle_ge. - rewrite Ropp_0. - hnf. left; auto. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - assert (- nF1 <= -nR1)%R by lra. - apply H2. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - apply Ropp_le_ge_contravar in H0. - apply Rge_le in H0. - apply H0. - lra. - } - + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. - rewrite Ropp_plus_distr in err1_bounded. - rewrite Ropp_involutive in err1_bounded. - assert (nF1 <= Q2R err1 + nR1)%R by lra. - assert (nF2 <= Q2R err2 + nR2)%R by lra. - unfold Rabs. - destruct Rcase_abs. - * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - destruct (Rle_lt_dec 0 nF1). - { (* Upper Bound ... *) - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. hnf. left; auto. - assert (nR1 <= nF1)%R by lra. - apply H2. - lra. - } - { - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (- nF2 <= - (nR2 - Q2R err2))%R by lra. - apply Ropp_le_ge_contravar in H2. - repeat rewrite Ropp_involutive in H2. - apply Rge_le in H2. - apply H2. - destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR1 < nF1)%R by lra. - apply Rlt_le in H2; apply H2. - lra. - } - * rewrite Rsub_eq_Ropp_Rplus. - destruct (Rle_lt_dec 0 nF1). - { - rewrite Ropp_mult_distr_r. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - assert (- nF2 <= - nR2 + Q2R err2)%R by lra. - apply H2. - destruct (Rle_lt_dec 0 (- nR2 + Q2R err2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR1 < nF1)%R by lra. - apply Rlt_le in H2; apply H2. - lra. - } - { - rewrite Ropp_mult_distr_l. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l. - rewrite <- (Ropp_involutive 0). - apply Ropp_ge_le_contravar. - apply Rle_ge. - rewrite Ropp_0. - hnf. left; auto. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - assert (- nF1 <= -nR1)%R by lra. - apply H2. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - apply Ropp_le_ge_contravar in H0. - apply Rge_le in H0. - apply H0. - lra. - } - + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. - rewrite Ropp_plus_distr in err2_bounded. - rewrite Ropp_involutive in err2_bounded. - assert (nF1 <= Q2R err1 + nR1)%R by lra. - assert (nF2 <= Q2R err2 + nR2)%R by lra. - unfold Rabs. - destruct Rcase_abs. - * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - destruct (Rle_lt_dec 0 nF1). - { (* Upper Bound ... *) - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. hnf. left; auto. - assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply Ropp_le_ge_contravar in H2. - repeat rewrite Ropp_involutive in H2. - apply Rge_le in H2. - apply H2. - lra. - } - { - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR2 < nF2)%R by lra. - apply Rlt_le in H2; apply H2. - destruct (Rle_lt_dec 0 nR2). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply Ropp_le_ge_contravar in H2. - repeat rewrite Ropp_involutive in H2. - apply Rge_le in H2. - apply H2. - lra. - } - * rewrite Rsub_eq_Ropp_Rplus. - destruct (Rle_lt_dec 0 nF1). - { - rewrite Ropp_mult_distr_r. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - assert (- nF2 <= - nR2)%R by lra. - apply H2. - destruct (Rle_lt_dec 0 (- nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply Ropp_le_ge_contravar in H2. - repeat rewrite Ropp_involutive in H2. - apply Rge_le in H2. - apply H2. - lra. - } - { - rewrite Ropp_mult_distr_l. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l. - lra. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply H2. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l; try lra. - apply Ropp_le_ge_contravar in H0. - apply Rge_le in H0. - apply H0. - lra. - } - (* All positive *) - + assert (nF1 <= Q2R err1 + nR1)%R by lra. - assert (nF2 <= Q2R err2 + nR2)%R by lra. - unfold Rabs. - destruct Rcase_abs. - * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - destruct (Rle_lt_dec 0 nF1). - { (* Upper Bound ... *) - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. hnf. left; auto. - assert (nR1 - Q2R err1 <= nF1)%R by lra. - apply H2. - lra. - } - { - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_neg_l. - hnf. left; auto. - assert (nR2 - Q2R err2 <= nF2)%R by lra. - apply H2. - destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - lra. - assert (nR1 - Q2R err1 <= nF1)%R by lra. - apply H2. - lra. - } - * rewrite Rsub_eq_Ropp_Rplus. - destruct (Rle_lt_dec 0 nF1). - { - rewrite Ropp_mult_distr_r. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l; auto. - assert (- nF2 <= Q2R err2 - nR2)%R by lra. - apply H2. - destruct (Rle_lt_dec 0 (Q2R err2 - nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - apply H0. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - lra. - assert (nR1 - Q2R err1 <= nF1)%R by lra. - apply H2. - lra. - } - { - rewrite Ropp_mult_distr_l. - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_l. - rewrite <- (Ropp_involutive 0). - apply Ropp_ge_le_contravar. - apply Rle_ge. - rewrite Ropp_0. - lra. - apply H1. - destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - - eapply Rle_trans. - eapply Rplus_le_compat_l. - eapply Rmult_le_compat_r; auto. - assert (- nF1 <= Q2R err1 - nR1)%R by lra. - apply H2. - lra. - - eapply Rle_trans. - eapply Rplus_le_compat_l. - rewrite Rmult_comm. - eapply Rmult_le_compat_neg_l. - lra. - apply Ropp_le_ge_contravar in H0. - apply Rge_le in H0. - apply H0. - lra. - } + - eauto using multiplicationErrorBounded. - remember (multIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv. iv_assert iv iv_unf. destruct iv_unf as [ivl [ivh iv_unf]]. @@ -1965,9 +1978,78 @@ Lemma validErrorboundCorrectFma E1 E2 absenv (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float - subexpr_ok valid_error valid_e1 valid_e2 valid_e3 absenv_e1 absenv_e2 absenv_e3 absenv_mult + subexpr_ok valid_error valid_e1 valid_e2 valid_e3 absenv_e1 absenv_e2 absenv_e3 absenv_fma err1_bounded err2_bounded err3_bounded. eapply Rle_trans. + eapply (fma_abs_err_bounded e1 e2 e3); eauto. + unfold validErrorbound in valid_error. + rewrite absenv_fma, absenv_e1, absenv_e2, absenv_e3 in valid_error. + case_eq (Gamma (Fma e1 e2 e3)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + simpl in subexpr_ok; rewrite H in subexpr_ok. + case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. + case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. + case_eq (Gamma e3); intros; rewrite H2 in subexpr_ok; [ | inversion subexpr_ok ]. + andb_to_prop subexpr_ok. + apply mTypeEq_compat_eq in L; subst. + pose proof (typingSoundnessExp _ _ R1 e1_float). + pose proof (typingSoundnessExp _ _ R0 e2_float). + pose proof (typingSoundnessExp _ _ R e3_float). + rewrite H0 in H3; rewrite H1 in H4; rewrite H2 in H5; inversion H3; inversion H4; inversion H5; subst. + clear H0 H1 H2 H3 H4 H5. + andb_to_prop valid_error. + rename R3 into valid_error. + assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv dVars); eauto). + assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv dVars); eauto). + assert (0 <= Q2R err3)%R as err3_pos by (eapply (err_always_positive e3 Gamma absenv dVars); eauto). + clear R2 R4 L0. + apply Qle_bool_iff in valid_error. + apply Qle_Rle in valid_error. + repeat rewrite Q2R_plus in valid_error. + repeat rewrite Q2R_mult in valid_error. + repeat rewrite Q2R_plus in valid_error. + repeat rewrite <- Rabs_eq_Qabs in valid_error. + repeat rewrite Q2R_plus in valid_error. + repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error. + eapply Rle_trans; eauto. + clear absenv_e1 absenv_e2 absenv_e3 valid_error e e1 e2 e3 absenv_fma + H L R1 R0 R e1_real e2_real e3_real e1_float e2_float e3_float eval_real eval_float. + apply Rplus_le_compat. + - eauto using Rle_trans, Rabs_triang, Rplus_le_compat, multiplicationErrorBounded. + - apply Rmult_le_compat_r; auto using mTypeToQ_pos_R. + remember (multIntv (widenIntv (e2lo, e2hi) err2) (widenIntv (e3lo, e3hi) err3)) as iv_prod. + remember (addIntv (widenIntv (e1lo, e1hi) err1) iv_prod) as iv_sum. + iv_assert iv_sum iv_unf. + destruct iv_unf as [ivl [ivh iv_unf]]. + rewrite iv_unf. + rewrite <- maxAbs_impl_RmaxAbs. + assert (ivlo iv_sum = ivl) by (rewrite iv_unf; auto). + assert (ivhi iv_sum = ivh) by (rewrite iv_unf; auto). + rewrite <- H, <- H0. + assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. + pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded). + assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. + pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded). + assert (contained nR3 (Q2R e3lo, Q2R e3hi)) as contained_intv3 by auto. + pose proof (distance_gives_iv (a:=nR3) _ _ contained_intv3 err3_bounded). + pose proof (IntervalArith.interval_multiplication_valid _ _ H2 H3). + pose proof (IntervalArith.interval_addition_valid _ _ H1 H4). + (* simpl in *. *) + destruct H5, H4. + unfold RmaxAbsFun. + subst. + apply RmaxAbs; subst; simpl in *. + unfold RmaxAbsFun. + + clear H6. + rewrite Q2R_min4. + repeat rewrite Q2R_mult; + repeat rewrite Q2R_minus; + repeat rewrite Q2R_plus; + repeat rewrite Q2R_minus; eauto. + + rewrite Q2R_max4. + repeat rewrite Q2R_mult; + repeat rewrite Q2R_minus; + repeat rewrite Q2R_plus; auto. + rewrite <- maxAbs_impl_RmaxAbs. Admitted. Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars: diff --git a/coq/Expressions.v b/coq/Expressions.v index c3aedeb31801e9872fbe8fb969baed1d1abf3a7d..d61210db4b846d804837b686458d6a37ae53fe40 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -92,7 +92,7 @@ Definition evalUnop (o:unop) (v:R):= end . Definition evalFma (v1:R) (v2:R) (v3:R):= - Rplus v1 (Rmult v2 v3). + evalBinop Plus v1 (evalBinop Mult v2 v3). (** Define expressions parametric over some value type V. diff --git a/coq/Infra/Ltacs.v b/coq/Infra/Ltacs.v index f7e2ae30e1d10bd6b950ae86755adf0e51a946c4..25be598d7df7f508230c2f5568e7d70beb8494d0 100644 --- a/coq/Infra/Ltacs.v +++ b/coq/Infra/Ltacs.v @@ -65,11 +65,6 @@ Ltac NatSet_prop := | _ => try auto end. -Ltac match_simpl := - match goal with - | [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl - end. - Ltac destruct_if := match goal with | [H: (if ?c then ?a else ?b) = _ |- _ ] => @@ -80,6 +75,60 @@ Ltac destruct_if := try congruence end. +Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) := +match v with +|Some val => f val +| None => e +end. + +Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y): +match v with |Some val => f val | None => e end = optionLift X Y v f e. +Proof. +cbv; auto. +Qed. + +Lemma optionLift_cond X (a:bool) (b c :X): +(if a then b else c) = match a with |true => b |false => c end. +Proof. +cbv; auto. +Qed. + +Ltac remove_matches := rewrite optionLift_eq in *. + +Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *. + +Ltac match_factorize := +match goal with +| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]] +=> rewrite H; cbn +| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ] +=> rewrite H1 in H2; cbn in H2 +| [ H: context [optionLift _ _ ?t _ _] |- _ ] +=> destruct t eqn:?; cbn in H; try congruence +| [ |- context [optionLift _ _ ?t _ _] ] +=> destruct t eqn:?; cbn; try congruence +end. + +Ltac pair_factorize := +match goal with +| [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H +end. + +Ltac match_simpl := +try remove_conds; +try remove_matches; +repeat match_factorize; +try pair_factorize. + +Ltac bool_factorize := +match goal with +| [H: _ = true |- _] => andb_to_prop H +end. + +Ltac Daisy_compute := +repeat +(match_simpl || bool_factorize). + (* HOL4 Style patter matching tactics *) Tactic Notation "lift " tactic(t) := fun H => t H. @@ -87,4 +136,4 @@ Tactic Notation "lift " tactic(t) := Tactic Notation "match_pat" open_constr(pat) tactic(t) := match goal with | [H: ?ty |- _ ] => unify pat ty; t H - end. \ No newline at end of file + end. diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 157f23e1642d3e7b0b2704acb9db15d7bc503851..a2011792b11361329f117cc8a79551137d26560c 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -440,6 +440,7 @@ Proof. repeat rewrite <- Q2R_min4, <- Q2R_max4 in *. specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul). unfold evalFma. + unfold evalBinop. unfold perturb. lra. - env_assert absenv (Downcast m f) absenv_d;