diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 22:37:29 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-10 22:37:29 +0100 |
| commit | d2669ab4948104c85b795c15a47df98f0b81a40c (patch) | |
| tree | 72f8ab987f24a034c6714d7e74593a10b6dd18f0 /lib | |
| parent | 9d4528e4edaa2b968d52628e6b5c10e6640f5e03 (diff) | |
| download | compcert-kvx-d2669ab4948104c85b795c15a47df98f0b81a40c.tar.gz compcert-kvx-d2669ab4948104c85b795c15a47df98f0b81a40c.zip | |
factor proofs
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 21 |
1 files changed, 20 insertions, 1 deletions
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]. |