Commit 1965172b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Split bpow_le and bpow_lt into implication theorems.

parent ec812f45
......@@ -34,7 +34,6 @@ Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
Notation ulp := (ulp beta (FLX_exp prec)).
Theorem pred_gt_0: forall f,
format f -> (0 < f)%R -> (0 < pred beta (FLX_exp prec) f)%R.
intros f Hf Zf.
......@@ -50,12 +49,12 @@ omega.
intros Hp1.
case Req_bool_spec; intros H; apply Rlt_Rminus;
apply Rlt_le_trans with (2:=proj1 Hef);
apply ->bpow_lt; omega.
apply bpow_lt; omega.
(* special case for p = 1 *)
intros Hp1.
case Req_bool_spec; intros H; apply Rlt_Rminus.
apply Rlt_le_trans with (2:=proj1 Hef).
apply ->bpow_lt; omega.
apply bpow_lt; omega.
rewrite <- Hp1.
case (proj1 Hef); trivial.
intros H'.
......
......@@ -83,7 +83,7 @@ replace (nb + (Z_of_nat k + 1) - 1)%Z with (nb + Z_of_nat k)%Z by ring.
apply le_Z2R.
rewrite Z2R_Zpower with (1 := Hnb).
rewrite Z2R_Zpower.
apply -> bpow_le.
apply bpow_le.
omega.
omega.
rewrite Zpower_exp.
......@@ -130,7 +130,7 @@ clear n Hn Hn'.
simpl.
assert (He1: (0 <= e - 1)%Z).
apply Zlt_0_le_0_pred.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
apply (Z2R_le 1).
now apply (Zlt_le_succ 0).
......@@ -165,7 +165,7 @@ rewrite He2.
cut (e - 1 < Z_of_nat (S (digits2_Pnat p)))%Z.
rewrite inj_S.
omega.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := proj1 He).
rewrite <- Z2R_Zpower_nat.
apply Z2R_lt.
......@@ -190,7 +190,7 @@ destruct (Z_eq_dec n 0) as [H|H].
now rewrite H.
rewrite digits_ln_beta with (1 := H).
destruct ln_beta as (e, He). simpl.
apply <- bpow_le.
apply (le_bpow beta).
apply Rlt_le.
apply Rle_lt_trans with (Rabs (Z2R n)).
simpl.
......
......@@ -85,7 +85,7 @@ rewrite canonic_exponent_fexp with (1 := Hx5).
unfold FLT_exp.
apply Zmax_lub. 2: exact Hx3.
cut (ex -1 < prec + xe)%Z. omega.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := proj1 Hx5).
rewrite Hx1.
apply F2R_lt_bpow.
......@@ -114,7 +114,7 @@ destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
apply -> bpow_le.
apply bpow_le.
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
apply Zle_max_l.
......@@ -143,7 +143,7 @@ destruct (ln_beta beta x) as (ex, He).
unfold FLX_exp. simpl.
specialize (He Hx0).
cut (emin + prec - 1 < ex)%Z. omega.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := Hx).
apply He.
Qed.
......@@ -214,7 +214,7 @@ unfold FIX_exp.
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 < emin + prec)%Z. omega.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.
......
......@@ -168,7 +168,7 @@ destruct (ln_beta beta (Z2R xm)) as (d,H4).
specialize (H4 (Z2R_neq _ _ H3)).
assert (H5: (0 <= prec - d)%Z).
cut (d - 1 < prec)%Z. omega.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rle_lt_trans with (Rabs (Z2R xm)).
apply H4.
rewrite <- Z2R_Zpower, <- Z2R_abs.
......
......@@ -88,7 +88,7 @@ case (Zlt_bool (ex - prec) emin) ; intros H1.
elim (Rlt_not_le _ _ (proj2 Hx6)).
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
rewrite <- bpow_plus.
apply -> bpow_le.
apply bpow_le.
omega.
rewrite Hx1, abs_F2R.
unfold F2R. simpl.
......@@ -99,9 +99,9 @@ rewrite <- Z2R_Zpower.
now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
now apply -> bpow_le.
now apply bpow_le.
cut (ex - 1 < prec + xe)%Z. omega.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := proj1 Hx6).
rewrite Hx1.
apply F2R_lt_bpow.
......@@ -142,7 +142,7 @@ rewrite Rmult_0_l.
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
rewrite <- abs_F2R, <- Hx2.
now apply Rabs_pos_lt.
apply -> bpow_le.
apply bpow_le.
omega.
rewrite Hx2.
eexists ; repeat split ; simpl.
......@@ -208,7 +208,7 @@ eexists. split. split. split.
now rewrite <- H1 at 1.
rewrite (Zsucc_pred emin).
apply Zlt_le_succ.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rmult_lt_reg_l with (Z2R (Zabs xm)).
apply Rmult_lt_reg_r with (bpow xe).
apply bpow_gt_0.
......@@ -320,7 +320,7 @@ rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rle_trans with (2 := proj1 He).
apply -> bpow_le.
apply bpow_le.
unfold FLX_exp.
omega.
apply bpow_ge_0.
......@@ -354,7 +354,7 @@ rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
apply Rlt_le_trans with (1 := Hx).
apply -> bpow_le.
apply bpow_le.
unfold FTZ_exp.
generalize (Zlt_cases (ex - prec) emin).
case Zlt_bool.
......@@ -363,7 +363,7 @@ apply Zle_refl.
intros He'.
elim Rlt_not_le with (1 := Hx).
apply Rle_trans with (2 := proj1 He).
apply -> bpow_le.
apply bpow_le.
omega.
apply bpow_ge_0.
Qed.
......
......@@ -1456,7 +1456,7 @@ split.
now elim H.
Qed.
Theorem bpow_lt_aux :
Theorem bpow_lt :
forall e1 e2 : Z,
(e1 < e2)%Z -> (bpow e1 < bpow e2)%R.
Proof.
......@@ -1492,42 +1492,43 @@ now split.
now split.
Qed.
Theorem bpow_lt :
Theorem lt_bpow :
forall e1 e2 : Z,
(e1 < e2)%Z <-> (bpow e1 < bpow e2)%R.
(bpow e1 < bpow e2)%R -> (e1 < e2)%Z.
Proof.
intros e1 e2.
split.
apply bpow_lt_aux.
intros H.
intros e1 e2 H.
apply Zgt_lt.
apply Znot_le_gt.
intros H'.
apply Rlt_not_le with (1 := H).
destruct (Zle_lt_or_eq _ _ H').
apply Rlt_le.
now apply bpow_lt_aux.
apply Req_le.
now apply f_equal.
now apply bpow_lt.
rewrite H0.
apply Rle_refl.
Qed.
Theorem bpow_le :
forall e1 e2 : Z,
(e1 <= e2)%Z <-> (bpow e1 <= bpow e2)%R.
(e1 <= e2)%Z -> (bpow e1 <= bpow e2)%R.
Proof.
intros e1 e2.
split.
intros H.
intros e1 e2 H.
apply Rnot_lt_le.
intros H'.
apply Zle_not_gt with (1 := H).
apply Zlt_gt.
now apply <- bpow_lt.
intros H.
now apply lt_bpow.
Qed.
Theorem le_bpow :
forall e1 e2 : Z,
(bpow e1 <= bpow e2)%R -> (e1 <= e2)%Z.
Proof.
intros e1 e2 H.
apply Znot_gt_le.
intros H'.
apply Rle_not_lt with (1 := H).
apply -> bpow_lt.
apply bpow_lt.
now apply Zgt_lt.
Qed.
......@@ -1537,9 +1538,9 @@ Theorem bpow_inj :
Proof.
intros.
apply Zle_antisym.
apply <- bpow_le.
apply le_bpow.
now apply Req_le.
apply <- bpow_le.
apply le_bpow.
now apply Req_le.
Qed.
......@@ -1643,7 +1644,7 @@ Proof.
intros e1 e2 He.
rewrite (Zsucc_pred e1).
apply Zlt_le_succ.
now apply <- bpow_lt.
now apply lt_bpow.
Qed.
Theorem bpow_unique :
......@@ -1745,7 +1746,7 @@ rewrite Rabs_right.
replace (e + 1 - 1)%Z with e by ring.
split.
apply Rle_refl.
apply -> bpow_lt.
apply bpow_lt.
apply Zlt_succ.
apply Rle_ge.
apply bpow_ge_0.
......@@ -1770,7 +1771,7 @@ Proof.
intros.
apply lt_Z2R.
rewrite Z2R_Zpower.
now apply -> (bpow_lt 0).
now apply (bpow_lt 0).
now apply Zlt_le_weak.
Qed.
......
......@@ -244,7 +244,7 @@ intros m e1 e2 Hm.
intros H.
assert (He : (e1 <= e2)%Z).
(* . *)
apply <- (bpow_le beta).
apply (le_bpow beta).
apply Rle_trans with (F2R (Float beta m e1)).
unfold F2R. simpl.
rewrite <- (Rmult_1_l (bpow e1)) at 1.
......@@ -296,7 +296,7 @@ now apply Zle_minus_le_0.
intros H.
apply Rle_trans with (1*bpow e1)%R.
rewrite Rmult_1_l.
apply -> bpow_le.
apply bpow_le.
now apply Zlt_le_weak.
unfold F2R. simpl.
apply Rmult_le_compat_r.
......@@ -357,7 +357,7 @@ now elim (Zle_not_lt _ _ (Zabs_pos m)).
replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.
apply F2R_change_exp.
cut (e' - 1 < e + p)%Z. omega.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := Hf).
rewrite abs_F2R, Zplus_comm, bpow_plus.
apply Rmult_lt_compat_r.
......
......@@ -250,7 +250,7 @@ apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
rewrite Rmult_1_r, Rmult_1_l.
apply Rlt_le_trans with (1 := proj2 Hx).
now apply -> bpow_le.
now apply bpow_le.
Qed.
Theorem scaled_mantissa_small :
......@@ -350,7 +350,7 @@ unfold canonic_exponent.
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
specialize (Ex Hxz).
apply Rlt_le_trans with (1 := proj2 Ex).
apply -> bpow_le.
apply bpow_le.
specialize (Hp ex).
omega.
Qed.
......@@ -383,7 +383,7 @@ split.
apply Req_le.
apply f_equal.
ring.
apply -> bpow_lt.
apply bpow_lt.
omega.
now rewrite ln_beta_bpow.
unfold scaled_mantissa.
......@@ -446,7 +446,7 @@ rewrite Rabs_pos_eq in Hey.
2: apply Rle_trans with (2:=Hxy); now apply Rlt_le.
assert (He: (ex <= ey)%Z).
cut (ex - 1 < ey)%Z. omega.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := proj1 Hex).
apply Rle_lt_trans with (1 := Hxy).
apply Hey.
......@@ -480,7 +480,7 @@ exact (proj2 (mantissa_small_pos _ _ Hex Hx1)).
unfold F2R. simpl.
rewrite Z2R_Zpower. 2: omega.
rewrite <- bpow_plus, Rmult_1_l.
apply -> bpow_le.
apply bpow_le.
omega.
apply Rle_trans with (F2R (Float beta (Zrnd (bpow ex * bpow (- fexp ex))) (fexp ex))).
apply F2R_le_compat.
......@@ -495,7 +495,7 @@ rewrite Zrnd_Z2R.
unfold F2R. simpl.
rewrite 2!Z2R_Zpower ; try omega.
rewrite <- 2!bpow_plus.
apply -> bpow_le.
apply bpow_le.
omega.
apply F2R_le_compat.
apply Zrnd_monotone.
......@@ -975,16 +975,16 @@ apply bpow_gt_0.
specialize (He (Rgt_not_eq _ _ Hx)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
apply Rle_trans with (bpow (ex - 1)).
apply -> bpow_le.
apply bpow_le.
cut (e < ex)%Z. omega.
apply <- bpow_lt.
apply (lt_bpow beta).
now apply Rle_lt_trans with (2 := proj2 He).
destruct (Zle_or_lt ex (fexp ex)).
destruct (round_bounded_small_pos rnd x ex H He) as [Hr|Hr].
rewrite Hr in Hd.
elim Rlt_irrefl with (1 := Hd).
rewrite Hr.
apply -> bpow_le.
apply bpow_le.
omega.
apply (round_bounded_large_pos rnd x ex H He).
Qed.
......
......@@ -435,7 +435,7 @@ Theorem ulp_monotone :
(ulp x <= ulp y)%R.
Proof.
intros Hm x y Hx Hxy.
apply -> bpow_le.
apply bpow_le.
apply Hm.
now apply ln_beta_monotone.
Qed.
......@@ -450,7 +450,7 @@ rewrite Rabs_pos_eq.
split.
ring_simplify (e + 1 - 1)%Z.
apply Rle_refl.
apply -> bpow_lt.
apply bpow_lt.
apply Zlt_succ.
apply bpow_ge_0.
Qed.
......@@ -612,7 +612,6 @@ unfold ulp, F2R; simpl.
now rewrite Rmult_1_l.
Qed.
Theorem format_pred_1:
forall x, (0 < x)%R -> F x ->
x <> bpow (ln_beta beta x - 1) ->
......@@ -648,7 +647,7 @@ split.
apply pred_ge_bpow; trivial.
unfold ulp; intro H.
assert (ex-1 < canonic_exponent beta fexp x < ex)%Z.
split; apply <- (bpow_lt beta); rewrite <- H; easy.
split ; apply (lt_bpow beta) ; rewrite <- H ; easy.
clear -H0. omega.
apply Ex'.
apply Rle_lt_trans with (2 := proj2 Ex').
......@@ -705,7 +704,7 @@ split.
apply Rplus_le_reg_l with (bpow (fexp (e-1))).
ring_simplify.
apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
apply Rplus_le_compat; apply -> bpow_le; omega.
apply Rplus_le_compat ; apply bpow_le ; omega.
apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
apply Rle_trans with (bpow 1*bpow (e - 2))%R.
apply Rmult_le_compat_r.
......@@ -727,7 +726,7 @@ rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
apply Rle_ge; apply Rle_0_minus.
apply -> bpow_le.
apply bpow_le.
omega.
replace f with 0%R.
apply generic_format_0.
......@@ -771,7 +770,7 @@ destruct Hex as ([H1|H1],H2).
apply pred_ge_bpow; trivial.
unfold ulp; intros H3.
assert (ex-1 < canonic_exponent beta fexp x < ex)%Z.
split; apply <- (bpow_lt beta); rewrite <- H3; easy.
split ; apply (lt_bpow beta) ; rewrite <- H3 ; easy.
omega.
contradict Hx; auto with real.
apply Rle_lt_trans with (2:=proj2 Hex).
......@@ -794,8 +793,7 @@ apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
now rewrite <- Fx.
Qed.
Theorem pred_ulp_2:
Theorem pred_ulp_2 :
forall x, (0 < x)%R -> F x ->
let e := ln_beta_val beta x (ln_beta beta x) in
x = bpow (e - 1) ->
......@@ -819,7 +817,7 @@ split.
apply Rplus_le_reg_l with (bpow (fexp (e-1))).
ring_simplify.
apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
apply Rplus_le_compat; apply -> bpow_le; omega.
apply Rplus_le_compat; apply bpow_le; omega.
apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
apply Rle_trans with (bpow 1*bpow (e - 2))%R.
apply Rmult_le_compat_r.
......@@ -842,7 +840,7 @@ apply Ropp_lt_contravar.
apply bpow_gt_0.
apply Rle_ge; apply Rle_0_minus.
rewrite Hxe.
apply -> bpow_le.
apply bpow_le.
omega.
(* *)
contradict Zp.
......@@ -882,7 +880,7 @@ apply Ropp_lt_contravar.
apply bpow_gt_0.
Qed.
Theorem pred_pos:
Theorem pred_ge_0 :
forall x,
(0 < x)%R -> F x -> (0 <= pred x)%R.
intros x Zx Fx.
......@@ -891,7 +889,7 @@ case Req_bool_spec; intros H.
(* *)
apply Rle_0_minus.
rewrite H.
apply -> bpow_le.
apply bpow_le.
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
rewrite ln_beta_bpow.
ring_simplify (ex - 1 + 1 - 1)%Z.
......@@ -918,7 +916,6 @@ apply Rlt_trans with (1:=Hx).
apply pred_lt.
Qed.
Theorem round_DN_pred :
forall x, (0 < pred x)%R -> F x ->
forall eps, (0 < eps <= ulp (pred x))%R ->
......@@ -944,12 +941,11 @@ apply Ropp_lt_contravar.
now apply Heps.
Qed.
Theorem le_pred_lt:
forall x y,
F x -> F y ->
(0 < x < y)%R ->
(x <= pred y)%R.
(x <= pred y)%R.
Proof.
intros x y Hx Hy H.
assert (Zy:(0 < y)%R).
......@@ -958,7 +954,7 @@ apply H.
(* *)
assert (Zp: (0 < pred y)%R).
assert (Zp:(0 <= pred y)%R).
apply pred_pos; trivial.
apply pred_ge_0 ; trivial.
destruct Zp; trivial.
generalize H0.
unfold pred.
......@@ -1031,9 +1027,9 @@ apply trans_eq with (ln_beta beta y).
apply sym_eq; apply ln_beta_unique.
rewrite H1, Rabs_right.
split.
apply -> bpow_le.
apply bpow_le.
omega.
apply -> bpow_lt.
apply bpow_lt.
omega.
apply Rle_ge; apply bpow_ge_0.
apply ln_beta_unique.
......@@ -1059,5 +1055,4 @@ now apply Rlt_Rminus.
now apply Rlt_le.
Qed.
End Fcore_ulp.
......@@ -105,7 +105,7 @@ apply Rmult_lt_compat_l.
now apply Rabs_pos_lt.
apply Rlt_le_trans with (1 := Heps1).
change R1 with (bpow 0).
apply -> bpow_le.
apply bpow_le.
clear -Hp. omega.
rewrite Rmult_1_r.
rewrite Hx2.
......@@ -115,7 +115,7 @@ simpl.
specialize (Hex Zx).
apply Rlt_le.
apply Rlt_le_trans with (1 := proj2 Hex).
apply -> bpow_le.
apply bpow_le.
unfold FLX_exp.
ring_simplify.
apply Zle_refl.
......@@ -198,7 +198,7 @@ apply Rmult_le_reg_l with 2%R.
now apply (Z2R_lt 0 2).
rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l.
apply Rle_trans with (bpow (-1)).
apply -> bpow_le.
apply bpow_le.
omega.
replace (2 * (-1 + 5 / 4))%R with (/2)%R by field.
apply Rinv_le.
......@@ -282,7 +282,7 @@ destruct (ln_beta beta (sqrt x)) as (es,Es).
specialize (Es H0).
apply Rle_trans with (bpow es).
now apply Rlt_le.
apply ->bpow_le.
apply bpow_le.
case (Zle_or_lt es (prec + Fexp fr)) ; trivial.
intros H1.
absurd (Rabs (F2R fr) < bpow (es - 1))%R.
......@@ -294,7 +294,8 @@ apply generic_format_bpow.
unfold FLX_exp; omega.
apply Es.
apply Rlt_le_trans with (1:=H).
apply ->bpow_le; omega.
apply bpow_le.
omega.
now apply Rlt_le.
Qed.
......
......@@ -33,7 +33,7 @@ Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exponent beta (FLX_exp prec)).
(** Auxiliary result that provides the exponent *)
Theorem mult_error_FLX_aux:
Lemma mult_error_FLX_aux:
forall rnd,
forall x y,
format x -> format y ->
......@@ -42,6 +42,7 @@ Theorem 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.
set (f := (round beta (FLX_exp prec) rnd (x * y))).
destruct (Req_dec (x * y) 0) as [Hxy0|Hxy0].
......@@ -70,7 +71,7 @@ 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 (lt_bpow beta).
apply Rle_lt_trans with (1 := proj1 Hexy).
rewrite Rabs_mult.
rewrite bpow_plus.
......@@ -86,7 +87,7 @@ 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 (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 Hexy).
rewrite Rabs_mult.
rewrite bpow_plus.
......@@ -126,7 +127,7 @@ 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.
apply bpow_le.
unfold canonic_exponent, FLX_exp.
rewrite ln_beta_unique with (1 := Hexy).
apply Zle_refl.
......@@ -151,8 +152,8 @@ apply generic_format_canonic_exponent; simpl.
simpl in H2; assumption.
Qed.
End Fprop_mult_error.
Section Fprop_mult_error_FLT.
Variable beta : radix.
......@@ -191,11 +192,11 @@ now apply FLX_generic_format_FLT with emin.
rewrite <- (FLT_round_FLX beta emin).
assumption.
apply Rle_trans with (2:=Hxy).
apply -> bpow_le.
apply bpow_le.
omega.
rewrite <- (FLT_round_FLX beta emin) in H1.
2:apply Rle_trans with (2:=Hxy).
2:apply -> bpow_le; omega.
2:apply bpow_le; omega.
unfold f; rewrite <- H1.
apply generic_format_canonic_exponent.
simpl in H2, H3.
......@@ -225,7 +226,7 @@ destruct (ln_beta beta y) as (ey,Ey) ; simpl.
specialize (Ey Hy0).
assert (emin + 2 * prec -1 < ex + ey)%Z.
2: omega.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rle_lt_trans with (1:=Hxy).
rewrite Rabs_mult, bpow_plus.
apply Rmult_le_0_lt_compat; try apply Rabs_pos.
......
......@@ -106,9 +106,9 @@ simpl.
specialize (He Hx').
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
rewrite <- bpow_plus.
apply -> bpow_le.
apply bpow_le.
assert (emin < ex)%Z.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
generalize (Hmin ex).
......@@ -177,12 +177,12 @@ destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He Hx').
assert (He': (emin < ex)%Z).
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
rewrite <- bpow_plus.
apply -> bpow_le.
apply bpow_le.
generalize (Hmin ex).
omega.
apply Rmult_le_compat_l.
......@@ -243,9 +243,9 @@ simpl.
specialize (He Hx').
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
rewrite <- bpow_plus.
apply -> bpow_le.
apply bpow_le.
assert (emin < ex)%Z.
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
generalize (Hmin ex).
......@@ -333,12 +333,12 @@ destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He Hx').
assert (He': (emin < ex)%Z).
apply <- bpow_lt.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
rewrite <- bpow_plus.
apply -> bpow_le.
apply bpow_le.
generalize (Hmin ex).
omega.
apply Rmult_le_compat_l.
......@@ -535,8 +535,7 @@ omega.
exact Hp.
Qed.
Theorem error_N_FLT_aux :
Lemma error_N_FLT_aux :
forall x,
(0 < x)%R ->
exists eps, exists eta,
......@@ -572,13 +571,14 @@ apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R.
apply ulp_half_error.
now apply FLT_exp_correct.
apply Rmult_le_compat_l; auto with real.
unfold ulp; apply ->bpow_le.
unfold ulp.
apply bpow_le.
unfold FLT_exp, canonic_exponent.
rewrite Zmax_right.
omega.
destruct (ln_beta beta x) as (e,He); simpl.
assert (e-1 < emin+prec)%Z.
apply <- (bpow_lt beta).
apply (lt_bpow beta).
apply Rle_lt_trans with (2:=Hx).
rewrite <- (Rabs_right x).
apply He; auto with real.
......@@ -587,7 +587,6 @@ omega.
split;ring.
Qed.
End Fprop_relative_FLT.
Section Fprop_relative_FLX.
......
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