From f89097cfd72492cf040612b5461887f15842ee52 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 26 May 2010 14:35:25 +0000
Subject: [PATCH] Proved that the error of multiplication is an FP number in
 FLX.

---
 src/Makefile.am             |   1 +
 src/Prop/Fprop_mult_error.v | 113 ++++++++++++++++++++++++++++++++++++
 2 files changed, 114 insertions(+)
 create mode 100644 src/Prop/Fprop_mult_error.v

diff --git a/src/Makefile.am b/src/Makefile.am
index 8888b5e..e109004 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -18,6 +18,7 @@ FILES = \
 	Calc/Fcalc_round.v \
 	Calc/Fcalc_round_FIX.v \
 	Calc/Fcalc_sqrt.v \
+	Prop/Fprop_mult_error.v \
 	Prop/Fprop_nearest.v \
 	Prop/Fprop_Sterbenz.v
 
diff --git a/src/Prop/Fprop_mult_error.v b/src/Prop/Fprop_mult_error.v
new file mode 100644
index 0000000..89f4ce5
--- /dev/null
+++ b/src/Prop/Fprop_mult_error.v
@@ -0,0 +1,113 @@
+Require Import Fcore.
+Require Import Fcalc_ops.
+
+Section Fprop_mult_error.
+
+Variable beta : radix.
+Notation bpow e := (bpow beta e).
+
+Variable prec : Z.
+Variable Hp : Zlt 0 prec.
+
+Notation format := (generic_format beta (FLX_exp prec)).
+Notation cexp := (canonic_exponent beta (FLX_exp prec)).
+
+Theorem mult_error_FLX :
+  forall rnd,
+  forall x y,
+  format x -> format y ->
+  format (rounding beta (FLX_exp prec) rnd (x * y) - (x * y))%R.
+Proof.
+intros rnd x y Hx Hy.
+set (f := (rounding beta (FLX_exp prec) rnd (x * y))).
+destruct (Req_dec (f - x * y) 0) as [Hr0|Hr0].
+rewrite Hr0.
+apply generic_format_0.
+destruct (Req_dec (x * y) 0) as [Hxy0|Hxy0].
+unfold f.
+rewrite Hxy0.
+rewrite rounding_0.
+ring_simplify (0 - 0)%R.
+apply generic_format_0.
+destruct (ln_beta beta (x * y)) as (exy, Hexy).
+specialize (Hexy Hxy0).
+destruct (ln_beta beta (f - x * y)) as (er, Her).
+specialize (Her Hr0).
+destruct (ln_beta beta x) as (ex, Hex).
+assert (Hx0: (x <> 0)%R).
+contradict Hxy0.
+now rewrite Hxy0, Rmult_0_l.
+specialize (Hex Hx0).
+destruct (ln_beta beta y) as (ey, Hey).
+assert (Hy0: (y <> 0)%R).
+contradict Hxy0.
+now rewrite Hxy0, Rmult_0_r.
+specialize (Hey Hy0).
+(* *)
+assert (Hc1: (cexp (x * y)%R - prec <= cexp x + cexp y)%Z).
+unfold canonic_exponent, FLX_exp.
+rewrite ln_beta_unique with (1 := Hex).
+rewrite ln_beta_unique with (1 := Hey).
+rewrite ln_beta_unique with (1 := Hexy).
+cut (exy - 1 < ex + ey)%Z. omega.
+apply <- (bpow_lt beta).
+apply Rle_lt_trans with (1 := proj1 Hexy).
+rewrite Rabs_mult.
+rewrite bpow_add.
+apply Rmult_le_0_lt_compat.
+apply Rabs_pos.
+apply Rabs_pos.
+apply Hex.
+apply Hey.
+(* *)
+assert (Hc2: (cexp x + cexp y <= cexp (x * y)%R)%Z).
+unfold canonic_exponent, FLX_exp.
+rewrite ln_beta_unique with (1 := Hex).
+rewrite ln_beta_unique with (1 := Hey).
+rewrite ln_beta_unique with (1 := Hexy).
+cut ((ex - 1) + (ey - 1) < exy)%Z. omega.
+apply <- (bpow_lt beta).
+apply Rle_lt_trans with (2 := proj2 Hexy).
+rewrite Rabs_mult.
+rewrite bpow_add.
+apply Rmult_le_compat.
+apply bpow_ge_0.
+apply bpow_ge_0.
+apply Hex.
+apply Hey.
+(* *)
+assert (Hr: ((F2R (Float beta (- (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) *
+  Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + Zrnd rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) *
+  radix_val beta ^ (cexp (x * y)%R - (cexp x + cexp y))) (cexp x + cexp y))) = f - x * y)%R).
+rewrite Hx at 6.
+rewrite Hy at 6.
+rewrite <- mult_F2R.
+simpl.
+unfold f, rounding, Rminus.
+rewrite opp_F2R, Rplus_comm, <- plus_F2R.
+unfold Fplus. simpl.
+now rewrite Zle_imp_le_bool with (1 := Hc2).
+(* *)
+rewrite <- Hr.
+apply generic_format_canonic_exponent.
+rewrite Hr.
+clear Hr.
+apply Zle_trans with (cexp (x * y)%R - prec)%Z.
+unfold canonic_exponent, FLX_exp.
+apply Zplus_le_compat_r.
+rewrite ln_beta_unique with (1 := Her).
+rewrite ln_beta_unique with (1 := Hexy).
+apply (bpow_lt_bpow beta).
+apply Rle_lt_trans with (1 := proj1 Her).
+apply Rlt_le_trans with (ulp beta (FLX_exp prec) (x * y)).
+apply ulp_error.
+now apply FLX_exp_correct.
+unfold ulp.
+apply -> bpow_le.
+unfold canonic_exponent, FLX_exp.
+rewrite ln_beta_unique with (1 := Hexy).
+apply Zle_refl.
+apply Hc1.
+Qed.
+
+End Fprop_mult_error.
\ No newline at end of file
-- 
GitLab