diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-07 12:00:54 +0100 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-07 13:39:53 +0100 |
commit | fbead38d40df6904dc0e446f673747b008c40022 (patch) | |
tree | 504c65f349df5cc74e9c710cd20de867030f5b51 /lib | |
parent | c5e74c17f2ab7f40d314417f2b20b18d4d2d057b (diff) | |
download | compcert-kvx-fbead38d40df6904dc0e446f673747b008c40022.tar.gz compcert-kvx-fbead38d40df6904dc0e446f673747b008c40022.zip |
ZnearestE_opp
Diffstat (limited to 'lib')
-rw-r--r-- | lib/IEEE754_extra.v | 87 |
1 files changed, 83 insertions, 4 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 1ee9c2e0..db4fbec7 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -929,12 +929,91 @@ Proof. rewrite Ropp_involutive. reflexivity. Qed. - -Lemma ZnearestE_opp - : forall x : R, ZnearestE (- x) = - ZnearestE x. -Admitted. +Lemma Zceil_non_floor: + forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + apply Zceil_imp. + split. + { rewrite minus_IZR. + rewrite plus_IZR. + lra. + } + rewrite plus_IZR. + pose proof (Zfloor_ub x). + lra. +Qed. + +Lemma Zceil_non_ceil: + forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + cut (Zfloor x = (Zceil x) - 1). { intros; lia. } + apply Zfloor_imp. + split. + { rewrite minus_IZR. + pose proof (Zceil_lb x). + lra. + } + rewrite plus_IZR. + rewrite minus_IZR. + lra. +Qed. +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro x. + unfold ZnearestE. + case (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)); intro CMP. + - pose proof (Zfloor_lb x) as LB. + destruct (Rcompare_spec x (IZR (Zfloor x))) as [ ABSURD | EXACT | INEXACT]. + lra. + { set (n := Zfloor x) in *. + rewrite EXACT. + rewrite <- opp_IZR. + rewrite Zfloor_IZR. + rewrite opp_IZR. + rewrite Rcompare_Lt by lra. + reflexivity. + } + rewrite Rcompare_Gt. + { apply Zceil_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by assumption. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Eq. + { rewrite Zceil_opp. + rewrite Zfloor_opp. + rewrite Z.even_opp. + rewrite Zceil_non_floor by lra. + rewrite Z.even_succ. + rewrite Z.negb_odd. + destruct (Z.even (Zfloor x)); reflexivity. + } + rewrite Zfloor_opp. + rewrite opp_IZR. + ring_simplify. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Lt. + { apply Zfloor_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. +Qed. + Theorem ZofB_ne_correct: forall f, ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. |