From 375344c9a3d528f3ba6882c3a55e79ba0f5c1777 Mon Sep 17 00:00:00 2001
From: Sylvie Boldo <sylvie.boldo@inria.fr>
Date: Mon, 6 Sep 2010 08:44:28 +0000
Subject: [PATCH] Remainder of the division and the square root are in the
 format

---
 src/Makefile.am                 |  1 +
 src/Prop/Fprop_div_sqrt_error.v | 44 +++++++++++++++++++++++++++------
 2 files changed, 38 insertions(+), 7 deletions(-)

diff --git a/src/Makefile.am b/src/Makefile.am
index a33cf09..627b001 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -21,6 +21,7 @@ FILES = \
 	Prop/Fprop_mult_error.v \
 	Prop/Fprop_plus_error.v \
 	Prop/Fprop_relative.v \
+	Prop/Fprop_div_sqrt_error.v \
 	Prop/Fprop_Sterbenz.v
 
 EXTRA_DIST = $(FILES)
diff --git a/src/Prop/Fprop_div_sqrt_error.v b/src/Prop/Fprop_div_sqrt_error.v
index c66e4a4..788fa02 100644
--- a/src/Prop/Fprop_div_sqrt_error.v
+++ b/src/Prop/Fprop_div_sqrt_error.v
@@ -6,23 +6,53 @@ Section Fprop_divsqrt_error.
 Variable beta : radix.
 Notation bpow e := (bpow beta e).
 
-Variable fexp : Z -> Z.
-Hypothesis prop_exp : valid_exp fexp.
-Notation format := (generic_format beta fexp).
+Variable prec : Z.
+Variable Hp : Zlt 0 prec.
+
+Notation format := (generic_format beta (FLX_exp prec)).
+Notation cexp := (canonic_exponent beta (FLX_exp prec)).
+
 Variable choice : R -> bool.
 
+Theorem format_FLX: forall x,
+  (exists f: float beta, x=F2R f /\ (cexp x <= Fexp f)%Z)
+  -> format x.
+intros x (f, (H1,H2)).
+unfold generic_format.
+rewrite H1 at 1; unfold F2R; simpl.
+replace (Ztrunc (scaled_mantissa beta (FLX_exp prec) x)) with (Fnum f * Zpower (radix_val beta) (Fexp f - cexp x))%Z.
+rewrite mult_Z2R.
+rewrite Z2R_Zpower.
+unfold Zminus; rewrite bpow_add.
+rewrite Rmult_assoc; rewrite Rmult_assoc.
+rewrite <- bpow_add.
+ring_simplify (-cexp x+cexp x)%Z.
+simpl; ring.
+omega.
+unfold scaled_mantissa.
+replace (x*bpow (-cexp x))%R with (Z2R ((Fnum f * radix_val beta ^ (Fexp f - cexp x)))).
+now rewrite Ztrunc_Z2R.
+rewrite mult_Z2R.
+rewrite Z2R_Zpower.
+unfold Zminus; rewrite bpow_add.
+rewrite H1 at 2; unfold F2R.
+ring.
+omega.
+Qed.
+
+
+
 Theorem div_error_N :
   forall x y,
   format x -> format y ->
-  format (x - rounding beta fexp (ZrndN choice) (x/y) * y)%R.
+  format (x - rounding beta (FLX_exp prec) (ZrndN choice) (x/y) * y)%R.
 Proof.
-(* probablement seulement en FLX *)
 Admitted. (* SB *)
 
 Theorem div_error_Z :
   forall x y,
   format x -> format y ->
-  format (x - rounding beta fexp (ZrndTZ) (x/y) * y)%R.
+  format (x - rounding beta (FLX_exp prec) (ZrndTZ) (x/y) * y)%R.
 Proof.
 (* probablement seulement en FLX *)
 Admitted. (* SB *) 
@@ -31,7 +61,7 @@ Admitted. (* SB *)
 Theorem sqrt_error_N :
   forall x, (0 <= x)%R ->
   format x ->
-  format (x - Rsqr (rounding beta fexp (ZrndN choice) (sqrt x)))%R.
+  format (x - Rsqr (rounding beta (FLX_exp prec) (ZrndN choice) (sqrt x)))%R.
 Proof.
 (* probablement seulement en FLX *)
 Admitted. (* SB *)
-- 
GitLab