diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 23:24:28 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 23:24:28 +0100 |
| commit | 4fb3896a10dac9137157262f532a6a5b6e390cf4 (patch) | |
| tree | f2b2efd7ee3012ec77f0b24bf2d03f05e66d3cfd /lib | |
| parent | d2669ab4948104c85b795c15a47df98f0b81a40c (diff) | |
| download | compcert-kvx-4fb3896a10dac9137157262f532a6a5b6e390cf4.tar.gz compcert-kvx-4fb3896a10dac9137157262f532a6a5b6e390cf4.zip | |
more properties on Znearest
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 37 |
1 files changed, 35 insertions, 2 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 761f218a..ed3d9f1f 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -954,7 +954,6 @@ Proof. apply Z.negb_odd. Qed. -(** more complicated way of proving Lemma Zceil_non_floor: forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). Proof. @@ -971,6 +970,7 @@ Proof. lra. Qed. +(** more complicated way of proving Lemma Zceil_non_ceil: forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x). Proof. @@ -1148,7 +1148,40 @@ Proof. pose proof (Z_mod_lt zm p2p POS) as MOD. lia. Qed. - + + +Lemma Znearest_imp2: + forall choice x, (Rabs (IZR (Znearest choice x) - x) <= /2)%R. +Proof. + intros. + unfold Znearest. + pose proof (Zfloor_lb x) as FL. + pose proof (Zceil_ub x) as CU. + pose proof (Zceil_non_floor x) as NF. + case Rcompare_spec; intro CMP; apply Rabs_le; split; try lra. + - destruct choice; lra. + - destruct choice. 2: lra. + rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. + - rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. +Qed. + +Lemma Rabs_le_rev : forall {a} {b}, (Rabs a <= b -> -b <= a <= b)%R. +Proof. + intros a b ABS. + unfold Rabs in ABS. + destruct Rcase_abs in ABS; lra. +Qed. + +Theorem ZofB_ne_range: + forall f n, ZofB_ne f = Some n -> (IZR n-1/2 <= B2R _ _ f <= IZR n+1/2)%R. +Proof. + intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H. + pose proof (Znearest_imp2 (fun x => negb (Z.even x)) (B2R prec emax f)) as ABS. + pose proof (Rabs_le_rev ABS). + lra. +Qed. (** ** Algebraic identities *) |