Commit be020b3f authored by Heiko Becker's avatar Heiko Becker

Get rid of annoying warning about 'Focus' in ErrorBounds.v

parent 19f50a82
......@@ -88,12 +88,12 @@ Proof.
apply Rabs_triang; apply Rplus_le_compat; try auto.
rewrite Rplus_0_r.
apply Rplus_le_compat; try auto. }
Focus 4.
eapply Rle_trans; [ apply Rabs_triang | rewrite (Rplus_assoc (Q2R err1)) ].
apply Rplus_le_compat; try auto.
eapply Rle_trans; [ apply Rabs_triang |].
apply Rplus_le_compat; try auto.
rewrite Rabs_Ropp; simpl. auto.
4: {
eapply Rle_trans; [ apply Rabs_triang | rewrite (Rplus_assoc (Q2R err1)) ].
apply Rplus_le_compat; try auto.
eapply Rle_trans; [ apply Rabs_triang |].
apply Rplus_le_compat; try auto.
rewrite Rabs_Ropp; simpl. auto. }
all: eapply Rle_trans; try eapply H.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -164,7 +164,7 @@ Proof.
apply Rplus_le_compat; try auto.
rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
auto. }
Focus 4.
4: {
eapply Rle_trans.
apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
apply Rplus_le_compat; try auto.
......@@ -172,8 +172,7 @@ Proof.
apply Rabs_triang.
rewrite Rabs_Ropp. apply Rplus_le_compat; try auto.
rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
auto.
auto. }
all: eapply Rle_trans; try eapply Rabs_triang.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -336,14 +335,13 @@ Proof.
unfold computeErrorR.
destruct m; rewrite Ropp_plus_distr.
{ rewrite Rplus_0_r; hnf; right; f_equal; lra. }
Focus 4.
rewrite <- Rplus_assoc.
eapply Rle_trans.
eapply Rabs_triang.
rewrite Rabs_Ropp.
eapply Rplus_le_compat; try auto.
hnf; right; f_equal; lra.
4: {
rewrite <- Rplus_assoc.
eapply Rle_trans.
eapply Rabs_triang.
rewrite Rabs_Ropp.
eapply Rplus_le_compat; try auto.
hnf; right; f_equal; lra. }
all: repeat rewrite <- Rplus_assoc.
all: setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
all: repeat rewrite Rsub_eq_Ropp_Rplus.
......
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