diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-06 19:34:23 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-06 19:34:23 +0100 |
| commit | 54e63022f92795ab9ffa5c67023a98b7d30ebc69 (patch) | |
| tree | 2172e173a54ff470ddd05a6a967bb97d0d5a16b8 /lib | |
| parent | 9e62bc5ba6af27e47b7d3f22cef8c2dd24a8fc5e (diff) | |
| download | compcert-kvx-54e63022f92795ab9ffa5c67023a98b7d30ebc69.tar.gz compcert-kvx-54e63022f92795ab9ffa5c67023a98b7d30ebc69.zip | |
Zdiv_ne
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index b0d1944e..d2372f17 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -879,6 +879,17 @@ Proof. unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto. Qed. +(** ZofB_ne : convert float to integer, round to nearest *) + +Definition Zdiv_ne (a b : Z) := + let q := Z.div a b in + let q1 := Z.succ q in + match Z.compare (a-b*q) (b*q1-a) with + | Lt => q + | Gt => q1 + | Eq => (if Z.even q then q else q1) + end. + (** ** Algebraic identities *) (** Commutativity of addition and multiplication *) |