From b3738592ea94931d659184eb28d1cb671528b0da Mon Sep 17 00:00:00 2001
From: Sylvie Boldo <sylvie.boldo@inria.fr>
Date: Mon, 20 Sep 2010 14:08:33 +0000
Subject: [PATCH] canonic_exp_ge made more generic

---
 src/Core/Fcore_generic_fmt.v | 21 +++++++++++++++++++++
 src/Prop/Fprop_mult_error.v  | 18 ------------------
 2 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index c0592cf..d47513a 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -300,6 +300,27 @@ rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
 now rewrite Ztrunc_Z2R.
 Qed.
 
+
+Theorem canonic_exp_ge:
+  forall prec,
+  (forall e, (e-prec <= fexp e)%Z) ->
+  (* OK with FLX, FLT and FTZ *)
+  forall x, generic_format x ->
+  (Rabs x < bpow (prec + canonic_exponent x))%R.
+intros prec Hp x Hx.
+case (Req_dec x 0); intros Hxz.
+rewrite Hxz, Rabs_R0.
+apply bpow_gt_0.
+unfold canonic_exponent.
+destruct (ln_beta beta x); simpl.
+specialize (a Hxz).
+apply Rlt_le_trans with (1:=proj2 a).
+apply -> bpow_le.
+specialize (Hp x0).
+omega.
+Qed.
+
+
 Section Fcore_generic_rounding_pos.
 
 Record Zrounding := mkZrounding {
diff --git a/src/Prop/Fprop_mult_error.v b/src/Prop/Fprop_mult_error.v
index 383d538..f9c30b4 100644
--- a/src/Prop/Fprop_mult_error.v
+++ b/src/Prop/Fprop_mult_error.v
@@ -145,24 +145,6 @@ Notation format := (generic_format beta (FLT_exp emin prec)).
 Notation cexp := (canonic_exponent beta (FLT_exp emin prec)).
 
 
-Theorem canonic_exp_ge_FLT:
-  forall x, format x ->
-  (Rabs x < bpow (prec + cexp x))%R.
-intros x Hx.
-case (Req_dec x 0); intros Hxz.
-rewrite Hxz, Rabs_R0.
-apply bpow_gt_0.
-unfold canonic_exponent, FLT_exp.
-destruct (ln_beta beta x); simpl.
-specialize (a Hxz).
-apply Rlt_le_trans with (1:=proj2 a).
-apply -> bpow_le.
-case (Zmax_spec (x0-prec) emin); intros (H1,H2).
-rewrite H2; omega.
-rewrite H2; omega.
-Qed.
-
-
 Theorem mult_error_FLT :
   forall rnd,
   forall x y,
-- 
GitLab