Commit 375344c9 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Remainder of the division and the square root are in the format

parent d696276a
...@@ -21,6 +21,7 @@ FILES = \ ...@@ -21,6 +21,7 @@ FILES = \
Prop/Fprop_mult_error.v \ Prop/Fprop_mult_error.v \
Prop/Fprop_plus_error.v \ Prop/Fprop_plus_error.v \
Prop/Fprop_relative.v \ Prop/Fprop_relative.v \
Prop/Fprop_div_sqrt_error.v \
Prop/Fprop_Sterbenz.v Prop/Fprop_Sterbenz.v
EXTRA_DIST = $(FILES) EXTRA_DIST = $(FILES)
......
...@@ -6,23 +6,53 @@ Section Fprop_divsqrt_error. ...@@ -6,23 +6,53 @@ Section Fprop_divsqrt_error.
Variable beta : radix. Variable beta : radix.
Notation bpow e := (bpow beta e). Notation bpow e := (bpow beta e).
Variable fexp : Z -> Z. Variable prec : Z.
Hypothesis prop_exp : valid_exp fexp. Variable Hp : Zlt 0 prec.
Notation format := (generic_format beta fexp).
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
Variable choice : R -> bool. 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 : Theorem div_error_N :
forall x y, forall x y,
format x -> format 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. Proof.
(* probablement seulement en FLX *)
Admitted. (* SB *) Admitted. (* SB *)
Theorem div_error_Z : Theorem div_error_Z :
forall x y, forall x y,
format x -> format 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. Proof.
(* probablement seulement en FLX *) (* probablement seulement en FLX *)
Admitted. (* SB *) Admitted. (* SB *)
...@@ -31,7 +61,7 @@ Admitted. (* SB *) ...@@ -31,7 +61,7 @@ Admitted. (* SB *)
Theorem sqrt_error_N : Theorem sqrt_error_N :
forall x, (0 <= x)%R -> forall x, (0 <= x)%R ->
format x -> 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. Proof.
(* probablement seulement en FLX *) (* probablement seulement en FLX *)
Admitted. (* SB *) Admitted. (* SB *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment