diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 17:56:31 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 17:56:31 +0100 |
| commit | df6918762b58dcda4913d7f15b61bd64673af567 (patch) | |
| tree | 399df240af24d7cf511bad6d173b146da7a4839f /lib | |
| parent | f6e1cd79c17461d50f5119818e788d1e07451ef6 (diff) | |
| download | compcert-kvx-df6918762b58dcda4913d7f15b61bd64673af567.tar.gz compcert-kvx-df6918762b58dcda4913d7f15b61bd64673af567.zip | |
moved stuff to appropriate places and removed irrelevant content
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 636ea1ff..35feb29d 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -29,6 +29,24 @@ Require Import Coq.Logic.FunctionalExtensionality. Local Open Scope Z_scope. +Lemma Znearest_lub : + forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z. +Proof. + intros until x. intro BND. + pose proof (Zfloor_lub n x BND). + pose proof (Znearest_ge_floor choice x). + lia. +Qed. + +Lemma Znearest_glb : + forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z. +Proof. + intros until x. intro BND. + pose proof (Zceil_glb n x BND). + pose proof (Znearest_le_ceil choice x). + lia. +Qed. + Lemma Znearest_IZR : forall choice n, (Znearest choice (IZR n)) = n. Proof. |