From df6918762b58dcda4913d7f15b61bd64673af567 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 11 Feb 2022 17:56:31 +0100 Subject: moved stuff to appropriate places and removed irrelevant content --- lib/IEEE754_extra.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'lib') 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. -- cgit