diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 19:02:35 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 19:39:41 +0100 |
| commit | d3f9053b783714151aab27eb153f1b727e843ad1 (patch) | |
| tree | fc6b2908f479275197983ce8d1636a2803697785 /lib | |
| parent | bfbcc770319a0d3b8935314b16f1e0c205436685 (diff) | |
| download | compcert-kvx-d3f9053b783714151aab27eb153f1b727e843ad1.tar.gz compcert-kvx-d3f9053b783714151aab27eb153f1b727e843ad1.zip | |
ZofB_ne_correct
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 33 |
1 files changed, 31 insertions, 2 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index edb3f105..d9329960 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1036,7 +1036,36 @@ Proof. { apply IZR_lt. assumption. } unfold Zdiv_ne, Z.succ in *. case Z.compare_spec; intro CMP. - * admit. + * pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. + destruct (Z_mod_lt zm p2p POS) as [MOD1 MOD2]. + set (q := zm / p2p) in *. + set (r := zm mod p2p) in *. + rewrite inbetween_int_NE with (m := q) (l := loc_Inexact Eq). + { cbn. unfold cond_incr. + destruct Z.even; reflexivity. + } + constructor. + split. + ** assert (0 < IZR zm / IZR p2p - IZR q)%R. + 2: lra. + field_simplify. + 2: lra. + apply Rdiv_lt_0_compat. + 2: lra. + 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. + rewrite <- mult_IZR. + rewrite <- minus_IZR. + apply IZR_lt. + lia. * symmetry. apply Znearest_imp with (n := zm / p2p). apply Rabs_lt. split. @@ -1103,7 +1132,7 @@ Proof. set (q := (zm / p2p)) in *. pose proof (Z_mod_lt zm p2p POS) as MOD. lia. -Admitted. +Qed. (** ** Algebraic identities *) |