diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-08 22:32:41 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-08 22:32:41 +0100 |
| commit | b08a818cbc7872b1a062a80ea478b2e32e3a3746 (patch) | |
| tree | 0c5234adf1f7bf0e2b35cf522556246ddef2d74a /lib | |
| parent | 3ee28038f0596aaa89b72ffb6e905610c259b8b2 (diff) | |
| download | compcert-kvx-b08a818cbc7872b1a062a80ea478b2e32e3a3746.tar.gz compcert-kvx-b08a818cbc7872b1a062a80ea478b2e32e3a3746.zip | |
ZofB_ne_correct unfinished
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 56b90727..a0ae3089 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1038,7 +1038,24 @@ Proof. apply Znearest_imp with (n := zm / p2p). apply Rabs_lt. split. - { admit. } + { assert (p2p > 0) as POS by lia. + pose proof (Z_mult_div_ge zm p2p POS). + assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R. + 2: lra. + assert (0 < IZR p2p)%R as POS2. + { apply IZR_lt. lia. } + field_simplify. + 2: lra. + apply Rmult_le_pos. + { rewrite <- mult_IZR. + rewrite <- minus_IZR. + apply IZR_le. + lia. + } + assert (0 < / IZR p2p)%R. + 2: lra. + apply Rinv_0_lt_compat. assumption. + } assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT. { rewrite <- mult_IZR. rewrite <- minus_IZR. |