From 0be6b3d13d2e8920653dde8cf8f7e27af608d812 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Dec 2021 21:47:42 +0100 Subject: beautify proof --- lib/IEEE754_extra.v | 40 ++++++++++++++++------------------------ 1 file changed, 16 insertions(+), 24 deletions(-) (limited to 'lib') diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 28da42ee..2806e572 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1014,7 +1014,10 @@ Proof. rewrite plus_IZR. lra. Qed. - + +Ltac field_simplify_den := field_simplify ; [idtac | lra]. +Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra]. + Theorem ZofB_ne_correct: forall f, ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. @@ -1048,27 +1051,23 @@ Proof. split. ** assert (0 < IZR zm / IZR p2p - IZR q)%R. 2: lra. - field_simplify. - 2: lra. - apply Rdiv_lt_0_compat. - 2: lra. + field_simplify_den. + Rdiv_lt_0_den. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_lt. lia. ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R. 2: lra. - field_simplify. - 2: lra. - apply Rdiv_lt_0_compat. - 2: lra. + field_simplify_den. + Rdiv_lt_0_den. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_lt. lia. ** apply Rcompare_Eq. assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra]. - field_simplify; [idtac | lra]. + field_simplify_den. rewrite <- mult_IZR. rewrite <- mult_IZR. rewrite <- mult_IZR. @@ -1082,8 +1081,7 @@ Proof. ** pose proof (Z_mult_div_ge zm p2p POS). assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R. 2: lra. - field_simplify. - 2: lra. + field_simplify_den. apply Rmult_le_pos. { rewrite <- mult_IZR. rewrite <- minus_IZR. @@ -1102,10 +1100,8 @@ Proof. lia. } assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT. 2: lra. - field_simplify. - 2: lra. - apply Rdiv_lt_0_compat. - 2: lra. + field_simplify_den. + Rdiv_lt_0_den. lra. * symmetry. apply Znearest_imp. @@ -1122,18 +1118,14 @@ Proof. } assert (0 < (/ 2) + IZR zm * / IZR p2p - IZR (zm / p2p + 1))%R. 2: lra. - field_simplify. - 2: lra. - apply Rdiv_lt_0_compat. - 2: lra. + field_simplify_den. + Rdiv_lt_0_den. rewrite plus_IZR. lra. ** assert (0 < IZR (zm / p2p + 1) - (IZR zm * / IZR p2p))%R. 2: lra. - field_simplify. - 2: lra. - apply Rdiv_lt_0_compat. - 2: lra. + field_simplify_den. + Rdiv_lt_0_den. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_lt. -- cgit