diff options
Diffstat (limited to 'flocq/Core/Fcore_FLX.v')
| -rw-r--r-- | flocq/Core/Fcore_FLX.v | 38 |
1 files changed, 38 insertions, 0 deletions
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. |