Commit 4e20a38b authored by Heiko Becker's avatar Heiko Becker

More simplifications in Coq

parent ee1be324
......@@ -952,7 +952,8 @@ Proof.
as bound_neg_nR1
by (apply Rmult_le_compat_r; auto).
unfold invertInterval in *; simpl in upperBound_nR2, upperBound_Ropp_nR2.
(* Case distinction for the divisor range *)
(* Case distinction for the divisor range
positive or negative in float and real valued execution *)
destruct no_div_zero_real as [ real_iv_neg | real_iv_pos];
destruct no_div_zero_float as [float_iv_neg | float_iv_pos].
(* The range of the divisor lies in the range from -infinity until 0 *)
......@@ -980,6 +981,7 @@ Proof.
assert (nF1 <= Q2R err1 + nR1)%R as ub_nF1 by lra.
assert (nR1 - Q2R err1 <= nF1)%R as lb_nF1 by lra.
destruct err2_bounded as [[nR2_sub_pos err2_bounded] | [nR2_sub_neg err2_bounded]].
(* Positive case for abs (nR2 - nF2) <= err2 *)
{ rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive.
apply Rgt_lt in nR2_sub_pos.
assert (nF2 < nR2)%R as nF2_le_nR2 by lra.
......@@ -996,10 +998,12 @@ Proof.
(* Next do a case distinction for the absolute value*)
unfold Rabs.
destruct Rcase_abs.
(* Case 1: Absolute value negative *)
- rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr.
rewrite Ropp_involutive.
(* To upper bound terms, do a case distinction for nF1 *)
destruct (Rle_lt_dec 0 nF1).
(* 0 <= nF1 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_l; try lra.
......@@ -1025,7 +1029,8 @@ Proof.
apply lb_nF1.
rewrite (Rmult_comm (Q2R err2) _).
remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv.
assert (- (nR1 * / nR2) + (/ nR2 + err_inv) * (nR1 - Q2R err1) = nR1 * err_inv - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R
assert (- (nR1 * / nR2) + (/ nR2 + err_inv) * (nR1 - Q2R err1) =
nR1 * err_inv - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R
as simpl_properr by lra.
rewrite simpl_properr.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -1042,6 +1047,7 @@ Proof.
- assert (0 <= (Q2R err1 * err_inv))%R
by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra).
apply (Rle_trans _ 0); lra. }
(* nF1 < 0 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_neg_l; try lra.
......@@ -1086,9 +1092,10 @@ Proof.
{ apply Rmult_le_compat_r; try lra. }
{ apply Rmult_le_compat_r; try lra.
repeat (rewrite Q2R_inv; try auto). }
- rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_mult_distr_l.
(* Case 2: Absolute value positive *)
- rewrite Rsub_eq_Ropp_Rplus, Ropp_mult_distr_l.
destruct (Rle_lt_dec 0 (- nF1)).
(* 0 <= - nF1 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_l; try lra.
......@@ -1132,6 +1139,7 @@ Proof.
- assert (0 <= (Q2R err1 * err_inv))%R
by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra).
apply (Rle_trans _ 0); lra. }
(* - nF1 <= 0 *)
+ eapply Rle_trans.
eapply Rplus_le_compat_l.
eapply Rmult_le_compat_neg_l; try lra.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment