Commit 7d6b6460 by Heiko Becker

### Beautification of error validator in Coq and simplify inversion proofs

parent ae4c9be8
 ... ... @@ -234,279 +234,181 @@ Proof. apply Rabs_pos. Qed. Lemma err_prop_inversion_pos nF2 nR2 err2 (e2lo e2hi:Q) (float_iv_pos : (Q2R 0 < Q2R (e2lo - err2))%R) (real_iv_pos : (Q2R 0 < Q2R e2lo)%R) (err2_bounded : (Rabs (nR2 - nF2) <= Q2R err2)%R) (valid_bounds_e2 : (Q2R e2lo <= nR2 <= Q2R e2hi)%R) (valid_bounds_e2_err : (Q2R e2lo - Q2R err2 <= nF2 <= Q2R e2hi + Q2R err2)%R) (err2_pos : (0 <= Q2R err2)%R): (Rabs (/nR2 - / nF2) <= Q2R err2 * / ((Q2R e2lo- Q2R err2) * (Q2R e2lo- Q2R err2)))%R. Lemma err_prop_inversion_pos_real nF nR err elo ehi (float_iv_pos : (0 < elo - err)%R) (real_iv_pos : (0 < elo)%R) (err_bounded : (Rabs (nR - nF) <= err)%R) (valid_bounds_e2 : (elo <= nR <= ehi)%R) (valid_bounds_e2_err : (elo - err <= nF <= ehi + err)%R) (err_pos : (0 <= err)%R): (Rabs (/nR - / nF) <= err * / ((elo - err) * (elo- err)))%R. Proof. unfold Rabs in err2_bounded. destruct Rcase_abs in err2_bounded. - rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr in err2_bounded. rewrite Ropp_involutive in err2_bounded. assert (nF2 <= nR2 + Q2R err2)%R by lra. assert (nR2 - Q2R err2 <= nF2)%R by lra. assert (0 < nR2 - Q2R err2)%R. + rewrite <- Q2R0_is_0. eapply Rlt_le_trans. apply float_iv_pos. rewrite Q2R_minus; lra. + assert (0 < nF2)%R by (rewrite <- Q2R0_is_0; lra). apply Rinv_le_contravar in H; try auto. apply Rinv_le_contravar in H0; try auto. assert (nR2 < nF2)%R by lra. apply Rinv_lt_contravar in H3. * assert (0 < /nR2 - /nF2)%R by lra. rewrite Rabs_right; try lra. repeat rewrite Rsub_eq_Ropp_Rplus. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Ropp_le_contravar. apply H. rewrite Ropp_inv_permute; try lra. rewrite Rabs_case_inverted in err_bounded. assert (0 < nF)%R as nF_pos by lra. destruct err_bounded as [ [diff_pos err_bounded] | [diff_neg err_bounded]]. - cut (0 < /nF - / nR)%R. + intros abs_neg. rewrite Rabs_left; try lra. rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive. rewrite Ropp_inv_permute; try lra. apply (Rle_trans _ (/ - nR + / (nR - err))). * apply Rplus_le_compat_l. apply Rinv_le_contravar; lra. * rewrite equal_naming_inv; try lra. assert (- nR + (nR - err) = - err)%R as simplify_up by lra. rewrite simplify_up. unfold Rdiv. repeat(rewrite <- Ropp_mult_distr_l); rewrite <- Ropp_inv_permute. { rewrite <- Ropp_mult_distr_r, Ropp_involutive. apply Rmult_le_compat_l; try lra. apply Rinv_le_contravar. - apply Rmult_0_lt_preserving; lra. - apply Rmult_le_compat; lra. } { assert (0 < nR * (nR - err))%R by (apply Rmult_0_lt_preserving; lra); lra. } + cut (/ nR < /nF)%R. * intros; lra. * apply Rinv_lt_contravar; try lra. apply Rmult_0_lt_preserving; lra. - cut (0 <= /nR - /nF)%R. + intros abs_pos. rewrite Rabs_right; try lra. rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive in err_bounded. rewrite Rsub_eq_Ropp_Rplus. apply (Rle_trans _ (/nR - / (nR + err))). * apply Rplus_le_compat_l. apply Ropp_le_contravar. apply Rinv_le_contravar; lra. * rewrite Rsub_eq_Ropp_Rplus, Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (nR + - (nR + err) = - err)%R as simpl_up by lra. rewrite simpl_up. unfold Rdiv. rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute. { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. - apply Rmult_0_lt_preserving; lra. - apply Rmult_le_compat; lra. } { assert (0 < nR * (nR + err))%R by (apply Rmult_0_lt_preserving; lra); lra. } + cut (/nF <= /nR)%R. * intros; lra. * apply Rinv_le_contravar; try lra. Qed. Lemma err_prop_inversion_pos nF nR err (elo ehi:Q) (float_iv_pos : (Q2R 0 < Q2R (elo - err))%R) (real_iv_pos : (Q2R 0 < Q2R elo)%R) (err_bounded : (Rabs (nR - nF) <= Q2R err)%R) (valid_bounds_e2 : (Q2R elo <= nR <= Q2R ehi)%R) (valid_bounds_e2_err : (Q2R elo - Q2R err <= nF <= Q2R ehi + Q2R err)%R) (err_pos : (0 <= Q2R err)%R): (Rabs (/nR - / nF) <= Q2R err * / ((Q2R elo- Q2R err) * (Q2R elo- Q2R err)))%R. Proof. eapply err_prop_inversion_pos_real; try rewrite <- Q2R0_is_0; eauto. rewrite <- Q2R_minus; auto. rewrite Q2R0_is_0; auto. Qed. Lemma err_prop_inversion_neg_real nF nR err elo ehi (float_iv_neg : (ehi + err < 0)%R) (real_iv_neg : (ehi < 0)%R) (err_bounded : (Rabs (nR - nF) <= err)%R) (valid_bounds_e : (elo <= nR <= ehi)%R) (valid_bounds_e_err : (elo - err <= nF <= ehi + err)%R) (err_pos : (0 <= err)%R): (Rabs (/nR - / nF) <= err * / ((ehi + err) * (ehi + err)))%R. Proof. rewrite Rabs_case_inverted in err_bounded. assert (nF < 0)%R as nF_neg by lra. destruct err_bounded as [ [diff_pos err_bounded] | [diff_neg err_bounded]]. - cut (0 < /nF - / nR)%R. + intros abs_neg. rewrite Rabs_left; try lra. rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive. rewrite Ropp_inv_permute; try lra. apply (Rle_trans _ (/ - nR + / (nR - err))). * apply Rplus_le_compat_l. assert (0 < - nF)%R by lra. assert (0 < - (nR - err))%R by lra. assert (nR - err <= nF)%R as nR_lower by lra. apply Ropp_le_contravar in nR_lower. apply Rinv_le_contravar in nR_lower; try lra. repeat (rewrite <- Ropp_inv_permute in nR_lower; try lra). * rewrite equal_naming_inv; try lra. assert (- nR + (nR - err) = - err)%R as simplify_up by lra. rewrite simplify_up. unfold Rdiv. repeat(rewrite <- Ropp_mult_distr_l); rewrite <- Ropp_inv_permute. { rewrite <- Ropp_mult_distr_r, Ropp_involutive. apply Rmult_le_compat_l; try lra. apply Rinv_le_contravar. - apply Rmult_lt_0_inverting; lra. - eapply Rle_trans. eapply Rmult_le_compat_neg_l; try lra. instantiate (1 := (nR - err)%R); try lra. setoid_rewrite Rmult_comm. eapply Rmult_le_compat_neg_l; lra. } { assert (0 < nR * (nR - err))%R by (apply Rmult_lt_0_inverting; lra); lra. } + cut (/ nR < /nF)%R. * intros; lra. * apply Rinv_lt_contravar; try lra. apply Rmult_lt_0_inverting; lra. - cut (0 <= /nR - /nF)%R. + intros abs_pos. rewrite Rabs_right; try lra. rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive in err_bounded. rewrite Rsub_eq_Ropp_Rplus. apply (Rle_trans _ (/nR - / (nR + err))). * apply Rplus_le_compat_l. apply Ropp_le_contravar. assert (0 < - nF)%R by lra. assert (0 < - (nR + err))%R by lra. assert (nF <= nR + err)%R as nR_upper by lra. apply Ropp_le_contravar in nR_upper. apply Rinv_le_contravar in nR_upper; try lra. repeat (rewrite <- Ropp_inv_permute in nR_upper; try lra). * rewrite Rsub_eq_Ropp_Rplus, Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (nR2 + - (nR2 + Q2R err2) = - Q2R err2)%R by lra. rewrite H5. assert (nR + - (nR + err) = - err)%R as simpl_up by lra. rewrite simpl_up. unfold Rdiv. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r. rewrite <- Ropp_inv_permute. rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute. { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. - rewrite <- Rsub_eq_Ropp_Rplus. apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra. - eapply Rmult_le_compat; try lra; rewrite <- Rsub_eq_Ropp_Rplus; rewrite <- Q2R_minus, <- Q2R0_is_0; lra. } { assert (0 < (nR2 + Q2R err2) * nR2)%R by (apply Rmult_0_lt_preserving; lra); lra. } * apply Rmult_0_lt_preserving; lra. - assert (nF2 <= Q2R err2 + nR2)%R by lra. assert (nR2 - Q2R err2 <= nF2)%R by lra. assert (0 < nR2 - Q2R err2)%R. + rewrite <- Q2R0_is_0. eapply Rlt_le_trans. apply float_iv_pos. rewrite Q2R_minus; lra. + assert (0 < nF2)%R. * rewrite <- Q2R0_is_0. eapply Rlt_le_trans. apply float_iv_pos. rewrite Q2R_minus. lra. * apply Rinv_le_contravar in H; try auto. apply Rinv_le_contravar in H0; try auto. assert (nF2 <= nR2)%R by lra. apply Rinv_le_contravar in H3; try lra. hnf in H3. destruct H3. { assert (0 < /nF2 - /nR2)%R by lra. rewrite Rabs_left; try lra. repeat rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. eapply Rle_trans. eapply Rplus_le_compat_l. apply H0. rewrite Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (- nR2 + (nR2 -Q2R err2) = - Q2R err2)%R by lra. rewrite H5. unfold Rdiv. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_inv_permute. - rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. + rewrite <- Rsub_eq_Ropp_Rplus. apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra. + eapply Rmult_le_compat; try lra; rewrite <- Rsub_eq_Ropp_Rplus; rewrite <- Q2R_minus, <- Q2R0_is_0; lra. - assert (0 < (nR2 - Q2R err2) * nR2)%R by (apply Rmult_0_lt_preserving; lra); lra. } { rewrite Rabs_right; try lra. repeat rewrite Rsub_eq_Ropp_Rplus. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Ropp_le_contravar. apply H. rewrite Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (nR2 + - (Q2R err2 + nR2) = - Q2R err2)%R by lra. rewrite H4. unfold Rdiv. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r. rewrite <- Ropp_inv_permute. - rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. + rewrite <- Rsub_eq_Ropp_Rplus. apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra. + eapply Rmult_le_compat; try lra; rewrite <- Rsub_eq_Ropp_Rplus; rewrite <- Q2R_minus, <- Q2R0_is_0; lra. - assert (0 < nR2 * (Q2R err2 + nR2))%R by (apply Rmult_0_lt_preserving; lra); lra. } - apply Rmult_lt_0_inverting; lra. - eapply Rle_trans. eapply Rmult_le_compat_neg_l; try lra. instantiate (1:= (nR + err)%R); try lra. setoid_rewrite Rmult_comm. eapply Rmult_le_compat_neg_l; lra. } { assert (0 < nR * (nR + err))%R by (apply Rmult_lt_0_inverting; lra); lra. } + cut (/nF <= /nR)%R. * intros; lra. * assert (nR <= nF)%R by lra. assert (- nF <= - nR)%R as le_inv by lra. apply Rinv_le_contravar in le_inv; try lra. repeat (rewrite <- Ropp_inv_permute in le_inv; try lra). Qed. Lemma err_prop_inversion_neg nF2 nR2 err2 (e2lo e2hi:Q) (float_iv_neg : (Q2R (e2hi + err2) < Q2R 0)%R) (real_iv_neg : (Q2R e2hi < Q2R 0)%R) (err2_bounded : (Rabs (nR2 - nF2) <= Q2R err2)%R) (valid_bounds_e2 : (Q2R e2lo <= nR2 <= Q2R e2hi)%R) (valid_bounds_e2_err : (Q2R e2lo - Q2R err2 <= nF2 <= Q2R e2hi + Q2R err2)%R) (err2_pos : (0 <= Q2R err2)%R): (Rabs (/nR2 - / nF2) <= Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R. Lemma err_prop_inversion_neg nF nR err (elo ehi:Q) (float_iv_neg : (Q2R (ehi + err) < Q2R 0)%R) (real_iv_neg : (Q2R ehi < Q2R 0)%R) (err_bounded : (Rabs (nR - nF) <= Q2R err)%R) (valid_bounds_e : (Q2R elo <= nR <= Q2R ehi)%R) (valid_bounds_e_err : (Q2R elo - Q2R err <= nF <= Q2R ehi + Q2R err)%R) (err_pos : (0 <= Q2R err)%R): (Rabs (/nR - / nF) <= Q2R err * / ((Q2R ehi + Q2R err) * (Q2R ehi + Q2R err)))%R. Proof. unfold Rabs in err2_bounded. destruct Rcase_abs in err2_bounded. - rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr in err2_bounded. rewrite Ropp_involutive in err2_bounded. assert (nF2 <= nR2 + Q2R err2)%R by lra. assert (nR2 - Q2R err2 <= nF2)%R by lra. assert (nR2 + Q2R err2 < 0)%R. + rewrite <- Q2R0_is_0. eapply Rle_lt_trans. Focus 2. apply float_iv_neg. rewrite Q2R_plus; lra. + assert (0 < - (nR2 + Q2R err2))%R by lra. assert (nF2 < 0)%R. * rewrite <- Q2R0_is_0; eapply Rle_lt_trans. apply H. eapply Rle_lt_trans. Focus 2. apply float_iv_neg. rewrite Q2R_plus; lra. * assert (0 < - nF2)%R by lra. apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H. apply Rinv_le_contravar in H0; try auto. apply Rinv_le_contravar in H; try auto. repeat (rewrite <- Ropp_inv_permute in H0; try lra). repeat (rewrite <- Ropp_inv_permute in H; try lra). apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H. repeat (rewrite Ropp_involutive in H, H0). assert (nR2 < nF2)%R by lra. apply Ropp_lt_contravar in H5. apply Rinv_lt_contravar in H5. { rewrite <- Ropp_inv_permute in H5; try lra. rewrite <- Ropp_inv_permute in H5; try lra. apply Ropp_lt_contravar in H5. assert (0 < /nR2 - /nF2)%R by lra. rewrite Rabs_right; try lra. repeat rewrite Rsub_eq_Ropp_Rplus. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Ropp_le_contravar. apply H. rewrite Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (nR2 + - (nR2 + Q2R err2) = - Q2R err2)%R by lra. rewrite H7. unfold Rdiv. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r. rewrite <- Ropp_inv_permute. - rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. + apply Rmult_lt_0_inverting; rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; try lra. + destruct valid_bounds_e2_err, valid_bounds_e2. eapply Rle_trans. eapply Rmult_le_compat_neg_l. rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; hnf; left; auto. eapply Rle_trans. apply H11. lra. setoid_rewrite Rmult_comm at 1. eapply Rmult_le_compat_neg_l. hnf; left; lra. lra. - assert (0 < (nR2 + Q2R err2) * nR2)%R by (apply Rmult_lt_0_inverting; lra); lra. } { rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive. apply Rmult_lt_0_inverting; lra. } - assert (nF2 <= Q2R err2 + nR2)%R by lra. assert (nR2 - Q2R err2 <= nF2)%R by lra. assert (nR2 + Q2R err2 < 0)%R. + rewrite <- Q2R0_is_0. eapply Rle_lt_trans. Focus 2. apply float_iv_neg. rewrite Q2R_plus; lra. + assert (0 < - (Q2R err2 + nR2))%R by lra. assert (nF2 < 0)%R. * rewrite <- Q2R0_is_0; eapply Rle_lt_trans. apply H. eapply Rle_lt_trans. Focus 2. apply float_iv_neg. rewrite Q2R_plus; lra. * assert (0 < - nF2)%R by lra. apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H. apply Rinv_le_contravar in H0; try auto. apply Rinv_le_contravar in H; try auto. repeat (rewrite <- Ropp_inv_permute in H0; try lra). repeat (rewrite <- Ropp_inv_permute in H; try lra). apply Ropp_le_contravar in H0; apply Ropp_le_contravar in H. repeat (rewrite Ropp_involutive in H, H0). assert (nF2 <= nR2)%R by lra. apply Ropp_le_contravar in H5. apply Rinv_le_contravar in H5; try lra. repeat (rewrite <- Ropp_inv_permute in H5; try lra). apply Ropp_le_contravar in H5. repeat rewrite Ropp_involutive in H5. hnf in H5. destruct H5. { assert (0 < /nF2 - /nR2)%R by lra. rewrite Rabs_left; try lra. repeat rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. eapply Rle_trans. eapply Rplus_le_compat_l. apply H0. rewrite Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (- nR2 + (nR2 - Q2R err2) = - Q2R err2)%R by lra. rewrite H7. unfold Rdiv. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_inv_permute. - rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. + apply Rmult_lt_0_inverting; rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; try lra. + destruct valid_bounds_e2_err, valid_bounds_e2. eapply Rle_trans. eapply Rmult_le_compat_neg_l. rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; hnf; left; auto. eapply Rle_trans. apply H11. lra. setoid_rewrite Rmult_comm at 1. eapply Rmult_le_compat_neg_l. hnf; left; lra. lra. - assert (0 < nR2 * (nR2 - Q2R err2))%R by (apply Rmult_lt_0_inverting; lra); lra. } { rewrite Rabs_right; try lra. repeat rewrite Rsub_eq_Ropp_Rplus. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Ropp_le_contravar. apply H. rewrite Ropp_inv_permute; try lra. rewrite equal_naming_inv; try lra. assert (nR2 + - (Q2R err2 + nR2) = - Q2R err2)%R by lra. rewrite H6. unfold Rdiv. rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r. rewrite <- Ropp_inv_permute. - rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. + apply Rmult_lt_0_inverting; rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; try lra. + destruct valid_bounds_e2_err, valid_bounds_e2. eapply Rle_trans. eapply Rmult_le_compat_neg_l. rewrite <- Q2R_plus; rewrite <- Q2R0_is_0; hnf; left; auto. eapply Rle_trans. apply H10. lra. setoid_rewrite Rmult_comm at 1. eapply Rmult_le_compat_neg_l. hnf; left; lra. lra. - assert (0 < (nR2 + Q2R err2) * nR2)%R by (apply Rmult_lt_0_inverting; lra); lra. } Qed. \ No newline at end of file eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra. rewrite <- Q2R_plus ; auto. apply valid_bounds_e. auto. rewrite Q2R0_is_0; auto. Qed.
 ... ... @@ -14,8 +14,8 @@ Require Import Daisy.IntervalArith Daisy.IntervalArithQ Daisy.ErrorBounds Daisy. Require Import Daisy.Environments. (** Error bound validator **) Fixpoint validErrorbound (e:exp Q) (env:analysisResult) := let (intv, err) := (env e) in Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) := let (intv, err) := (absenv e) in let errPos := Qleb 0 err in match e with |Var _ v => false ... ... @@ -23,9 +23,9 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) := |Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err) |Unop _ _ => false |Binop b e1 e2 => let (ive1, err1) := env e1 in let (ive2, err2) := env e2 in let rec := andb (validErrorbound e1 env) (validErrorbound e2 env) in let (ive1, err1) := absenv e1 in let (ive2, err2) := absenv e2 in let rec := andb (validErrorbound e1 absenv) (validErrorbound e2 absenv) in let errIve1 := widenIntv ive1 err1 in let errIve2 := widenIntv ive2 err2 in let upperBoundE1 := maxAbs ive1 in ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!