diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 21:47:42 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 21:47:42 +0100 |
| commit | 0be6b3d13d2e8920653dde8cf8f7e27af608d812 (patch) | |
| tree | c6238c08af795ddbd10271cba038a480201da894 /lib | |
| parent | 75ae1bbac93b1f3cdbdd16a266c5658a28bde90c (diff) | |
| download | compcert-kvx-0be6b3d13d2e8920653dde8cf8f7e27af608d812.tar.gz compcert-kvx-0be6b3d13d2e8920653dde8cf8f7e27af608d812.zip | |
beautify proof
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 40 |
1 files changed, 16 insertions, 24 deletions
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. |