diff options
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. |