From d2669ab4948104c85b795c15a47df98f0b81a40c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Dec 2021 22:37:29 +0100 Subject: factor proofs --- lib/IEEE754_extra.v | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index b8397210..761f218a 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -24,6 +24,8 @@ Require Import Psatz. Require Import Bool. Require Import Eqdep_dec. +Require Import Coq.Logic.FunctionalExtensionality. + Local Open Scope Z_scope. Section Extra_ops. @@ -936,6 +938,23 @@ Proof. reflexivity. Qed. +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro. + rewrite Znearest_opp. + f_equal. + f_equal. + apply functional_extensionality. + intro. + rewrite Z.even_opp. + fold (Z.succ x0). + rewrite Z.even_succ. + f_equal. + apply Z.negb_odd. +Qed. + +(** more complicated way of proving Lemma Zceil_non_floor: forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). Proof. @@ -969,7 +988,6 @@ Proof. lra. Qed. -(* Can be also done with Znearest_opp and functional extensionality *) Lemma ZnearestE_opp : forall x : R, ZnearestE (- x) = - ZnearestE x. Proof. @@ -1020,6 +1038,7 @@ Proof. rewrite plus_IZR. lra. Qed. + *) Ltac field_simplify_den := field_simplify ; [idtac | lra]. Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra]. -- cgit