diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 15:19:01 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 15:19:01 +0100 |
| commit | bfbcc770319a0d3b8935314b16f1e0c205436685 (patch) | |
| tree | 3598bf35120a6657ed87a6bdd93d7d6c50f0b4b1 /lib | |
| parent | b08a818cbc7872b1a062a80ea478b2e32e3a3746 (diff) | |
| download | compcert-kvx-bfbcc770319a0d3b8935314b16f1e0c205436685.tar.gz compcert-kvx-bfbcc770319a0d3b8935314b16f1e0c205436685.zip | |
progress on ZnearestE
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 78 |
1 files changed, 54 insertions, 24 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index a0ae3089..edb3f105 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1031,19 +1031,18 @@ Proof. generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros. set (p2p := (Z.pow_pos 2 p)) in *. set (zm := Z.pos m) in *. + assert (p2p > 0) as POS by lia. + assert (0 < IZR p2p)%R as POS2. + { apply IZR_lt. assumption. } unfold Zdiv_ne, Z.succ in *. case Z.compare_spec; intro CMP. * admit. * symmetry. apply Znearest_imp with (n := zm / p2p). - apply Rabs_lt. - split. - { assert (p2p > 0) as POS by lia. - pose proof (Z_mult_div_ge zm p2p POS). + apply Rabs_lt. split. + ** 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. @@ -1055,24 +1054,55 @@ Proof. 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. - rewrite <- mult_IZR. - rewrite <- plus_IZR. - apply IZR_lt. - lia. } - assert (0 < IZR p2p)%R. - { apply IZR_lt. assumption. } - 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. - lra. - * admit. + ** assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT. + { rewrite <- mult_IZR. + rewrite <- minus_IZR. + rewrite <- mult_IZR. + rewrite <- plus_IZR. + apply IZR_lt. + 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. + lra. + * symmetry. + apply Znearest_imp. + apply Rabs_lt. split. + ** assert (0 < (IZR zm - IZR p2p * IZR (zm / p2p)) - (IZR p2p * (IZR (zm / p2p) + 1) - IZR zm))%R. + { ring_simplify. + rewrite <- mult_IZR. + rewrite <- mult_IZR. + rewrite <- mult_IZR. + rewrite <- minus_IZR. + rewrite <- minus_IZR. + apply IZR_lt. + lia. + } + 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. + 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. + rewrite <- mult_IZR. + rewrite <- minus_IZR. + apply IZR_lt. + pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. + ring_simplify. + set (q := (zm / p2p)) in *. + pose proof (Z_mod_lt zm p2p POS) as MOD. + lia. Admitted. |