diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 19:53:15 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 19:53:15 +0100 |
| commit | 75ae1bbac93b1f3cdbdd16a266c5658a28bde90c (patch) | |
| tree | dce1454d7aa3972e5593cf8ba48d8def3783c1ba /lib | |
| parent | 66376f2e1b66b9a68a4d21454c4b145c1d363a27 (diff) | |
| download | compcert-kvx-75ae1bbac93b1f3cdbdd16a266c5658a28bde90c.tar.gz compcert-kvx-75ae1bbac93b1f3cdbdd16a266c5658a28bde90c.zip | |
ZofB_ne_correct
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index d9329960..28da42ee 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1066,6 +1066,16 @@ Proof. 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]. + rewrite <- mult_IZR. + rewrite <- mult_IZR. + rewrite <- mult_IZR. + rewrite <- plus_IZR. + rewrite <- minus_IZR. + replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia. + field. lra. * symmetry. apply Znearest_imp with (n := zm / p2p). apply Rabs_lt. split. |