From 4bb55b24d52b3580b8b875d5d35856befd852a24 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 23 Sep 2009 16:29:05 +0000 Subject: [PATCH] Removed absolute value from ln_beta. --- src/Flocq_Raux.v | 71 +++++++++++++++++++++---------- src/Flocq_rnd_FLT.v | 13 +++--- src/Flocq_rnd_FLX.v | 21 ++++------ src/Flocq_rnd_FTZ.v | 8 ++-- src/Flocq_rnd_generic.v | 92 ++++++++++++++++++++--------------------- src/Flocq_rnd_ne.v | 46 ++++++++++----------- src/Flocq_ulp.v | 14 +++---- 7 files changed, 141 insertions(+), 124 deletions(-) diff --git a/src/Flocq_Raux.v b/src/Flocq_Raux.v index 41c9096..60be379 100644 --- a/src/Flocq_Raux.v +++ b/src/Flocq_Raux.v @@ -655,7 +655,7 @@ Qed. Lemma ln_beta : forall x : R, - {e | (0 < x)%R -> (epow (e - 1)%Z <= x < epow e)%R}. + {e | (x <> 0)%R -> (epow (e - 1)%Z <= Rabs x < epow e)%R}. Proof. intros x. set (fact := ln (Z2R (radix_val r))). @@ -670,8 +670,11 @@ now apply Zlt_le_trans with (2 := radix_prop r). apply (Z2R_lt 0). now apply Zlt_le_trans with (2 := radix_prop r). (* . *) -exists (Zfloor (ln x / fact) + 1)%Z. -intros Hx. +exists (Zfloor (ln (Rabs x) / fact) + 1)%Z. +intros Hx'. +generalize (Rabs_pos_lt _ Hx'). clear Hx'. +generalize (Rabs x). clear x. +intros x Hx. rewrite 2!epow_exp. fold fact. pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)). @@ -723,16 +726,32 @@ Qed. Lemma ln_beta_unique : forall (x : R) (e : Z), - (epow (e - 1) <= x < epow e)%R -> + (epow (e - 1) <= Rabs x < epow e)%R -> projT1 (ln_beta x) = e. Proof. -intros x e1 Hx1. +intros x e1 He. +destruct (Req_dec x 0) as [Hx|Hx]. +elim Rle_not_lt with (1 := proj1 He). +rewrite Hx, Rabs_R0. +apply epow_gt_0. destruct (ln_beta x) as (e2, Hx2). -apply epow_unique with (2 := Hx1). simpl. -apply Hx2. -apply Rlt_le_trans with (2 := proj1 Hx1). -apply epow_gt_0. +apply epow_unique with (2 := He). +now apply Hx2. +Qed. + +Lemma ln_beta_opp : + forall x, + projT1 (ln_beta (-x)) = projT1 (ln_beta x). +Proof. +intros x. +destruct (Req_dec x 0) as [Hx|Hx]. +now rewrite Hx, Ropp_0. +destruct (ln_beta x) as (e, He). +simpl. +specialize (He Hx). +apply ln_beta_unique. +now rewrite Rabs_Ropp. Qed. Lemma ln_beta_monotone : @@ -745,10 +764,15 @@ destruct (ln_beta x) as (ex, Hx). destruct (ln_beta y) as (ey, Hy). simpl. apply epow_lt_epow. -specialize (Hx H0x). -specialize (Hy (Rlt_le_trans _ _ _ H0x Hxy)). +specialize (Hx (Rgt_not_eq _ _ H0x)). +specialize (Hy (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ H0x Hxy))). apply Rle_lt_trans with (1 := proj1 Hx). -now apply Rle_lt_trans with (2 := proj2 Hy). +apply Rle_lt_trans with (2 := proj2 Hy). +rewrite 2!Rabs_pos_eq. +exact Hxy. +apply Rle_trans with (2 := Hxy). +now apply Rlt_le. +now apply Rlt_le. Qed. Lemma Zpower_pos_gt_0 : @@ -792,31 +816,34 @@ Lemma Zln_beta : {e | (Zpower (radix_val r) (e - 1) <= Zabs x < Zpower (radix_val r) e)%Z}. Proof. intros x. -destruct (Z_le_lt_eq_dec 0 _ (Zabs_pos x)) as [Hx|Hx]. +destruct (Z_eq_dec x 0) as [Hx|Hx]. (* . *) -destruct (ln_beta (Z2R (Zabs x))) as (e, H). -specialize (H (Z2R_lt _ _ Hx)). +exists Z0. +rewrite Hx. +now split. +(* . *) +destruct (ln_beta (Z2R x)) as (e, H). +specialize (H (Z2R_neq _ _ Hx)). exists e. assert (He: (1 <= e)%Z). apply (Zlt_le_succ 0). apply <- epow_lt. apply Rle_lt_trans with (2 := proj2 H). +rewrite Rabs_Z2R. apply (Z2R_le 1). -now apply (Zlt_le_succ 0). +apply (Zlt_le_succ 0). +generalize (Zabs_spec x). +omega. (* . . *) split. apply le_Z2R. -rewrite Z2R_Zpower. +rewrite Z2R_Zpower, <- Rabs_Z2R. apply H. now apply Zle_minus_le_0. apply lt_Z2R. -rewrite Z2R_Zpower. +rewrite Z2R_Zpower, <- Rabs_Z2R. apply H. now apply Zle_succ_le. -(* . *) -exists Z0. -rewrite <- Hx. -now split. Qed. End pow. diff --git a/src/Flocq_rnd_FLT.v b/src/Flocq_rnd_FLT.v index 673bd98..af365d7 100644 --- a/src/Flocq_rnd_FLT.v +++ b/src/Flocq_rnd_FLT.v @@ -67,9 +67,9 @@ now apply Zlt_le_weak. apply Zle_refl. rewrite Hx1. eexists ; repeat split. -destruct (ln_beta beta (Rabs x)) as (ex, Hx4). +destruct (ln_beta beta x) as (ex, Hx4). simpl in Hx2. -specialize (Hx4 (Rabs_pos_lt x Hx3)). +specialize (Hx4 Hx3). apply lt_Z2R. rewrite Z2R_Zpower. apply Rmult_lt_reg_r with (bpow (ex - prec)). @@ -97,9 +97,9 @@ rewrite Hx4. apply generic_format_0. simpl in Hx2, Hx3. unfold generic_format, canonic, FLT_exp. -destruct (ln_beta beta (Rabs x)) as (ex, Hx5). +destruct (ln_beta beta x) as (ex, Hx5). simpl. -specialize (Hx5 (Rabs_pos_lt _ Hx4)). +specialize (Hx5 Hx4). destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ; rewrite H2 ; clear H2. rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2). @@ -143,7 +143,7 @@ rewrite Hx4. eexists ; repeat split. rewrite Hx5. clear Hx5. rewrite <- Hx4. -destruct (ln_beta beta (Rabs x)) as (ex, Hx5). +destruct (ln_beta beta x) as (ex, Hx5). unfold FLX_exp, FLT_exp. simpl. apply sym_eq. @@ -151,8 +151,7 @@ apply Zmax_left. cut (emin + prec <= ex)%Z. omega. apply epow_lt_epow with beta. apply Rle_lt_trans with (1 := Hx1). -apply Hx5. -now apply Rabs_pos_lt. +now apply Hx5. Qed. Theorem FLT_format_FIX : diff --git a/src/Flocq_rnd_FLX.v b/src/Flocq_rnd_FLX.v index 9d1809d..c3f1676 100644 --- a/src/Flocq_rnd_FLX.v +++ b/src/Flocq_rnd_FLX.v @@ -100,11 +100,11 @@ now apply Zlt_le_trans with (2 := radix_prop beta). now apply Zlt_le_weak. apply generic_format_0. (* . *) -destruct (ln_beta beta (Rabs x)) as (ex, Hx2). +destruct (ln_beta beta x) as (ex, Hx2). simpl. -specialize (Hx2 (Rabs_pos_lt _ Hx1)). +specialize (Hx2 Hx1). apply iff_trans with (generic_format beta (FIX_exp (ex - prec)) x). -assert (Hf: FLX_exp (projT1 (ln_beta beta (Rabs x))) = FIX_exp (ex - prec) (projT1 (ln_beta beta (Rabs x)))). +assert (Hf: FLX_exp (projT1 (ln_beta beta x)) = FIX_exp (ex - prec) (projT1 (ln_beta beta x))). unfold FIX_exp, FLX_exp. now rewrite ln_beta_unique with (1 := Hx2). split ; apply generic_format_fun_eq ; now rewrite Hf. @@ -149,18 +149,15 @@ intros H. elim H. rewrite H1, H3. apply Rmult_0_l. -destruct (ln_beta beta (Z2R (Zabs xm))) as (d,H4). -assert (H5: (0 < Z2R (Zabs xm))%R). -rewrite <- Rabs_Z2R. -apply Rabs_pos_lt. -now apply (Z2R_neq _ 0). -specialize (H4 H5). clear H5. +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 <- (epow_lt beta). -apply Rle_lt_trans with (Z2R (Zabs xm)). +apply Rle_lt_trans with (Rabs (Z2R xm)). apply H4. rewrite <- Z2R_Zpower. +rewrite Rabs_Z2R. now apply Z2R_lt. now apply Zlt_le_weak. exists (Float beta (xm * Zpower (radix_val beta) (prec - d)) (xe + d - prec)). @@ -183,7 +180,7 @@ rewrite Rabs_pos_eq. rewrite Rmult_assoc, <- epow_add. ring_simplify (prec - 1 + (d - prec))%Z. ring_simplify (prec - d + (d - prec))%Z. -now rewrite Rmult_1_r. +now rewrite Rmult_1_r, <- Rabs_Z2R. apply epow_ge_0. exact H5. omega. @@ -196,7 +193,7 @@ apply epow_gt_0. rewrite Rmult_assoc, <- 2!epow_add. ring_simplify (prec + (d - prec))%Z. ring_simplify (prec - d + (d - prec))%Z. -now rewrite Rmult_1_r. +now rewrite Rmult_1_r, <- Rabs_Z2R. apply epow_ge_0. now apply Zlt_le_weak. exact H5. diff --git a/src/Flocq_rnd_FTZ.v b/src/Flocq_rnd_FTZ.v index 29fa520..e54c669 100644 --- a/src/Flocq_rnd_FTZ.v +++ b/src/Flocq_rnd_FTZ.v @@ -63,9 +63,9 @@ split. intros H. now elim H. apply Zle_refl. -destruct (ln_beta beta (Rabs x)) as (ex, Hx4). +destruct (ln_beta beta x) as (ex, Hx4). simpl in Hx2. -specialize (Hx4 (Rabs_pos_lt x Hx3)). +specialize (Hx4 Hx3). unfold FTZ_exp in Hx2. generalize (Zlt_cases (ex - prec) emin) Hx2. clear Hx2. case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2. @@ -127,9 +127,9 @@ rewrite Hx4. apply generic_format_0. specialize (Hx2 Hx4). unfold generic_format, canonic, FTZ_exp. -destruct (ln_beta beta (Rabs x)) as (ex, Hx6). +destruct (ln_beta beta x) as (ex, Hx6). simpl. -specialize (Hx6 (Rabs_pos_lt _ Hx4)). +specialize (Hx6 Hx4). generalize (Zlt_cases (ex - prec) emin). case (Zlt_bool (ex - prec) emin) ; intros H1. elim (Rlt_not_ge _ _ (proj2 Hx6)). diff --git a/src/Flocq_rnd_generic.v b/src/Flocq_rnd_generic.v index 981ddfb..8787399 100644 --- a/src/Flocq_rnd_generic.v +++ b/src/Flocq_rnd_generic.v @@ -22,7 +22,7 @@ Definition valid_exp := Variable prop_exp : valid_exp. Definition canonic x (f : float beta) := - x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))). + x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta x)). Definition generic_format (x : R) := exists f : float beta, @@ -83,11 +83,10 @@ simpl. apply f_equal. apply sym_eq. apply ln_beta_unique. -rewrite Rabs_right. +rewrite Rabs_pos_eq. split. exact Hbl. now apply Rle_lt_trans with (2 := Hx2). -apply Rle_ge. apply Rle_trans with (2 := Hbl). apply epow_ge_0. split. @@ -142,10 +141,9 @@ intros g ((gm, ge), (Hg1, Hg2)) Hgx. apply Rnot_lt_le. intros Hg3. destruct (ln_beta beta g) as (ge', Hg4). -specialize (Hg4 Hg3). -generalize Hg4. intros Hg5. -rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in Hg5. -rewrite ln_beta_unique with (1 := Hg5) in Hg2. +simpl in Hg2. +specialize (Hg4 (Rgt_not_eq _ _ Hg3)). +rewrite Rabs_pos_eq in Hg4. apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)). apply Rle_trans with (bpow ge). apply -> epow_le. @@ -172,6 +170,7 @@ apply epow_gt_0. rewrite Rmult_0_l. unfold F2R in Hg1. simpl in Hg1. now rewrite <- Hg1. +now apply Rlt_le. (* - . . *) apply sym_eq. apply Zfloor_imp. @@ -296,9 +295,9 @@ apply Rnot_lt_le. intros Hg3. assert (Hg4 : (g < 0)%R). now apply Rle_lt_trans with (1 := Hgx). -destruct (ln_beta beta (Rabs g)) as (ge', Hge). +destruct (ln_beta beta g) as (ge', Hge). simpl in Hg2. -specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))). +specialize (Hge (Rlt_not_eq _ _ Hg4)). apply Rlt_not_le with (1 := Hg3). rewrite Hg1. unfold F2R. simpl. @@ -371,9 +370,9 @@ apply Rnot_lt_le. intros Hg3. assert (Hg4 : (g < 0)%R). now apply Rle_lt_trans with (1 := Hgx). -destruct (ln_beta beta (Rabs g)) as (ge', Hge). +destruct (ln_beta beta g) as (ge', Hge). simpl in Hg2. -specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))). +specialize (Hge (Rlt_not_eq g 0 Hg4)). rewrite (Rabs_left _ Hg4) in Hge. assert (Hge' : (ge' <= fexp ex)%Z). cut (ge' - 1 < fexp ex)%Z. omega. @@ -465,11 +464,20 @@ Theorem canonic_sym : canonic x (Float beta m e) -> canonic (-x) (Float beta (-m) e). Proof. -intros x m e (H1,H2). +intros x m e. +destruct (Req_dec x 0) as [Hx|Hx]. +(* . *) +rewrite Hx, Ropp_0. +intros (H1,H2). +split. +now rewrite <- opp_F2R, <- H1, Ropp_0. +exact H2. +(* . *) +intros (H1,H2). split. rewrite H1. apply opp_F2R. -now rewrite Rabs_Ropp. +now rewrite ln_beta_opp. Qed. Theorem generic_format_sym : @@ -489,39 +497,32 @@ exact generic_format_0. exact generic_format_sym. (* rounding down *) exists (fun x => - match total_order_T 0 x with - | inleft (left Hx) => + match Req_EM_T x 0 with + | left Hx => R0 + | right Hx => let e := fexp (projT1 (ln_beta beta x)) in F2R (Float beta (Zfloor (x * bpow (Zopp e))) e) - | inleft (right _) => R0 - | inright Hx => - let e := fexp (projT1 (ln_beta beta (-x))) in - F2R (Float beta (Zfloor (x * bpow (Zopp e))) e) end). intros x. -destruct (total_order_T 0 x) as [[Hx|Hx]|Hx]. -(* positive *) -destruct (ln_beta beta x) as (ex, Hx'). -simpl. -apply generic_DN_pt_pos. -now apply Hx'. -(* zero *) +destruct (Req_EM_T x 0) as [Hx|Hx]. +(* . *) split. -exists (Float beta 0 _) ; repeat split. -unfold F2R. simpl. -now rewrite Rmult_0_l. -rewrite <- Hx. +apply generic_format_0. +rewrite Hx. split. apply Rle_refl. -intros g _ H. -exact H. -(* negative *) -destruct (ln_beta beta (- x)) as (ex, Hx'). +now intros g _ H. +(* . *) +destruct (ln_beta beta x) as (ex, H1). simpl. +specialize (H1 Hx). +destruct (Rdichotomy _ _ Hx) as [H2|H2]. apply generic_DN_pt_neg. -apply Hx'. -rewrite <- Ropp_0. -now apply Ropp_lt_contravar. +now rewrite <- Rabs_left. +apply generic_DN_pt_pos. +rewrite Rabs_right in H1. +exact H1. +now apply Rgt_ge. Qed. Theorem generic_DN_pt_small_pos : @@ -542,9 +543,9 @@ apply epow_ge_0. intros g ((gm, ge), (Hg1, Hg2)) Hgx. apply Rnot_lt_le. intros Hg3. -destruct (ln_beta beta (Rabs g)) as (eg, Hg4). +destruct (ln_beta beta g) as (eg, Hg4). simpl in Hg2. -specialize (Hg4 (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))). +specialize (Hg4 (Rgt_not_eq g 0 Hg3)). rewrite Rabs_right in Hg4. apply Rle_not_lt with (1 := Hgx). rewrite Hg1. @@ -587,16 +588,15 @@ eexists ; repeat split. simpl. apply f_equal. apply sym_eq. -apply ln_beta_unique. rewrite <- H. +apply ln_beta_unique. split. replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring. apply RRle_abs. -rewrite Rabs_right. +rewrite Rabs_pos_eq. apply -> epow_lt. apply Zle_lt_succ. apply Zle_refl. -apply Rle_ge. apply epow_ge_0. split. (* . *) @@ -610,9 +610,9 @@ apply Rgt_not_eq. apply Rlt_le_trans with (2 := Hgx). apply Rlt_le_trans with (2 := proj1 Hx). apply epow_gt_0. -destruct (ln_beta beta (Rabs g)) as (eg, Hg3). +destruct (ln_beta beta g) as (eg, Hg3). simpl in Hg2. -specialize (Hg3 (Rabs_pos_lt g H0)). +specialize (Hg3 H0). apply Rnot_lt_le. intros Hgp. apply Rlt_not_le with (1 := Hgp). @@ -702,7 +702,7 @@ End RND_generic. Theorem canonic_fun_eq : forall beta : radix, forall f1 f2 : Z -> Z, forall x f, - f1 (projT1 (ln_beta beta (Rabs x))) = f2 (projT1 (ln_beta beta (Rabs x))) -> + f1 (projT1 (ln_beta beta x)) = f2 (projT1 (ln_beta beta x)) -> canonic beta f1 x f -> canonic beta f2 x f. Proof. intros beta f1 f2 x f Hf (Hx1,Hx2). @@ -713,7 +713,7 @@ Qed. Theorem generic_format_fun_eq : forall beta : radix, forall f1 f2 : Z -> Z, forall x, - f1 (projT1 (ln_beta beta (Rabs x))) = f2 (projT1 (ln_beta beta (Rabs x))) -> + f1 (projT1 (ln_beta beta x)) = f2 (projT1 (ln_beta beta x)) -> generic_format beta f1 x -> generic_format beta f2 x. Proof. intros beta f1 f2 x Hf (f,Hx). diff --git a/src/Flocq_rnd_ne.v b/src/Flocq_rnd_ne.v index d1e5937..ce18006 100644 --- a/src/Flocq_rnd_ne.v +++ b/src/Flocq_rnd_ne.v @@ -50,7 +50,7 @@ exists (Float beta (-m) e). repeat split. now rewrite <- opp_F2R, <- H2, Ropp_involutive. simpl in H3 |- *. -now rewrite H3, Rabs_Ropp. +now rewrite <- ln_beta_opp. simpl in H4 |- *. rewrite Zopp_eq_mult_neg_1. now apply Zeven_mult_Zeven_l. @@ -80,13 +80,13 @@ Lemma canonic_imp_Fnum : forall x, forall f : float beta, x <> R0 -> canonic x f -> - (Zabs (Fnum f) < Zpower (radix_val beta) (projT1 (ln_beta beta (Rabs x)) - Fexp f))%Z. + (Zabs (Fnum f) < Zpower (radix_val beta) (projT1 (ln_beta beta x) - Fexp f))%Z. Proof. intros x f Hx. unfold Flocq_rnd_generic.canonic. -destruct (ln_beta beta (Rabs x)) as (ex, H). +destruct (ln_beta beta x) as (ex, H). simpl. -specialize (H (Rabs_pos_lt x Hx)). +specialize (H Hx). intros (H1, H2). destruct (Zle_or_lt (Fexp f) ex) as [He|He]. (* . *) @@ -380,8 +380,10 @@ Theorem DN_UP_parity_FLX_pos : False. Proof. intros x xd xu cd cu H0x Hfx (Hd1,Hd2) (Hu1,Hu2) Hxd Hxu Hed Heu. -destruct (ln_beta beta x) as (ex, Hex). -specialize (Hex H0x). +destruct (ln_beta beta x) as (ex, Hexa). +specialize (Hexa (Rgt_not_eq _ _ H0x)). +generalize Hexa. intros Hex. +rewrite (Rabs_pos_eq _ (Rlt_le _ _ H0x)) in Hex. assert (Hd4: (bpow (ex - 1) <= Rabs xd < bpow ex)%R). rewrite Rabs_pos_eq. split. @@ -431,9 +433,9 @@ apply Zle_minus_le_0. now apply (Zlt_le_succ 0). simpl. rewrite <- Hu. -rewrite Rabs_pos_eq. rewrite ln_beta_unique with beta (bpow ex) (ex + 1)%Z. unfold FLX_exp. ring. +rewrite Rabs_pos_eq. split. replace (ex + 1 - 1)%Z with ex by ring. apply Rle_refl. @@ -453,16 +455,15 @@ rewrite Z2R_Zpower, <- epow_add. ring_simplify (prec + (ex - prec))%Z. rewrite Hu, Hud. unfold ulp. +rewrite ln_beta_unique with beta x ex. +unfold FLX_exp, F2R. +simpl. ring. rewrite Rabs_pos_eq. -rewrite ln_beta_unique with (1 := Hex). -unfold FLX_exp. -unfold F2R. simpl. ring. +exact Hex. now apply Rlt_le. now apply Zlt_le_weak. simpl. -rewrite ln_beta_unique with beta (Rabs xd) ex. -apply refl_equal. -exact Hd4. +now rewrite ln_beta_unique with (1 := Hd4). rewrite Hd3 in Hed. simpl in Hed. rewrite Hu3 in Heu. simpl in Heu. clear -Hp Hed Heu. @@ -500,9 +501,9 @@ generalize (ulp_pred_succ_pt beta FLXf (FLX_exp_correct prec Hp) x xd xu Hfx Hxd rewrite Hd1, Hu1. unfold ulp, F2R. rewrite Hd2, Hu2. -rewrite (ln_beta_unique beta (Rabs xu) ex). -rewrite (ln_beta_unique beta (Rabs xd) ex). -rewrite (ln_beta_unique beta (Rabs x) ex). +rewrite ln_beta_unique with beta xu ex. +rewrite ln_beta_unique with (1 := Hd4). +rewrite ln_beta_unique with (1 := Hexa). simpl. rewrite <- Rmult_plus_distr_r. intros H. @@ -518,10 +519,6 @@ exact H. apply Rgt_not_eq. apply epow_gt_0. rewrite Rabs_pos_eq. -exact Hex. -now apply Rlt_le. -exact Hd4. -rewrite Rabs_pos_eq. split. apply Rle_trans with (1 := proj1 Hex). apply Hxu. @@ -554,21 +551,20 @@ Variable Hp : Zlt 0 prec. Notation FLTf := (FLT_exp emin prec). Theorem FIX_FLT_exp_subnormal : - forall x, (x <> 0)%R -> + forall x, x <> R0 -> (Rabs x < bpow (emin + prec))%R -> - FIX_exp emin (projT1 (ln_beta beta (Rabs x))) = FLTf (projT1 (ln_beta beta (Rabs x))). + FIX_exp emin (projT1 (ln_beta beta x)) = FLTf (projT1 (ln_beta beta x)). Proof. intros x Hx0 Hx. unfold FIX_exp, FLT_exp. rewrite Zmax_right. apply refl_equal. -destruct (ln_beta beta (Rabs x)) as (ex, Hex). +destruct (ln_beta beta x) as (ex, Hex). simpl. cut (ex - 1 < emin + prec)%Z. omega. apply <- epow_lt. eapply Rle_lt_trans with (2 := Hx). -apply Hex. -now apply Rabs_pos_lt. +now apply Hex. Qed. Theorem DN_UP_parity_FLT_pos : diff --git a/src/Flocq_ulp.v b/src/Flocq_ulp.v index 43149c2..0349b10 100644 --- a/src/Flocq_ulp.v +++ b/src/Flocq_ulp.v @@ -15,7 +15,7 @@ Variable fexp : Z -> Z. Variable prop_exp : valid_exp fexp. -Definition ulp x := F2R (Float beta 1 (fexp (projT1 (ln_beta beta (Rabs x))))). +Definition ulp x := F2R (Float beta 1 (fexp (projT1 (ln_beta beta x)))). Definition F := generic_format beta fexp. @@ -27,10 +27,10 @@ Theorem ulp_pred_succ_pt_pos : Proof. intros x xd xu Hx1 Fx Hd1 Hu1. unfold ulp. -rewrite Rabs_pos_eq. destruct (ln_beta beta x) as (ex, Hx2). simpl. -specialize (Hx2 Hx1). +specialize (Hx2 (Rgt_not_eq _ _ Hx1)). +rewrite Rabs_pos_eq in Hx2. destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1]. (* positive big *) assert (Hd2 := generic_DN_pt_pos _ _ prop_exp _ _ Hx2). @@ -95,7 +95,7 @@ now rewrite 2!Ropp_involutive. rewrite <- (Ropp_involutive xd). rewrite ulp_pred_succ_pt_pos with (3 := Hu2) (4 := Hd2). unfold ulp. -rewrite Rabs_Ropp. +rewrite ln_beta_opp. ring. rewrite <- Ropp_0. now apply Ropp_lt_contravar. @@ -106,7 +106,7 @@ split. rewrite <- opp_F2R. rewrite <- H1. now rewrite Ropp_involutive. -now rewrite <- Rabs_Ropp. +now rewrite <- ln_beta_opp. (* positive *) now apply ulp_pred_succ_pt_pos. Qed. @@ -247,16 +247,14 @@ unfold F2R. simpl. rewrite 2!Rmult_1_l. apply -> epow_le. apply Hm. -rewrite 2!Rabs_pos_eq ; try apply Rlt_le ; trivial. now apply ln_beta_monotone. -now apply Rlt_le_trans with x. Qed. Theorem ulp_epow : forall e, ulp (bpow e) = bpow (fexp (e + 1)). intros e. unfold ulp. -rewrite (ln_beta_unique beta (Rabs (bpow e)) (e + 1)). +rewrite (ln_beta_unique beta (bpow e) (e + 1)). unfold F2R. now rewrite Rmult_1_l. rewrite Rabs_pos_eq. -- GitLab