diff options
Diffstat (limited to 'flocq/Core/Generic_fmt.v')
| -rw-r--r-- | flocq/Core/Generic_fmt.v | 34 |
1 files changed, 30 insertions, 4 deletions
diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index af1bf3c1..a74c81b9 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * What is a real number belonging to a format, and many properties. *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Float_prop. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Float_prop. Section Generic. @@ -427,7 +428,7 @@ rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. -clear ; zify ; lia. +clear ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. @@ -1579,6 +1580,31 @@ apply Zlt_le_succ. now apply mag_gt_bpow. Qed. +Lemma lt_cexp_pos : + forall x y, + (0 < y)%R -> + (cexp x < cexp y)%Z -> + (x < y)%R. +Proof. +intros x y Zy He. +unfold cexp in He. +apply (lt_mag beta) with (1 := Zy). +generalize (monotone_exp (mag beta y) (mag beta x)). +lia. +Qed. + +Theorem lt_cexp : + forall x y, + (y <> 0)%R -> + (cexp x < cexp y)%Z -> + (Rabs x < Rabs y)%R. +Proof. +intros x y Zy He. +apply lt_cexp_pos. +now apply Rabs_pos_lt. +now rewrite 2!cexp_abs. +Qed. + Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. @@ -1804,7 +1830,7 @@ Theorem Znearest_imp : Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. -clear ; zify ; lia. +clear ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. |