Commit 01858c76 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added a typeclass for rounding functions.

parent de2f0164
......@@ -63,8 +63,8 @@ Qed.
Definition MinOrMax x f :=
((f = round beta (FLX_exp prec) rndDN x)
\/ (f = round beta (FLX_exp prec) rndUP x)).
((f = round beta (FLX_exp prec) Zfloor x)
\/ (f = round beta (FLX_exp prec) Zceil x)).
Theorem MinOrMax_opp: forall x f,
MinOrMax x f <-> MinOrMax (-x) (-f).
......@@ -85,7 +85,7 @@ Theorem implies_DN_lt_ulp:
forall x f, format f ->
(0 < f <= x)%R ->
(Rabs (f-x) < ulp f)%R ->
(f = round beta (FLX_exp prec) rndDN x)%R.
(f = round beta (FLX_exp prec) Zfloor x)%R.
intros x f Hf Hxf1 Hxf2.
apply sym_eq.
replace x with (f+-(f-x))%R by ring.
......@@ -160,8 +160,8 @@ Hypothesis Ha: format a.
Hypothesis Hx: format x.
Hypothesis Hy: format y.
Notation t := (round beta (FLX_exp prec) (rndN choice) (a*x)).
Notation u := (round beta (FLX_exp prec) (rndN choice) (t+y)).
Notation t := (round beta (FLX_exp prec) (Znearest choice) (a*x)).
Notation u := (round beta (FLX_exp prec) (Znearest choice) (t+y)).
(*
Axpy_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
......
......@@ -52,6 +52,7 @@ Hypothesis Hmax : (prec < emax)%Z.
Let emin := (3 - emax - prec)%Z.
Let fexp := FLT_exp emin prec.
Instance fexp_correct : Valid_exp fexp := FLT_exp_valid emin prec.
Instance fexp_monotone : Monotone_exp fexp := FLT_exp_monotone emin prec.
Definition bounded_prec m e :=
Zeq_bool (fexp (Z_of_nat (S (digits2_Pnat m)) + e)) e.
......@@ -526,11 +527,11 @@ Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA.
Definition round_mode m :=
match m with
| mode_NE => rndNE
| mode_ZR => rndZR
| mode_DN => rndDN
| mode_UP => rndUP
| mode_NA => rndNA
| mode_NE => ZnearestE
| mode_ZR => Ztrunc
| mode_DN => Zfloor
| mode_UP => Zceil
| mode_NA => ZnearestA
end.
Definition choice_mode m sx mx lx :=
......@@ -542,6 +543,11 @@ Definition choice_mode m sx mx lx :=
| mode_NA => cond_incr (round_N true lx) mx
end.
Global Instance valid_rnd_round_mode : forall m, Valid_rnd (round_mode m).
Proof.
destruct m ; unfold round_mode ; auto with typeclass_instances.
Qed.
Definition overflow_to_inf m s :=
match m with
| mode_NE => true
......@@ -573,7 +579,7 @@ Theorem binary_round_sign_correct :
FF2R radix2 (binary_round_sign mode (Rlt_bool x 0) mx ex lx) = round radix2 fexp (round_mode mode) x
else
binary_round_sign mode (Rlt_bool x 0) mx ex lx = binary_overflow mode (Rlt_bool x 0).
Proof.
Proof with auto with typeclass_instances.
intros m x mx ex lx Bx Ex.
unfold binary_round_sign.
rewrite shr_truncate. 2: easy.
......@@ -627,9 +633,7 @@ rewrite <- ln_beta_F2R_digits, <- Hr, ln_beta_abs.
rewrite H1b.
rewrite canonic_exponent_abs.
fold (canonic_exponent radix2 fexp (round radix2 fexp (round_mode m) x)).
apply canonic_exponent_round.
apply fexp_correct.
apply FLT_exp_monotone.
apply canonic_exponent_round...
rewrite H1c.
case (Rlt_bool x 0).
apply Rlt_not_eq.
......@@ -718,9 +722,8 @@ apply Rlt_trans with R0.
now apply F2R_lt_0_compat.
now apply F2R_gt_0_compat.
rewrite <- Hr.
apply generic_format_abs.
apply generic_format_round.
apply fexp_correct.
apply generic_format_abs...
apply generic_format_round...
(* . not m1' < 0 *)
elim Rgt_not_eq with (2 := Hr).
apply Rlt_le_trans with R0.
......@@ -822,7 +825,7 @@ Theorem Bmult_correct :
B2FF (Bmult m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ;
try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ apply refl_equal | apply bpow_gt_0 ] ).
try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ).
simpl.
case Bmult_correct_aux.
intros H1 H2.
......@@ -978,22 +981,20 @@ Theorem Bplus_correct :
B2R (Bplus m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y)
else
(B2FF (Bplus m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
Proof.
Proof with auto with typeclass_instances.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy.
(* *)
rewrite Rplus_0_r, round_0, Rabs_R0, Rlt_bool_true.
rewrite Rplus_0_r, round_0, Rabs_R0, Rlt_bool_true...
simpl.
case (Bool.eqb sx sy) ; try easy.
now case m.
apply bpow_gt_0.
(* *)
rewrite Rplus_0_l, round_generic, Rlt_bool_true.
apply refl_equal.
rewrite Rplus_0_l, round_generic, Rlt_bool_true...
apply B2R_lt_emax.
apply generic_format_B2R.
(* *)
rewrite Rplus_0_r, round_generic, Rlt_bool_true.
apply refl_equal.
rewrite Rplus_0_r, round_generic, Rlt_bool_true...
apply B2R_lt_emax.
apply generic_format_B2R.
(* *)
......@@ -1058,15 +1059,13 @@ split.
apply Rlt_le_trans with (F2R (Float radix2 (cond_Zopp true (Zpos mx)) ex)).
rewrite <- opp_F2R.
now apply Ropp_lt_contravar.
apply round_monotone_l.
apply fexp_correct.
apply round_monotone_l...
now apply generic_format_canonic.
pattern (F2R (Float radix2 (cond_Zopp true (Zpos mx)) ex)) at 1 ; rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
now apply F2R_ge_0_compat.
apply Rle_lt_trans with (2 := By).
apply round_monotone_r.
apply fexp_correct.
apply round_monotone_r...
now apply generic_format_canonic.
rewrite <- (Rplus_0_l (F2R (Float radix2 (Zpos my) ey))).
apply Rplus_le_compat_r.
......@@ -1080,22 +1079,20 @@ split.
apply Rlt_le_trans with (F2R (Float radix2 (cond_Zopp true (Zpos my)) ey)).
rewrite <- opp_F2R.
now apply Ropp_lt_contravar.
apply round_monotone_l.
apply fexp_correct.
apply round_monotone_l...
now apply generic_format_canonic.
pattern (F2R (Float radix2 (cond_Zopp true (Zpos my)) ey)) at 1 ; rewrite <- Rplus_0_l.
apply Rplus_le_compat_r.
now apply F2R_ge_0_compat.
apply Rle_lt_trans with (2 := Bx).
apply round_monotone_r.
apply fexp_correct.
apply round_monotone_r...
now apply generic_format_canonic.
rewrite <- (Rplus_0_r (F2R (Float radix2 (Zpos mx) ex))).
apply Rplus_le_compat_l.
now apply F2R_le_0_compat.
destruct mz as [|mz|mz].
(* . mz = 0 *)
rewrite F2R_0, round_0, Rabs_R0, Rlt_bool_true.
rewrite F2R_0, round_0, Rabs_R0, Rlt_bool_true...
now case m.
apply bpow_gt_0.
(* . mz > 0 *)
......@@ -1253,7 +1250,7 @@ intros m x [sy|sy| |sy my ey Hy] Zy ; try now elim Zy.
revert x.
unfold Rdiv.
intros [sx|sx| |sx mx ex Hx] ;
try ( rewrite Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ apply refl_equal | apply bpow_gt_0 ] ).
try ( rewrite Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ).
simpl.
case Bdiv_correct_aux.
intros H1 H2.
......@@ -1275,7 +1272,7 @@ Lemma Bsqrt_correct_aux :
end in
valid_binary z = true /\
FF2R radix2 z = round radix2 fexp (round_mode m) (sqrt x).
Proof.
Proof with auto with typeclass_instances.
intros m mx ex Hx.
simpl.
refine (_ (Fsqrt_core_correct radix2 prec (Zpos mx) ex _)) ; try easy.
......@@ -1353,8 +1350,7 @@ apply generic_format_canonic.
apply (canonic_bounded_prec false).
apply (andb_prop _ _ Hx).
(* .. *)
apply round_monotone_l.
apply fexp_correct.
apply round_monotone_l...
apply generic_format_0.
apply sqrt_ge_0.
rewrite Rabs_pos_eq.
......@@ -1389,7 +1385,7 @@ Theorem Bsqrt_correct :
forall m x,
B2R (Bsqrt m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)).
Proof.
intros m [sx|[|]| |sx mx ex Hx] ; try ( now simpl ; rewrite sqrt_0, round_0 ).
intros m [sx|[|]| |sx mx ex Hx] ; try ( now simpl ; rewrite sqrt_0, round_0 ; auto with typeclass_instances ).
simpl.
case Bsqrt_correct_aux.
intros H1 H2.
......@@ -1399,6 +1395,7 @@ unfold sqrt.
case Rcase_abs.
intros _.
apply round_0.
auto with typeclass_instances.
intros H.
elim Rge_not_lt with (1 := H).
now apply F2R_lt_0_compat.
......
......@@ -44,7 +44,7 @@ Theorem Fsqrt_FLT_ne_correct :
Rnd_NE_pt beta (FLT_exp emin prec) (sqrt (F2R x)) (F2R (Fsqrt_FLT_ne x)).
Proof with auto with typeclass_instances.
intros x.
replace (F2R (Fsqrt_FLT_ne x)) with (round beta (FLT_exp emin prec) rndNE (sqrt (F2R x))).
replace (F2R (Fsqrt_FLT_ne x)) with (round beta (FLT_exp emin prec) ZnearestE (sqrt (F2R x))).
apply round_NE_pt...
unfold Fsqrt_FLT_ne.
destruct x as (mx, ex).
......@@ -53,7 +53,7 @@ case (Zle_bool mx 0) ; intros Hm.
(* mx = 0 *)
rewrite F2R_0.
replace (sqrt (F2R (Float beta mx ex))) with R0.
apply round_0.
apply round_0...
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
unfold sqrt.
case Rcase_abs ; intros Hs.
......
This diff is collapsed.
......@@ -236,30 +236,16 @@ Qed.
Section FTZ_round.
(** Rounding with FTZ *)
Hypothesis rnd : Zround.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_FTZ x :=
if Rle_bool R1 (Rabs x) then Zrnd rnd x else Z0.
if Rle_bool R1 (Rabs x) then rnd x else Z0.
Theorem Z_FTZ_Z2R :
forall n, Zrnd_FTZ (Z2R n) = n.
Proof.
intros n.
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R.
case Rle_bool_spec.
easy.
rewrite <- Z2R_abs.
intros H.
generalize (lt_Z2R _ 1 H).
clear.
now case n ; trivial ; simpl ; intros [p|p|].
Qed.
Theorem Z_FTZ_monotone :
forall x y, (x <= y)%R ->
(Zrnd_FTZ x <= Zrnd_FTZ y)%Z.
Proof.
Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
Proof with auto with typeclass_instances.
split.
(* *)
intros x y Hxy.
unfold Zrnd_FTZ.
case Rle_bool_spec ; intros Hx ;
......@@ -268,7 +254,7 @@ case Rle_bool_spec ; intros Hx ;
(* 1 <= |x| *)
now apply Zrnd_monotone.
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
apply Zrnd_monotone...
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
exact Hx1.
......@@ -278,7 +264,7 @@ apply Rle_trans with (1 := Hxy).
apply RRle_abs.
(* |x| < 1 *)
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
apply Zrnd_monotone...
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
......@@ -286,14 +272,23 @@ elim Rle_not_lt with (1 := Hy1).
apply Rlt_le_trans with (2 := Hxy).
apply (Rabs_def2 _ _ Hx).
exact Hy1.
(* *)
intros n.
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R...
case Rle_bool_spec.
easy.
rewrite <- Z2R_abs.
intros H.
generalize (lt_Z2R _ 1 H).
clear.
now case n ; trivial ; simpl ; intros [p|p|].
Qed.
Definition ZrFTZ := mkZround Zrnd_FTZ Z_FTZ_monotone Z_FTZ_Z2R.
Theorem FTZ_round :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FTZ_exp ZrFTZ x = round beta (FLX_exp prec) rnd x.
round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.
Proof.
intros x Hx.
unfold round, scaled_mantissa, canonic_exponent.
......@@ -335,12 +330,12 @@ Qed.
Theorem FTZ_round_small :
forall x : R,
(Rabs x < bpow (emin + prec - 1))%R ->
round beta FTZ_exp ZrFTZ x = R0.
Proof.
round beta FTZ_exp Zrnd_FTZ x = R0.
Proof with auto with typeclass_instances.
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply round_0.
apply round_0...
unfold round, scaled_mantissa, canonic_exponent.
destruct (ln_beta beta x) as (ex, He). simpl.
specialize (He Hx0).
......
This diff is collapsed.
......@@ -25,6 +25,8 @@ Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_ulp.
Notation ZnearestE := (Znearest (fun x => negb (Zeven x))).
Section Fcore_rnd_NE.
Variable beta : radix.
......@@ -50,8 +52,8 @@ Definition DN_UP_parity_pos_prop :=
~ format x ->
canonic xd ->
canonic xu ->
F2R xd = round beta fexp rndDN x ->
F2R xu = round beta fexp rndUP x ->
F2R xd = round beta fexp Zfloor x ->
F2R xu = round beta fexp Zceil x ->
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Definition DN_UP_parity_prop :=
......@@ -59,8 +61,8 @@ Definition DN_UP_parity_prop :=
~ format x ->
canonic xd ->
canonic xu ->
F2R xd = round beta fexp rndDN x ->
F2R xu = round beta fexp rndUP x ->
F2R xd = round beta fexp Zfloor x ->
F2R xu = round beta fexp Zceil x ->
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Lemma DN_UP_parity_aux :
......@@ -107,7 +109,7 @@ Context { exists_NE_ : Exists_NE }.
Theorem DN_UP_parity_generic_pos :
DN_UP_parity_pos_prop.
Proof.
Proof with auto with typeclass_instances.
intros x xd xu H0x Hfx Hd Hu Hxd Hxu.
destruct (ln_beta beta x) as (ex, Hexa).
specialize (Hexa (Rgt_not_eq _ _ H0x)).
......@@ -167,7 +169,7 @@ destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2].
(* - xu > bpow ex *)
elim (Rlt_not_le _ _ Hu2).
rewrite Hxu.
now apply (round_bounded_large_pos beta fexp rndUP x ex).
apply round_bounded_large_pos...
(* - xu = bpow ex *)
assert (Hu3: xu = Float beta (1 * Zpower beta (ex - fexp (ex + 1))) (fexp (ex + 1))).
apply canonic_unicity with (1 := Hu).
......@@ -333,57 +335,54 @@ apply Rnd_NE_pt_total.
apply Rnd_NE_pt_monotone.
Qed.
Definition rndNE := rndN (fun x => negb (Zeven x)).
Theorem round_NE_pt_pos :
forall x,
(0 < x)%R ->
Rnd_NE_pt x (round beta fexp rndNE x).
Proof.
Rnd_NE_pt x (round beta fexp ZnearestE x).
Proof with auto with typeclass_instances.
intros x Hx.
split.
now apply generic_N_pt.
unfold NE_prop.
set (mx := scaled_mantissa beta fexp x).
set (xr := round beta fexp rndNE x).
set (xr := round beta fexp ZnearestE x).
destruct (Req_dec (mx - Z2R (Zfloor mx)) (/2)) as [Hm|Hm].
(* midpoint *)
left.
exists (Float beta (Ztrunc (scaled_mantissa beta fexp xr)) (canonic_exponent beta fexp xr)).
split.
apply (generic_N_pt beta fexp _ x).
apply generic_N_pt...
split.
unfold Fcore_generic_fmt.canonic. simpl.
apply f_equal.
apply (generic_N_pt beta fexp _ x).
apply generic_N_pt...
simpl.
unfold xr, round, Zrnd. simpl.
unfold Znearest.
unfold xr, round, Znearest.
fold mx.
rewrite Hm.
rewrite Rcompare_Eq. 2: apply refl_equal.
case_eq (Zeven (Zfloor mx)) ; intros Hmx.
(* . even floor *)
change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp rndDN x))) = true).
destruct (Rle_or_lt (round beta fexp rndDN x) 0) as [Hr|Hr].
change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zfloor x))) = true).
destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr].
rewrite (Rle_antisym _ _ Hr).
unfold scaled_mantissa.
rewrite Rmult_0_l.
change R0 with (Z2R 0).
now rewrite (Ztrunc_Z2R 0).
erewrite <- round_0.
apply round_monotone ; try easy.
rewrite <- (round_0 beta fexp Zfloor).
apply round_monotone...
now apply Rlt_le.
rewrite scaled_mantissa_DN ; try easy.
rewrite scaled_mantissa_DN...
now rewrite Ztrunc_Z2R.
(* . odd floor *)
change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp rndUP x))) = true).
change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zceil x))) = true).
destruct (ln_beta beta x) as (ex, Hex).
specialize (Hex (Rgt_not_eq _ _ Hx)).
rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx)) in Hex.
destruct (Z_lt_le_dec (fexp ex) ex) as [He|He].
(* .. large pos *)
assert (Hu := round_bounded_large_pos _ _ rndUP _ _ He Hex).
assert (Hu := round_bounded_large_pos _ _ Zceil _ _ He Hex).
assert (Hfc: Zceil mx = (Zfloor mx + 1)%Z).
apply Zceil_floor_neq.
intros H.
......@@ -450,11 +449,11 @@ intros g Hg.
destruct (Req_dec x g) as [Hxg|Hxg].
rewrite <- Hxg.
apply sym_eq.
apply round_generic.
apply round_generic...
rewrite Hxg.
apply Hg.
set (d := round beta fexp rndDN x).
set (u := round beta fexp rndUP x).
set (d := round beta fexp Zfloor x).
set (u := round beta fexp Zceil x).
apply Rnd_N_pt_unicity with (d := d) (u := u) (4 := Hg).
now apply round_DN_pt.
now apply round_UP_pt.
......@@ -482,10 +481,10 @@ Qed.
Theorem round_NE_opp :
forall x,
round beta fexp rndNE (-x) = (- round beta fexp rndNE x)%R.
round beta fexp ZnearestE (-x) = (- round beta fexp ZnearestE x)%R.
Proof.
intros x.
unfold rndNE, round. simpl.
unfold round. simpl.
rewrite scaled_mantissa_opp, canonic_exponent_opp.
rewrite Znearest_opp.
rewrite opp_F2R.
......@@ -502,8 +501,8 @@ Qed.
Theorem round_NE_pt :
forall x,
Rnd_NE_pt x (round beta fexp rndNE x).
Proof.
Rnd_NE_pt x (round beta fexp ZnearestE x).
Proof with auto with typeclass_instances.
intros x.
destruct (total_order_T x 0) as [[Hx|Hx]|Hx].
apply Rnd_NG_pt_sym.
......@@ -520,7 +519,7 @@ now rewrite Zeven_opp.
rewrite <- round_NE_opp.
apply round_NE_pt_pos.
now apply Ropp_0_gt_lt_contravar.
rewrite Hx, round_0.
rewrite Hx, round_0...
apply Rnd_NG_pt_refl.
apply generic_format_0.
now apply round_NE_pt_pos.
......
This diff is collapsed.
......@@ -70,14 +70,14 @@ Qed.
(** Remainder of the division in FLX *)
Theorem div_error_FLX :
forall Zrnd x y,
forall rnd { Zrnd : Valid_rnd rnd } x y,
format x -> format y ->
format (x - round beta (FLX_exp prec) Zrnd (x/y) * y)%R.
Proof.
intros Zrnd x y Hx Hy.
format (x - round beta (FLX_exp prec) rnd (x/y) * y)%R.
Proof with auto with typeclass_instances.
intros rnd Zrnd x y Hx Hy.
destruct (Req_dec y 0) as [Zy|Zy].
now rewrite Zy, Rmult_0_r, Rminus_0_r.
case (Req_dec (round beta (FLX_exp prec) Zrnd (x/y)) 0); intros Hr.
destruct (Req_dec (round beta (FLX_exp prec) rnd (x/y)) 0) as [Hr|Hr].
rewrite Hr; ring_simplify (x-0*y)%R; assumption.
assert (Zx: x <> R0).
contradict Hr.
......@@ -86,13 +86,12 @@ unfold Rdiv.
now rewrite Rmult_0_l, round_0.
destruct (format_nx x Hx) as (fx,(Hx1,Hx2)).
destruct (format_nx y Hy) as (fy,(Hy1,Hy2)).
destruct (format_nx (round beta (FLX_exp prec) Zrnd (x / y))) as (fr,(Hr1,Hr2)).
apply generic_format_round.
now apply FLX_exp_valid.
destruct (format_nx (round beta (FLX_exp prec) rnd (x / y))) as (fr,(Hr1,Hr2)).
apply generic_format_round...
unfold Rminus; apply format_add with fx (Fopp beta (Fmult beta fr fy)); trivial.
now rewrite Fopp_F2R,mult_F2R, <- Hr1, <- Hy1.
(* *)
destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) Zrnd (x / y)%R) as (eps,(Heps1,Heps2)).
destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)).
apply Rmult_integral_contrapositive_currified.
exact Zx.
now apply Rinv_neq_0_compat.
......@@ -123,8 +122,8 @@ apply Zle_refl.
(* *)
replace (Fexp (Fopp beta (Fmult beta fr fy))) with (Fexp fr + Fexp fy)%Z.
2: unfold Fopp, Fmult; destruct fr; destruct fy; now simpl.
replace (x + - (round beta (FLX_exp prec) Zrnd (x / y) * y))%R with
(y * (-(round beta (FLX_exp prec) Zrnd (x / y) - x/y)))%R.
replace (x + - (round beta (FLX_exp prec) rnd (x / y) * y))%R with
(y * (-(round beta (FLX_exp prec) rnd (x / y) - x/y)))%R.
2: field; assumption.
rewrite Rabs_mult.
apply Rlt_le_trans with (Rabs y * bpow (Fexp fr))%R.
......@@ -133,10 +132,7 @@ now apply Rabs_pos_lt.
rewrite Rabs_Ropp.
replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)).
rewrite <- Hr1.
apply ulp_error_f.
now apply FLX_exp_valid.
apply FLX_exp_monotone.
exact Hr.
apply ulp_error_f...
unfold ulp; apply f_equal.
now rewrite Hr2, <- Hr1.
replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring.
......@@ -154,27 +150,26 @@ Variable Hp1 : Zlt 1 prec.
Theorem sqrt_error_FLX_N :
forall x, format x ->
format (x - Rsqr (round beta (FLX_exp prec) (rndN choice) (sqrt x)))%R.
Proof.
format (x - Rsqr (round beta (FLX_exp prec) (Znearest choice) (sqrt x)))%R.
Proof with auto with typeclass_instances.
intros x Hx.
destruct (total_order_T x 0) as [[Hxz|Hxz]|Hxz].
unfold sqrt.
destruct (Rcase_abs x).
rewrite round_0.
rewrite round_0...
unfold Rsqr.
now rewrite Rmult_0_l, Rminus_0_r.
elim (Rlt_irrefl 0).
now apply Rgt_ge_trans with x.
rewrite Hxz, sqrt_0, round_0.
rewrite Hxz, sqrt_0, round_0...
unfold Rsqr.
rewrite Rmult_0_l, Rminus_0_r.
apply generic_format_0.
case (Req_dec (round beta (FLX_exp prec) (rndN choice) (sqrt x)) 0); intros Hr.
case (Req_dec (round beta (FLX_exp prec) (Znearest choice) (sqrt x)) 0); intros Hr.
rewrite Hr; unfold Rsqr; ring_simplify (x-0*0)%R; assumption.
destruct (format_nx x Hx) as (fx,(Hx1,Hx2)).
destruct (format_nx (round beta (FLX_exp prec) (rndN choice) (sqrt x))) as (fr,(Hr1,Hr2)).
apply generic_format_round.
now apply FLX_exp_valid.
destruct (format_nx (round beta (FLX_exp prec) (Znearest choice) (sqrt x))) as (fr,(Hr1,Hr2)).
apply generic_format_round...
unfold Rminus; apply format_add with fx (Fopp beta (Fmult beta fr fr)); trivial.
unfold Rsqr; now rewrite Fopp_F2R,mult_F2R, <- Hr1.
(* *)
......@@ -247,9 +242,7 @@ apply Rmult_le_compat_r.
apply Rabs_pos.
apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R.
rewrite <- Hr1.
apply ulp_half_error_f; trivial.
now apply FLX_exp_valid.
apply FLX_exp_monotone.
apply ulp_half_error_f...
right; unfold ulp; apply f_equal.
rewrite Hr2, <- Hr1; trivial.
rewrite Rmult_assoc, Rmult_comm.
......@@ -289,8 +282,7 @@ intros H1.
absurd (Rabs (F2R fr) < bpow (es - 1))%R.
apply Rle_not_lt.
rewrite <- Hr1.
apply round_monotone_abs_l.
now apply FLX_exp_valid.
apply round_monotone_abs_l...
apply generic_format_bpow.
unfold FLX_exp; omega.
apply Es.
......
......@@ -32,9 +32,11 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
(** Auxiliary result that provides the exponent *)
Lemma mult_error_FLX_aux:
forall rnd,
forall x y,
format x -> format y ->
(round beta (FLX_exp prec) rnd (x * y) - (x * y) <> 0)%R ->
......@@ -42,13 +44,13 @@ Lemma mult_error_FLX_aux:
(F2R f = round beta (FLX_exp prec) rnd (x * y) - (x * y))%R
/\ (canonic_exponent beta (FLX_exp prec) (F2R f) <= Fexp f)%Z
/\ (Fexp f = cexp x + cexp y)%Z.
Proof.
intros rnd x y Hx Hy Hz.
Proof with auto with typeclass_instances.
intros x y Hx Hy Hz.
set (f := (round beta (FLX_exp prec) rnd (x * y))).
destruct (Req_dec (x * y) 0) as [Hxy0|Hxy0].
contradict Hz.
rewrite Hxy0.
rewrite round_0.
rewrite round_0...
ring.
destruct (ln_beta beta (x * y)) as (exy, Hexy).
specialize (Hexy Hxy0).
......@@ -100,7 +102,7 @@ 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)) *
Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) *
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.
......@@ -112,7 +114,7 @@ unfold Fplus. simpl.
now rewrite Zle_imp_le_bool with (1 := Hc2).
(* *)