From 0af966a42eb60e9af43f9a450d924758a83946c6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Sep 2015 15:41:50 +0200 Subject: Upgrade to Flocq 2.5.0. Note: this version of Flocq is compatible with both Coq 8.4 and 8.5. --- flocq/Core/Fcore_FIX.v | 13 + flocq/Core/Fcore_FLT.v | 71 +- flocq/Core/Fcore_FLX.v | 38 + flocq/Core/Fcore_FTZ.v | 17 +- flocq/Core/Fcore_Raux.v | 185 +++ flocq/Core/Fcore_Zaux.v | 62 + flocq/Core/Fcore_digits.v | 11 +- flocq/Core/Fcore_float_prop.v | 31 + flocq/Core/Fcore_generic_fmt.v | 25 +- flocq/Core/Fcore_rnd.v | 4 +- flocq/Core/Fcore_rnd_ne.v | 8 +- flocq/Core/Fcore_ulp.v | 2906 ++++++++++++++++++++++++++-------------- 12 files changed, 2361 insertions(+), 1010 deletions(-) (limited to 'flocq/Core') diff --git a/flocq/Core/Fcore_FIX.v b/flocq/Core/Fcore_FIX.v index a3b8d4d0..e224a64a 100644 --- a/flocq/Core/Fcore_FIX.v +++ b/flocq/Core/Fcore_FIX.v @@ -22,6 +22,7 @@ Require Import Fcore_Raux. Require Import Fcore_defs. Require Import Fcore_rnd. Require Import Fcore_generic_fmt. +Require Import Fcore_ulp. Require Import Fcore_rnd_ne. Section RND_FIX. @@ -84,4 +85,16 @@ intros ex ey H. apply Zle_refl. Qed. +Theorem ulp_FIX: forall x, ulp beta FIX_exp x = bpow emin. +Proof. +intros x; unfold ulp. +case Req_bool_spec; intros Zx. +case (negligible_exp_spec FIX_exp). +intros T; specialize (T (emin-1)%Z); contradict T. +unfold FIX_exp; omega. +intros n _; reflexivity. +reflexivity. +Qed. + + End RND_FIX. diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v index 273ff69f..372af6ad 100644 --- a/flocq/Core/Fcore_FLT.v +++ b/flocq/Core/Fcore_FLT.v @@ -25,6 +25,7 @@ Require Import Fcore_generic_fmt. Require Import Fcore_float_prop. Require Import Fcore_FLX. Require Import Fcore_FIX. +Require Import Fcore_ulp. Require Import Fcore_rnd_ne. Section RND_FLT. @@ -222,7 +223,6 @@ Theorem generic_format_FLT_FIX : generic_format beta (FIX_exp emin) x -> generic_format beta FLT_exp x. Proof with auto with typeclass_instances. -clear prec_gt_0_. apply generic_inclusion_le... intros e He. unfold FIX_exp. @@ -231,6 +231,75 @@ omega. apply Zle_refl. Qed. +Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R -> + ulp beta FLT_exp x = bpow emin. +Proof with auto with typeclass_instances. +intros x Hx. +unfold ulp; case Req_bool_spec; intros Hx2. +(* x = 0 *) +case (negligible_exp_spec FLT_exp). +intros T; specialize (T (emin-1)%Z); contradict T. +apply Zle_not_lt; unfold FLT_exp. +apply Zle_trans with (2:=Z.le_max_r _ _); omega. +assert (V:FLT_exp emin = emin). +unfold FLT_exp; apply Z.max_r. +unfold Prec_gt_0 in prec_gt_0_; omega. +intros n H2; rewrite <-V. +apply f_equal, fexp_negligible_exp_eq... +omega. +(* x <> 0 *) +apply f_equal; unfold canonic_exp, FLT_exp. +apply Z.max_r. +assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega]. +destruct (ln_beta beta x) as (e,He); simpl. +apply lt_bpow with beta. +apply Rle_lt_trans with (2:=Hx). +now apply He. +Qed. + +Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R -> + (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R. +Proof. +intros x Hx. +assert (x <> 0)%R. +intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt. +rewrite Z, Rabs_R0; apply bpow_gt_0. +rewrite ulp_neq_0; try assumption. +unfold canonic_exp, FLT_exp. +destruct (ln_beta beta x) as (e,He). +apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R. +rewrite <- bpow_plus. +right; apply f_equal. +apply trans_eq with (e-prec)%Z;[idtac|ring]. +simpl; apply Z.max_l. +assert (emin+prec <= e)%Z; try omega. +apply le_bpow with beta. +apply Rle_trans with (1:=Hx). +left; now apply He. +apply Rmult_le_compat_r. +apply bpow_ge_0. +now apply He. +Qed. + + +Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R. +Proof. +intros x; case (Req_dec x 0); intros Hx. +rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0. +rewrite Rabs_R0; apply bpow_gt_0. +rewrite ulp_neq_0; try exact Hx. +unfold canonic_exp, FLT_exp. +apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R. +apply Rmult_lt_compat_r. +apply bpow_gt_0. +now apply bpow_ln_beta_gt. +rewrite <- bpow_plus. +apply bpow_le. +apply Z.le_max_l. +Qed. + + + (** FLT is a nice format: it has a monotone exponent... *) Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. Proof. diff --git a/flocq/Core/Fcore_FLX.v b/flocq/Core/Fcore_FLX.v index 800540f2..55f6db61 100644 --- a/flocq/Core/Fcore_FLX.v +++ b/flocq/Core/Fcore_FLX.v @@ -24,6 +24,7 @@ Require Import Fcore_rnd. Require Import Fcore_generic_fmt. Require Import Fcore_float_prop. Require Import Fcore_FIX. +Require Import Fcore_ulp. Require Import Fcore_rnd_ne. Section RND_FLX. @@ -211,6 +212,43 @@ now apply FLXN_format_generic. now apply generic_format_FLXN. Qed. +Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. +Proof. +unfold ulp; rewrite Req_bool_true; trivial. +case (negligible_exp_spec FLX_exp). +intros _; reflexivity. +intros n H2; contradict H2. +unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. +Qed. + +Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R. +Proof. +intros x; case (Req_dec x 0); intros Hx. +rewrite Hx, ulp_FLX_0, Rabs_R0. +right; ring. +rewrite ulp_neq_0; try exact Hx. +unfold canonic_exp, FLX_exp. +replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring. +rewrite bpow_plus. +apply Rmult_le_compat_r. +apply bpow_ge_0. +now apply bpow_ln_beta_le. +Qed. + + +Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R. +Proof. +intros x; case (Req_dec x 0); intros Hx. +rewrite Hx, ulp_FLX_0, Rabs_R0. +right; ring. +rewrite ulp_neq_0; try exact Hx. +unfold canonic_exp, FLX_exp. +unfold Zminus; rewrite bpow_plus. +apply Rmult_le_compat_r. +apply bpow_ge_0. +left; now apply bpow_ln_beta_gt. +Qed. + (** FLX is a nice format: it has a monotone exponent... *) Global Instance FLX_exp_monotone : Monotone_exp FLX_exp. Proof. diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v index 5f3e5337..2ebc7851 100644 --- a/flocq/Core/Fcore_FTZ.v +++ b/flocq/Core/Fcore_FTZ.v @@ -23,6 +23,7 @@ Require Import Fcore_defs. Require Import Fcore_rnd. Require Import Fcore_generic_fmt. Require Import Fcore_float_prop. +Require Import Fcore_ulp. Require Import Fcore_FLX. Section RND_FTZ. @@ -182,7 +183,6 @@ Theorem FTZ_format_FLXN : (bpow (emin + prec - 1) <= Rabs x)%R -> FLXN_format beta prec x -> FTZ_format x. Proof. -clear prec_gt_0_. intros x Hx Fx. apply FTZ_format_generic. apply generic_format_FLXN in Fx. @@ -195,6 +195,21 @@ apply Zle_refl. omega. Qed. +Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1). +Proof with auto with typeclass_instances. +unfold ulp; rewrite Req_bool_true; trivial. +case (negligible_exp_spec FTZ_exp). +intros T; specialize (T (emin-1)%Z); contradict T. +apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_. +rewrite Zlt_bool_true; omega. +assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z). +unfold FTZ_exp; rewrite Zlt_bool_true; omega. +intros n H2; rewrite <-V. +apply f_equal, fexp_negligible_exp_eq... +omega. +Qed. + + Section FTZ_round. (** Rounding with FTZ *) diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index 3758324f..d728e0ba 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -207,6 +207,27 @@ rewrite 3!(Rmult_comm r). now apply Rmult_min_distr_r. Qed. +Lemma Rmin_opp: forall x y, (Rmin (-x) (-y) = - Rmax x y)%R. +Proof. +intros x y. +apply Rmax_case_strong; intros H. +rewrite Rmin_left; trivial. +now apply Ropp_le_contravar. +rewrite Rmin_right; trivial. +now apply Ropp_le_contravar. +Qed. + +Lemma Rmax_opp: forall x y, (Rmax (-x) (-y) = - Rmin x y)%R. +Proof. +intros x y. +apply Rmin_case_strong; intros H. +rewrite Rmax_left; trivial. +now apply Ropp_le_contravar. +rewrite Rmax_right; trivial. +now apply Ropp_le_contravar. +Qed. + + Theorem exp_le : forall x y : R, (x <= y)%R -> (exp x <= exp y)%R. @@ -1930,6 +1951,16 @@ destruct (ln_beta x) as (ex, Ex) ; simpl. now apply Ex. Qed. +Theorem bpow_ln_beta_le : + forall x, (x <> 0)%R -> + (bpow (ln_beta x-1) <= Rabs x)%R. +Proof. +intros x Hx. +destruct (ln_beta x) as (ex, Ex) ; simpl. +now apply Ex. +Qed. + + Theorem ln_beta_le_Zpower : forall m e, m <> Z0 -> @@ -2306,6 +2337,160 @@ Qed. End cond_Ropp. + +(** LPO taken from Coquelicot *) + +Theorem LPO_min : + forall P : nat -> Prop, (forall n, P n \/ ~ P n) -> + {n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}. +Proof. +assert (Hi: forall n, (0 < INR n + 1)%R). + intros N. + rewrite <- S_INR. + apply lt_0_INR. + apply lt_0_Sn. +intros P HP. +set (E y := exists n, (P n /\ y = / (INR n + 1))%R \/ (~ P n /\ y = 0)%R). +assert (HE: forall n, P n -> E (/ (INR n + 1))%R). + intros n Pn. + exists n. + left. + now split. +assert (BE: is_upper_bound E 1). + intros x [y [[_ ->]|[_ ->]]]. + rewrite <- Rinv_1 at 2. + apply Rinv_le. + exact Rlt_0_1. + rewrite <- S_INR. + apply (le_INR 1), le_n_S, le_0_n. + exact Rle_0_1. +destruct (completeness E) as [l [ub lub]]. + now exists 1%R. + destruct (HP O) as [H0|H0]. + exists 1%R. + exists O. + left. + apply (conj H0). + rewrite Rplus_0_l. + apply sym_eq, Rinv_1. + exists 0%R. + exists O. + right. + now split. +destruct (Rle_lt_dec l 0) as [Hl|Hl]. + right. + intros n Pn. + apply Rle_not_lt with (1 := Hl). + apply Rlt_le_trans with (/ (INR n + 1))%R. + now apply Rinv_0_lt_compat. + apply ub. + now apply HE. +left. +set (N := Zabs_nat (up (/l) - 2)). +exists N. +assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). + unfold N. + rewrite INR_IZR_INZ. + rewrite inj_Zabs_nat. + replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R. + apply (f_equal (fun v => IZR v + 1)%R). + apply Zabs_eq. + apply Zle_minus_le_0. + apply (Zlt_le_succ 1). + apply lt_IZR. + apply Rle_lt_trans with (/l)%R. + apply Rmult_le_reg_r with (1 := Hl). + rewrite Rmult_1_l, Rinv_l by now apply Rgt_not_eq. + apply lub. + exact BE. + apply archimed. + rewrite minus_IZR. + simpl. + ring. +assert (H: forall i, (i < N)%nat -> ~ P i). + intros i HiN Pi. + unfold is_upper_bound in ub. + refine (Rle_not_lt _ _ (ub (/ (INR i + 1))%R _) _). + now apply HE. + rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. + apply Rinv_1_lt_contravar. + rewrite <- S_INR. + apply (le_INR 1). + apply le_n_S. + apply le_0_n. + apply Rlt_le_trans with (INR N + 1)%R. + apply Rplus_lt_compat_r. + now apply lt_INR. + rewrite HN. + apply Rplus_le_reg_r with (-/l + 1)%R. + ring_simplify. + apply archimed. +destruct (HP N) as [PN|PN]. + now split. +elimtype False. +refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). + intros x [y [[Py ->]|[_ ->]]]. + destruct (eq_nat_dec y N) as [HyN|HyN]. + elim PN. + now rewrite <- HyN. + apply Rinv_le. + apply Hi. + apply Rplus_le_compat_r. + apply Rnot_lt_le. + intros Hy. + refine (H _ _ Py). + apply INR_lt in Hy. + clear -Hy HyN. + omega. + now apply Rlt_le, Rinv_0_lt_compat. +rewrite S_INR, HN. +ring_simplify (IZR (up (/ l)) - 1 + 1)%R. +rewrite <- (Rinv_involutive l) at 2 by now apply Rgt_not_eq. +apply Rinv_1_lt_contravar. +rewrite <- Rinv_1. +apply Rinv_le. +exact Hl. +now apply lub. +apply archimed. +Qed. + +Theorem LPO : + forall P : nat -> Prop, (forall n, P n \/ ~ P n) -> + {n : nat | P n} + {forall n, ~ P n}. +Proof. +intros P HP. +destruct (LPO_min P HP) as [[n [Pn _]]|Pn]. +left. +now exists n. +now right. +Qed. + + +Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) -> + {n : Z| P n} + {forall n, ~ P n}. +Proof. +intros P H. +destruct (LPO (fun n => P (Z.of_nat n))) as [J|J]. +intros n; apply H. +destruct J as (n, Hn). +left; now exists (Z.of_nat n). +destruct (LPO (fun n => P (-Z.of_nat n)%Z)) as [K|K]. +intros n; apply H. +destruct K as (n, Hn). +left; now exists (-Z.of_nat n)%Z. +right; intros n; case (Zle_or_lt 0 n); intros M. +rewrite <- (Zabs_eq n); trivial. +rewrite <- Zabs2Nat.id_abs. +apply J. +rewrite <- (Zopp_involutive n). +rewrite <- (Z.abs_neq n). +rewrite <- Zabs2Nat.id_abs. +apply K. +omega. +Qed. + + + (** A little tactic to simplify terms of the form [bpow a * bpow b]. *) Ltac bpow_simplify := (* bpow ex * bpow ey ~~> bpow (ex + ey) *) diff --git a/flocq/Core/Fcore_Zaux.v b/flocq/Core/Fcore_Zaux.v index 4702d62e..f6731b4c 100644 --- a/flocq/Core/Fcore_Zaux.v +++ b/flocq/Core/Fcore_Zaux.v @@ -927,3 +927,65 @@ intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy. Qed. End faster_div. + +Section Iter. + +Context {A : Type}. +Variable (f : A -> A). + +Fixpoint iter_nat (n : nat) (x : A) {struct n} : A := + match n with + | S n' => iter_nat n' (f x) + | O => x + end. + +Lemma iter_nat_plus : + forall (p q : nat) (x : A), + iter_nat (p + q) x = iter_nat p (iter_nat q x). +Proof. +induction q. +now rewrite plus_0_r. +intros x. +rewrite <- plus_n_Sm. +apply IHq. +Qed. + +Lemma iter_nat_S : + forall (p : nat) (x : A), + iter_nat (S p) x = f (iter_nat p x). +Proof. +induction p. +easy. +simpl. +intros x. +apply IHp. +Qed. + +Fixpoint iter_pos (n : positive) (x : A) {struct n} : A := + match n with + | xI n' => iter_pos n' (iter_pos n' (f x)) + | xO n' => iter_pos n' (iter_pos n' x) + | xH => f x + end. + +Lemma iter_pos_nat : + forall (p : positive) (x : A), + iter_pos p x = iter_nat (Pos.to_nat p) x. +Proof. +induction p ; intros x. +rewrite Pos2Nat.inj_xI. +simpl. +rewrite plus_0_r. +rewrite iter_nat_plus. +rewrite (IHp (f x)). +apply IHp. +rewrite Pos2Nat.inj_xO. +simpl. +rewrite plus_0_r. +rewrite iter_nat_plus. +rewrite (IHp x). +apply IHp. +easy. +Qed. + +End Iter. diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index 13174d29..d40c1a09 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -21,7 +21,7 @@ Require Import ZArith. Require Import Zquot. Require Import Fcore_Zaux. -(** Computes the number of bits (radix 2) of a positive integer. +(** Number of bits (radix 2) of a positive integer. It serves as an upper bound on the number of digits to ensure termination. *) @@ -466,6 +466,8 @@ now apply Hd. now rewrite 3!Zdigit_lt. Qed. +(** Left and right shifts *) + Definition Zscale n k := if Zle_bool 0 k then (n * Zpower beta k)%Z else Z.quot n (Zpower beta (-k)). @@ -545,6 +547,8 @@ rewrite Zle_bool_true with (1 := Hk). now apply Zscale_mul_pow. Qed. +(** Slice of an integer *) + Definition Zslice n k1 k2 := if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0. @@ -756,6 +760,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z := End digits_aux. (** Number of digits of an integer *) + Definition Zdigits n := match n with | Z0 => Z0 @@ -1011,7 +1016,7 @@ generalize (Zpower_gt_Zdigits e x). omega. Qed. -(** Characterizes the number digits of a product. +(** Number of digits of a product. This strong version is needed for proofs of division and square root algorithms, since they involve operation remainders. @@ -1126,6 +1131,8 @@ Qed. End Fcore_digits. +(** Specialized version for computing the number of bits of an integer *) + Section Zdigits2. Theorem Z_of_nat_S_digits2_Pnat : diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v index e1535bc9..8199ede6 100644 --- a/flocq/Core/Fcore_float_prop.v +++ b/flocq/Core/Fcore_float_prop.v @@ -233,6 +233,37 @@ rewrite <- F2R_0 with (Fexp f). now apply F2R_lt_compat. Qed. +Theorem F2R_neq_0_compat : + forall f : float beta, + (Fnum f <> 0)%Z -> + (F2R f <> 0)%R. +Proof. +intros f H H1. +apply H. +now apply F2R_eq_0_reg with (Fexp f). +Qed. + + +Lemma Fnum_ge_0_compat: forall (f : float beta), + (0 <= F2R f)%R -> (0 <= Fnum f)%Z. +Proof. +intros f H. +case (Zle_or_lt 0 (Fnum f)); trivial. +intros H1; contradict H. +apply Rlt_not_le. +now apply F2R_lt_0_compat. +Qed. + +Lemma Fnum_le_0_compat: forall (f : float beta), + (F2R f <= 0)%R -> (Fnum f <= 0)%Z. +Proof. +intros f H. +case (Zle_or_lt (Fnum f) 0); trivial. +intros H1; contradict H. +apply Rlt_not_le. +now apply F2R_gt_0_compat. +Qed. + (** Floats and bpow *) Theorem F2R_bpow : forall e : Z, diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v index 45729f2a..bac65b9d 100644 --- a/flocq/Core/Fcore_generic_fmt.v +++ b/flocq/Core/Fcore_generic_fmt.v @@ -1015,7 +1015,7 @@ Qed. End monotone. -Theorem round_abs_abs' : +Theorem round_abs_abs : forall P : R -> R -> Prop, ( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) -> forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)). @@ -1043,18 +1043,6 @@ apply round_le... now apply Rlt_le. Qed. -(* TODO: remove *) -Theorem round_abs_abs : - forall P : R -> R -> Prop, - ( forall rnd (Hr : Valid_rnd rnd) x, P x (round rnd x) ) -> - forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)). -Proof. -intros P HP. -apply round_abs_abs'. -intros. -now apply HP. -Qed. - Theorem round_bounded_large : forall rnd {Hr : Valid_rnd rnd} x ex, (fexp ex < ex)%Z -> @@ -1064,7 +1052,7 @@ Proof with auto with typeclass_instances. intros rnd Hr x ex He. apply round_abs_abs... clear rnd Hr x. -intros rnd' Hr x. +intros rnd' Hr x _. apply round_bounded_large_pos... Qed. @@ -1076,7 +1064,7 @@ Proof. intros rnd Hr x ex H1 H2. generalize Rabs_R0. rewrite <- H2 at 1. -apply (round_abs_abs' (fun t rt => forall (ex : Z), +apply (round_abs_abs (fun t rt => forall (ex : Z), (bpow (ex - 1) <= t < bpow ex)%R -> rt = 0%R -> (ex <= fexp ex)%Z)); trivial. clear; intros rnd Hr x Hx. @@ -1496,7 +1484,7 @@ right. now rewrite Zmax_l with (1 := Zlt_le_weak _ _ He). Qed. -Theorem ln_beta_round_DN : +Theorem ln_beta_DN : forall x, (0 < round Zfloor x)%R -> (ln_beta beta (round Zfloor x) = ln_beta beta x :> Z). @@ -1513,7 +1501,6 @@ now apply Rgt_not_eq. now apply Rlt_le. Qed. -(* TODO: remove *) Theorem canonic_exp_DN : forall x, (0 < round Zfloor x)%R -> @@ -1521,7 +1508,7 @@ Theorem canonic_exp_DN : Proof. intros x Hd. apply (f_equal fexp). -now apply ln_beta_round_DN. +now apply ln_beta_DN. Qed. Theorem scaled_mantissa_DN : @@ -2312,7 +2299,7 @@ intros x Gx. apply generic_format_abs_inv. apply generic_format_abs in Gx. revert rnd valid_rnd x Gx. -refine (round_abs_abs' _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _). +refine (round_abs_abs _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _). intros rnd valid_rnd x [Hx|Hx] Gx. (* x > 0 *) generalize (ln_beta_generic_gt _ x (Rgt_not_eq _ _ Hx) Gx). diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v index 94c94203..171c27fc 100644 --- a/flocq/Core/Fcore_rnd.v +++ b/flocq/Core/Fcore_rnd.v @@ -39,7 +39,7 @@ exists f. intros g Hg. now apply H2 with (3 := Rle_refl x). (* . *) -exists (projT1 (completeness _ H3 H1)). +exists (proj1_sig (completeness _ H3 H1)). destruct completeness as (f1, (H4, H5)). simpl. destruct H1 as (f2, H1). @@ -58,7 +58,7 @@ Theorem round_fun_of_pred : { f : R -> R | forall x, rnd x (f x) }. Proof. intros rnd H. -exists (fun x => projT1 (round_val_of_pred rnd H x)). +exists (fun x => proj1_sig (round_val_of_pred rnd H x)). intros x. now destruct round_val_of_pred as (f, H1). Qed. diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v index 6829c0c8..1f265406 100644 --- a/flocq/Core/Fcore_rnd_ne.v +++ b/flocq/Core/Fcore_rnd_ne.v @@ -164,7 +164,7 @@ now apply Rlt_le. assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp. assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R). rewrite Hxu, Hxd. -now apply ulp_DN_UP. +now apply round_UP_DN_ulp. destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2]. (* - xu > bpow ex *) elim (Rlt_not_le _ _ Hu2). @@ -191,7 +191,8 @@ rewrite Rmult_plus_distr_r. rewrite Z2R_Zpower, <- bpow_plus. ring_simplify (ex - fexp ex + fexp ex)%Z. rewrite Hu2, Hud. -unfold ulp, canonic_exp. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold canonic_exp. rewrite ln_beta_unique with beta x ex. unfold F2R. simpl. ring. @@ -223,7 +224,8 @@ specialize (H ex). omega. (* - xu < bpow ex *) revert Hud. -unfold ulp, F2R. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold F2R. rewrite Hd, Hu. unfold canonic_exp. rewrite ln_beta_unique with beta (F2R xu) ex. diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v index 04bed01c..1c27de31 100644 --- a/flocq/Core/Fcore_ulp.v +++ b/flocq/Core/Fcore_ulp.v @@ -32,9 +32,79 @@ Notation bpow e := (bpow beta e). Variable fexp : Z -> Z. +(** Definition and basic properties about the minimal exponent, when it exists *) + +Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z. +intros. +destruct (Z_le_dec x y). +now left. +now right. +Qed. + + +(** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *) +Definition negligible_exp: option Z := + match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with + | inleft N => Some (proj1_sig N) + | inright _ => None + end. + + +Inductive negligible_exp_prop: option Z -> Prop := + | negligible_None: (forall n, (fexp n < n)%Z) -> negligible_exp_prop None + | negligible_Some: forall n, (n <= fexp n)%Z -> negligible_exp_prop (Some n). + + +Lemma negligible_exp_spec: negligible_exp_prop negligible_exp. +Proof. +unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. +now apply negligible_Some. +apply negligible_None. +intros n; specialize (Hn n); omega. +Qed. + +Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z) + \/ exists n, (negligible_exp = Some n /\ (n <= fexp n)%Z). +Proof. +unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. +right; simpl; exists n; now split. +left; split; trivial. +intros n; specialize (Hn n); omega. +Qed. + Context { valid_exp : Valid_exp fexp }. -Definition ulp x := bpow (canonic_exp beta fexp x). +Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> fexp n = fexp m. +Proof. +intros n m Hn Hm. +case (Zle_or_lt n m); intros H. +apply valid_exp; omega. +apply sym_eq, valid_exp; omega. +Qed. + + +(** Definition and basic properties about the ulp *) +(** Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal + exponent, such as in FLX, and beta^(fexp n) when there is a n such + that n <= fexp n. For instance, the value of ulp(O) is then + beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that + is equivalent to the previous "unfold ulp" provided the value is + not zero. *) + +Definition ulp x := match Req_bool x 0 with + | true => match negligible_exp with + | Some n => bpow (fexp n) + | None => 0%R + end + | false => bpow (canonic_exp beta fexp x) + end. + +Lemma ulp_neq_0 : forall x:R, (x <> 0)%R -> ulp x = bpow (canonic_exp beta fexp x). +Proof. +intros x Hx. +unfold ulp; case (Req_bool_spec x); trivial. +intros H; now contradict H. +Qed. Notation F := (generic_format beta fexp). @@ -43,17 +113,37 @@ Theorem ulp_opp : Proof. intros x. unfold ulp. +case Req_bool_spec; intros H1. +rewrite Req_bool_true; trivial. +rewrite <- (Ropp_involutive x), H1; ring. +rewrite Req_bool_false. now rewrite canonic_exp_opp. +intros H2; apply H1; rewrite H2; ring. Qed. Theorem ulp_abs : forall x, ulp (Rabs x) = ulp x. Proof. intros x. -unfold ulp. +unfold ulp; case (Req_bool_spec x 0); intros H1. +rewrite Req_bool_true; trivial. +now rewrite H1, Rabs_R0. +rewrite Req_bool_false. now rewrite canonic_exp_abs. +now apply Rabs_no_R0. +Qed. + +Theorem ulp_ge_0: + forall x, (0 <= ulp x)%R. +Proof. +intros x; unfold ulp; case Req_bool_spec; intros. +case negligible_exp; intros. +apply bpow_ge_0. +apply Rle_refl. +apply bpow_ge_0. Qed. + Theorem ulp_le_id: forall x, (0 < x)%R -> @@ -63,7 +153,9 @@ Proof. intros x Zx Fx. rewrite <- (Rmult_1_l (ulp x)). pattern x at 2; rewrite Fx. -unfold F2R, ulp; simpl. +rewrite ulp_neq_0. +2: now apply Rgt_not_eq. +unfold F2R; simpl. apply Rmult_le_compat_r. apply bpow_ge_0. replace 1%R with (Z2R (Zsucc 0)) by reflexivity. @@ -86,12 +178,15 @@ now apply Rabs_pos_lt. now apply generic_format_abs. Qed. -Theorem ulp_DN_UP : + +(* was ulp_DN_UP *) +Theorem round_UP_DN_ulp : forall x, ~ F x -> round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R. Proof. intros x Fx. -unfold round, ulp. simpl. +rewrite ulp_neq_0. +unfold round. simpl. unfold F2R. simpl. rewrite Zceil_floor_neq. rewrite Z2R_plus. simpl. @@ -103,17 +198,282 @@ rewrite <- H. rewrite Ztrunc_Z2R. rewrite H. now rewrite scaled_mantissa_mult_bpow. +intros V; apply Fx. +rewrite V. +apply generic_format_0. +Qed. + + +Theorem ulp_bpow : + forall e, ulp (bpow e) = bpow (fexp (e + 1)). +intros e. +rewrite ulp_neq_0. +apply f_equal. +apply canonic_exp_fexp. +rewrite Rabs_pos_eq. +split. +ring_simplify (e + 1 - 1)%Z. +apply Rle_refl. +apply bpow_lt. +apply Zlt_succ. +apply bpow_ge_0. +apply Rgt_not_eq, Rlt_gt, bpow_gt_0. +Qed. + + +Lemma generic_format_ulp_0: + F (ulp 0). +Proof. +unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros _; apply generic_format_0. +intros n H1. +apply generic_format_bpow. +now apply valid_exp. +Qed. + +Lemma generic_format_bpow_ge_ulp_0: forall e, + (ulp 0 <= bpow e)%R -> F (bpow e). +Proof. +intros e; unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros H1 _. +apply generic_format_bpow. +specialize (H1 (e+1)%Z); omega. +intros n H1 H2. +apply generic_format_bpow. +case (Zle_or_lt (e+1) (fexp (e+1))); intros H4. +absurd (e+1 <= e)%Z. +omega. +apply Zle_trans with (1:=H4). +replace (fexp (e+1)) with (fexp n). +now apply le_bpow with beta. +now apply fexp_negligible_exp_eq. +omega. +Qed. + +(** The three following properties are equivalent: + [Exp_not_FTZ] ; forall x, F (ulp x) ; forall x, ulp 0 <= ulp x *) + +Lemma generic_format_ulp: Exp_not_FTZ fexp -> + forall x, F (ulp x). +Proof. +unfold Exp_not_FTZ; intros H x. +case (Req_dec x 0); intros Hx. +rewrite Hx; apply generic_format_ulp_0. +rewrite (ulp_neq_0 _ Hx). +apply generic_format_bpow; unfold canonic_exp. +apply H. +Qed. + +Lemma not_FTZ_generic_format_ulp: + (forall x, F (ulp x)) -> Exp_not_FTZ fexp. +intros H e. +specialize (H (bpow (e-1))). +rewrite ulp_neq_0 in H. +2: apply Rgt_not_eq, bpow_gt_0. +unfold canonic_exp in H. +rewrite ln_beta_bpow in H. +apply generic_format_bpow_inv' in H... +now replace (e-1+1)%Z with e in H by ring. +Qed. + + +Lemma ulp_ge_ulp_0: Exp_not_FTZ fexp -> + forall x, (ulp 0 <= ulp x)%R. +Proof. +unfold Exp_not_FTZ; intros H x. +case (Req_dec x 0); intros Hx. +rewrite Hx; now right. +unfold ulp at 1. +rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +intros (H1,H2); rewrite H1; apply ulp_ge_0. +intros (n,(H1,H2)); rewrite H1. +rewrite ulp_neq_0; trivial. +apply bpow_le; unfold canonic_exp. +generalize (ln_beta beta x); intros l. +case (Zle_or_lt l (fexp l)); intros Hl. +rewrite (fexp_negligible_exp_eq n l); trivial; apply Zle_refl. +case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K. +absurd (fexp n <= fexp l)%Z. +omega. +apply Zle_trans with (2:= H _). +apply Zeq_le, sym_eq, valid_exp; trivial. +omega. +Qed. + +Lemma not_FTZ_ulp_ge_ulp_0: + (forall x, (ulp 0 <= ulp x)%R) -> Exp_not_FTZ fexp. +Proof. +intros H e. +apply generic_format_bpow_inv' with beta. +apply generic_format_bpow_ge_ulp_0. +replace e with ((e-1)+1)%Z by ring. +rewrite <- ulp_bpow. +apply H. +Qed. + + + +Theorem ulp_le_pos : + forall { Hm : Monotone_exp fexp }, + forall x y: R, + (0 <= x)%R -> (x <= y)%R -> + (ulp x <= ulp y)%R. +Proof with auto with typeclass_instances. +intros Hm x y Hx Hxy. +destruct Hx as [Hx|Hx]. +rewrite ulp_neq_0. +rewrite ulp_neq_0. +apply bpow_le. +apply Hm. +now apply ln_beta_le. +apply Rgt_not_eq, Rlt_gt. +now apply Rlt_le_trans with (1:=Hx). +now apply Rgt_not_eq. +rewrite <- Hx. +apply ulp_ge_ulp_0. +apply monotone_exp_not_FTZ... +Qed. + + +Theorem ulp_le : + forall { Hm : Monotone_exp fexp }, + forall x y: R, + (Rabs x <= Rabs y)%R -> + (ulp x <= ulp y)%R. +Proof. +intros Hm x y Hxy. +rewrite <- ulp_abs. +rewrite <- (ulp_abs y). +apply ulp_le_pos; trivial. +apply Rabs_pos. +Qed. + + + +(** Definition and properties of pred and succ *) + +Definition pred_pos x := + if Req_bool x (bpow (ln_beta beta x - 1)) then + (x - bpow (fexp (ln_beta beta x - 1)))%R + else + (x - ulp x)%R. + +Definition succ x := + if (Rle_bool 0 x) then + (x+ulp x)%R + else + (- pred_pos (-x))%R. + +Definition pred x := (- succ (-x))%R. + +Theorem pred_eq_pos: + forall x, (0 <= x)%R -> (pred x = pred_pos x)%R. +Proof. +intros x Hx; unfold pred, succ. +case Rle_bool_spec; intros Hx'. +assert (K:(x = 0)%R). +apply Rle_antisym; try assumption. +apply Ropp_le_cancel. +now rewrite Ropp_0. +rewrite K; unfold pred_pos. +rewrite Req_bool_false. +2: apply Rlt_not_eq, bpow_gt_0. +rewrite Ropp_0; ring. +now rewrite 2!Ropp_involutive. +Qed. + +Theorem succ_eq_pos: + forall x, (0 <= x)%R -> (succ x = x + ulp x)%R. +Proof. +intros x Hx; unfold succ. +now rewrite Rle_bool_true. +Qed. + +Lemma pred_eq_opp_succ_opp: forall x, pred x = (- succ (-x))%R. +Proof. +reflexivity. +Qed. + +Lemma succ_eq_opp_pred_opp: forall x, succ x = (- pred (-x))%R. +Proof. +intros x; unfold pred. +now rewrite 2!Ropp_involutive. +Qed. + +Lemma succ_opp: forall x, (succ (-x) = - pred x)%R. +Proof. +intros x; rewrite succ_eq_opp_pred_opp. +now rewrite Ropp_involutive. +Qed. + +Lemma pred_opp: forall x, (pred (-x) = - succ x)%R. +Proof. +intros x; rewrite pred_eq_opp_succ_opp. +now rewrite Ropp_involutive. +Qed. + + + + +(** pred and succ are in the format *) + +(* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *) +(* was pred_ge_bpow *) +Theorem id_m_ulp_ge_bpow : + forall x e, F x -> + x <> ulp x -> + (bpow e < x)%R -> + (bpow e <= x - ulp x)%R. +Proof. +intros x e Fx Hx' Hx. +(* *) +assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z. +assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. +apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). +rewrite <- Fx. +apply Rle_lt_trans with (2:=Hx). +apply bpow_ge_0. +omega. +case (Zle_lt_or_eq _ _ H); intros Hm. +(* *) +pattern x at 1 ; rewrite Fx. +rewrite ulp_neq_0. +unfold F2R. simpl. +pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. +rewrite <- Rmult_minus_distr_r. +change 1%R with (Z2R 1). +rewrite <- Z2R_minus. +change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R. +apply bpow_le_F2R_m1; trivial. +now rewrite <- Fx. +apply Rgt_not_eq, Rlt_gt. +apply Rlt_trans with (2:=Hx), bpow_gt_0. +(* *) +contradict Hx'. +pattern x at 1; rewrite Fx. +rewrite <- Hm. +rewrite ulp_neq_0. +unfold F2R; simpl. +now rewrite Rmult_1_l. +apply Rgt_not_eq, Rlt_gt. +apply Rlt_trans with (2:=Hx), bpow_gt_0. Qed. -(** The successor of x is x + ulp x *) -Theorem succ_le_bpow : +(* was succ_le_bpow *) +Theorem id_p_ulp_le_bpow : forall x e, (0 < x)%R -> F x -> (x < bpow e)%R -> (x + ulp x <= bpow e)%R. Proof. intros x e Zx Fx Hx. pattern x at 1 ; rewrite Fx. -unfold ulp, F2R. simpl. +rewrite ulp_neq_0. +unfold F2R. simpl. pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_plus_distr_r. change 1%R with (Z2R 1). @@ -123,88 +483,142 @@ apply F2R_p1_le_bpow. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). now rewrite <- Fx. now rewrite <- Fx. +now apply Rgt_not_eq. Qed. -Theorem ln_beta_succ : + + +Lemma generic_format_pred_aux1: forall x, (0 < x)%R -> F x -> - forall eps, (0 <= eps < ulp x)%R -> - ln_beta beta (x + eps) = ln_beta beta x :> Z. + x <> bpow (ln_beta beta x - 1) -> + F (x - ulp x). Proof. -intros x Zx Fx eps Heps. -destruct (ln_beta beta x) as (ex, He). -simpl. -specialize (He (Rgt_not_eq _ _ Zx)). -apply ln_beta_unique. +intros x Zx Fx Hx. +destruct (ln_beta beta x) as (ex, Ex). +simpl in Hx. +specialize (Ex (Rgt_not_eq _ _ Zx)). +assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R). +rewrite Rabs_pos_eq in Ex. +destruct Ex as (H,H'); destruct H; split; trivial. +contradict Hx; easy. +now apply Rlt_le. +unfold generic_format, scaled_mantissa, canonic_exp. +rewrite ln_beta_unique with beta (x - ulp x)%R ex. +pattern x at 1 3 ; rewrite Fx. +rewrite ulp_neq_0. +unfold scaled_mantissa. +rewrite canonic_exp_fexp with (1 := Ex). +unfold F2R. simpl. +rewrite Rmult_minus_distr_r. +rewrite Rmult_assoc. +rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. +change (bpow 0) with (Z2R 1). +rewrite <- Z2R_minus. +rewrite Ztrunc_Z2R. +rewrite Z2R_minus. +rewrite Rmult_minus_distr_r. +now rewrite Rmult_1_l. +now apply Rgt_not_eq. rewrite Rabs_pos_eq. -rewrite Rabs_pos_eq in He. split. -apply Rle_trans with (1 := proj1 He). -pattern x at 1 ; rewrite <- Rplus_0_r. -now apply Rplus_le_compat_l. -apply Rlt_le_trans with (x + ulp x)%R. -now apply Rplus_lt_compat_l. -pattern x at 1 ; rewrite Fx. -unfold ulp, F2R. simpl. -pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. -rewrite <- Rmult_plus_distr_r. -change 1%R with (Z2R 1). -rewrite <- Z2R_plus. -change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R. -apply F2R_p1_le_bpow. +apply id_m_ulp_ge_bpow; trivial. +rewrite ulp_neq_0. +intro H. +assert (ex-1 < canonic_exp beta fexp x < ex)%Z. +split ; apply (lt_bpow beta) ; rewrite <- H ; easy. +clear -H0. omega. +now apply Rgt_not_eq. +apply Ex'. +apply Rle_lt_trans with (2 := proj2 Ex'). +pattern x at 3 ; rewrite <- Rplus_0_r. +apply Rplus_le_compat_l. +rewrite <-Ropp_0. +apply Ropp_le_contravar. +apply ulp_ge_0. +apply Rle_0_minus. +pattern x at 2; rewrite Fx. +rewrite ulp_neq_0. +unfold F2R; simpl. +pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l. +apply Rmult_le_compat_r. +apply bpow_ge_0. +replace 1%R with (Z2R 1) by reflexivity. +apply Z2R_le. +assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -now rewrite <- Fx. -now rewrite <- Fx. -now apply Rlt_le. -apply Rplus_le_le_0_compat. -now apply Rlt_le. -apply Heps. +rewrite <- Fx. +apply Rle_lt_trans with (2:=proj1 Ex'). +apply bpow_ge_0. +omega. +now apply Rgt_not_eq. Qed. -Theorem round_DN_succ : +Lemma generic_format_pred_aux2 : forall x, (0 < x)%R -> F x -> - forall eps, (0 <= eps < ulp x)%R -> - round beta fexp Zfloor (x + eps) = x. + let e := ln_beta_val beta x (ln_beta beta x) in + x = bpow (e - 1) -> + F (x - bpow (fexp (e - 1))). Proof. -intros x Zx Fx eps Heps. -pattern x at 2 ; rewrite Fx. -unfold round. -unfold scaled_mantissa. simpl. -unfold canonic_exp at 1 2. -rewrite ln_beta_succ ; trivial. -apply (f_equal (fun m => F2R (Float beta m _))). -rewrite Ztrunc_floor. -apply Zfloor_imp. +intros x Zx Fx e Hx. +pose (f:=(x - bpow (fexp (e - 1)))%R). +fold f. +assert (He:(fexp (e-1) <= e-1)%Z). +apply generic_format_bpow_inv with beta; trivial. +rewrite <- Hx; assumption. +case (Zle_lt_or_eq _ _ He); clear He; intros He. +assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R. +unfold f; rewrite Hx. +unfold F2R; simpl. +rewrite Z2R_minus, Z2R_Zpower. +rewrite Rmult_minus_distr_r, Rmult_1_l. +rewrite <- bpow_plus. +now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. +omega. +rewrite H. +apply generic_format_F2R. +intros _. +apply Zeq_le. +apply canonic_exp_fexp. +rewrite <- H. +unfold f; rewrite Hx. +rewrite Rabs_right. split. -apply (Rle_trans _ _ _ (Zfloor_lb _)). +apply Rplus_le_reg_l with (bpow (fexp (e-1))). +ring_simplify. +apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. +apply Rplus_le_compat ; apply bpow_le ; omega. +apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. +apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. apply bpow_ge_0. -pattern x at 1 ; rewrite <- Rplus_0_r. -now apply Rplus_le_compat_l. -apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R. -apply Rmult_lt_compat_r. -apply bpow_gt_0. -now apply Rplus_lt_compat_l. -rewrite Rmult_plus_distr_r. -rewrite Z2R_plus. -apply Rplus_le_compat. -pattern x at 1 3 ; rewrite Fx. -unfold F2R. simpl. -rewrite Rmult_assoc. -rewrite <- bpow_plus. -rewrite Zplus_opp_r. -rewrite Rmult_1_r. -rewrite Zfloor_Z2R. -apply Rle_refl. -unfold ulp. +replace 2%R with (Z2R 2) by reflexivity. +replace (bpow 1) with (Z2R beta). +apply Z2R_le. +apply <- Zle_is_le_bool. +now destruct beta. +simpl. +unfold Zpower_pos; simpl. +now rewrite Zmult_1_r. rewrite <- bpow_plus. -rewrite Zplus_opp_r. -apply Rle_refl. -apply Rmult_le_pos. -now apply Rlt_le. -apply bpow_ge_0. +replace (1+(e-2))%Z with (e-1)%Z by ring. +now right. +rewrite <- Rplus_0_r. +apply Rplus_lt_compat_l. +rewrite <- Ropp_0. +apply Ropp_lt_contravar. +apply bpow_gt_0. +apply Rle_ge; apply Rle_0_minus. +apply bpow_le. +omega. +replace f with 0%R. +apply generic_format_0. +unfold f. +rewrite Hx, He. +ring. Qed. -Theorem generic_format_succ : + +Theorem generic_format_succ_aux1 : forall x, (0 < x)%R -> F x -> F (x + ulp x). Proof. @@ -213,11 +627,12 @@ destruct (ln_beta beta x) as (ex, Ex). specialize (Ex (Rgt_not_eq _ _ Zx)). assert (Ex' := Ex). rewrite Rabs_pos_eq in Ex'. -destruct (succ_le_bpow x ex) ; try easy. +destruct (id_p_ulp_le_bpow x ex) ; try easy. unfold generic_format, scaled_mantissa, canonic_exp. rewrite ln_beta_unique with beta (x + ulp x)%R ex. pattern x at 1 3 ; rewrite Fx. -unfold ulp, scaled_mantissa. +rewrite ulp_neq_0. +unfold scaled_mantissa. rewrite canonic_exp_fexp with (1 := Ex). unfold F2R. simpl. rewrite Rmult_plus_distr_r. @@ -229,16 +644,17 @@ rewrite Ztrunc_Z2R. rewrite Z2R_plus. rewrite Rmult_plus_distr_r. now rewrite Rmult_1_l. +now apply Rgt_not_eq. rewrite Rabs_pos_eq. split. apply Rle_trans with (1 := proj1 Ex'). pattern x at 1 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. -apply bpow_ge_0. +apply ulp_ge_0. exact H. apply Rplus_le_le_0_compat. now apply Rlt_le. -apply bpow_ge_0. +apply ulp_ge_0. rewrite H. apply generic_format_bpow. apply valid_exp. @@ -261,427 +677,240 @@ now apply Rlt_le. now apply Rlt_le. Qed. -Theorem round_UP_succ : - forall x, (0 < x)%R -> F x -> - forall eps, (0 < eps <= ulp x)%R -> - round beta fexp Zceil (x + eps) = (x + ulp x)%R. -Proof with auto with typeclass_instances. -intros x Zx Fx eps (Heps1,[Heps2|Heps2]). -assert (Heps: (0 <= eps < ulp x)%R). -split. -now apply Rlt_le. -exact Heps2. -assert (Hd := round_DN_succ x Zx Fx eps Heps). -rewrite ulp_DN_UP. -rewrite Hd. -unfold ulp, canonic_exp. -now rewrite ln_beta_succ. -intros Fs. -rewrite round_generic in Hd... -apply Rgt_not_eq with (2 := Hd). -pattern x at 2 ; rewrite <- Rplus_0_r. -now apply Rplus_lt_compat_l. -rewrite Heps2. -apply round_generic... -now apply generic_format_succ. +Theorem generic_format_pred_pos : + forall x, F x -> (0 < x)%R -> + F (pred_pos x). +Proof. +intros x Fx Zx. +unfold pred_pos; case Req_bool_spec; intros H. +now apply generic_format_pred_aux2. +now apply generic_format_pred_aux1. Qed. -Theorem succ_le_lt: - forall x y, - F x -> F y -> - (0 < x < y)%R -> - (x + ulp x <= y)%R. -Proof with auto with typeclass_instances. -intros x y Hx Hy H. -case (Rle_or_lt (ulp x) (y-x)); intros H1. -apply Rplus_le_reg_r with (-x)%R. -now ring_simplify (x+ulp x + -x)%R. -replace y with (x+(y-x))%R by ring. -absurd (x < y)%R. -2: apply H. -apply Rle_not_lt; apply Req_le. -rewrite <- round_DN_succ with (eps:=(y-x)%R); try easy. -ring_simplify (x+(y-x))%R. -apply sym_eq. -apply round_generic... -split; trivial. -apply Rlt_le; now apply Rlt_Rminus. + +Theorem generic_format_succ : + forall x, F x -> + F (succ x). +Proof. +intros x Fx. +unfold succ; case Rle_bool_spec; intros Zx. +destruct Zx as [Zx|Zx]. +now apply generic_format_succ_aux1. +rewrite <- Zx, Rplus_0_l. +apply generic_format_ulp_0. +apply generic_format_opp. +apply generic_format_pred_pos. +now apply generic_format_opp. +now apply Ropp_0_gt_lt_contravar. Qed. -(** Error of a rounding, expressed in number of ulps *) -Theorem ulp_error : - forall rnd { Zrnd : Valid_rnd rnd } x, - (Rabs (round beta fexp rnd x - x) < ulp x)%R. -Proof with auto with typeclass_instances. -intros rnd Zrnd x. -destruct (generic_format_EM beta fexp x) as [Hx|Hx]. -(* x = rnd x *) -rewrite round_generic... -unfold Rminus. -rewrite Rplus_opp_r, Rabs_R0. -apply bpow_gt_0. -(* x <> rnd x *) -destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H. -(* . *) -rewrite Rabs_left1. -rewrite Ropp_minus_distr. -apply Rplus_lt_reg_l with (round beta fexp Zfloor x). -rewrite <- ulp_DN_UP with (1 := Hx). -ring_simplify. -assert (Hu: (x <= round beta fexp Zceil x)%R). -apply round_UP_pt... -destruct Hu as [Hu|Hu]. -exact Hu. -elim Hx. -rewrite Hu. -apply generic_format_round... -apply Rle_minus. -apply round_DN_pt... -(* . *) -rewrite Rabs_pos_eq. -rewrite ulp_DN_UP with (1 := Hx). -apply Rplus_lt_reg_r with (x - ulp x)%R. -ring_simplify. -assert (Hd: (round beta fexp Zfloor x <= x)%R). -apply round_DN_pt... -destruct Hd as [Hd|Hd]. -exact Hd. -elim Hx. -rewrite <- Hd. -apply generic_format_round... -apply Rle_0_minus. -apply round_UP_pt... +Theorem generic_format_pred : + forall x, F x -> + F (pred x). +Proof. +intros x Fx. +unfold pred. +apply generic_format_opp. +apply generic_format_succ. +now apply generic_format_opp. Qed. -Theorem ulp_half_error : - forall choice x, - (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R. -Proof with auto with typeclass_instances. -intros choice x. -destruct (generic_format_EM beta fexp x) as [Hx|Hx]. -(* x = rnd x *) -rewrite round_generic... -unfold Rminus. -rewrite Rplus_opp_r, Rabs_R0. -apply Rmult_le_pos. -apply Rlt_le. -apply Rinv_0_lt_compat. -now apply (Z2R_lt 0 2). -apply bpow_ge_0. -(* x <> rnd x *) -set (d := round beta fexp Zfloor x). -destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2). -destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. -(* . rnd(x) = rndd(x) *) -apply Rle_trans with (Rabs (d - x)). -apply Hr2. -apply (round_DN_pt beta fexp x). -rewrite Rabs_left1. -rewrite Ropp_minus_distr. -apply Rmult_le_reg_r with 2%R. -now apply (Z2R_lt 0 2). -apply Rplus_le_reg_r with (d - x)%R. -ring_simplify. -apply Rle_trans with (1 := H). -right. field. -apply Rle_minus. -apply (round_DN_pt beta fexp x). -(* . rnd(x) = rndu(x) *) -assert (Hu: (d + ulp x)%R = round beta fexp Zceil x). -unfold d. -now rewrite <- ulp_DN_UP. -apply Rle_trans with (Rabs (d + ulp x - x)). -apply Hr2. -rewrite Hu. -apply (round_UP_pt beta fexp x). -rewrite Rabs_pos_eq. -apply Rmult_le_reg_r with 2%R. -now apply (Z2R_lt 0 2). -apply Rplus_le_reg_r with (- (d + ulp x - x))%R. -ring_simplify. -apply Rlt_le. -apply Rlt_le_trans with (1 := H). -right. field. -apply Rle_0_minus. -rewrite Hu. -apply (round_UP_pt beta fexp x). + + +Theorem pred_pos_lt_id : + forall x, (x <> 0)%R -> + (pred_pos x < x)%R. +Proof. +intros x Zx. +unfold pred_pos. +case Req_bool_spec; intros H. +(* *) +rewrite <- Rplus_0_r. +apply Rplus_lt_compat_l. +rewrite <- Ropp_0. +apply Ropp_lt_contravar. +apply bpow_gt_0. +(* *) +rewrite <- Rplus_0_r. +apply Rplus_lt_compat_l. +rewrite <- Ropp_0. +apply Ropp_lt_contravar. +rewrite ulp_neq_0; trivial. +apply bpow_gt_0. Qed. -Theorem ulp_le : - forall { Hm : Monotone_exp fexp }, - forall x y: R, - (0 < x)%R -> (x <= y)%R -> - (ulp x <= ulp y)%R. +Theorem succ_gt_id : + forall x, (x <> 0)%R -> + (x < succ x)%R. Proof. -intros Hm x y Hx Hxy. -apply bpow_le. -apply Hm. -now apply ln_beta_le. +intros x Zx; unfold succ. +case Rle_bool_spec; intros Hx. +pattern x at 1; rewrite <- (Rplus_0_r x). +apply Rplus_lt_compat_l. +rewrite ulp_neq_0; trivial. +apply bpow_gt_0. +pattern x at 1; rewrite <- (Ropp_involutive x). +apply Ropp_lt_contravar. +apply pred_pos_lt_id. +now auto with real. Qed. -Theorem ulp_bpow : - forall e, ulp (bpow e) = bpow (fexp (e + 1)). -intros e. -unfold ulp. -apply f_equal. -apply canonic_exp_fexp. -rewrite Rabs_pos_eq. -split. -ring_simplify (e + 1 - 1)%Z. -apply Rle_refl. -apply bpow_lt. -apply Zlt_succ. -apply bpow_ge_0. -Qed. -Theorem ulp_DN : - forall x, - (0 < round beta fexp Zfloor x)%R -> - ulp (round beta fexp Zfloor x) = ulp x. +Theorem pred_lt_id : + forall x, (x <> 0)%R -> + (pred x < x)%R. Proof. -intros x Hd. -unfold ulp. -now rewrite canonic_exp_DN with (2 := Hd). +intros x Zx; unfold pred. +pattern x at 2; rewrite <- (Ropp_involutive x). +apply Ropp_lt_contravar. +apply succ_gt_id. +now auto with real. Qed. -Theorem ulp_error_f : - forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x, - (round beta fexp rnd x <> 0)%R -> - (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R. -Proof with auto with typeclass_instances. -intros Hm rnd Zrnd x Hfx. -case (round_DN_or_UP beta fexp rnd x); intros Hx. -(* *) -case (Rle_or_lt 0 (round beta fexp Zfloor x)). -intros H; destruct H. -rewrite Hx at 2. -rewrite ulp_DN; trivial. -apply ulp_error... -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -apply Rlt_le_trans with (1:=ulp_error _ _). -rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp rnd x)). -apply ulp_le; trivial. -apply Ropp_0_gt_lt_contravar; apply Rlt_gt. -case (Rle_or_lt 0 x); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_ge_generic... -apply generic_format_0. -apply Ropp_le_contravar; rewrite Hx. -apply (round_DN_pt beta fexp x). -(* *) -rewrite Hx; case (Rle_or_lt 0 (round beta fexp Zceil x)). -intros H; destruct H. -apply Rlt_le_trans with (1:=ulp_error _ _). -apply ulp_le; trivial. -case (Rle_or_lt x 0); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_le_generic... -apply generic_format_0. -apply round_UP_pt... -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -rewrite <- (ulp_opp (round beta fexp Zceil x)). -rewrite <- round_DN_opp. -rewrite ulp_DN; trivial. -replace (round beta fexp Zceil x - x)%R with (-((round beta fexp Zfloor (-x) - (-x))))%R. -rewrite Rabs_Ropp. -apply ulp_error... -rewrite round_DN_opp; ring. -rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. +Theorem succ_ge_id : + forall x, (x <= succ x)%R. +Proof. +intros x; case (Req_dec x 0). +intros V; rewrite V. +unfold succ; rewrite Rle_bool_true;[idtac|now right]. +rewrite Rplus_0_l; apply ulp_ge_0. +intros; left; now apply succ_gt_id. Qed. -Theorem ulp_half_error_f : - forall { Hm : Monotone_exp fexp }, - forall choice x, - (round beta fexp (Znearest choice) x <> 0)%R -> - (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R. -Proof with auto with typeclass_instances. -intros Hm choice x Hfx. -case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx. -(* *) -case (Rle_or_lt 0 (round beta fexp Zfloor x)). -intros H; destruct H. -rewrite Hx at 2. -rewrite ulp_DN; trivial. -apply ulp_half_error. -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -apply Rle_trans with (1:=ulp_half_error _ _). -apply Rmult_le_compat_l. -auto with real. -rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp (Znearest choice) x)). -apply ulp_le; trivial. -apply Ropp_0_gt_lt_contravar; apply Rlt_gt. -case (Rle_or_lt 0 x); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_ge_generic... -apply generic_format_0. -apply Ropp_le_contravar; rewrite Hx. -apply (round_DN_pt beta fexp x). -(* *) -case (Rle_or_lt 0 (round beta fexp Zceil x)). -intros H; destruct H. -apply Rle_trans with (1:=ulp_half_error _ _). -apply Rmult_le_compat_l. -auto with real. -apply ulp_le; trivial. -case (Rle_or_lt x 0); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_le_generic... -apply generic_format_0. -rewrite Hx; apply (round_UP_pt beta fexp x). -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)). -rewrite <- round_DN_opp. -rewrite ulp_DN; trivial. -pattern x at 1 2; rewrite <- Ropp_involutive. -rewrite round_N_opp. -unfold Rminus. -rewrite <- Ropp_plus_distr, Rabs_Ropp. -apply ulp_half_error. -rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. + +Theorem pred_le_id : + forall x, (pred x <= x)%R. +Proof. +intros x; unfold pred. +pattern x at 2; rewrite <- (Ropp_involutive x). +apply Ropp_le_contravar. +apply succ_ge_id. Qed. -(** Predecessor *) -Definition pred x := - if Req_bool x (bpow (ln_beta beta x - 1)) then - (x - bpow (fexp (ln_beta beta x - 1)))%R - else - (x - ulp x)%R. -Theorem pred_ge_bpow : - forall x e, F x -> - x <> ulp x -> - (bpow e < x)%R -> - (bpow e <= x - ulp x)%R. +Theorem pred_pos_ge_0 : + forall x, + (0 < x)%R -> F x -> (0 <= pred_pos x)%R. Proof. -intros x e Fx Hx' Hx. -(* *) -assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z. -assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. -apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -rewrite <- Fx. -apply Rle_lt_trans with (2:=Hx). -apply bpow_ge_0. -omega. -case (Zle_lt_or_eq _ _ H); intros Hm. -(* *) -pattern x at 1 ; rewrite Fx. -unfold ulp, F2R. simpl. -pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. -rewrite <- Rmult_minus_distr_r. -change 1%R with (Z2R 1). -rewrite <- Z2R_minus. -change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R. -apply bpow_le_F2R_m1; trivial. -now rewrite <- Fx. +intros x Zx Fx. +unfold pred_pos. +case Req_bool_spec; intros H. (* *) -contradict Hx'. -pattern x at 1; rewrite Fx. -rewrite <- Hm. -unfold ulp, F2R; simpl. -now rewrite Rmult_1_l. +apply Rle_0_minus. +rewrite H. +apply bpow_le. +destruct (ln_beta beta x) as (ex,Ex) ; simpl. +rewrite ln_beta_bpow. +ring_simplify (ex - 1 + 1 - 1)%Z. +apply generic_format_bpow_inv with beta; trivial. +simpl in H. +rewrite <- H; assumption. +apply Rle_0_minus. +now apply ulp_le_id. +Qed. + +Theorem pred_ge_0 : + forall x, + (0 < x)%R -> F x -> (0 <= pred x)%R. +Proof. +intros x Zx Fx. +rewrite pred_eq_pos. +now apply pred_pos_ge_0. +now left. Qed. -Lemma generic_format_pred_1: + +Lemma pred_pos_plus_ulp_aux1 : forall x, (0 < x)%R -> F x -> x <> bpow (ln_beta beta x - 1) -> - F (x - ulp x). + ((x - ulp x) + ulp (x-ulp x) = x)%R. Proof. intros x Zx Fx Hx. -destruct (ln_beta beta x) as (ex, Ex). -simpl in Hx. -specialize (Ex (Rgt_not_eq _ _ Zx)). -assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R). -rewrite Rabs_pos_eq in Ex. -destruct Ex as (H,H'); destruct H; split; trivial. -contradict Hx; easy. -now apply Rlt_le. -unfold generic_format, scaled_mantissa, canonic_exp. -rewrite ln_beta_unique with beta (x - ulp x)%R ex. -pattern x at 1 3 ; rewrite Fx. -unfold ulp, scaled_mantissa. -rewrite canonic_exp_fexp with (1 := Ex). -unfold F2R. simpl. -rewrite Rmult_minus_distr_r. -rewrite Rmult_assoc. -rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. -change (bpow 0) with (Z2R 1). -rewrite <- Z2R_minus. -rewrite Ztrunc_Z2R. -rewrite Z2R_minus. -rewrite Rmult_minus_distr_r. -now rewrite Rmult_1_l. -rewrite Rabs_pos_eq. +replace (ulp (x - ulp x)) with (ulp x). +ring. +assert (H:(x <> 0)%R) by auto with real. +assert (H':(x <> bpow (canonic_exp beta fexp x))%R). +unfold canonic_exp; intros M. +case_eq (ln_beta beta x); intros ex Hex T. +assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z). +rewrite T; reflexivity. +rewrite Lex in *. +clear T; simpl in *; specialize (Hex H). +rewrite Rabs_right in Hex. +2: apply Rle_ge; apply Rlt_le; easy. +assert (ex-1 < fexp ex < ex)%Z. +split ; apply (lt_bpow beta); rewrite <- M;[idtac|easy]. +destruct (proj1 Hex);[trivial|idtac]. +contradict Hx; auto with real. +omega. +rewrite 2!ulp_neq_0; try auto with real. +apply f_equal. +unfold canonic_exp; apply f_equal. +case_eq (ln_beta beta x); intros ex Hex T. +assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z). +rewrite T; reflexivity. +rewrite Lex in *; simpl in *; clear T. +specialize (Hex H). +apply sym_eq, ln_beta_unique. +rewrite Rabs_right. +rewrite Rabs_right in Hex. +2: apply Rle_ge; apply Rlt_le; easy. split. -apply pred_ge_bpow; trivial. -unfold ulp; intro H. -assert (ex-1 < canonic_exp beta fexp x < ex)%Z. -split ; apply (lt_bpow beta) ; rewrite <- H ; easy. -clear -H0. omega. -apply Ex'. -apply Rle_lt_trans with (2 := proj2 Ex'). -pattern x at 3 ; rewrite <- Rplus_0_r. +destruct Hex as ([H1|H1],H2). +apply Rle_trans with (x-ulp x)%R. +apply id_m_ulp_ge_bpow; trivial. +rewrite ulp_neq_0; trivial. +rewrite ulp_neq_0; trivial. +right; unfold canonic_exp; now rewrite Lex. +contradict Hx; auto with real. +apply Rle_lt_trans with (2:=proj2 Hex). +rewrite <- Rplus_0_r. apply Rplus_le_compat_l. -rewrite <-Ropp_0. +rewrite <- Ropp_0. apply Ropp_le_contravar. apply bpow_ge_0. +apply Rle_ge. apply Rle_0_minus. -pattern x at 2; rewrite Fx. -unfold ulp, F2R; simpl. -pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l. +rewrite Fx. +unfold F2R, canonic_exp; simpl. +rewrite Lex. +pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l. apply Rmult_le_compat_r. apply bpow_ge_0. -replace 1%R with (Z2R 1) by reflexivity. +replace 1%R with (Z2R (Zsucc 0)) by reflexivity. apply Z2R_le. -assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. +apply Zlt_le_succ. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -rewrite <- Fx. -apply Rle_lt_trans with (2:=proj1 Ex'). -apply bpow_ge_0. -omega. +now rewrite <- Fx. Qed. -Lemma generic_format_pred_2 : + +Lemma pred_pos_plus_ulp_aux2 : forall x, (0 < x)%R -> F x -> let e := ln_beta_val beta x (ln_beta beta x) in x = bpow (e - 1) -> - F (x - bpow (fexp (e - 1))). + (x - bpow (fexp (e-1)) <> 0)%R -> + ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R. Proof. -intros x Zx Fx e Hx. -pose (f:=(x - bpow (fexp (e - 1)))%R). -fold f. +intros x Zx Fx e Hxe Zp. +replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))). +ring. assert (He:(fexp (e-1) <= e-1)%Z). apply generic_format_bpow_inv with beta; trivial. -rewrite <- Hx; assumption. +rewrite <- Hxe; assumption. case (Zle_lt_or_eq _ _ He); clear He; intros He. -assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R. -unfold f; rewrite Hx. -unfold F2R; simpl. -rewrite Z2R_minus, Z2R_Zpower. -rewrite Rmult_minus_distr_r, Rmult_1_l. -rewrite <- bpow_plus. -now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. -omega. -rewrite H. -apply generic_format_F2R. -intros _. -apply Zeq_le. -apply canonic_exp_fexp. -rewrite <- H. -unfold f; rewrite Hx. +(* *) +rewrite ulp_neq_0; trivial. +apply f_equal. +unfold canonic_exp; apply f_equal. +apply sym_eq. +apply ln_beta_unique. rewrite Rabs_right. split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat ; apply bpow_le ; omega. +apply Rplus_le_compat; apply bpow_le; omega. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. @@ -697,308 +926,285 @@ now rewrite Zmult_1_r. rewrite <- bpow_plus. replace (1+(e-2))%Z with (e-1)%Z by ring. now right. -rewrite <- Rplus_0_r. +rewrite <- Rplus_0_r, Hxe. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. +rewrite Hxe. apply bpow_le. omega. -replace f with 0%R. -apply generic_format_0. -unfold f. -rewrite Hx, He. -ring. -Qed. - -Theorem generic_format_pred : +(* *) +contradict Zp. +rewrite Hxe, He; ring. +Qed. + +Lemma pred_pos_plus_ulp_aux3 : forall x, (0 < x)%R -> F x -> - F (pred x). + let e := ln_beta_val beta x (ln_beta beta x) in + x = bpow (e - 1) -> + (x - bpow (fexp (e-1)) = 0)%R -> + (ulp 0 = x)%R. Proof. -intros x Zx Fx. -unfold pred. -case Req_bool_spec; intros H. -now apply generic_format_pred_2. -now apply generic_format_pred_1. +intros x Hx Fx e H1 H2. +assert (H3:(x = bpow (fexp (e - 1)))). +now apply Rminus_diag_uniq. +assert (H4: (fexp (e-1) = e-1)%Z). +apply bpow_inj with beta. +now rewrite <- H1. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros K. +specialize (K (e-1)%Z). +contradict K; omega. +intros n Hn. +rewrite H3; apply f_equal. +case (Zle_or_lt n (e-1)); intros H6. +apply valid_exp; omega. +apply sym_eq, valid_exp; omega. Qed. -Theorem generic_format_plus_ulp : - forall { monotone_exp : Monotone_exp fexp }, - forall x, (x <> 0)%R -> - F x -> F (x + ulp x). -Proof with auto with typeclass_instances. -intros monotone_exp x Zx Fx. -destruct (Rtotal_order x 0) as [Hx|[Hx|Hx]]. -rewrite <- Ropp_involutive. -apply generic_format_opp. -rewrite Ropp_plus_distr, <- ulp_opp. -apply generic_format_opp in Fx. -destruct (Req_dec (-x) (bpow (ln_beta beta (-x) - 1))) as [Hx'|Hx']. -rewrite Hx' in Fx |- *. -apply generic_format_bpow_inv' in Fx... -unfold ulp, canonic_exp. -rewrite ln_beta_bpow. -revert Fx. -generalize (ln_beta_val _ _ (ln_beta beta (-x)) - 1)%Z. -clear -monotone_exp valid_exp. -intros e He. -destruct (Zle_lt_or_eq _ _ He) as [He1|He1]. -assert (He2 : e = (e - fexp (e + 1) + fexp (e + 1))%Z) by ring. -rewrite He2 at 1. -rewrite bpow_plus. -assert (Hb := Z2R_Zpower beta _ (Zle_minus_le_0 _ _ He)). -match goal with |- F (?a * ?b + - ?b) => - replace (a * b + -b)%R with ((a - 1) * b)%R by ring end. -rewrite <- Hb. -rewrite <- (Z2R_minus _ 1). -change (F (F2R (Float beta (Zpower beta (e - fexp (e + 1)) - 1) (fexp (e + 1))))). -apply generic_format_F2R. -intros Zb. -unfold canonic_exp. -rewrite ln_beta_F2R with (1 := Zb). -rewrite (ln_beta_unique beta _ (e - fexp (e + 1))). -apply monotone_exp. -rewrite <- He2. -apply Zle_succ. -rewrite Rabs_pos_eq. -rewrite Z2R_minus, Hb. -split. -apply Rplus_le_reg_r with (- bpow (e - fexp (e + 1) - 1) + Z2R 1)%R. -apply Rmult_le_reg_r with (bpow (-(e - fexp (e+1) - 1))). -apply bpow_gt_0. -ring_simplify. -apply Rle_trans with R1. -rewrite Rmult_1_l. -apply (bpow_le _ _ 0). -clear -He1 ; omega. -rewrite Ropp_mult_distr_l_reverse. -rewrite <- 2!bpow_plus. -ring_simplify (e - fexp (e + 1) - 1 + - (e - fexp (e + 1) - 1))%Z. -ring_simplify (- (e - fexp (e + 1) - 1) + (e - fexp (e + 1)))%Z. -rewrite bpow_1. -rewrite <- (Z2R_plus (-1) _). -apply (Z2R_le 1). -generalize (Zle_bool_imp_le _ _ (radix_prop beta)). -clear ; omega. -rewrite <- (Rplus_0_r (bpow (e - fexp (e + 1)))) at 2. -apply Rplus_lt_compat_l. -now apply (Z2R_lt (-1) 0). -rewrite Z2R_minus. -apply Rle_0_minus. -rewrite Hb. -apply (bpow_le _ 0). -now apply Zle_minus_le_0. -rewrite He1, Rplus_opp_r. -apply generic_format_0. -apply generic_format_pred_1 ; try easy. -rewrite <- Ropp_0. -now apply Ropp_lt_contravar. -now elim Zx. -now apply generic_format_succ. -Qed. -Theorem generic_format_minus_ulp : - forall { monotone_exp : Monotone_exp fexp }, - forall x, (x <> 0)%R -> - F x -> F (x - ulp x). + + +(** The following one is false for x = 0 in FTZ *) + +Theorem pred_pos_plus_ulp : + forall x, (0 < x)%R -> F x -> + (pred_pos x + ulp (pred_pos x) = x)%R. Proof. -intros monotone_exp x Zx Fx. -replace (x - ulp x)%R with (-(-x + ulp x))%R by ring. -apply generic_format_opp. -rewrite <- ulp_opp. -apply generic_format_plus_ulp. -contradict Zx. -rewrite <- (Ropp_involutive x), Zx. -apply Ropp_0. -now apply generic_format_opp. +intros x Zx Fx. +unfold pred_pos. +case Req_bool_spec; intros H. +case (Req_EM_T (x - bpow (fexp (ln_beta_val beta x (ln_beta beta x) -1))) 0); intros H1. +rewrite H1, Rplus_0_l. +now apply pred_pos_plus_ulp_aux3. +now apply pred_pos_plus_ulp_aux2. +now apply pred_pos_plus_ulp_aux1. Qed. -Lemma pred_plus_ulp_1 : + + + +(** Rounding x + small epsilon *) + +Theorem ln_beta_plus_eps: forall x, (0 < x)%R -> F x -> - x <> bpow (ln_beta beta x - 1) -> - ((x - ulp x) + ulp (x-ulp x) = x)%R. + forall eps, (0 <= eps < ulp x)%R -> + ln_beta beta (x + eps) = ln_beta beta x :> Z. Proof. -intros x Zx Fx Hx. -replace (ulp (x - ulp x)) with (ulp x). -ring. -unfold ulp at 1 2; apply f_equal. -unfold canonic_exp; apply f_equal. -destruct (ln_beta beta x) as (ex, Hex). -simpl in *. -assert (x <> 0)%R by auto with real. -specialize (Hex H). -apply sym_eq. +intros x Zx Fx eps Heps. +destruct (ln_beta beta x) as (ex, He). +simpl. +specialize (He (Rgt_not_eq _ _ Zx)). apply ln_beta_unique. -rewrite Rabs_right. -rewrite Rabs_right in Hex. -2: apply Rle_ge; apply Rlt_le; easy. +rewrite Rabs_pos_eq. +rewrite Rabs_pos_eq in He. split. -destruct Hex as ([H1|H1],H2). -apply pred_ge_bpow; trivial. -unfold ulp; intros H3. -assert (ex-1 < canonic_exp beta fexp x < ex)%Z. -split ; apply (lt_bpow beta) ; rewrite <- H3 ; easy. -omega. -contradict Hx; auto with real. -apply Rle_lt_trans with (2:=proj2 Hex). -rewrite <- Rplus_0_r. -apply Rplus_le_compat_l. -rewrite <- Ropp_0. -apply Ropp_le_contravar. -apply bpow_ge_0. -apply Rle_ge. -apply Rle_0_minus. -pattern x at 2; rewrite Fx. -unfold ulp, F2R; simpl. -pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l. -apply Rmult_le_compat_r. -apply bpow_ge_0. -replace 1%R with (Z2R (Zsucc 0)) by reflexivity. -apply Z2R_le. -apply Zlt_le_succ. +apply Rle_trans with (1 := proj1 He). +pattern x at 1 ; rewrite <- Rplus_0_r. +now apply Rplus_le_compat_l. +apply Rlt_le_trans with (x + ulp x)%R. +now apply Rplus_lt_compat_l. +pattern x at 1 ; rewrite Fx. +rewrite ulp_neq_0. +unfold F2R. simpl. +pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. +rewrite <- Rmult_plus_distr_r. +change 1%R with (Z2R 1). +rewrite <- Z2R_plus. +change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R. +apply F2R_p1_le_bpow. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). now rewrite <- Fx. +now rewrite <- Fx. +now apply Rgt_not_eq. +now apply Rlt_le. +apply Rplus_le_le_0_compat. +now apply Rlt_le. +apply Heps. Qed. -Lemma pred_plus_ulp_2 : - forall x, (0 < x)%R -> F x -> - let e := ln_beta_val beta x (ln_beta beta x) in - x = bpow (e - 1) -> - (x - bpow (fexp (e-1)) <> 0)%R -> - ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R. +Theorem round_DN_plus_eps_pos: + forall x, (0 <= x)%R -> F x -> + forall eps, (0 <= eps < ulp x)%R -> + round beta fexp Zfloor (x + eps) = x. Proof. -intros x Zx Fx e Hxe Zp. -replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))). -ring. -assert (He:(fexp (e-1) <= e-1)%Z). -apply generic_format_bpow_inv with beta; trivial. -rewrite <- Hxe; assumption. -case (Zle_lt_or_eq _ _ He); clear He; intros He. -(* *) -unfold ulp; apply f_equal. -unfold canonic_exp; apply f_equal. -apply sym_eq. -apply ln_beta_unique. -rewrite Rabs_right. +intros x Zx Fx eps Heps. +destruct Zx as [Zx|Zx]. +(* . 0 < x *) +pattern x at 2 ; rewrite Fx. +unfold round. +unfold scaled_mantissa. simpl. +unfold canonic_exp at 1 2. +rewrite ln_beta_plus_eps ; trivial. +apply (f_equal (fun m => F2R (Float beta m _))). +rewrite Ztrunc_floor. +apply Zfloor_imp. split. -apply Rplus_le_reg_l with (bpow (fexp (e-1))). -ring_simplify. -apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat; apply bpow_le; omega. -apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. -apply Rle_trans with (bpow 1*bpow (e - 2))%R. +apply (Rle_trans _ _ _ (Zfloor_lb _)). apply Rmult_le_compat_r. apply bpow_ge_0. -replace 2%R with (Z2R 2) by reflexivity. -replace (bpow 1) with (Z2R beta). -apply Z2R_le. -apply <- Zle_is_le_bool. -now destruct beta. -simpl. -unfold Zpower_pos; simpl. -now rewrite Zmult_1_r. +pattern x at 1 ; rewrite <- Rplus_0_r. +now apply Rplus_le_compat_l. +apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R. +apply Rmult_lt_compat_r. +apply bpow_gt_0. +now apply Rplus_lt_compat_l. +rewrite Rmult_plus_distr_r. +rewrite Z2R_plus. +apply Rplus_le_compat. +pattern x at 1 3 ; rewrite Fx. +unfold F2R. simpl. +rewrite Rmult_assoc. rewrite <- bpow_plus. -replace (1+(e-2))%Z with (e-1)%Z by ring. -now right. -rewrite <- Rplus_0_r, Hxe. -apply Rplus_lt_compat_l. -rewrite <- Ropp_0. -apply Ropp_lt_contravar. +rewrite Zplus_opp_r. +rewrite Rmult_1_r. +rewrite Zfloor_Z2R. +apply Rle_refl. +rewrite ulp_neq_0. +2: now apply Rgt_not_eq. +rewrite <- bpow_plus. +rewrite Zplus_opp_r. +apply Rle_refl. +apply Rmult_le_pos. +now apply Rlt_le. +apply bpow_ge_0. +(* . x=0 *) +rewrite <- Zx, Rplus_0_l; rewrite <- Zx in Heps. +case (proj1 Heps); intros P. +unfold round, scaled_mantissa, canonic_exp. +revert Heps; unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros _ (H1,H2). +absurd (0 < 0)%R; auto with real. +now apply Rle_lt_trans with (1:=H1). +intros n Hn H. +assert (fexp (ln_beta beta eps) = fexp n). +apply valid_exp; try assumption. +assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega]. +apply lt_bpow with beta. +apply Rle_lt_trans with (2:=proj2 H). +destruct (ln_beta beta eps) as (e,He). +simpl; rewrite Rabs_pos_eq in He. +now apply He, Rgt_not_eq. +now left. +replace (Zfloor (eps * bpow (- fexp (ln_beta beta eps)))) with 0%Z. +unfold F2R; simpl; ring. +apply sym_eq, Zfloor_imp. +split. +apply Rmult_le_pos. +now left. +apply bpow_ge_0. +apply Rmult_lt_reg_r with (bpow (fexp n)). apply bpow_gt_0. -apply Rle_ge; apply Rle_0_minus. -rewrite Hxe. -apply bpow_le. -omega. -(* *) -contradict Zp. -rewrite Hxe, He; ring. +rewrite Rmult_assoc, <- bpow_plus. +rewrite H0; ring_simplify (-fexp n + fexp n)%Z. +simpl; rewrite Rmult_1_l, Rmult_1_r. +apply H. +rewrite <- P, round_0; trivial. +apply valid_rnd_DN. Qed. -Theorem pred_plus_ulp : - forall x, (0 < x)%R -> F x -> - (pred x <> 0)%R -> - (pred x + ulp (pred x) = x)%R. -Proof. -intros x Zx Fx. -unfold pred. -case Req_bool_spec; intros H Zp. -now apply pred_plus_ulp_2. -now apply pred_plus_ulp_1. -Qed. -Theorem pred_lt_id : - forall x, - (pred x < x)%R. -Proof. -intros. -unfold pred. -case Req_bool_spec; intros H. -(* *) -rewrite <- Rplus_0_r. -apply Rplus_lt_compat_l. -rewrite <- Ropp_0. -apply Ropp_lt_contravar. +Theorem round_UP_plus_eps_pos : + forall x, (0 <= x)%R -> F x -> + forall eps, (0 < eps <= ulp x)%R -> + round beta fexp Zceil (x + eps) = (x + ulp x)%R. +Proof with auto with typeclass_instances. +intros x Zx Fx eps. +case Zx; intros Zx1. +(* . 0 < x *) +intros (Heps1,[Heps2|Heps2]). +assert (Heps: (0 <= eps < ulp x)%R). +split. +now apply Rlt_le. +exact Heps2. +assert (Hd := round_DN_plus_eps_pos x Zx Fx eps Heps). +rewrite round_UP_DN_ulp. +rewrite Hd. +rewrite 2!ulp_neq_0. +unfold canonic_exp. +now rewrite ln_beta_plus_eps. +now apply Rgt_not_eq. +now apply Rgt_not_eq, Rplus_lt_0_compat. +intros Fs. +rewrite round_generic in Hd... +apply Rgt_not_eq with (2 := Hd). +pattern x at 2 ; rewrite <- Rplus_0_r. +now apply Rplus_lt_compat_l. +rewrite Heps2. +apply round_generic... +now apply generic_format_succ_aux1. +(* . x=0 *) +rewrite <- Zx1, 2!Rplus_0_l. +intros Heps. +case (proj2 Heps). +unfold round, scaled_mantissa, canonic_exp. +unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros H2. +intros J; absurd (0 < 0)%R; auto with real. +apply Rlt_trans with eps; try assumption; apply Heps. +intros n Hn H. +assert (fexp (ln_beta beta eps) = fexp n). +apply valid_exp; try assumption. +assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega]. +apply lt_bpow with beta. +apply Rle_lt_trans with (2:=H). +destruct (ln_beta beta eps) as (e,He). +simpl; rewrite Rabs_pos_eq in He. +now apply He, Rgt_not_eq. +now left. +replace (Zceil (eps * bpow (- fexp (ln_beta beta eps)))) with 1%Z. +unfold F2R; simpl; rewrite H0; ring. +apply sym_eq, Zceil_imp. +split. +simpl; apply Rmult_lt_0_compat. +apply Heps. apply bpow_gt_0. -(* *) -rewrite <- Rplus_0_r. -apply Rplus_lt_compat_l. -rewrite <- Ropp_0. -apply Ropp_lt_contravar. +apply Rmult_le_reg_r with (bpow (fexp n)). apply bpow_gt_0. +rewrite Rmult_assoc, <- bpow_plus. +rewrite H0; ring_simplify (-fexp n + fexp n)%Z. +simpl; rewrite Rmult_1_l, Rmult_1_r. +now left. +intros P; rewrite P. +apply round_generic... +apply generic_format_ulp_0. Qed. -Theorem pred_ge_0 : - forall x, - (0 < x)%R -> F x -> (0 <= pred x)%R. -intros x Zx Fx. -unfold pred. -case Req_bool_spec; intros H. -(* *) -apply Rle_0_minus. -rewrite H. -apply bpow_le. -destruct (ln_beta beta x) as (ex,Ex) ; simpl. -rewrite ln_beta_bpow. -ring_simplify (ex - 1 + 1 - 1)%Z. -apply generic_format_bpow_inv with beta; trivial. -simpl in H. -rewrite <- H; assumption. -apply Rle_0_minus. -now apply ulp_le_id. -Qed. -Theorem round_UP_pred : - forall x, (0 < pred x)%R -> F x -> +Theorem round_UP_pred_plus_eps_pos : + forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x) )%R -> round beta fexp Zceil (pred x + eps) = x. Proof. intros x Hx Fx eps Heps. -rewrite round_UP_succ; trivial. -apply pred_plus_ulp; trivial. -apply Rlt_trans with (1:=Hx). -apply pred_lt_id. -now apply Rgt_not_eq. +rewrite round_UP_plus_eps_pos; trivial. +rewrite pred_eq_pos. +apply pred_pos_plus_ulp; trivial. +now left. +now apply pred_ge_0. apply generic_format_pred; trivial. -apply Rlt_trans with (1:=Hx). -apply pred_lt_id. Qed. -Theorem round_DN_pred : - forall x, (0 < pred x)%R -> F x -> +Theorem round_DN_minus_eps_pos : + forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x))%R -> round beta fexp Zfloor (x - eps) = pred x. Proof. -intros x Hpx Fx eps Heps. -assert (Hx:(0 < x)%R). -apply Rlt_trans with (1:=Hpx). -apply pred_lt_id. -replace (x-eps)%R with (pred x + (ulp (pred x)-eps))%R. -2: pattern x at 3; rewrite <- (pred_plus_ulp x); trivial. +intros x Hpx Fx eps. +rewrite pred_eq_pos;[intros Heps|now left]. +replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R. +2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial. 2: ring. -2: now apply Rgt_not_eq. -rewrite round_DN_succ; trivial. -now apply generic_format_pred. +rewrite round_DN_plus_eps_pos; trivial. +now apply pred_pos_ge_0. +now apply generic_format_pred_pos. split. apply Rle_0_minus. now apply Heps. @@ -1009,15 +1215,96 @@ apply Ropp_lt_contravar. now apply Heps. Qed. -Lemma le_pred_lt_aux : + +Theorem round_DN_plus_eps: + forall x, F x -> + forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x) + else (ulp (pred (-x))))%R -> + round beta fexp Zfloor (x + eps) = x. +Proof. +intros x Fx eps Heps. +case (Rle_or_lt 0 x); intros Zx. +apply round_DN_plus_eps_pos; try assumption. +split; try apply Heps. +rewrite Rle_bool_true in Heps; trivial. +now apply Heps. +(* *) +rewrite Rle_bool_false in Heps; trivial. +rewrite <- (Ropp_involutive (x+eps)). +pattern x at 2; rewrite <- (Ropp_involutive x). +rewrite round_DN_opp. +apply f_equal. +replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R. +rewrite round_UP_pred_plus_eps_pos; try reflexivity. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +split. +apply Rplus_lt_reg_l with eps; ring_simplify. +apply Heps. +apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify. +apply Heps. +unfold pred. +rewrite Ropp_involutive. +unfold succ; rewrite Rle_bool_false; try assumption. +rewrite Ropp_involutive; unfold Rminus. +rewrite <- Rplus_assoc, pred_pos_plus_ulp. +ring. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +Qed. + + +Theorem round_UP_plus_eps : + forall x, F x -> + forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x) + else (ulp (pred (-x))))%R -> + round beta fexp Zceil (x + eps) = (succ x)%R. +Proof with auto with typeclass_instances. +intros x Fx eps Heps. +case (Rle_or_lt 0 x); intros Zx. +rewrite succ_eq_pos; try assumption. +rewrite Rle_bool_true in Heps; trivial. +apply round_UP_plus_eps_pos; assumption. +(* *) +rewrite Rle_bool_false in Heps; trivial. +rewrite <- (Ropp_involutive (x+eps)). +rewrite <- (Ropp_involutive (succ x)). +rewrite round_UP_opp. +apply f_equal. +replace (-(x+eps))%R with (-succ x + (-eps + ulp (pred (-x))))%R. +apply round_DN_plus_eps_pos. +rewrite <- pred_opp. +apply pred_ge_0. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +now apply generic_format_opp, generic_format_succ. +split. +apply Rplus_le_reg_l with eps; ring_simplify. +apply Heps. +unfold pred; rewrite Ropp_involutive. +apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify. +apply Heps. +unfold succ; rewrite Rle_bool_false; try assumption. +apply trans_eq with (-x +-eps)%R;[idtac|ring]. +pattern (-x)%R at 3; rewrite <- (pred_pos_plus_ulp (-x)). +rewrite pred_eq_pos. +ring. +left; now apply Ropp_0_gt_lt_contravar. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +Qed. + + +Lemma le_pred_pos_lt : forall x y, F x -> F y -> - (0 < x < y)%R -> - (x <= pred y)%R. + (0 <= x < y)%R -> + (x <= pred_pos y)%R. Proof with auto with typeclass_instances. -intros x y Hx Hy H. +intros x y Fx Fy H. +case (proj1 H); intros V. assert (Zy:(0 < y)%R). -apply Rlt_trans with (1:=proj1 H). +apply Rle_lt_trans with (1:=proj1 H). apply H. (* *) assert (Zp: (0 < pred y)%R). @@ -1025,7 +1312,8 @@ assert (Zp:(0 <= pred y)%R). apply pred_ge_0 ; trivial. destruct Zp; trivial. generalize H0. -unfold pred. +rewrite pred_eq_pos;[idtac|now left]. +unfold pred_pos. destruct (ln_beta beta y) as (ey,Hey); simpl. case Req_bool_spec; intros Hy2. (* . *) @@ -1048,124 +1336,758 @@ now apply Rgt_ge. now apply Rgt_ge. apply Hey. now apply Rgt_not_eq. -case (Zle_lt_or_eq _ _ H2); intros Hexy. -assert (fexp ex = fexp (ey-1))%Z. -apply valid_exp. -omega. -rewrite <- H1. -omega. -absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. -omega. -split. -apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -now rewrite <- Hx. -apply lt_Z2R. -apply Rmult_lt_reg_r with (bpow (canonic_exp beta fexp x)). +case (Zle_lt_or_eq _ _ H2); intros Hexy. +assert (fexp ex = fexp (ey-1))%Z. +apply valid_exp. +omega. +rewrite <- H1. +omega. +absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. +omega. +split. +apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). +now rewrite <- Fx. +apply lt_Z2R. +apply Rmult_lt_reg_r with (bpow (canonic_exp beta fexp x)). +apply bpow_gt_0. +replace (Z2R (Ztrunc (scaled_mantissa beta fexp x)) * + bpow (canonic_exp beta fexp x))%R with x. +rewrite Rmult_1_l. +unfold canonic_exp. +rewrite ln_beta_unique with beta x ex. +rewrite H3,<-H1, <- Hy2. +apply H. +exact Hex. +absurd (y <= x)%R. +now apply Rlt_not_le. +rewrite Rabs_right in Hex. +apply Rle_trans with (2:=proj1 Hex). +rewrite Hexy, Hy2. +now apply Rle_refl. +now apply Rgt_ge. +(* . *) +intros Hy3. +assert (y = bpow (fexp ey))%R. +apply Rminus_diag_uniq. +rewrite Hy3. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold canonic_exp. +rewrite (ln_beta_unique beta y ey); trivial. +apply Hey. +now apply Rgt_not_eq. +contradict Hy2. +rewrite H1. +apply f_equal. +apply Zplus_reg_l with 1%Z. +ring_simplify. +apply trans_eq with (ln_beta beta y). +apply sym_eq; apply ln_beta_unique. +rewrite H1, Rabs_right. +split. +apply bpow_le. +omega. +apply bpow_lt. +omega. +apply Rle_ge; apply bpow_ge_0. +apply ln_beta_unique. +apply Hey. +now apply Rgt_not_eq. +(* *) +case (Rle_or_lt (ulp (pred_pos y)) (y-x)); intros H1. +(* . *) +apply Rplus_le_reg_r with (-x + ulp (pred_pos y))%R. +ring_simplify (x+(-x+ulp (pred_pos y)))%R. +apply Rle_trans with (1:=H1). +rewrite <- (pred_pos_plus_ulp y) at 1; trivial. +apply Req_le; ring. +(* . *) +replace x with (y-(y-x))%R by ring. +rewrite <- pred_eq_pos;[idtac|now left]. +rewrite <- round_DN_minus_eps_pos with (eps:=(y-x)%R); try easy. +ring_simplify (y-(y-x))%R. +apply Req_le. +apply sym_eq. +apply round_generic... +split; trivial. +now apply Rlt_Rminus. +rewrite pred_eq_pos;[idtac|now left]. +now apply Rlt_le. +rewrite <- V; apply pred_pos_ge_0; trivial. +apply Rle_lt_trans with (1:=proj1 H); apply H. +Qed. + +Theorem succ_le_lt_aux: + forall x y, + F x -> F y -> + (0 <= x)%R -> (x < y)%R -> + (succ x <= y)%R. +Proof with auto with typeclass_instances. +intros x y Hx Hy Zx H. +rewrite succ_eq_pos; trivial. +case (Rle_or_lt (ulp x) (y-x)); intros H1. +apply Rplus_le_reg_r with (-x)%R. +now ring_simplify (x+ulp x + -x)%R. +replace y with (x+(y-x))%R by ring. +absurd (x < y)%R. +2: apply H. +apply Rle_not_lt; apply Req_le. +rewrite <- round_DN_plus_eps_pos with (eps:=(y-x)%R); try easy. +ring_simplify (x+(y-x))%R. +apply sym_eq. +apply round_generic... +split; trivial. +apply Rlt_le; now apply Rlt_Rminus. +Qed. + +Theorem succ_le_lt: + forall x y, + F x -> F y -> + (x < y)%R -> + (succ x <= y)%R. +Proof with auto with typeclass_instances. +intros x y Fx Fy H. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +now apply succ_le_lt_aux. +unfold succ; rewrite Rle_bool_false; try assumption. +case (Rle_or_lt y 0); intros Hy. +rewrite <- (Ropp_involutive y). +apply Ropp_le_contravar. +apply le_pred_pos_lt. +now apply generic_format_opp. +now apply generic_format_opp. +split. +rewrite <- Ropp_0; now apply Ropp_le_contravar. +now apply Ropp_lt_contravar. +apply Rle_trans with (-0)%R. +apply Ropp_le_contravar. +apply pred_pos_ge_0. +rewrite <- Ropp_0; now apply Ropp_lt_contravar. +now apply generic_format_opp. +rewrite Ropp_0; now left. +Qed. + +Theorem le_pred_lt : + forall x y, + F x -> F y -> + (x < y)%R -> + (x <= pred y)%R. +Proof. +intros x y Fx Fy Hxy. +rewrite <- (Ropp_involutive x). +unfold pred; apply Ropp_le_contravar. +apply succ_le_lt. +now apply generic_format_opp. +now apply generic_format_opp. +now apply Ropp_lt_contravar. +Qed. + + +Theorem lt_succ_le: + forall x y, + F x -> F y -> (y <> 0)%R -> + (x <= y)%R -> + (x < succ y)%R. +Proof. +intros x y Fx Fy Zy Hxy. +case (Rle_or_lt (succ y) x); trivial; intros H. +absurd (succ y = y)%R. +apply Rgt_not_eq. +now apply succ_gt_id. +apply Rle_antisym. +now apply Rle_trans with x. +apply succ_ge_id. +Qed. + + +Theorem succ_pred_aux : forall x, F x -> (0 < x)%R -> succ (pred x)=x. +Proof. +intros x Fx Hx. +rewrite pred_eq_pos;[idtac|now left]. +rewrite succ_eq_pos. +2: now apply pred_pos_ge_0. +now apply pred_pos_plus_ulp. +Qed. + +Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R. +Proof. +unfold succ; rewrite Rle_bool_true. +2: apply Rle_refl. +rewrite Rplus_0_l. +rewrite pred_eq_pos. +2: apply ulp_ge_0. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +(* *) +intros (H1,H2); rewrite H1. +unfold pred_pos; rewrite Req_bool_false. +2: apply Rlt_not_eq, bpow_gt_0. +unfold ulp; rewrite Req_bool_true; trivial. +rewrite H1; ring. +(* *) +intros (n,(H1,H2)); rewrite H1. +unfold pred_pos. +rewrite ln_beta_bpow. +replace (fexp n + 1 - 1)%Z with (fexp n) by ring. +rewrite Req_bool_true; trivial. +apply Rminus_diag_eq, f_equal. +apply sym_eq, valid_exp; omega. +Qed. + +Theorem pred_succ_aux : forall x, F x -> (0 < x)%R -> pred (succ x)=x. +Proof. +intros x Fx Hx. +rewrite succ_eq_pos;[idtac|now left]. +rewrite pred_eq_pos. +2: apply Rplus_le_le_0_compat;[now left| apply ulp_ge_0]. +unfold pred_pos. +case Req_bool_spec; intros H1. +(* *) +pose (l:=(ln_beta beta (x+ulp x))). +rewrite H1 at 1; fold l. +apply Rplus_eq_reg_r with (ulp x). +rewrite H1; fold l. +rewrite (ulp_neq_0 x) at 3. +2: now apply Rgt_not_eq. +unfold canonic_exp. +replace (fexp (ln_beta beta x)) with (fexp (l-1))%Z. +ring. +apply f_equal, sym_eq. +apply Zle_antisym. +assert (ln_beta beta x - 1 < l - 1)%Z;[idtac|omega]. +apply lt_bpow with beta. +unfold l; rewrite <- H1. +apply Rle_lt_trans with x. +destruct (ln_beta beta x) as (e,He); simpl. +rewrite <- (Rabs_right x) at 1. +2: apply Rle_ge; now left. +now apply He, Rgt_not_eq. +apply Rplus_lt_reg_l with (-x)%R; ring_simplify. +rewrite ulp_neq_0. +apply bpow_gt_0. +now apply Rgt_not_eq. +apply le_bpow with beta. +unfold l; rewrite <- H1. +apply id_p_ulp_le_bpow; trivial. +rewrite <- (Rabs_right x) at 1. +2: apply Rle_ge; now left. +apply bpow_ln_beta_gt. +(* *) +replace (ulp (x+ ulp x)) with (ulp x). +ring. +rewrite ulp_neq_0 at 1. +2: now apply Rgt_not_eq. +rewrite ulp_neq_0 at 1. +2: apply Rgt_not_eq, Rlt_gt. +2: apply Rlt_le_trans with (1:=Hx). +2: apply Rplus_le_reg_l with (-x)%R; ring_simplify. +2: apply ulp_ge_0. +apply f_equal; unfold canonic_exp; apply f_equal. +apply sym_eq, ln_beta_unique. +rewrite Rabs_right. +2: apply Rle_ge; left. +2: apply Rlt_le_trans with (1:=Hx). +2: apply Rplus_le_reg_l with (-x)%R; ring_simplify. +2: apply ulp_ge_0. +destruct (ln_beta beta x) as (e,He); simpl. +rewrite Rabs_right in He. +2: apply Rle_ge; now left. +split. +apply Rle_trans with x. +apply He, Rgt_not_eq; assumption. +apply Rplus_le_reg_l with (-x)%R; ring_simplify. +apply ulp_ge_0. +case (Rle_lt_or_eq_dec (x+ulp x) (bpow e)); trivial. +apply id_p_ulp_le_bpow; trivial. +apply He, Rgt_not_eq; assumption. +intros K; contradict H1. +rewrite K, ln_beta_bpow. +apply f_equal; ring. +Qed. + + + +Theorem succ_pred : forall x, F x -> succ (pred x)=x. +Proof. +intros x Fx. +case (Rle_or_lt 0 x); intros Hx. +destruct Hx as [Hx|Hx]. +now apply succ_pred_aux. +rewrite <- Hx. +rewrite pred_eq_opp_succ_opp, succ_opp, Ropp_0. +rewrite pred_succ_aux_0; ring. +rewrite pred_eq_opp_succ_opp, succ_opp. +rewrite pred_succ_aux. +ring. +now apply generic_format_opp. +now apply Ropp_0_gt_lt_contravar. +Qed. + +Theorem pred_succ : forall x, F x -> pred (succ x)=x. +Proof. +intros x Fx. +case (Rle_or_lt 0 x); intros Hx. +destruct Hx as [Hx|Hx]. +now apply pred_succ_aux. +rewrite <- Hx. +apply pred_succ_aux_0. +rewrite succ_eq_opp_pred_opp, pred_opp. +rewrite succ_pred_aux. +ring. +now apply generic_format_opp. +now apply Ropp_0_gt_lt_contravar. +Qed. + + +Theorem round_UP_pred_plus_eps : + forall x, F x -> + forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) + else (ulp (pred x)))%R -> + round beta fexp Zceil (pred x + eps) = x. +Proof. +intros x Fx eps Heps. +rewrite round_UP_plus_eps. +now apply succ_pred. +now apply generic_format_pred. +unfold pred at 4. +rewrite Ropp_involutive, pred_succ. +rewrite ulp_opp. +generalize Heps; case (Rle_bool_spec x 0); intros H1 H2. +rewrite Rle_bool_false; trivial. +case H1; intros H1'. +apply Rlt_le_trans with (2:=H1). +apply pred_lt_id. +now apply Rlt_not_eq. +rewrite H1'; unfold pred, succ. +rewrite Ropp_0; rewrite Rle_bool_true;[idtac|now right]. +rewrite Rplus_0_l. +rewrite <- Ropp_0; apply Ropp_lt_contravar. +apply Rlt_le_trans with (1:=proj1 H2). +apply Rle_trans with (1:=proj2 H2). +rewrite Ropp_0, H1'. +now right. +rewrite Rle_bool_true; trivial. +now apply pred_ge_0. +now apply generic_format_opp. +Qed. + + +Theorem round_DN_minus_eps: + forall x, F x -> + forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) + else (ulp (pred x)))%R -> + round beta fexp Zfloor (x - eps) = pred x. +Proof. +intros x Fx eps Heps. +replace (x-eps)%R with (-(-x+eps))%R by ring. +rewrite round_DN_opp. +unfold pred; apply f_equal. +pattern (-x)%R at 1; rewrite <- (pred_succ (-x)). +apply round_UP_pred_plus_eps. +now apply generic_format_succ, generic_format_opp. +rewrite pred_succ. +rewrite ulp_opp. +generalize Heps; case (Rle_bool_spec x 0); intros H1 H2. +rewrite Rle_bool_false; trivial. +case H1; intros H1'. +apply Rlt_le_trans with (-x)%R. +now apply Ropp_0_gt_lt_contravar. +apply succ_ge_id. +rewrite H1', Ropp_0, succ_eq_pos;[idtac|now right]. +rewrite Rplus_0_l. +apply Rlt_le_trans with (1:=proj1 H2). +rewrite H1' in H2; apply H2. +rewrite Rle_bool_true. +now rewrite succ_opp, ulp_opp. +rewrite succ_opp. +rewrite <- Ropp_0; apply Ropp_le_contravar. +now apply pred_ge_0. +now apply generic_format_opp. +now apply generic_format_opp. +Qed. + +(** Error of a rounding, expressed in number of ulps *) +(** false for x=0 in the FLX format *) +(* was ulp_error *) +Theorem error_lt_ulp : + forall rnd { Zrnd : Valid_rnd rnd } x, + (x <> 0)%R -> + (Rabs (round beta fexp rnd x - x) < ulp x)%R. +Proof with auto with typeclass_instances. +intros rnd Zrnd x Zx. +destruct (generic_format_EM beta fexp x) as [Hx|Hx]. +(* x = rnd x *) +rewrite round_generic... +unfold Rminus. +rewrite Rplus_opp_r, Rabs_R0. +rewrite ulp_neq_0; trivial. +apply bpow_gt_0. +(* x <> rnd x *) +destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H. +(* . *) +rewrite Rabs_left1. +rewrite Ropp_minus_distr. +apply Rplus_lt_reg_l with (round beta fexp Zfloor x). +rewrite <- round_UP_DN_ulp with (1 := Hx). +ring_simplify. +assert (Hu: (x <= round beta fexp Zceil x)%R). +apply round_UP_pt... +destruct Hu as [Hu|Hu]. +exact Hu. +elim Hx. +rewrite Hu. +apply generic_format_round... +apply Rle_minus. +apply round_DN_pt... +(* . *) +rewrite Rabs_pos_eq. +rewrite round_UP_DN_ulp with (1 := Hx). +apply Rplus_lt_reg_r with (x - ulp x)%R. +ring_simplify. +assert (Hd: (round beta fexp Zfloor x <= x)%R). +apply round_DN_pt... +destruct Hd as [Hd|Hd]. +exact Hd. +elim Hx. +rewrite <- Hd. +apply generic_format_round... +apply Rle_0_minus. +apply round_UP_pt... +Qed. + +(* was ulp_error_le *) +Theorem error_le_ulp : + forall rnd { Zrnd : Valid_rnd rnd } x, + (Rabs (round beta fexp rnd x - x) <= ulp x)%R. +Proof with auto with typeclass_instances. +intros rnd Zrnd x. +case (Req_dec x 0). +intros Zx; rewrite Zx, round_0... +unfold Rminus; rewrite Rplus_0_l, Ropp_0, Rabs_R0. +apply ulp_ge_0. +intros Zx; left. +now apply error_lt_ulp. +Qed. + +(* was ulp_half_error *) +Theorem error_le_half_ulp : + forall choice x, + (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R. +Proof with auto with typeclass_instances. +intros choice x. +destruct (generic_format_EM beta fexp x) as [Hx|Hx]. +(* x = rnd x *) +rewrite round_generic... +unfold Rminus. +rewrite Rplus_opp_r, Rabs_R0. +apply Rmult_le_pos. +apply Rlt_le. +apply Rinv_0_lt_compat. +now apply (Z2R_lt 0 2). +apply ulp_ge_0. +(* x <> rnd x *) +set (d := round beta fexp Zfloor x). +destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2). +destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. +(* . rnd(x) = rndd(x) *) +apply Rle_trans with (Rabs (d - x)). +apply Hr2. +apply (round_DN_pt beta fexp x). +rewrite Rabs_left1. +rewrite Ropp_minus_distr. +apply Rmult_le_reg_r with 2%R. +now apply (Z2R_lt 0 2). +apply Rplus_le_reg_r with (d - x)%R. +ring_simplify. +apply Rle_trans with (1 := H). +right. field. +apply Rle_minus. +apply (round_DN_pt beta fexp x). +(* . rnd(x) = rndu(x) *) +assert (Hu: (d + ulp x)%R = round beta fexp Zceil x). +unfold d. +now rewrite <- round_UP_DN_ulp. +apply Rle_trans with (Rabs (d + ulp x - x)). +apply Hr2. +rewrite Hu. +apply (round_UP_pt beta fexp x). +rewrite Rabs_pos_eq. +apply Rmult_le_reg_r with 2%R. +now apply (Z2R_lt 0 2). +apply Rplus_le_reg_r with (- (d + ulp x - x))%R. +ring_simplify. +apply Rlt_le. +apply Rlt_le_trans with (1 := H). +right. field. +apply Rle_0_minus. +rewrite Hu. +apply (round_UP_pt beta fexp x). +Qed. + + +Theorem ulp_DN : + forall x, + (0 < round beta fexp Zfloor x)%R -> + ulp (round beta fexp Zfloor x) = ulp x. +Proof with auto with typeclass_instances. +intros x Hd. +rewrite 2!ulp_neq_0. +now rewrite canonic_exp_DN with (2 := Hd). +intros T; contradict Hd; rewrite T, round_0... +apply Rlt_irrefl. +now apply Rgt_not_eq. +Qed. + +Theorem round_neq_0_negligible_exp: + negligible_exp=None -> forall rnd { Zrnd : Valid_rnd rnd } x, + (x <> 0)%R -> (round beta fexp rnd x <> 0)%R. +Proof with auto with typeclass_instances. +intros H rndn Hrnd x Hx K. +case negligible_exp_spec'. +intros (_,Hn). +destruct (ln_beta beta x) as (e,He). +absurd (fexp e < e)%Z. +apply Zle_not_lt. +apply exp_small_round_0 with beta rndn x... +apply (Hn e). +intros (n,(H1,_)). +rewrite H in H1; discriminate. +Qed. + + +(** allows rnd x to be 0 *) +(* was ulp_error_f *) +Theorem error_lt_ulp_round : + forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x, + ( x <> 0)%R -> + (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R. +Proof with auto with typeclass_instances. +intros Hm. +(* wlog *) +cut (forall rnd : R -> Z, Valid_rnd rnd -> forall x : R, (0 < x)%R -> + (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R). +intros M rnd Hrnd x Zx. +case (Rle_or_lt 0 x). +intros H; destruct H. +now apply M. +contradict H; now apply sym_not_eq. +intros H. +rewrite <- (Ropp_involutive x). +rewrite round_opp, ulp_opp. +replace (- round beta fexp (Zrnd_opp rnd) (- x) - - - x)%R with + (-(round beta fexp (Zrnd_opp rnd) (- x) - (-x)))%R by ring. +rewrite Rabs_Ropp. +apply M. +now apply valid_rnd_opp. +now apply Ropp_0_gt_lt_contravar. +(* 0 < x *) +intros rnd Hrnd x Hx. +case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)). +apply round_ge_generic... +apply generic_format_0. +now left. +(* . 0 < round Zfloor x *) +intros Hx2. +apply Rlt_le_trans with (ulp x). +apply error_lt_ulp... +now apply Rgt_not_eq. +rewrite <- ulp_DN; trivial. +apply ulp_le_pos. +now left. +case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V. +apply Rle_refl. +apply Rle_trans with x. +apply round_DN_pt... +apply round_UP_pt... +(* . 0 = round Zfloor x *) +intros Hx2. +case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V; clear V. +(* .. round down -- difficult case *) +rewrite <- Hx2. +unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec. +(* without minimal exponent *) +intros K; contradict Hx2. +apply Rlt_not_eq. +apply F2R_gt_0_compat; simpl. +apply Zlt_le_trans with 1%Z. +apply Pos2Z.is_pos. +apply Zfloor_lub. +simpl; unfold scaled_mantissa, canonic_exp. +destruct (ln_beta beta x) as (e,He); simpl. +apply Rle_trans with (bpow (e-1) * bpow (- fexp e))%R. +rewrite <- bpow_plus. +replace 1%R with (bpow 0) by reflexivity. +apply bpow_le. +specialize (K e); omega. +apply Rmult_le_compat_r. +apply bpow_ge_0. +rewrite <- (Rabs_pos_eq x). +now apply He, Rgt_not_eq. +now left. +(* with a minimal exponent *) +intros n Hn. +rewrite Rabs_pos_eq;[idtac|now left]. +case (Rle_or_lt (bpow (fexp n)) x); trivial. +intros K; contradict Hx2. +apply Rlt_not_eq. +apply Rlt_le_trans with (bpow (fexp n)). apply bpow_gt_0. -replace (Z2R (Ztrunc (scaled_mantissa beta fexp x)) * - bpow (canonic_exp beta fexp x))%R with x. -rewrite Rmult_1_l. -unfold canonic_exp. -rewrite ln_beta_unique with beta x ex. -rewrite H3,<-H1, <- Hy2. -apply H. -exact Hex. -absurd (y <= x)%R. -now apply Rlt_not_le. -rewrite Rabs_right in Hex. -apply Rle_trans with (2:=proj1 Hex). -rewrite Hexy, Hy2. -now apply Rle_refl. -now apply Rgt_ge. -(* . *) -intros Hy3. -assert (y = bpow (fexp ey))%R. -apply Rminus_diag_uniq. -rewrite Hy3. -unfold ulp, canonic_exp. -rewrite (ln_beta_unique beta y ey); trivial. -apply Hey. +apply round_ge_generic... +apply generic_format_bpow. +now apply valid_exp. +(* .. round up *) +apply Rlt_le_trans with (ulp x). +apply error_lt_ulp... now apply Rgt_not_eq. -contradict Hy2. -rewrite H1. +apply ulp_le_pos. +now left. +apply round_UP_pt... +Qed. + +(** allows both x and rnd x to be 0 *) +(* was ulp_half_error_f *) +Theorem error_le_half_ulp_round : + forall { Hm : Monotone_exp fexp }, + forall choice x, + (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R. +Proof with auto with typeclass_instances. +intros Hm choice x. +case (Req_dec (round beta fexp (Znearest choice) x) 0); intros Hfx. +(* *) +case (Req_dec x 0); intros Hx. +apply Rle_trans with (1:=error_le_half_ulp _ _). +rewrite Hx, round_0... +right; ring. +generalize (error_le_half_ulp choice x). +rewrite Hfx. +unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp. +intros N. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +intros (H1,H2). +contradict Hfx. +apply round_neq_0_negligible_exp... +intros (n,(H1,Hn)); rewrite H1. +apply Rle_trans with (1:=N). +right; apply f_equal. +rewrite ulp_neq_0; trivial. apply f_equal. -apply Zplus_reg_l with 1%Z. -ring_simplify. -apply trans_eq with (ln_beta beta y). -apply sym_eq; apply ln_beta_unique. -rewrite H1, Rabs_right. -split. -apply bpow_le. -omega. -apply bpow_lt. -omega. -apply Rle_ge; apply bpow_ge_0. -apply ln_beta_unique. -apply Hey. -now apply Rgt_not_eq. +unfold canonic_exp. +apply valid_exp; trivial. +assert (ln_beta beta x -1 < fexp n)%Z;[idtac|omega]. +apply lt_bpow with beta. +destruct (ln_beta beta x) as (e,He). +simpl. +apply Rle_lt_trans with (Rabs x). +now apply He. +apply Rle_lt_trans with (Rabs (round beta fexp (Znearest choice) x - x)). +right; rewrite Hfx; unfold Rminus; rewrite Rplus_0_l. +apply sym_eq, Rabs_Ropp. +apply Rlt_le_trans with (ulp 0). +rewrite <- Hfx. +apply error_lt_ulp_round... +unfold ulp; rewrite Req_bool_true, H1; trivial. +now right. (* *) -case (Rle_or_lt (ulp (pred y)) (y-x)); intros H1. +case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx. (* . *) -apply Rplus_le_reg_r with (-x + ulp (pred y))%R. -ring_simplify (x+(-x+ulp (pred y)))%R. -apply Rle_trans with (1:=H1). -rewrite <- (pred_plus_ulp y) at 1; trivial. -apply Req_le; ring. -now apply Rgt_not_eq. +case (Rle_or_lt 0 (round beta fexp Zfloor x)). +intros H; destruct H. +rewrite Hx at 2. +rewrite ulp_DN; trivial. +apply error_le_half_ulp. +rewrite Hx in Hfx; contradict Hfx; auto with real. +intros H. +apply Rle_trans with (1:=error_le_half_ulp _ _). +apply Rmult_le_compat_l. +auto with real. +apply ulp_le. +rewrite Hx; rewrite (Rabs_left1 x), Rabs_left; try assumption. +apply Ropp_le_contravar. +apply (round_DN_pt beta fexp x). +case (Rle_or_lt x 0); trivial. +intros H1; contradict H. +apply Rle_not_lt. +apply round_ge_generic... +apply generic_format_0. +now left. (* . *) -replace x with (y-(y-x))%R by ring. -rewrite <- round_DN_pred with (eps:=(y-x)%R); try easy. -ring_simplify (y-(y-x))%R. -apply Req_le. -apply sym_eq. -apply round_generic... -split; trivial. -now apply Rlt_Rminus. -now apply Rlt_le. +case (Rle_or_lt 0 (round beta fexp Zceil x)). +intros H; destruct H. +apply Rle_trans with (1:=error_le_half_ulp _ _). +apply Rmult_le_compat_l. +auto with real. +apply ulp_le_pos; trivial. +case (Rle_or_lt 0 x); trivial. +intros H1; contradict H. +apply Rle_not_lt. +apply round_le_generic... +apply generic_format_0. +now left. +rewrite Hx; apply (round_UP_pt beta fexp x). +rewrite Hx in Hfx; contradict Hfx; auto with real. +intros H. +rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)). +rewrite <- round_DN_opp. +rewrite ulp_DN; trivial. +pattern x at 1 2; rewrite <- Ropp_involutive. +rewrite round_N_opp. +unfold Rminus. +rewrite <- Ropp_plus_distr, Rabs_Ropp. +apply error_le_half_ulp. +rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. Qed. -Theorem le_pred_lt : - forall x y, - F x -> F y -> - (0 < y)%R -> - (x < y)%R -> - (x <= pred y)%R. + +Theorem pred_le: forall x y, + F x -> F y -> (x <= y)%R -> (pred x <= pred y)%R. Proof. -intros x y Fx Fy Hy Hxy. -destruct (Rle_or_lt x 0) as [Hx|Hx]. -apply Rle_trans with (1 := Hx). -now apply pred_ge_0. -apply le_pred_lt_aux ; try easy. -now split. +intros x y Fx Fy Hxy. +assert (V:( ((x = 0) /\ (y = 0)) \/ (x <>0 \/ x < y))%R). +case (Req_dec x 0); intros Zx. +case Hxy; intros Zy. +now right; right. +left; split; trivial; now rewrite <- Zy. +now right; left. +destruct V as [(V1,V2)|V]. +rewrite V1,V2; now right. +apply le_pred_lt; try assumption. +apply generic_format_pred; try assumption. +case V; intros V1. +apply Rlt_le_trans with (2:=Hxy). +now apply pred_lt_id. +apply Rle_lt_trans with (2:=V1). +now apply pred_le_id. Qed. +Theorem succ_le: forall x y, + F x -> F y -> (x <= y)%R -> (succ x <= succ y)%R. +Proof. +intros x y Fx Fy Hxy. +rewrite 2!succ_eq_opp_pred_opp. +apply Ropp_le_contravar, pred_le; try apply generic_format_opp; try assumption. +now apply Ropp_le_contravar. +Qed. -Theorem pred_succ : forall { monotone_exp : Monotone_exp fexp }, - forall x, F x -> (0 < x)%R -> pred (x + ulp x)=x. +Theorem pred_le_inv: forall x y, F x -> F y + -> (pred x <= pred y)%R -> (x <= y)%R. Proof. -intros L x Fx Hx. -assert (x <= pred (x + ulp x))%R. -apply le_pred_lt. -assumption. -now apply generic_format_succ. -replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx. -apply bpow_gt_0. -apply Rplus_lt_reg_r with (-x)%R; ring_simplify. -apply bpow_gt_0. -apply Rle_antisym; trivial. -apply Rplus_le_reg_r with (ulp (pred (x + ulp x))). -rewrite pred_plus_ulp. -apply Rplus_le_compat_l. -now apply ulp_le. -replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx. -apply bpow_gt_0. -now apply generic_format_succ. -apply Rgt_not_eq. -now apply Rlt_le_trans with x. +intros x y Fx Fy Hxy. +rewrite <- (succ_pred x), <- (succ_pred y); try assumption. +apply succ_le; trivial; now apply generic_format_pred. Qed. +Theorem succ_le_inv: forall x y, F x -> F y + -> (succ x <= succ y)%R -> (x <= y)%R. +Proof. +intros x y Fx Fy Hxy. +rewrite <- (pred_succ x), <- (pred_succ y); try assumption. +apply pred_le; trivial; now apply generic_format_succ. +Qed. -Theorem lt_UP_le_DN : +(* was lt_UP_le_DN *) +Theorem le_round_DN_lt_UP : forall x y, F y -> (y < round beta fexp Zceil x -> y <= round beta fexp Zfloor x)%R. Proof with auto with typeclass_instances. @@ -1178,26 +2100,58 @@ apply round_UP_pt... now apply Rlt_le. Qed. +(* was lt_DN_le_UP *) +Theorem round_UP_le_gt_DN : + forall x y, F y -> + (round beta fexp Zfloor x < y -> round beta fexp Zceil x <= y)%R. +Proof with auto with typeclass_instances. +intros x y Fy Hlt. +apply round_UP_pt... +apply Rnot_lt_le. +contradict Hlt. +apply RIneq.Rle_not_lt. +apply round_DN_pt... +now apply Rlt_le. +Qed. + + + Theorem pred_UP_le_DN : - forall x, (0 < round beta fexp Zceil x)%R -> - (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R. + forall x, (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R. Proof with auto with typeclass_instances. -intros x Pxu. +intros x. destruct (generic_format_EM beta fexp x) as [Fx|Fx]. rewrite !round_generic... -now apply Rlt_le; apply pred_lt_id. +apply pred_le_id. +case (Req_dec (round beta fexp Zceil x) 0); intros Zx. +rewrite Zx; unfold pred; rewrite Ropp_0. +unfold succ; rewrite Rle_bool_true;[idtac|now right]. +rewrite Rplus_0_l; unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +intros (H1,H2). +contradict Zx; apply round_neq_0_negligible_exp... +intros L; apply Fx; rewrite L; apply generic_format_0. +intros (n,(H1,Hn)); rewrite H1. +case (Rle_or_lt (- bpow (fexp n)) (round beta fexp Zfloor x)); trivial; intros K. +absurd (round beta fexp Zceil x <= - bpow (fexp n))%R. +apply Rlt_not_le. +rewrite Zx, <- Ropp_0. +apply Ropp_lt_contravar, bpow_gt_0. +apply round_UP_le_gt_DN; try assumption. +apply generic_format_opp, generic_format_bpow. +now apply valid_exp. assert (let u := round beta fexp Zceil x in pred u < u)%R as Hup. - now apply pred_lt_id. -apply lt_UP_le_DN... +now apply pred_lt_id. +apply le_round_DN_lt_UP... apply generic_format_pred... now apply round_UP_pt. Qed. Theorem pred_UP_eq_DN : - forall x, (0 < round beta fexp Zceil x)%R -> ~ F x -> + forall x, ~ F x -> (pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R. Proof with auto with typeclass_instances. -intros x Px Fx. +intros x Fx. apply Rle_antisym. now apply pred_UP_le_DN. apply le_pred_lt; try apply generic_format_round... @@ -1205,212 +2159,200 @@ pose proof round_DN_UP_lt _ _ _ Fx as HE. now apply Rlt_trans with (1 := proj1 HE) (2 := proj2 HE). Qed. +Theorem succ_DN_eq_UP : + forall x, ~ F x -> + (succ (round beta fexp Zfloor x) = round beta fexp Zceil x)%R. +Proof with auto with typeclass_instances. +intros x Fx. +rewrite <- pred_UP_eq_DN; trivial. +rewrite succ_pred; trivial. +apply generic_format_round... +Qed. + + +(* was betw_eq_DN *) +Theorem round_DN_eq_betw: forall x d, F d + -> (d <= x < succ d)%R + -> round beta fexp Zfloor x = d. +Proof with auto with typeclass_instances. +intros x d Fd (Hxd1,Hxd2). +generalize (round_DN_pt beta fexp x); intros (T1,(T2,T3)). +apply sym_eq, Rle_antisym. +now apply T3. +destruct (generic_format_EM beta fexp x) as [Fx|NFx]. +rewrite round_generic... +apply succ_le_inv; try assumption. +apply succ_le_lt; try assumption. +apply generic_format_succ... +apply succ_le_inv; try assumption. +rewrite succ_DN_eq_UP; trivial. +apply round_UP_pt... +apply generic_format_succ... +now left. +Qed. + +(* was betw_eq_UP *) +Theorem round_UP_eq_betw: forall x u, F u + -> (pred u < x <= u)%R + -> round beta fexp Zceil x = u. +Proof with auto with typeclass_instances. +intros x u Fu Hux. +rewrite <- (Ropp_involutive (round beta fexp Zceil x)). +rewrite <- round_DN_opp. +rewrite <- (Ropp_involutive u). +apply f_equal. +apply round_DN_eq_betw; try assumption. +now apply generic_format_opp. +split;[now apply Ropp_le_contravar|idtac]. +rewrite succ_opp. +now apply Ropp_lt_contravar. +Qed. (** Properties of rounding to nearest and ulp *) -Theorem rnd_N_le_half_an_ulp: forall choice u v, - F u -> (0 < u)%R -> (v < u + (ulp u)/2)%R +Theorem round_N_le_midp: forall choice u v, + F u -> (v < (u + succ u)/2)%R -> (round beta fexp (Znearest choice) v <= u)%R. Proof with auto with typeclass_instances. -intros choice u v Fu Hu H. -(* . *) -assert (0 < ulp u / 2)%R. -unfold Rdiv; apply Rmult_lt_0_compat. -unfold ulp; apply bpow_gt_0. -auto with real. +intros choice u v Fu H. (* . *) -assert (ulp u / 2 < ulp u)%R. -apply Rlt_le_trans with (ulp u *1)%R;[idtac|right; ring]. -unfold Rdiv; apply Rmult_lt_compat_l. -apply bpow_gt_0. +assert (V: ((succ u = 0 /\ u = 0) \/ u < succ u)%R). +specialize (succ_ge_id u); intros P; destruct P as [P|P]. +now right. +case (Req_dec u 0); intros Zu. +left; split; trivial. +now rewrite <- P. +right; now apply succ_gt_id. +(* *) +destruct V as [(V1,V2)|V]. +rewrite V2; apply round_le_generic... +apply generic_format_0. +left; apply Rlt_le_trans with (1:=H). +rewrite V1,V2; right; field. +(* *) +assert (T: (u < (u + succ u) / 2 < succ u)%R). +split. apply Rmult_lt_reg_l with 2%R. -auto with real. -apply Rle_lt_trans with 1%R. +now auto with real. +apply Rplus_lt_reg_l with (-u)%R. +apply Rle_lt_trans with u;[right; ring|idtac]. +apply Rlt_le_trans with (1:=V). right; field. -rewrite Rmult_1_r; auto with real. +apply Rmult_lt_reg_l with 2%R. +now auto with real. +apply Rplus_lt_reg_l with (-succ u)%R. +apply Rle_lt_trans with u;[right; field|idtac]. +apply Rlt_le_trans with (1:=V). +right; ring. (* *) -apply Rnd_N_pt_monotone with F v (u + ulp u / 2)%R... +destruct T as (T1,T2). +apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R... apply round_N_pt... -apply Rnd_DN_pt_N with (u+ulp u)%R. -pattern u at 3; replace u with (round beta fexp Zfloor (u + ulp u / 2)). +apply Rnd_DN_pt_N with (succ u)%R. +pattern u at 3; replace u with (round beta fexp Zfloor ((u + succ u) / 2)). apply round_DN_pt... -apply round_DN_succ; try assumption. +apply round_DN_eq_betw; trivial. split; try left; assumption. -replace (u+ulp u)%R with (round beta fexp Zceil (u + ulp u / 2)). +pattern (succ u) at 2; replace (succ u) with (round beta fexp Zceil ((u + succ u) / 2)). apply round_UP_pt... -apply round_UP_succ; try assumption... +apply round_UP_eq_betw; trivial. +apply generic_format_succ... +rewrite pred_succ; trivial. split; try left; assumption. right; field. Qed. -Theorem rnd_N_ge_half_an_ulp_pred: forall choice u v, - F u -> (0 < pred u)%R -> (u - (ulp (pred u))/2 < v)%R +Theorem round_N_ge_midp: forall choice u v, + F u -> ((u + pred u)/2 < v)%R -> (u <= round beta fexp (Znearest choice) v)%R. Proof with auto with typeclass_instances. -intros choice u v Fu Hu H. -(* . *) -assert (0 < u)%R. -apply Rlt_trans with (1:= Hu). -apply pred_lt_id. -assert (0 < ulp (pred u) / 2)%R. -unfold Rdiv; apply Rmult_lt_0_compat. -unfold ulp; apply bpow_gt_0. -auto with real. -assert (ulp (pred u) / 2 < ulp (pred u))%R. -apply Rlt_le_trans with (ulp (pred u) *1)%R;[idtac|right; ring]. -unfold Rdiv; apply Rmult_lt_compat_l. -apply bpow_gt_0. -apply Rmult_lt_reg_l with 2%R. -auto with real. -apply Rle_lt_trans with 1%R. -right; field. -rewrite Rmult_1_r; auto with real. -(* *) -apply Rnd_N_pt_monotone with F (u - ulp (pred u) / 2)%R v... -2: apply round_N_pt... -apply Rnd_UP_pt_N with (pred u). -pattern (pred u) at 2; replace (pred u) with (round beta fexp Zfloor (u - ulp (pred u) / 2)). -apply round_DN_pt... -replace (u - ulp (pred u) / 2)%R with (pred u + ulp (pred u) / 2)%R. -apply round_DN_succ; try assumption. -apply generic_format_pred; assumption. -split; [left|idtac]; assumption. -pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption. -field. -now apply Rgt_not_eq. -pattern u at 3; replace u with (round beta fexp Zceil (u - ulp (pred u) / 2)). -apply round_UP_pt... -replace (u - ulp (pred u) / 2)%R with (pred u + ulp (pred u) / 2)%R. -apply trans_eq with (pred u +ulp(pred u))%R. -apply round_UP_succ; try assumption... -apply generic_format_pred; assumption. -split; [idtac|left]; assumption. -apply pred_plus_ulp; try assumption. -now apply Rgt_not_eq. -pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption. -field. -now apply Rgt_not_eq. -pattern u at 4; rewrite <- (pred_plus_ulp u); try assumption. +intros choice u v Fu H. +rewrite <- (Ropp_involutive v). +rewrite round_N_opp. +rewrite <- (Ropp_involutive u). +apply Ropp_le_contravar. +apply round_N_le_midp. +now apply generic_format_opp. +apply Ropp_lt_cancel. +rewrite Ropp_involutive. +apply Rle_lt_trans with (2:=H). +unfold pred. right; field. -now apply Rgt_not_eq. Qed. -Theorem rnd_N_ge_half_an_ulp: forall choice u v, - F u -> (0 < u)%R -> (u <> bpow (ln_beta beta u - 1))%R - -> (u - (ulp u)/2 < v)%R - -> (u <= round beta fexp (Znearest choice) v)%R. +Lemma round_N_eq_DN: forall choice x, + let d:=round beta fexp Zfloor x in + let u:=round beta fexp Zceil x in + (x<(d+u)/2)%R -> + round beta fexp (Znearest choice) x = d. Proof with auto with typeclass_instances. -intros choice u v Fu Hupos Hu H. -(* *) -assert (bpow (ln_beta beta u-1) <= pred u)%R. -apply le_pred_lt; try assumption. -apply generic_format_bpow. -assert (canonic_exp beta fexp u < ln_beta beta u)%Z. -apply ln_beta_generic_gt; try assumption. -now apply Rgt_not_eq. -unfold canonic_exp in H0. -ring_simplify (ln_beta beta u - 1 + 1)%Z. -omega. -destruct ln_beta as (e,He); simpl in *. -assert (bpow (e - 1) <= Rabs u)%R. -apply He. -now apply Rgt_not_eq. -rewrite Rabs_right in H0. -case H0; auto. -intros T; contradict T. -now apply sym_not_eq. -apply Rle_ge; now left. -assert (Hu2:(ulp (pred u) = ulp u)). -unfold ulp, canonic_exp. -apply f_equal; apply f_equal. -apply ln_beta_unique. -rewrite Rabs_right. -split. -assumption. -apply Rlt_trans with (1:=pred_lt_id _). -destruct ln_beta as (e,He); simpl in *. -rewrite Rabs_right in He. -apply He. -now apply Rgt_not_eq. -apply Rle_ge; now left. -apply Rle_ge, pred_ge_0; assumption. -apply rnd_N_ge_half_an_ulp_pred; try assumption. -apply Rlt_le_trans with (2:=H0). -apply bpow_gt_0. -rewrite Hu2; assumption. +intros choice x d u H. +apply Rle_antisym. +destruct (generic_format_EM beta fexp x) as [Fx|Fx]. +rewrite round_generic... +apply round_DN_pt; trivial; now right. +apply round_N_le_midp. +apply round_DN_pt... +apply Rlt_le_trans with (1:=H). +right; apply f_equal2; trivial; apply f_equal. +now apply sym_eq, succ_DN_eq_UP. +apply round_ge_generic; try apply round_DN_pt... Qed. - -Lemma round_N_DN_betw: forall choice x d u, - Rnd_DN_pt (generic_format beta fexp) x d -> - Rnd_UP_pt (generic_format beta fexp) x u -> - (d<=x<(d+u)/2)%R -> +Lemma round_N_eq_DN_pt: forall choice x d u, + Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> + (x<(d+u)/2)%R -> round beta fexp (Znearest choice) x = d. Proof with auto with typeclass_instances. intros choice x d u Hd Hu H. -apply Rnd_N_pt_unicity with (generic_format beta fexp) x d u; try assumption. -intros Y. -absurd (x < (d+u)/2)%R; try apply H. -apply Rle_not_lt; right. -apply Rplus_eq_reg_r with (-x)%R. -apply trans_eq with (- (x-d)/2 + (u-x)/2)%R. -field. -rewrite Y; field. -apply round_N_pt... -apply Rnd_DN_UP_pt_N with d u... -apply Hd. -right; apply trans_eq with (-(d-x))%R;[idtac|ring]. -apply Rabs_left1. -apply Rplus_le_reg_l with x; ring_simplify. -apply H. -rewrite Rabs_left1. -apply Rplus_le_reg_l with (d+x)%R. -apply Rmult_le_reg_l with (/2)%R. -auto with real. -apply Rle_trans with x. -right; field. -apply Rle_trans with ((d+u)/2)%R. -now left. -right; field. -apply Rplus_le_reg_l with x; ring_simplify. -apply H. +assert (H0:(d = round beta fexp Zfloor x)%R). +apply Rnd_DN_pt_unicity with (1:=Hd). +apply round_DN_pt... +rewrite H0. +apply round_N_eq_DN. +rewrite <- H0. +rewrite Rnd_UP_pt_unicity with F x (round beta fexp Zceil x) u; try assumption. +apply round_UP_pt... Qed. +Lemma round_N_eq_UP: forall choice x, + let d:=round beta fexp Zfloor x in + let u:=round beta fexp Zceil x in + ((d+u)/2 < x)%R -> + round beta fexp (Znearest choice) x = u. +Proof with auto with typeclass_instances. +intros choice x d u H. +apply Rle_antisym. +apply round_le_generic; try apply round_UP_pt... +destruct (generic_format_EM beta fexp x) as [Fx|Fx]. +rewrite round_generic... +apply round_UP_pt; trivial; now right. +apply round_N_ge_midp. +apply round_UP_pt... +apply Rle_lt_trans with (2:=H). +right; apply f_equal2; trivial; rewrite Rplus_comm; apply f_equal2; trivial. +now apply pred_UP_eq_DN. +Qed. -Lemma round_N_UP_betw: forall choice x d u, - Rnd_DN_pt (generic_format beta fexp) x d -> - Rnd_UP_pt (generic_format beta fexp) x u -> - ((d+u)/2 < x <= u)%R -> +Lemma round_N_eq_UP_pt: forall choice x d u, + Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> + ((d+u)/2 < x)%R -> round beta fexp (Znearest choice) x = u. Proof with auto with typeclass_instances. intros choice x d u Hd Hu H. -rewrite <- (Ropp_involutive (round beta fexp (Znearest choice) x )), - <- (Ropp_involutive u) . -apply f_equal. -rewrite <- (Ropp_involutive x) . -rewrite round_N_opp, Ropp_involutive. -apply round_N_DN_betw with (-d)%R. -replace u with (round beta fexp Zceil x). -rewrite <- round_DN_opp. -apply round_DN_pt... -apply Rnd_UP_pt_unicity with (generic_format beta fexp) x... -apply round_UP_pt... -replace d with (round beta fexp Zfloor x). -rewrite <- round_UP_opp. +assert (H0:(u = round beta fexp Zceil x)%R). +apply Rnd_UP_pt_unicity with (1:=Hu). apply round_UP_pt... -apply Rnd_DN_pt_unicity with (generic_format beta fexp) x... +rewrite H0. +apply round_N_eq_UP. +rewrite <- H0. +rewrite Rnd_DN_pt_unicity with F x (round beta fexp Zfloor x) d; try assumption. apply round_DN_pt... -split. -apply Ropp_le_contravar, H. -apply Rlt_le_trans with (-((d + u) / 2))%R. -apply Ropp_lt_contravar, H. -unfold Rdiv; right; ring. Qed. - End Fcore_ulp. -- cgit