Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit dae54a95 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Propagate naming changes to fix compilation. Update list of changes.

parent d1c2186e
round_monotone -> round_le
round_monotone_l -> round_ge_generic
round_monotone_r -> round_le_generic
round_monotone_abs_l -> abs_round_ge_generic
round_monotone_abs_r -> abs_round_le_generic
canonic_exponent_round -> canonic_exponent_round_ge
generic_N_pt -> round_N_pt
ulp_le_pos -> ulp_le_id
succ_lt_le -> succ_le_lt
ulp_monotone -> ulp_le
ulp_DN_pt_eq -> ulp_DN
format_pred -> generic_format_pred
pred_ulp -> pred_plus_ulp
pred_lt -> pred_lt_id
FLT_canonic_FLX -> canonic_exp_FLT_FLX
FLT_generic_format_FLX -> generic_format_FLT_FLX
FLX_generic_format_FLT -> generic_format_FLX_FLT
FLT_round_FLX -> round_FLT_FLX
FLT_canonic_FIX -> canonic_FLT_FIX
FIX_generic_format_FLT -> generic_format_FIX_FLT
FLT_generic_format_FIX -> generic_format_FLT_FIX
Type classes (Valid_exp, Valid_rnd, Exp_not_FTZ, Monotone_exp
Exists_NE
Equivalences FIX/FLX (...) cassées
Version 2.0.0:
- changed rounding modes from records to R -> Z functions as arguments
to the round function
. rndDN -> Zfloor
. rndUP -> Zceil
. rndZE -> Ztrunc
. rndNE -> ZnearestE
. rndNA -> ZnearestA
- added typeclasses for automatic inference of properties:
. Valid_exp for Z -> Z functions describing formats
. Valid_rnd for R -> Z functions describing rounding modes
. Exp_not_FTZ for Z -> Z functions describing formats with subnormal
. Monotone_exp for Z -> Z functions describing regular formats
. Exists_NE for radix/formats supporting rounding to nearest even
- removed theorems superseded by typeclasses:
. FIX_exp_correct, FLX_exp_correct, FLT_exp_correct, FTZ_exp_correct
. FIX_exp_monotone, FLX_exp_monotone, FLT_monotone
. Rnd_NE_pt_FIX, Rnd_NE_pt_FLX, Rnd_NE_pt_FLT
. round_NE_pt_FLX, round_NE_pt_FLT
. Zrnd_opp_le, Zrnd_Z2R_opp
- split theorems on equivalence between specific and generic formats
into both directions:
. FIX_format_generic and generic_format_FIX
. FLX_format_generic and generic_format_FLX
. FLT_format_generic and generic_format_FLT
. FTZ_format_generic and generic_format_FTZ
- modified correctness theorems for IEEE-754 operators so that they also
mention finiteness of the results
- added a Flocq_version.Flocq_version Coq variable for Flocq detection
and version testing in configure scripts
- moved parts of some files into other files:
. Fcore_Raux -> Fcore_Zaux
. Fcalc_digits -> Fcore_digits
. Fappli_IEEE -> Fappli_IEEE_bits
- renamed theorems more uniformly:
. Rabs_Rminus_pos -> Rabs_minus_le
. exp_increasing_weak -> exp_le
. ln_beta_monotone -> ln_beta_le
. ln_beta_monotone_abs -> ln_beta_le_abs
. abs_F2R -> F2R_abs (changed direction)
. opp_F2R -> F2R_opp (changed direction)
. scaled_mantissa_bpow -> scaled_mantissa_mult_bpow
. round_monotone -> round_le
. round_monotone_l -> round_ge_generic
. round_monotone_r -> round_le_generic
. round_monotone_abs_l -> abs_round_ge_generic
. round_monotone_abs_r -> abs_round_le_generic
. generic_format_canonic_exponent -> generic_format_F2R (modified hypothesis)
. canonic_exponent_round -> canonic_exponent_round_ge
. generic_N_pt -> round_N_pt
. round_pred_pos_imp_rnd -> round_pred_ge_0
. round_pred_rnd_imp_pos -> round_pred_gt_0
. round_pred_neg_imp_rnd -> round_pred_le_0
. round_pred_rnd_imp_neg -> round_pred_lt_0
. ulp_le_pos -> ulp_le_id
. succ_lt_le -> succ_le_lt
. ulp_monotone -> ulp_le
. ulp_DN_pt_eq -> ulp_DN
. format_pred -> generic_format_pred
. pred_ulp -> pred_plus_ulp
. pred_lt -> pred_lt_id
. FLT_generic_format_FLX -> generic_format_FLT_FLX
. FLX_generic_format_FLT -> generic_format_FLX_FLT
. FIX_generic_format_FLT -> generic_format_FIX_FLT
. FLT_generic_format_FIX -> generic_format_FLT_FIX
. FLT_round_FLX -> round_FLT_FLX
. FTZ_round -> round_FTZ_FLX
. FTZ_round_small -> round_FTZ_small
. FLT_canonic_FLX -> canonic_exp_FLT_FLX
. FLT_canonic_FIX -> canonic_exp_FLT_FIX
Version 1.4.0:
- improved efficiency of IEEE-754 addition
......
......@@ -307,7 +307,7 @@ Theorem B2R_Bopp :
Proof.
intros [sx|sx| |sx mx ex Hx] ; apply sym_eq ; try apply Ropp_0.
simpl.
rewrite opp_F2R.
rewrite <- F2R_opp.
now case sx.
Qed.
......@@ -326,7 +326,7 @@ unfold ln_beta_val.
intros H.
apply Rlt_le_trans with (bpow radix2 e').
change (Zpos mx) with (Zabs (Zpos mx)).
rewrite <- abs_F2R.
rewrite F2R_abs.
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
......@@ -347,7 +347,7 @@ Theorem B2R_lt_emax :
(Rabs (B2R x) < bpow radix2 emax)%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
rewrite abs_F2R, abs_cond_Zopp.
rewrite <- F2R_abs, abs_cond_Zopp.
now apply bounded_lt_emax.
Qed.
......@@ -378,7 +378,7 @@ cut (e' - 1 < emax)%Z. clear ; omega.
apply lt_bpow with radix2.
apply Rle_lt_trans with (2 := Bx).
change (Zpos mx) with (Zabs (Zpos mx)).
rewrite <- abs_F2R.
rewrite F2R_abs.
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
......@@ -659,7 +659,7 @@ assert (Hr: Rabs (round radix2 fexp (round_mode m) x) = F2R (Float radix2 m1' e1
(* . *)
rewrite <- (Zabs_eq m1').
replace (Zabs m1') with (Zabs (cond_Zopp (Rlt_bool x 0) m1')).
rewrite <- abs_F2R.
rewrite F2R_abs.
now apply f_equal.
apply abs_cond_Zopp.
apply Zle_trans with (2 := Hm).
......@@ -684,7 +684,7 @@ rewrite Rlt_bool_true.
repeat split.
apply sym_eq.
case Rlt_bool ; apply F2R_0.
rewrite abs_F2R, abs_cond_Zopp, F2R_0.
rewrite <- F2R_abs, abs_cond_Zopp, F2R_0.
apply bpow_gt_0.
(* . 0 < m1' *)
assert (He: (e1 <= fexp (digits radix2 (Zpos m1') + e1))%Z).
......@@ -693,7 +693,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 canonic_exponent_round_ge...
rewrite H1c.
case (Rlt_bool x 0).
apply Rlt_not_eq.
......@@ -712,7 +712,7 @@ destruct m2 as [|m2|m2].
elim Rgt_not_eq with (2 := H3).
rewrite F2R_0.
now apply F2R_gt_0_compat.
rewrite F2R_cond_Zopp, H3, abs_cond_Ropp, abs_F2R.
rewrite F2R_cond_Zopp, H3, abs_cond_Ropp, <- F2R_abs.
simpl Zabs.
case_eq (Zle_bool e2 (emax - prec)) ; intros He2.
assert (bounded m2 e2 = true).
......@@ -844,7 +844,7 @@ simpl.
replace (xorb sx sy) with (Rlt_bool (F2R (Float radix2 (cond_Zopp sx (Zpos mx) * cond_Zopp sy (Zpos my)) (ex + ey))) 0).
apply binary_round_sign_correct.
constructor.
rewrite abs_F2R.
rewrite <- F2R_abs.
apply F2R_eq_compat.
rewrite Zabs_Zmult.
now rewrite 2!abs_cond_Zopp.
......@@ -1044,7 +1044,7 @@ replace sx with (Rlt_bool x 0).
apply binary_round_sign_correct.
constructor.
unfold x.
now rewrite abs_F2R, abs_cond_Zopp.
now rewrite <- F2R_abs, abs_cond_Zopp.
exact H2.
unfold x.
case sx.
......@@ -1208,15 +1208,15 @@ clear Hs.
apply Rabs_lt.
split.
apply Rlt_le_trans with (F2R (Float radix2 (cond_Zopp true (Zpos mx)) ex)).
rewrite <- opp_F2R.
rewrite F2R_opp.
now apply Ropp_lt_contravar.
apply round_monotone_l...
apply round_ge_generic...
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 round_le_generic...
now apply generic_format_canonic.
rewrite <- (Rplus_0_l (F2R (Float radix2 (Zpos my) ey))).
apply Rplus_le_compat_r.
......@@ -1228,15 +1228,15 @@ clear Hs.
apply Rabs_lt.
split.
apply Rlt_le_trans with (F2R (Float radix2 (cond_Zopp true (Zpos my)) ey)).
rewrite <- opp_F2R.
rewrite F2R_opp.
now apply Ropp_lt_contravar.
apply round_monotone_l...
apply round_ge_generic...
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 round_le_generic...
now apply generic_format_canonic.
rewrite <- (Rplus_0_r (F2R (Float radix2 (Zpos mx) ex))).
apply Rplus_le_compat_l.
......@@ -1301,7 +1301,7 @@ now apply Zle_lt_trans with Z0.
(* . mz > 0 *)
apply binary_round_sign_correct.
rewrite Rabs_mult, Rabs_Rinv.
now rewrite 2!abs_F2R, 2!abs_cond_Zopp.
now rewrite <- 2!F2R_abs, 2!abs_cond_Zopp.
case sy.
apply Rlt_not_eq.
now apply F2R_lt_0_compat.
......@@ -1326,14 +1326,14 @@ now apply F2R_gt_0_compat.
(* *)
case sy ; simpl.
change (Zneg my) with (Zopp (Zpos my)).
rewrite <- opp_F2R.
rewrite F2R_opp.
rewrite <- Ropp_inv_permute.
rewrite Ropp_mult_distr_r_reverse.
case sx ; simpl.
apply Rlt_bool_false.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_pos.
rewrite opp_F2R.
rewrite <- F2R_opp.
now apply F2R_ge_0_compat.
apply Rlt_le.
apply Rinv_0_lt_compat.
......@@ -1349,7 +1349,7 @@ apply Rgt_not_eq.
now apply F2R_gt_0_compat.
case sx.
apply Rlt_bool_true.
rewrite <- opp_F2R.
rewrite F2R_opp.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
......@@ -1516,7 +1516,7 @@ apply generic_format_canonic.
apply (canonic_bounded_prec false).
apply (andb_prop _ _ Hx).
(* .. *)
apply round_monotone_l...
apply round_ge_generic...
apply generic_format_0.
apply sqrt_ge_0.
rewrite Rabs_pos_eq.
......
......@@ -281,7 +281,7 @@ clear -H Hprec.
unfold prec ; omega.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_monotone radix2 _ _ _ H0)).
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_digits. 2: discriminate.
unfold emin, prec.
......@@ -340,7 +340,7 @@ apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_monotone radix2 _ _ _ H0)).
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_digits. 2: discriminate.
rewrite <- H.
......
......@@ -117,7 +117,7 @@ intros x y Hx Hxy.
case (Z_lt_le_dec 0 x).
clear Hx. intros Hx.
rewrite 2!digits_ln_beta.
apply ln_beta_monotone.
apply ln_beta_le.
now apply (Z2R_lt 0).
now apply Z2R_le.
apply Zgt_not_eq.
......@@ -206,7 +206,7 @@ apply Zplus_lt_compat.
now apply Zplus_lt_compat.
now apply Zmult_lt_0_compat.
rewrite 3!digits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
apply ln_beta_le with (1 := Rgt_not_eq _ _ Hxy).
apply ln_beta_le_bpow with (1 := Rgt_not_eq _ _ Hxy).
rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy).
destruct (ln_beta beta (Z2R x)) as (ex, Hex). simpl.
specialize (Hex (Rgt_not_eq _ _ (Z2R_lt _ _ Hx))).
......
......@@ -80,7 +80,7 @@ Theorem Fabs_F2R :
forall f1 : float beta,
(F2R (Fabs f1) = Rabs (F2R f1))%R.
intros (m1,e1).
now rewrite abs_F2R.
apply F2R_abs.
Qed.
Definition Fplus (f1 f2 : float beta) :=
......
......@@ -50,7 +50,7 @@ apply (f_equal (fun m => (Z2R m * bpow e)%R)).
apply Hc.
apply inbetween_mult_reg with (bpow e).
apply bpow_gt_0.
now rewrite scaled_mantissa_bpow.
now rewrite scaled_mantissa_mult_bpow.
Qed.
Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.
......@@ -74,7 +74,7 @@ apply inbetween_mult_reg with (bpow e).
apply bpow_gt_0.
rewrite <- (Rabs_right (bpow e)) at 3.
rewrite <- Rabs_mult.
now rewrite scaled_mantissa_bpow.
now rewrite scaled_mantissa_mult_bpow.
apply Rle_ge.
apply bpow_ge_0.
(* *)
......@@ -902,7 +902,7 @@ unfold Rabs in H.
destruct (Rcase_abs x) as [Zx|Zx].
rewrite Rlt_bool_true with (1 := Zx).
simpl.
rewrite <- opp_F2R.
rewrite F2R_opp.
rewrite <- H, Ropp_involutive.
apply round_generic...
rewrite Rlt_bool_false.
......
......@@ -143,7 +143,7 @@ destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply generic_format_0.
unfold generic_format, scaled_mantissa.
now rewrite (FLT_canonic_FLX x Hx0 Hx).
now rewrite canonic_exp_FLT_FLX.
Qed.
Theorem generic_format_FLX_FLT :
......@@ -165,14 +165,15 @@ Theorem round_FLT_FLX : forall rnd x,
round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
intros rnd x Hx.
unfold round, scaled_mantissa.
rewrite ->FLT_canonic_FLX; trivial.
intros H; contradict Hx.
rewrite H, Rabs_R0; apply Rlt_not_le.
rewrite canonic_exp_FLT_FLX ; trivial.
contradict Hx.
rewrite Hx, Rabs_R0.
apply Rlt_not_le.
apply bpow_gt_0.
Qed.
(** Links between FLT and FIX (underflow) *)
Theorem canonic_FLT_FIX :
Theorem canonic_exp_FLT_FIX :
forall x, x <> R0 ->
(Rabs x < bpow (emin + prec))%R ->
canonic_exponent beta FLT_exp x = canonic_exponent beta (FIX_exp emin) x.
......
......@@ -97,7 +97,7 @@ apply Zle_refl.
rewrite Hx1, ln_beta_F2R with (1 := Zxm).
cut (prec - 1 < ln_beta beta (Z2R xm))%Z.
clear -Hx3 ; omega.
apply ln_beta_Z2R_gt with (1 := Zxm).
apply ln_beta_gt_Zpower with (1 := Zxm).
apply Hx2.
apply generic_format_FLXN.
now apply FLXN_format_FTZ.
......@@ -124,7 +124,7 @@ generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx.
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
elim Rlt_not_ge with (1 := proj2 Hx4).
apply Rle_ge.
rewrite Hx2, abs_F2R.
rewrite Hx2, <- F2R_abs.
rewrite <- (Rmult_1_l (bpow ex)).
unfold F2R. simpl.
apply Rmult_le_compat.
......@@ -137,7 +137,7 @@ apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
apply bpow_gt_0.
rewrite Rmult_0_l.
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
rewrite <- abs_F2R, <- Hx2.
rewrite F2R_abs, <- Hx2.
now apply Rabs_pos_lt.
apply bpow_le.
omega.
......@@ -150,7 +150,7 @@ apply bpow_gt_0.
rewrite <- bpow_plus.
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
rewrite <- abs_F2R, <- Hx2.
rewrite F2R_abs, <- Hx2.
apply Hx4.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
......@@ -161,7 +161,7 @@ apply bpow_gt_0.
rewrite <- bpow_plus.
replace (prec + (ex - prec))%Z with ex by ring.
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
rewrite <- abs_F2R, <- Hx2.
rewrite F2R_abs, <- Hx2.
apply Hx4.
now apply Zlt_le_weak.
now apply Zge_le.
......@@ -214,9 +214,9 @@ case Rle_bool_spec ; intros Hx ;
case Rle_bool_spec ; intros Hy.
4: easy.
(* 1 <= |x| *)
now apply Zrnd_monotone.
now apply Zrnd_le.
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone...
apply Zrnd_le...
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
exact Hx1.
......@@ -226,7 +226,7 @@ apply Rle_trans with (1 := Hxy).
apply RRle_abs.
(* |x| < 1 *)
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone...
apply Zrnd_le...
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
......@@ -247,7 +247,7 @@ clear.
now case n ; trivial ; simpl ; intros [p|p|].
Qed.
Theorem FTZ_round :
Theorem round_FTZ_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.
......@@ -288,7 +288,7 @@ apply refl_equal.
clear -He' ; omega.
Qed.
Theorem FTZ_round_small :
Theorem round_FTZ_small :
forall x : R,
(Rabs x < bpow (emin + prec - 1))%R ->
round beta FTZ_exp Zrnd_FTZ x = R0.
......
......@@ -74,15 +74,15 @@ rewrite <- Pxy, plus_F2R, <- Hx, <- Hy.
unfold canonic_exponent.
replace exy with (fexp (Zmin ex ey)).
apply monotone_exp.
now apply ln_beta_le.
now apply ln_beta_le_bpow.
replace exy with (Fexp (Fplus beta fx fy)) by exact (f_equal Fexp Pxy).
rewrite Fexp_Fplus.
simpl. clear -monotone_exp.
apply sym_eq.
destruct (Zmin_spec ex ey) as [(H1,H2)|(H1,H2)] ; rewrite H2.
apply Zmin_left.
apply Zmin_l.
now apply monotone_exp.
apply Zmin_right.
apply Zmin_r.
apply monotone_exp.
apply Zlt_le_weak.
now apply Zgt_lt.
......@@ -103,14 +103,14 @@ apply generic_format_plus ; try assumption.
apply Rle_lt_trans with (1 := Hxy).
unfold Rmin.
destruct (Rle_dec (Rabs x) (Rabs y)) as [Hxy'|Hxy'].
rewrite Zmin_left.
rewrite Zmin_l.
destruct (ln_beta beta x) as (ex, Hx).
now apply Hx.
now apply ln_beta_monotone_abs.
rewrite Zmin_right.
now apply ln_beta_le_abs.
rewrite Zmin_r.
destruct (ln_beta beta y) as (ex, Hy).
now apply Hy.
apply ln_beta_monotone_abs.
apply ln_beta_le_abs.
exact Zy.
apply Rlt_le.
now apply Rnot_le_lt.
......
......@@ -51,7 +51,7 @@ apply Zle_trans with (Zmin (Fexp fx) (Fexp fy)).
unfold canonic_exponent, FLX_exp.
rewrite plus_F2R, <- Hx, <- Hy.
apply Zplus_le_reg_l with prec; ring_simplify.
apply ln_beta_le with (1 := H).
apply ln_beta_le_bpow with (1 := H).
now apply Zmin_case.
rewrite <- Fexp_Fplus, Hz.
apply Zle_refl.
......@@ -169,7 +169,7 @@ unfold Rminus; apply format_add with fx (Fopp beta (Fmult beta fr fr)); trivial.
unfold Rsqr; now rewrite Fopp_F2R,mult_F2R, <- Hr1.
(* *)
apply Rle_lt_trans with x.
apply Rabs_Rminus_pos.
apply Rabs_minus_le.
apply Rle_0_sqr.
destruct (relative_error_N_FLX_ex beta prec (prec_gt_0 prec) choice (sqrt x)) as (eps,(Heps1,Heps2)).
rewrite Heps2.
......@@ -277,7 +277,7 @@ intros H1.
absurd (Rabs (F2R fr) < bpow (es - 1))%R.
apply Rle_not_lt.
rewrite <- Hr1.
apply round_monotone_abs_l...
apply abs_round_ge_generic...
apply generic_format_bpow.
unfold FLX_exp; omega.
apply Es.
......
......@@ -109,7 +109,7 @@ rewrite Hy at 6.
rewrite <- mult_F2R.
simpl.
unfold f, round, Rminus.
rewrite opp_F2R, Rplus_comm, <- plus_F2R.
rewrite <- F2R_opp, Rplus_comm, <- plus_F2R.
unfold Fplus. simpl.
now rewrite Zle_imp_le_bool with (1 := Hc2).
(* *)
......@@ -124,7 +124,7 @@ 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 := Hexy).
apply ln_beta_le with (1 := Hz).
apply ln_beta_le_bpow with (1 := Hz).
replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)).
apply ulp_error...
unfold ulp, canonic_exponent.
......@@ -185,15 +185,15 @@ rewrite round_0...
ring_simplify (0 - 0)%R.
apply generic_format_0.
destruct (mult_error_FLX_aux beta prec rnd x y) as ((m,e),(H1,(H2,H3))).
now apply FLX_generic_format_FLT with emin.
now apply FLX_generic_format_FLT with emin.
rewrite <- (FLT_round_FLX beta emin).
now apply generic_format_FLX_FLT with emin.
now apply generic_format_FLX_FLT with emin.
rewrite <- (round_FLT_FLX beta emin).
assumption.
apply Rle_trans with (2:=Hxy).
apply bpow_le.
generalize (prec_gt_0 prec).
clear ; omega.
rewrite <- (FLT_round_FLX beta emin) in H1.
rewrite <- (round_FLT_FLX beta emin) in H1.
2:apply Rle_trans with (2:=Hxy).
2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega.
unfold f; rewrite <- H1.
......
......@@ -110,11 +110,11 @@ apply generic_format_F2R.
intros _.
apply monotone_exp.
rewrite <- H, <- Hxy', <- Hxy.
apply ln_beta_monotone_abs.
apply ln_beta_le_abs.
exact H0.
pattern x at 3 ; replace x with (-(y - (x + y)))%R by ring.
rewrite Rabs_Ropp.
now apply (generic_N_pt beta _ choice (x + y)).
now apply (round_N_pt beta _ choice (x + y)).
Qed.
(** Error of the addition *)
......@@ -179,7 +179,7 @@ unfold canonic_exponent.
rewrite ln_beta_unique with (1 := Hexy).
apply Zle_refl.
(* . *)
elim Rle_not_lt with (1 := round_monotone beta _ rnd _ _ (proj1 Hexy)).
elim Rle_not_lt with (1 := round_le beta _ rnd _ _ (proj1 Hexy)).
rewrite (Rabs_pos_eq _ Hp).
rewrite Hxy.
rewrite round_generic...
......
......@@ -147,10 +147,10 @@ Proof.
intros m x Hx.
apply generic_relative_error.
unfold x.
rewrite abs_F2R.
rewrite <- F2R_abs.
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
rewrite F2R_0, <- abs_F2R.
rewrite F2R_0, F2R_abs.
now apply Rabs_pos_lt.
Qed.
......@@ -200,7 +200,7 @@ apply round_abs_abs...
clear rnd valid_rnd x Hx Hx' He.
intros rnd valid_rnd x Hx.
rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
now apply round_monotone.
now apply round_le.
apply generic_format_bpow.
ring_simplify (ex - 1 + 1)%Z.
generalize (Hmin ex).
......@@ -217,10 +217,10 @@ intros Hp m x Hx.
apply generic_relative_error_2.
exact Hp.
unfold x.
rewrite abs_F2R.
rewrite <- F2R_abs.
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
rewrite F2R_0, <- abs_F2R.
rewrite F2R_0, F2R_abs.
now apply Rabs_pos_lt.
Qed.
......@@ -294,10 +294,10 @@ apply Rle_refl.
(* . *)
apply generic_relative_error_N.