diff --git a/src/Appli/Fappli_Axpy.v b/src/Appli/Fappli_Axpy.v index 5a19bfdc33d1c2b800eaa49973a6d09d3bf993c3..bf1d1289823b2aaeeca00b7d073d798769cdba38 100644 --- a/src/Appli/Fappli_Axpy.v +++ b/src/Appli/Fappli_Axpy.v @@ -15,17 +15,17 @@ Notation cexp := (canonic_exponent beta (FLX_exp prec)). Notation ulp := (ulp beta (FLX_exp prec)). Definition MinOrMax x f := - ((f = rounding beta (FLX_exp prec) ZrndDN x) - \/ (f = rounding beta (FLX_exp prec) ZrndUP x)). + ((f = round beta (FLX_exp prec) rndDN x) + \/ (f = round beta (FLX_exp prec) rndUP x)). Theorem MinOrMax_opp: forall x f, MinOrMax x f <-> MinOrMax (-x) (-f). assert (forall x f, MinOrMax x f -> MinOrMax (- x) (- f)). unfold MinOrMax; intros x f [H|H]. right. -now rewrite H, rounding_UP_opp. +now rewrite H, round_UP_opp. left. -now rewrite H, rounding_DN_opp. +now rewrite H, round_DN_opp. intros x f; split; intros H1. now apply H. rewrite <- (Ropp_involutive x), <- (Ropp_involutive f). @@ -37,11 +37,11 @@ Theorem implies_DN_lt_ulp: forall x f, format f -> (0 < f <= x)%R -> (Rabs (f-x) < ulp f)%R -> - (f = rounding beta (FLX_exp prec) ZrndDN x)%R. + (f = round beta (FLX_exp prec) rndDN x)%R. intros x f Hf Hxf1 Hxf2. apply sym_eq. replace x with (f+-(f-x))%R by ring. -apply rounding_DN_succ; trivial. +apply round_DN_succ; trivial. apply Hxf1. replace (- (f - x))%R with (Rabs (f-x)). split; trivial; apply Rabs_pos. @@ -66,7 +66,7 @@ right; apply sym_eq. replace f with ((f-ulp f) + (ulp (f-ulp f)))%R. 2: rewrite H; ring. replace x with ((f-ulp f)+-(f-ulp f-x))%R by ring. -apply rounding_UP_succ; trivial. +apply round_UP_succ; trivial. apply Hxf1. replace (- (f - x))%R with (Rabs (f-x)). @@ -104,8 +104,8 @@ Hypothesis Ha: format a. Hypothesis Hx: format x. Hypothesis Hy: format y. -Notation t := (rounding beta (FLX_exp prec) (ZrndN choice) (a*x)). -Notation u := (rounding beta (FLX_exp prec) (ZrndN choice) (t+y)). +Notation t := (round beta (FLX_exp prec) (rndN choice) (a*x)). +Notation u := (round beta (FLX_exp prec) (rndN choice) (t+y)). diff --git a/src/Calc/Fcalc_bracket.v b/src/Calc/Fcalc_bracket.v index 513189bea6ae2c5120a1d69e40c5a49e7999082f..4d1ffc89b3ea21aabbc7492572dc7decdf2fa483 100644 --- a/src/Calc/Fcalc_bracket.v +++ b/src/Calc/Fcalc_bracket.v @@ -161,7 +161,7 @@ apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_not_Lt. change 2%R with (Z2R 2). -rewrite <- mult_Z2R. +rewrite <- Z2R_mult. apply Z2R_le. omega. exact Hstep. @@ -183,7 +183,7 @@ apply Rcompare_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_Lt. change 2%R with (Z2R 2). -rewrite <- mult_Z2R. +rewrite <- Z2R_mult. apply Z2R_lt. omega. exact Hstep. @@ -228,7 +228,7 @@ Lemma middle_odd : Proof. intros k Hk. rewrite <- Hk. -rewrite 2!plus_Z2R, mult_Z2R. +rewrite 2!Z2R_plus, Z2R_mult. simpl. field. Qed. @@ -259,7 +259,7 @@ rewrite Hl. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. apply Rcompare_Lt. change 2%R with (Z2R 2). -rewrite <- mult_Z2R. +rewrite <- Z2R_mult. apply Z2R_lt. rewrite <- Hk. apply Zlt_succ. @@ -282,7 +282,7 @@ apply Rle_lt_trans with (2 := proj1 Hx'). apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. change 2%R with (Z2R 2). -rewrite <- mult_Z2R. +rewrite <- Z2R_mult. apply Rcompare_not_Lt. apply Z2R_le. rewrite Hk. @@ -301,7 +301,7 @@ apply inbetween_step_not_Eq with (1 := Hx). omega. apply Rcompare_Eq. inversion_clear Hx as [Hx'|]. -rewrite Hx', <- Hk, mult_Z2R. +rewrite Hx', <- Hk, Z2R_mult. simpl (Z2R 2). field. Qed. @@ -524,12 +524,12 @@ now apply Zpower_gt_0. rewrite 2!Hr. rewrite Zmult_plus_distr_l, Zmult_1_l. unfold F2R at 2. simpl. -rewrite plus_Z2R, Rmult_plus_distr_r. +rewrite Z2R_plus, Rmult_plus_distr_r. apply new_location_correct. apply bpow_gt_0. now apply Zpower_gt_1. now apply Z_mod_lt. -rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_Z2R. +rewrite <- 2!Rmult_plus_distr_r, <- 2!Z2R_plus. rewrite Zmult_comm, Zplus_assoc. now rewrite <- Z_div_mod_eq. Qed. @@ -545,16 +545,16 @@ now apply inbetween_float_new_location. apply Zmult_1_r. Qed. -Theorem inbetween_float_rounding : +Theorem inbetween_float_round : forall rnd choice, ( forall x m l, inbetween_int m x l -> Zrnd rnd x = choice m l ) -> forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> - rounding beta fexp rnd x = F2R (Float beta (choice m l) e). + round beta fexp rnd x = F2R (Float beta (choice m l) e). Proof. intros rnd choice Hc x m l e Hl. -unfold rounding, F2R. simpl. +unfold round, F2R. simpl. apply (f_equal (fun m => (Z2R m * bpow e)%R)). apply Hc. apply inbetween_mult_reg with (bpow e). @@ -566,9 +566,9 @@ Theorem inbetween_float_DN : forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> - rounding beta fexp ZrndDN x = F2R (Float beta m e). + round beta fexp rndDN x = F2R (Float beta m e). Proof. -apply inbetween_float_rounding with (choice := fun m l => m). +apply inbetween_float_round with (choice := fun m l => m). intros x m l Hl. refine (Zfloor_imp m _ _). apply inbetween_bounds with (2 := Hl). @@ -588,9 +588,9 @@ Theorem inbetween_float_UP : forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> - rounding beta fexp ZrndUP x = F2R (Float beta (cond_incr (round_UP l) m) e). + round beta fexp rndUP x = F2R (Float beta (cond_incr (round_UP l) m) e). Proof. -apply inbetween_float_rounding with (choice := fun m l => cond_incr (round_UP l) m). +apply inbetween_float_round with (choice := fun m l => cond_incr (round_UP l) m). intros x m l Hl. assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)). case l ; try (now left) ; now right ; split. @@ -621,16 +621,16 @@ Theorem inbetween_float_NE : forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> - rounding beta fexp ZrndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e). + round beta fexp rndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e). Proof. -apply inbetween_float_rounding with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m). +apply inbetween_float_round with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m). intros x m l Hl. inversion_clear Hl as [Hx|l' Hx Hl']. (* Exact *) rewrite Hx. now rewrite Zrnd_Z2R. (* not Exact *) -unfold Zrnd, ZrndNE, ZrndN, Znearest. +unfold Zrnd, rndNE, rndN, Znearest. assert (Hm: Zfloor x = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). @@ -639,7 +639,7 @@ rewrite Hm. replace (Rcompare (x - Z2R m) (/2)) with l'. now case l'. rewrite <- Hl'. -rewrite plus_Z2R. +rewrite Z2R_plus. rewrite <- (Rcompare_plus_r (- Z2R m) x). apply f_equal. simpl (Z2R 1). diff --git a/src/Calc/Fcalc_digits.v b/src/Calc/Fcalc_digits.v index 45e223bdd91289ea3291372e8abdffcd43ba4bd0..a5de75381a0aafd0bca9fd8cb7493be7b61dd1cd 100644 --- a/src/Calc/Fcalc_digits.v +++ b/src/Calc/Fcalc_digits.v @@ -100,7 +100,7 @@ intros n Hn. destruct (ln_beta beta (Z2R n)) as (e, He). simpl. specialize (He (Z2R_neq _ _ Hn)). -rewrite <- abs_Z2R in He. +rewrite <- Z2R_abs in He. assert (Hn': (0 < Zabs n)%Z). destruct n ; try easy. now elim Hn. @@ -174,7 +174,7 @@ apply <- bpow_le. apply Rlt_le. apply Rle_lt_trans with (Rabs (Z2R n)). simpl. -rewrite <- abs_Z2R. +rewrite <- Z2R_abs. apply (Z2R_le 1). apply (Zlt_le_succ 0). revert H. @@ -192,7 +192,7 @@ Theorem digits_shift : Proof. intros m e Hm He. rewrite 2!digits_ln_beta. -rewrite mult_Z2R. +rewrite Z2R_mult. rewrite Z2R_Zpower with (1 := He). change (Z2R m * bpow e)%R with (F2R (Float beta m e)). apply ln_beta_F2R. @@ -281,11 +281,11 @@ apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R. apply Rle_lt_trans with (Z2R (x + y + x * y)). rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Hxy)). apply Hexy. -rewrite <- mult_Z2R. +rewrite <- Z2R_mult. apply Z2R_lt. apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z. now ring_simplify. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat ; try (apply (Z2R_le 0) ; omega). rewrite <- (Rmult_1_r (Z2R (x + 1))). change (F2R (Float beta (x + 1) 0) <= bpow ex)%R. diff --git a/src/Calc/Fcalc_div.v b/src/Calc/Fcalc_div.v index c4d0f27e6d291ca42f780fdcd216a4bf69b219e0..f12b0c1f5ba476037c579d1ce14c699b26380ecf 100644 --- a/src/Calc/Fcalc_div.v +++ b/src/Calc/Fcalc_div.v @@ -110,8 +110,8 @@ omega. now apply Zlt_le_weak. (* . the location is correctly computed *) unfold inbetween_float, F2R. simpl. -rewrite bpow_add, plus_Z2R. -rewrite Hq, plus_Z2R, mult_Z2R. +rewrite bpow_plus, Z2R_plus. +rewrite Hq, Z2R_plus, Z2R_mult. replace ((Z2R m2 * Z2R q + Z2R r) * (bpow e' * bpow e2) / (Z2R m2 * bpow e2))%R with ((Z2R q + Z2R r / Z2R m2) * bpow e')%R. apply inbetween_mult_compat. diff --git a/src/Calc/Fcalc_ops.v b/src/Calc/Fcalc_ops.v index 9669b83eb0351a2c0b867628a6482ddaaba84e05..bea0948ec063428c3ec751a873fdbd9d8eacc560 100644 --- a/src/Calc/Fcalc_ops.v +++ b/src/Calc/Fcalc_ops.v @@ -49,7 +49,7 @@ Theorem Fopp_F2R : forall f1 : float beta, (F2R (Fopp f1) = -F2R f1)%R. unfold Fopp, F2R; intros (m1,e1). -simpl; rewrite opp_Z2R; ring. +simpl; rewrite Z2R_opp; ring. Qed. Definition Fabs (f1: float beta) := @@ -78,7 +78,7 @@ destruct (Falign f1 f2) as ((m1, m2), e). intros (H1, H2). rewrite H1, H2. unfold F2R. simpl. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Rmult_plus_distr_r. Qed. @@ -115,7 +115,7 @@ Theorem mult_F2R : Proof. intros (m1, e1) (m2, e2). unfold Fmult, F2R. simpl. -rewrite mult_Z2R, bpow_add. +rewrite Z2R_mult, bpow_plus. ring. Qed. diff --git a/src/Calc/Fcalc_round.v b/src/Calc/Fcalc_round.v index c8e4715c5d97c6cf1de2814fb3046efe5e057cda..681a8568c8f245719c6be2b5cd5a4b0359789dad 100644 --- a/src/Calc/Fcalc_round.v +++ b/src/Calc/Fcalc_round.v @@ -150,20 +150,20 @@ Qed. Section round_dir. -Variable rnd: Zrounding. +Variable rnd: Zround. Variable choice : Z -> location -> Z. Hypothesis choice_valid : forall m, choice m loc_Exact = m. Hypothesis inbetween_float_valid : forall x m l, let e := canonic_exponent beta fexp x in inbetween_float beta m e x l -> - rounding beta fexp rnd x = F2R (Float beta (choice m l) e). + round beta fexp rnd x = F2R (Float beta (choice m l) e). Theorem round_any_correct : forall x m e l, inbetween_float beta m e x l -> (e = canonic_exponent beta fexp x \/ (l = loc_Exact /\ format x)) -> - rounding beta fexp rnd x = F2R (Float beta (choice m l) e). + round beta fexp rnd x = F2R (Float beta (choice m l) e). Proof. intros x m e l Hin [He|(Hl,Hf)]. rewrite He in Hin |- *. @@ -172,7 +172,7 @@ rewrite Hl in Hin. inversion_clear Hin. rewrite Hl, choice_valid. rewrite <- H. -now apply rounding_generic. +now apply round_generic. Qed. Theorem round_trunc_any_correct : @@ -180,7 +180,7 @@ Theorem round_trunc_any_correct : (0 <= x)%R -> inbetween_float beta m e x l -> (e <= fexp (digits beta m + e))%Z \/ l = loc_Exact -> - rounding beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (choice m' l') e'). + round beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (choice m' l') e'). Proof. intros x m e l Hx Hl He. generalize (truncate_correct x m e l Hx Hl He). diff --git a/src/Calc/Fcalc_sqrt.v b/src/Calc/Fcalc_sqrt.v index fd3824d6d8f3098717604d0bcf36d12d3e512b39..5a8a782ce9a9b3ecc9b789cd6f1c636a8dbee9a6 100644 --- a/src/Calc/Fcalc_sqrt.v +++ b/src/Calc/Fcalc_sqrt.v @@ -223,7 +223,7 @@ replace (digits beta q * 2)%Z with (digits beta q + digits beta q)%Z by ring. apply digits_mult_strong. omega. omega. -(* . rounding *) +(* . round *) unfold inbetween_float, F2R. simpl. rewrite sqrt_mult. 2: now apply (Z2R_le 0) ; apply Zlt_le_weak. @@ -233,7 +233,7 @@ rewrite He1, Zplus_0_r in Hev. clear He1. rewrite Hev. replace (Zdiv2 (2 * e2)) with e2 by now case e2. replace (2 * e2)%Z with (e2 + e2)%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. fold (Rsqr (bpow e2)). rewrite sqrt_Rsqr. 2: apply Rlt_le ; apply bpow_gt_0. @@ -242,7 +242,7 @@ apply bpow_gt_0. rewrite Hq. case Zeq_bool_spec ; intros Hr'. (* .. r = 0 *) -rewrite Hr', Zplus_0_r, mult_Z2R. +rewrite Hr', Zplus_0_r, Z2R_mult. fold (Rsqr (Z2R q)). rewrite sqrt_Rsqr. now constructor. @@ -253,14 +253,14 @@ constructor. split. (* ... bounds *) apply Rle_lt_trans with (sqrt (Z2R (q * q))). -rewrite mult_Z2R. +rewrite Z2R_mult. fold (Rsqr (Z2R q)). rewrite sqrt_Rsqr. apply Rle_refl. apply (Z2R_le 0). omega. apply sqrt_lt_1. -rewrite mult_Z2R. +rewrite Z2R_mult. apply Rle_0_sqr. rewrite <- Hq. apply (Z2R_le 0). @@ -272,12 +272,12 @@ apply sqrt_lt_1. rewrite <- Hq. apply (Z2R_le 0). now apply Zlt_le_weak. -rewrite mult_Z2R. +rewrite Z2R_mult. apply Rle_0_sqr. apply Z2R_lt. ring_simplify. omega. -rewrite mult_Z2R. +rewrite Z2R_mult. fold (Rsqr (Z2R (q + 1))). rewrite sqrt_Rsqr. apply Rle_refl. @@ -290,7 +290,7 @@ replace ((2 * sqrt (Z2R (q * q + r))) * (2 * sqrt (Z2R (q * q + r))))%R with (4 * Rsqr (sqrt (Z2R (q * q + r))))%R by (unfold Rsqr ; ring). rewrite Rsqr_sqrt. change 4%R with (Z2R 4). -rewrite <- plus_Z2R, <- 2!mult_Z2R. +rewrite <- Z2R_plus, <- 2!Z2R_mult. rewrite Rcompare_Z2R. replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ring. generalize (Zle_cases r q). @@ -305,7 +305,7 @@ now apply Zlt_le_weak. apply Rmult_le_pos. now apply (Z2R_le 0 2). apply sqrt_ge_0. -rewrite <- plus_Z2R. +rewrite <- Z2R_plus. apply (Z2R_le 0). omega. Qed. diff --git a/src/Core/Fcore_FIX.v b/src/Core/Fcore_FIX.v index df880b0a25d577af6fc821819cad252d254f9cf7..d77f00d2315f2788ddd2e59669929dfdd5bc9809 100644 --- a/src/Core/Fcore_FIX.v +++ b/src/Core/Fcore_FIX.v @@ -58,9 +58,9 @@ exact FIX_exp_correct. Qed. Theorem Rnd_NE_pt_FIX : - rounding_pred (Rnd_NE_pt beta FIX_exp). + round_pred (Rnd_NE_pt beta FIX_exp). Proof. -apply Rnd_NE_pt_rounding. +apply Rnd_NE_pt_round. apply FIX_exp_correct. right. split ; easy. diff --git a/src/Core/Fcore_FLT.v b/src/Core/Fcore_FLT.v index c74afcabffb5bd7248aeb734e8114ca88f245bbf..ea112eac7595272083cf28863ca20ac9195c7725 100644 --- a/src/Core/Fcore_FLT.v +++ b/src/Core/Fcore_FLT.v @@ -84,7 +84,7 @@ apply lt_Z2R. rewrite Z2R_Zpower. 2: now apply Zlt_le_weak. apply Rmult_lt_reg_r with (bpow ex). apply bpow_gt_0. -rewrite <- bpow_add. +rewrite <- bpow_plus. change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R. rewrite <- abs_F2R. rewrite <- Hx. @@ -170,11 +170,11 @@ now apply FLX_format_generic. Qed. -Theorem FLT_rounding_FLX : forall rnd x, +Theorem FLT_round_FLX : forall rnd x, (bpow (emin + prec - 1) <= Rabs x)%R -> - rounding beta FLT_exp rnd x = rounding beta (FLX_exp prec) rnd x. + round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x. intros rnd x Hx. -unfold rounding, scaled_mantissa. +unfold round, scaled_mantissa. rewrite ->FLT_canonic_FLX; trivial. intros H; contradict Hx. rewrite H, Rabs_R0; apply Rlt_not_le. @@ -278,7 +278,7 @@ Qed. Theorem generic_NE_pt_FLT : forall x, - Rnd_NE_pt beta FLT_exp x (rounding beta FLT_exp ZrndNE x). + Rnd_NE_pt beta FLT_exp x (round beta FLT_exp rndNE x). Proof. intros x. apply generic_NE_pt. @@ -287,9 +287,9 @@ apply NE_ex_prop_FLT. Qed. Theorem Rnd_NE_pt_FLT : - rounding_pred (Rnd_NE_pt beta FLT_exp). + round_pred (Rnd_NE_pt beta FLT_exp). Proof. -apply Rnd_NE_pt_rounding. +apply Rnd_NE_pt_round. apply FLT_exp_correct. apply NE_ex_prop_FLT. Qed. diff --git a/src/Core/Fcore_FLX.v b/src/Core/Fcore_FLX.v index 99ef91de45a286ecad6076da72149798dcf5c8e0..7869988ba13011c5b17d3952d557ed7cba8cf7e1 100644 --- a/src/Core/Fcore_FLX.v +++ b/src/Core/Fcore_FLX.v @@ -54,7 +54,7 @@ eexists ; repeat split. apply lt_Z2R. apply Rmult_lt_reg_r with (bpow (e - prec)). apply bpow_gt_0. -rewrite Z2R_Zpower, <- bpow_add. +rewrite Z2R_Zpower, <- bpow_plus. ring_simplify (prec + (e - prec))%Z. rewrite <- H2. simpl. @@ -156,14 +156,14 @@ cut (d - 1 < prec)%Z. omega. apply <- (bpow_lt beta). apply Rle_lt_trans with (Rabs (Z2R xm)). apply H4. -rewrite <- Z2R_Zpower, <- abs_Z2R. +rewrite <- Z2R_Zpower, <- Z2R_abs. now apply Z2R_lt. now apply Zlt_le_weak. exists (Float beta (xm * Zpower beta (prec - d)) (xe + d - prec)). split. unfold F2R. simpl. -rewrite mult_Z2R, Z2R_Zpower. -rewrite Rmult_assoc, <- bpow_add. +rewrite Z2R_mult, Z2R_Zpower. +rewrite Rmult_assoc, <- bpow_plus. rewrite H1. now ring_simplify (prec - d + (xe + d - prec))%Z. exact H5. @@ -172,27 +172,27 @@ split. apply le_Z2R. apply Rmult_le_reg_r with (bpow (d - prec)). apply bpow_gt_0. -rewrite abs_Z2R, mult_Z2R, Rabs_mult, 2!Z2R_Zpower. -rewrite <- bpow_add. -rewrite <- abs_Z2R. +rewrite Z2R_abs, Z2R_mult, Rabs_mult, 2!Z2R_Zpower. +rewrite <- bpow_plus. +rewrite <- Z2R_abs. rewrite Rabs_pos_eq. -rewrite Rmult_assoc, <- bpow_add. +rewrite Rmult_assoc, <- bpow_plus. ring_simplify (prec - 1 + (d - prec))%Z. ring_simplify (prec - d + (d - prec))%Z. -now rewrite Rmult_1_r, abs_Z2R. +now rewrite Rmult_1_r, Z2R_abs. apply bpow_ge_0. exact H5. omega. apply lt_Z2R. -rewrite abs_Z2R, mult_Z2R, Rabs_mult. +rewrite Z2R_abs, Z2R_mult, Rabs_mult. rewrite 2!Z2R_Zpower. -rewrite <- abs_Z2R, Rabs_pos_eq. +rewrite <- Z2R_abs, Rabs_pos_eq. apply Rmult_lt_reg_r with (bpow (d - prec)). apply bpow_gt_0. -rewrite Rmult_assoc, <- 2!bpow_add. +rewrite Rmult_assoc, <- 2!bpow_plus. ring_simplify (prec + (d - prec))%Z. ring_simplify (prec - d + (d - prec))%Z. -now rewrite Rmult_1_r, abs_Z2R. +now rewrite Rmult_1_r, Z2R_abs. apply bpow_ge_0. now apply Zlt_le_weak. exact H5. @@ -242,7 +242,7 @@ Qed. Theorem generic_NE_pt_FLX : forall x, - Rnd_NE_pt beta FLX_exp x (rounding beta FLX_exp ZrndNE x). + Rnd_NE_pt beta FLX_exp x (round beta FLX_exp rndNE x). Proof. intros x. apply generic_NE_pt. @@ -251,9 +251,9 @@ apply NE_ex_prop_FLX. Qed. Theorem Rnd_NE_pt_FLX : - rounding_pred (Rnd_NE_pt beta FLX_exp). + round_pred (Rnd_NE_pt beta FLX_exp). Proof. -apply Rnd_NE_pt_rounding. +apply Rnd_NE_pt_round. apply FLX_exp_correct. apply NE_ex_prop_FLX. Qed. diff --git a/src/Core/Fcore_FTZ.v b/src/Core/Fcore_FTZ.v index ead1790179153cc527c66cdc15a0498d07d618e0..58bcc8bb85c3a0d433e2cc8b786ed3eb79ff46a5 100644 --- a/src/Core/Fcore_FTZ.v +++ b/src/Core/Fcore_FTZ.v @@ -69,7 +69,7 @@ generalize (Zlt_cases (ex - prec) emin). 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_add. +rewrite <- bpow_plus. apply -> bpow_le. omega. rewrite Hx1, abs_F2R. @@ -132,7 +132,7 @@ apply le_Z2R. rewrite Z2R_Zpower. apply Rmult_le_reg_r with (bpow (ex - prec)). apply bpow_gt_0. -rewrite <- bpow_add. +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. @@ -143,7 +143,7 @@ apply lt_Z2R. rewrite Z2R_Zpower. apply Rmult_lt_reg_r with (bpow (ex - prec)). apply bpow_gt_0. -rewrite <- bpow_add. +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. @@ -201,7 +201,7 @@ apply bpow_gt_0. rewrite H1, abs_F2R in Hx. apply Rlt_le_trans with (2 := Hx). replace (emin + prec - 1)%Z with (prec + (emin - 1))%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite <- Z2R_Zpower. @@ -215,9 +215,9 @@ apply Rle_refl. now apply Zlt_le_weak. Qed. -Section FTZ_rounding. +Section FTZ_round. -Hypothesis rnd : Zrounding. +Hypothesis rnd : Zround. Definition Zrnd_FTZ x := if Rle_bool R1 (Rabs x) then Zrnd rnd x else Z0. @@ -230,7 +230,7 @@ unfold Zrnd_FTZ. rewrite Zrnd_Z2R. case Rle_bool_spec. easy. -rewrite <- abs_Z2R. +rewrite <- Z2R_abs. intros H. generalize (lt_Z2R _ 1 H). clear. @@ -269,15 +269,15 @@ apply (Rabs_def2 _ _ Hx). exact Hy1. Qed. -Definition ZrFTZ := mkZrounding Zrnd_FTZ Z_FTZ_monotone Z_FTZ_Z2R. +Definition ZrFTZ := mkZround Zrnd_FTZ Z_FTZ_monotone Z_FTZ_Z2R. -Theorem FTZ_rounding : +Theorem FTZ_round : forall x : R, (bpow (emin + prec - 1) <= Rabs x)%R -> - rounding beta FTZ_exp ZrFTZ x = rounding beta (FLX_exp prec) rnd x. + round beta FTZ_exp ZrFTZ x = round beta (FLX_exp prec) rnd x. Proof. intros x Hx. -unfold rounding, scaled_mantissa, canonic_exponent. +unfold round, scaled_mantissa, canonic_exponent. destruct (ln_beta beta x) as (ex, He). simpl. unfold Zrnd_FTZ. assert (Hx0: x <> R0). @@ -297,7 +297,7 @@ rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))). change R1 with (bpow 0). rewrite <- (Zplus_opp_r (FLX_exp prec ex)). -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rle_trans with (2 := proj1 He). @@ -312,16 +312,16 @@ omega. easy. Qed. -Theorem FTZ_rounding_small : +Theorem FTZ_round_small : forall x : R, (Rabs x < bpow (emin + prec - 1))%R -> - rounding beta FTZ_exp ZrFTZ x = R0. + round beta FTZ_exp ZrFTZ x = R0. Proof. intros x Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0. -apply rounding_0. -unfold rounding, scaled_mantissa, canonic_exponent. +apply round_0. +unfold round, scaled_mantissa, canonic_exponent. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx0). unfold Zrnd_FTZ. @@ -331,7 +331,7 @@ rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))). change R1 with (bpow 0). rewrite <- (Zplus_opp_r (FTZ_exp ex)). -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. apply Rlt_le_trans with (1 := Hx). @@ -349,6 +349,6 @@ omega. apply bpow_ge_0. Qed. -End FTZ_rounding. +End FTZ_round. End RND_FTZ. diff --git a/src/Core/Fcore_Raux.v b/src/Core/Fcore_Raux.v index cd1e2274bc33d843783a5a95fcaa3c1e8fdac0fd..f4a50a7e3f766d1a32fd9bc359fd83de89a58b0b 100644 --- a/src/Core/Fcore_Raux.v +++ b/src/Core/Fcore_Raux.v @@ -358,7 +358,7 @@ apply Ropp_eq_compat. apply P2R_INR. Qed. -Theorem opp_Z2R : +Theorem Z2R_opp : forall n, Z2R (-n) = (- Z2R n)%R. Proof. intros. @@ -366,7 +366,7 @@ repeat rewrite Z2R_IZR. apply Ropp_Ropp_IZR. Qed. -Theorem plus_Z2R : +Theorem Z2R_plus : forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R. Proof. intros. @@ -385,7 +385,7 @@ rewrite Ropp_Ropp_IZR. apply refl_equal. Qed. -Theorem minus_Z2R : +Theorem Z2R_minus : forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R. Proof. intros. @@ -393,7 +393,7 @@ repeat rewrite Z2R_IZR. apply minus_IZR. Qed. -Theorem mult_Z2R : +Theorem Z2R_mult : forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R. Proof. intros. @@ -475,7 +475,7 @@ repeat rewrite Z2R_IZR. apply IZR_neq. Qed. -Theorem abs_Z2R : +Theorem Z2R_abs : forall z, Z2R (Zabs z) = Rabs (Z2R z). Proof. intros. @@ -900,7 +900,7 @@ Theorem Zfloor_lb : Proof. intros x. unfold Zfloor. -rewrite minus_Z2R. +rewrite Z2R_minus. simpl. rewrite Z2R_IZR. apply Rplus_le_reg_r with (1 - x)%R. @@ -914,7 +914,7 @@ Theorem Zfloor_ub : Proof. intros x. unfold Zfloor. -rewrite minus_Z2R. +rewrite Z2R_minus. unfold Rminus. rewrite Rplus_assoc. rewrite Rplus_opp_l, Rplus_0_r. @@ -932,7 +932,7 @@ apply Zlt_succ_le. apply lt_Z2R. apply Rle_lt_trans with (1 := Hnx). unfold Zsucc. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Zfloor_ub. Qed. @@ -980,7 +980,7 @@ Theorem Zceil_ub : Proof. intros x. unfold Zceil. -rewrite opp_Z2R. +rewrite Z2R_opp. apply Ropp_le_cancel. rewrite Ropp_involutive. apply Zfloor_lb. @@ -996,7 +996,7 @@ unfold Zceil. apply Zopp_le_cancel. rewrite Zopp_involutive. apply Zfloor_lub. -rewrite opp_Z2R. +rewrite Z2R_opp. now apply Ropp_le_contravar. Qed. @@ -1011,11 +1011,11 @@ rewrite <- (Zopp_involutive n). apply f_equal. apply Zfloor_imp. split. -rewrite opp_Z2R. +rewrite Z2R_opp. now apply Ropp_le_contravar. rewrite <- (Zopp_involutive 1). rewrite <- Zopp_plus_distr. -rewrite opp_Z2R. +rewrite Z2R_opp. now apply Ropp_lt_contravar. Qed. @@ -1025,7 +1025,7 @@ Theorem Zceil_Z2R : Proof. intros n. unfold Zceil. -rewrite <- opp_Z2R, Zfloor_Z2R. +rewrite <- Z2R_opp, Zfloor_Z2R. apply Zopp_involutive. Qed. @@ -1055,7 +1055,7 @@ apply Rle_antisym. apply Zfloor_lb. exact H. apply Rlt_le. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Zfloor_ub. Qed. @@ -1309,7 +1309,7 @@ Definition bpow e := | Z0 => R1 end. -Theorem Zpower_pos_powerRZ : +Theorem Z2R_Zpower_pos : forall n m, Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m). Proof. @@ -1320,7 +1320,7 @@ induction (nat_of_P m). apply refl_equal. unfold Zpower_nat. simpl. -rewrite mult_Z2R. +rewrite Z2R_mult. apply Rmult_eq_compat_l. exact IHn0. Qed. @@ -1331,8 +1331,8 @@ Theorem bpow_powerRZ : Proof. destruct e ; unfold bpow. reflexivity. -now rewrite Zpower_pos_powerRZ. -now rewrite Zpower_pos_powerRZ. +now rewrite Z2R_Zpower_pos. +now rewrite Z2R_Zpower_pos. Qed. Theorem bpow_ge_0 : @@ -1353,7 +1353,7 @@ apply powerRZ_lt. apply radix_pos. Qed. -Theorem bpow_add : +Theorem bpow_plus : forall e1 e2 : Z, (bpow (e1 + e2) = bpow e1 * bpow e2)%R. Proof. intros. @@ -1370,12 +1370,12 @@ unfold bpow, Zpower_pos, iter_pos. now rewrite Zmult_1_r. Qed. -Theorem bpow_add1 : +Theorem bpow_plus1 : forall e : Z, (bpow (e + 1) = Z2R r * bpow e)%R. Proof. intros. rewrite <- bpow_1. -rewrite <- bpow_add. +rewrite <- bpow_plus. now rewrite Zplus_comm. Qed. @@ -1420,7 +1420,7 @@ Proof. intros e1 e2 H. replace e2 with (e1 + (e2 - e1))%Z by ring. rewrite <- (Rmult_1_r (bpow e1)). -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_lt_compat_l. apply bpow_gt_0. assert (0 < e2 - e1)%Z by omega. @@ -1523,7 +1523,7 @@ rewrite exp_plus. rewrite Rmult_1_l. rewrite exp_ln. rewrite <- IHn. -rewrite <- mult_Z2R. +rewrite <- Z2R_mult. apply f_equal. unfold Zpower_nat at 1, iter_nat. now rewrite Zmult_1_r. @@ -1538,7 +1538,7 @@ change (Z2R (Zpower_pos r e)) with (bpow (Zpos e)). rewrite H. rewrite <- exp_Ropp. rewrite <- Ropp_mult_distr_l_reverse. -now rewrite <- opp_Z2R. +now rewrite <- Z2R_opp. Qed. Record ln_beta_prop x := { @@ -1570,19 +1570,19 @@ rewrite 2!bpow_exp. fold fact. pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)). split. -rewrite minus_Z2R. +rewrite Z2R_minus. apply exp_increasing_weak. apply Rmult_le_compat_r. now apply Rlt_le. unfold Rminus. -rewrite plus_Z2R. +rewrite Z2R_plus. rewrite Rplus_assoc. rewrite Rplus_opp_r, Rplus_0_r. apply Zfloor_lb. apply exp_increasing. apply Rmult_lt_compat_r. exact H. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Zfloor_ub. rewrite Rmult_assoc. rewrite Rinv_l. @@ -1713,7 +1713,7 @@ Theorem Zpower_pos_gt_0 : Proof. intros b p Hb. apply lt_Z2R. -rewrite Zpower_pos_powerRZ. +rewrite Z2R_Zpower_pos. apply powerRZ_lt. now apply (Z2R_lt 0). Qed. @@ -1778,7 +1778,7 @@ now rewrite Hb. now apply Zlt_le_weak. Qed. -Theorem Zodd_Zpower : +Theorem Zeven_Zpower_odd : forall b e, (0 <= e)%Z -> Zeven b = false -> Zeven (Zpower b e) = false. Proof. diff --git a/src/Core/Fcore_defs.v b/src/Core/Fcore_defs.v index c75eff3a0dd80deccb2def64eb67f82ef9d8e337..053d2d73da6dcb8fa2616a66c553962a3fc33f04 100644 --- a/src/Core/Fcore_defs.v +++ b/src/Core/Fcore_defs.v @@ -23,15 +23,15 @@ Definition IdempotentP (F : R -> Prop) (rnd : R -> R) := Definition Rounding_for_Format (F : R -> Prop) (rnd : R -> R) := MonotoneP rnd /\ IdempotentP F rnd. -Definition rounding_pred_total (P : R -> R -> Prop) := +Definition round_pred_total (P : R -> R -> Prop) := forall x, exists f, P x f. -Definition rounding_pred_monotone (P : R -> R -> Prop) := +Definition round_pred_monotone (P : R -> R -> Prop) := forall x y f g, P x f -> P y g -> (x <= y)%R -> (f <= g)%R. -Definition rounding_pred (P : R -> R -> Prop) := - rounding_pred_total P /\ - rounding_pred_monotone P. +Definition round_pred (P : R -> R -> Prop) := + round_pred_total P /\ + round_pred_monotone P. End Def. @@ -41,7 +41,7 @@ Implicit Arguments F2R [[beta]]. Section RND. -(* property of being a rounding toward -inf *) +(* property of being a round toward -inf *) Definition Rnd_DN_pt (F : R -> Prop) (x f : R) := F f /\ (f <= x)%R /\ forall g : R, F g -> (g <= x)%R -> (g <= f)%R. @@ -49,7 +49,7 @@ Definition Rnd_DN_pt (F : R -> Prop) (x f : R) := Definition Rnd_DN (F : R -> Prop) (rnd : R -> R) := forall x : R, Rnd_DN_pt F x (rnd x). -(* property of being a rounding toward +inf *) +(* property of being a round toward +inf *) Definition Rnd_UP_pt (F : R -> Prop) (x f : R) := F f /\ (x <= f)%R /\ forall g : R, F g -> (x <= g)%R -> (f <= g)%R. @@ -57,7 +57,7 @@ Definition Rnd_UP_pt (F : R -> Prop) (x f : R) := Definition Rnd_UP (F : R -> Prop) (rnd : R -> R) := forall x : R, Rnd_UP_pt F x (rnd x). -(* property of being a rounding toward zero *) +(* property of being a round toward zero *) Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) := ( (0 <= x)%R -> Rnd_DN_pt F x f ) /\ ( (x <= 0)%R -> Rnd_UP_pt F x f ). @@ -65,7 +65,7 @@ Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) := Definition Rnd_ZR (F : R -> Prop) (rnd : R -> R) := forall x : R, Rnd_ZR_pt F x (rnd x). -(* property of being a rounding to nearest *) +(* property of being a round to nearest *) Definition Rnd_N_pt (F : R -> Prop) (x f : R) := F f /\ forall g : R, F g -> (Rabs (f - x) <= Rabs (g - x))%R. diff --git a/src/Core/Fcore_float_prop.v b/src/Core/Fcore_float_prop.v index 53295415aef8cc1d833ad2297d99432eeee7e7fe..b77e2d619e8401289501ca2073b77fb6abf4c6d6 100644 --- a/src/Core/Fcore_float_prop.v +++ b/src/Core/Fcore_float_prop.v @@ -208,7 +208,7 @@ now apply Rlt_le. (* . *) revert H. replace e2 with (e2 - e1 + e1)%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. unfold F2R. simpl. rewrite <- (Z2R_Zpower beta (e2 - e1)). intros H. @@ -231,7 +231,7 @@ Proof. intros m e1 e2 Hm. case (Zle_or_lt e1 e2); intros He. replace e2 with (e2 - e1 + e1)%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. unfold F2R. simpl. rewrite <- (Z2R_Zpower beta (e2 - e1)). intros H. @@ -288,7 +288,7 @@ Proof. intros m e. unfold F2R. rewrite Rabs_mult. -rewrite <- abs_Z2R. +rewrite <- Z2R_abs. simpl. apply f_equal. apply Rabs_right. @@ -303,7 +303,7 @@ Proof. intros m e. unfold F2R. simpl. rewrite <- Ropp_mult_distr_l_reverse. -now rewrite opp_Z2R. +now rewrite Z2R_opp. Qed. Theorem F2R_lt_bpow : @@ -317,7 +317,7 @@ destruct (Zle_or_lt e e') as [He|He]. unfold F2R. simpl. apply Rmult_lt_reg_r with (bpow (-e)). apply bpow_gt_0. -rewrite Rmult_assoc, <- 2!bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- 2!bpow_plus, Zplus_opp_r, Rmult_1_r. rewrite <-Z2R_Zpower. 2: now apply Zle_left. now apply Z2R_lt. elim Zlt_not_le with (1 := Hm). @@ -336,10 +336,10 @@ Theorem F2R_change_exp : Proof. intros e' m e He. unfold F2R. simpl. -rewrite mult_Z2R, Z2R_Zpower, Rmult_assoc. +rewrite Z2R_mult, Z2R_Zpower, Rmult_assoc. apply f_equal. pattern e at 1 ; replace e with (e - e' + e')%Z by ring. -apply bpow_add. +apply bpow_plus. now apply Zle_minus_le_0. Qed. @@ -359,7 +359,7 @@ apply F2R_change_exp. cut (e' - 1 < e + p)%Z. omega. apply <- bpow_lt. apply Rle_lt_trans with (1 := Hf). -rewrite abs_F2R, Zplus_comm, bpow_add. +rewrite abs_F2R, Zplus_comm, bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite <- Z2R_Zpower. @@ -379,14 +379,14 @@ specialize (Hd (Z2R_neq _ _ H)). apply ln_beta_unique. rewrite abs_F2R. unfold F2R. simpl. -rewrite <- abs_Z2R in Hd. +rewrite <- Z2R_abs in Hd. split. replace (d + e - 1)%Z with (d - 1 + e)%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Hd. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. apply Hd. diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v index 015a924e299a5eb0e81ad9db6ee3420cd94e9e09..91fb8907c394f6c5edc461a65846466ccf7bb7e9 100644 --- a/src/Core/Fcore_generic_fmt.v +++ b/src/Core/Fcore_generic_fmt.v @@ -66,7 +66,7 @@ Proof. intros e H. unfold generic_format, scaled_mantissa, canonic_exponent. rewrite ln_beta_bpow. -rewrite <- bpow_add. +rewrite <- bpow_plus. rewrite <- (Z2R_Zpower beta (e + - fexp (e + 1))). rewrite Ztrunc_Z2R. rewrite <- F2R_bpow. @@ -86,14 +86,14 @@ set (e' := canonic_exponent (F2R (Float beta m e))). intros He. unfold F2R at 3. simpl. assert (H: (Z2R m * bpow e * bpow (- e') = Z2R (m * Zpower beta (e + -e')))%R). -rewrite Rmult_assoc, <- bpow_add, mult_Z2R. +rewrite Rmult_assoc, <- bpow_plus, Z2R_mult. rewrite Z2R_Zpower. apply refl_equal. now apply Zle_left. rewrite H, Ztrunc_Z2R. unfold F2R. simpl. rewrite <- H. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l. now rewrite Rmult_1_r. Qed. @@ -133,7 +133,7 @@ intros x Hx. unfold scaled_mantissa. pattern x at 1 3 ; rewrite Hx. unfold F2R. simpl. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. now rewrite Ztrunc_Z2R. Qed. @@ -143,7 +143,7 @@ Theorem scaled_mantissa_bpow : Proof. intros x. unfold scaled_mantissa. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l. apply Rmult_1_r. Qed. @@ -224,7 +224,7 @@ apply bpow_gt_0. apply bpow_gt_0. apply Rmult_lt_reg_r with (bpow (fexp ex)). apply bpow_gt_0. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l. +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. @@ -308,7 +308,7 @@ unfold generic_format, scaled_mantissa. rewrite <- Hf. apply (f_equal (fun m => F2R (Float beta m e))). unfold F2R. simpl. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. now rewrite Ztrunc_Z2R. Qed. @@ -366,15 +366,15 @@ unfold scaled_mantissa. apply Rmult_le_pos; apply bpow_ge_0. Qed. -Section Fcore_generic_rounding_pos. +Section Fcore_generic_round_pos. -Record Zrounding := mkZrounding { +Record Zround := mkZround { Zrnd : R -> Z ; Zrnd_monotone : forall x y, (x <= y)%R -> (Zrnd x <= Zrnd y)%Z ; Zrnd_Z2R : forall n, Zrnd (Z2R n) = n }. -Variable rnd : Zrounding. +Variable rnd : Zround. Let Zrnd := Zrnd rnd. Let Zrnd_monotone := Zrnd_monotone rnd. Let Zrnd_Z2R := Zrnd_Z2R rnd. @@ -402,14 +402,14 @@ rewrite Zfloor_Z2R, Zrnd_Z2R in Hx. apply Zlt_irrefl with (1 := Hx). Qed. -Definition rounding x := +Definition round x := F2R (Float beta (Zrnd (scaled_mantissa x)) (canonic_exponent x)). -Theorem rounding_monotone_pos : - forall x y, (0 < x)%R -> (x <= y)%R -> (rounding x <= rounding y)%R. +Theorem round_monotone_pos : + forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R. Proof. intros x y Hx Hxy. -unfold rounding, scaled_mantissa, canonic_exponent. +unfold round, scaled_mantissa, canonic_exponent. destruct (ln_beta beta x) as (ex, Hex). simpl. destruct (ln_beta beta y) as (ey, Hey). simpl. specialize (Hex (Rgt_not_eq _ _ Hx)). @@ -441,7 +441,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. exact Hxy. apply Rle_trans with (F2R (Float beta (Zrnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))). -rewrite <- bpow_add. +rewrite <- bpow_plus. rewrite <- (Z2R_Zpower beta (ey - 1 + -fexp ey)). 2: omega. rewrite Zrnd_Z2R. destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. @@ -453,7 +453,7 @@ apply Rlt_le. exact (proj2 (mantissa_small_pos _ _ Hex Hx1)). unfold F2R. simpl. rewrite Z2R_Zpower. 2: omega. -rewrite <- bpow_add, Rmult_1_l. +rewrite <- bpow_plus, Rmult_1_l. apply -> bpow_le. omega. apply Rle_trans with (F2R (Float beta (Zrnd (bpow ex * bpow (- fexp ex))) (fexp ex))). @@ -463,12 +463,12 @@ apply Rmult_le_compat_r. apply bpow_ge_0. apply Rlt_le. apply Hex. -rewrite <- bpow_add. +rewrite <- bpow_plus. rewrite <- Z2R_Zpower. 2: omega. rewrite Zrnd_Z2R. unfold F2R. simpl. rewrite 2!Z2R_Zpower ; try omega. -rewrite <- 2!bpow_add. +rewrite <- 2!bpow_plus. apply -> bpow_le. omega. apply F2R_le_compat. @@ -484,43 +484,43 @@ apply bpow_ge_0. exact Hxy. Qed. -Theorem rounding_generic : +Theorem round_generic : forall x, generic_format x -> - rounding x = x. + round x = x. Proof. intros x Hx. -unfold rounding. +unfold round. rewrite scaled_mantissa_generic with (1 := Hx). rewrite Zrnd_Z2R. now apply sym_eq. Qed. -Theorem rounding_0 : - rounding 0 = R0. +Theorem round_0 : + round 0 = R0. Proof. -unfold rounding, scaled_mantissa. +unfold round, scaled_mantissa. rewrite Rmult_0_l. fold (Z2R 0). rewrite Zrnd_Z2R. apply F2R_0. Qed. -Theorem rounding_bounded_large_pos : +Theorem round_bounded_large_pos : forall x ex, (fexp ex < ex)%Z -> (bpow (ex - 1) <= x < bpow ex)%R -> - (bpow (ex - 1) <= rounding x <= bpow ex)%R. + (bpow (ex - 1) <= round x <= bpow ex)%R. Proof. intros x ex He Hx. -unfold rounding, scaled_mantissa. +unfold round, scaled_mantissa. rewrite (canonic_exponent_fexp_pos _ _ Hx). unfold F2R. simpl. destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr. (* DN *) split. replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: Z2R (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)). @@ -530,24 +530,24 @@ rewrite <- Hf. apply Z2R_le. apply Zfloor_lub. rewrite Hf. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Hx. apply Rle_trans with (2 := Rlt_le _ _ (proj2 Hx)). apply Rmult_le_reg_r with (bpow (- fexp ex)). apply bpow_gt_0. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. apply Zfloor_lb. (* UP *) split. apply Rle_trans with (1 := proj1 Hx). apply Rmult_le_reg_r with (bpow (- fexp ex)). apply bpow_gt_0. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. apply Zceil_ub. pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: Z2R (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)). @@ -558,21 +558,21 @@ apply Z2R_le. apply Zceil_glb. rewrite Hf. unfold Zminus. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rlt_le. apply Hx. Qed. -Theorem rounding_bounded_small_pos : +Theorem round_bounded_small_pos : forall x ex, (ex <= fexp ex)%Z -> (bpow (ex - 1) <= x < bpow ex)%R -> - rounding x = R0 \/ rounding x = bpow (fexp ex). + round x = R0 \/ round x = bpow (fexp ex). Proof. intros x ex He Hx. -unfold rounding, scaled_mantissa. +unfold round, scaled_mantissa. rewrite (canonic_exponent_fexp_pos _ _ Hx). unfold F2R. simpl. destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex))) as [Hr|Hr] ; rewrite Hr. @@ -593,10 +593,10 @@ refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))). now apply mantissa_small_pos. Qed. -Theorem generic_format_rounding_pos : +Theorem generic_format_round_pos : forall x, (0 < x)%R -> - generic_format (rounding x). + generic_format (round x). Proof. intros x Hx0. destruct (ln_beta beta x) as (ex, Hex). @@ -604,43 +604,43 @@ specialize (Hex (Rgt_not_eq _ _ Hx0)). rewrite Rabs_pos_eq in Hex. 2: now apply Rlt_le. destruct (Zle_or_lt ex (fexp ex)) as [He|He]. (* small *) -destruct (rounding_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr. +destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr. apply generic_format_0. apply generic_format_bpow. now apply (proj2 (prop_exp ex)). (* large *) -generalize (rounding_bounded_large_pos _ _ He Hex). +generalize (round_bounded_large_pos _ _ He Hex). intros (Hr1, Hr2). -destruct (Rle_or_lt (bpow ex) (rounding x)) as [Hr|Hr]. +destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr]. rewrite <- (Rle_antisym _ _ Hr Hr2). apply generic_format_bpow. now apply (proj1 (prop_exp ex)). assert (Hr' := conj Hr1 Hr). unfold generic_format, scaled_mantissa. rewrite (canonic_exponent_fexp_pos _ _ Hr'). -unfold rounding, scaled_mantissa. +unfold round, scaled_mantissa. rewrite (canonic_exponent_fexp_pos _ _ Hex). unfold F2R at 3. simpl. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. now rewrite Ztrunc_Z2R. Qed. -End Fcore_generic_rounding_pos. +End Fcore_generic_round_pos. -Theorem rounding_ext : +Theorem round_ext : forall rnd1 rnd2, ( forall x, Zrnd rnd1 x = Zrnd rnd2 x ) -> forall x, - rounding rnd1 x = rounding rnd2 x. + round rnd1 x = round rnd2 x. Proof. intros rnd1 rnd2 Hext x. -unfold rounding. +unfold round. now rewrite Hext. Qed. -Section Zrounding_opp. +Section Zround_opp. -Variable rnd : Zrounding. +Variable rnd : Zround. Definition Zrnd_opp x := Zopp (Zrnd rnd (-x)). @@ -655,55 +655,55 @@ apply Zrnd_monotone. now apply Ropp_le_contravar. Qed. -Lemma Zrnd_opp_Z2R : +Lemma Zrnd_Z2R_opp : forall n, Zrnd_opp (Z2R n) = n. Proof. intros n. unfold Zrnd_opp. -rewrite <- opp_Z2R, Zrnd_Z2R. +rewrite <- Z2R_opp, Zrnd_Z2R. apply Zopp_involutive. Qed. -Definition Zrounding_opp := mkZrounding Zrnd_opp Zrnd_opp_le Zrnd_opp_Z2R. +Definition Zround_opp := mkZround Zrnd_opp Zrnd_opp_le Zrnd_Z2R_opp. -Theorem rounding_opp : +Theorem round_opp : forall x, - rounding rnd (- x) = Ropp (rounding Zrounding_opp x). + round rnd (- x) = Ropp (round Zround_opp x). Proof. intros x. -unfold rounding. +unfold round. rewrite opp_F2R, canonic_exponent_opp, scaled_mantissa_opp. apply (f_equal (fun m => F2R (Float beta m _))). apply sym_eq. exact (Zopp_involutive _). Qed. -End Zrounding_opp. +End Zround_opp. -Definition ZrndDN := mkZrounding Zfloor Zfloor_le Zfloor_Z2R. -Definition ZrndUP := mkZrounding Zceil Zceil_le Zceil_Z2R. -Definition ZrndTZ := mkZrounding Ztrunc Ztrunc_le Ztrunc_Z2R. +Definition rndDN := mkZround Zfloor Zfloor_le Zfloor_Z2R. +Definition rndUP := mkZround Zceil Zceil_le Zceil_Z2R. +Definition ZrndTZ := mkZround Ztrunc Ztrunc_le Ztrunc_Z2R. -Theorem rounding_DN_or_UP : +Theorem round_DN_or_UP : forall rnd x, - rounding rnd x = rounding ZrndDN x \/ rounding rnd x = rounding ZrndUP x. + round rnd x = round rndDN x \/ round rnd x = round rndUP x. Proof. intros rnd x. -unfold rounding. +unfold round. unfold Zrnd at 2 4. simpl. destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx]. left. now rewrite Hx. right. now rewrite Hx. Qed. -Theorem rounding_monotone : - forall rnd x y, (x <= y)%R -> (rounding rnd x <= rounding rnd y)%R. +Theorem round_monotone : + forall rnd x y, (x <= y)%R -> (round rnd x <= round rnd y)%R. Proof. intros rnd x y Hxy. destruct (total_order_T x 0) as [[Hx|Hx]|Hx]. -3: now apply rounding_monotone_pos. +3: now apply round_monotone_pos. (* x < 0 *) -unfold rounding. +unfold round. destruct (Rlt_or_le y 0) as [Hy|Hy]. (* . y < 0 *) rewrite <- (Ropp_involutive x), <- (Ropp_involutive y). @@ -711,7 +711,7 @@ rewrite (scaled_mantissa_opp (-x)), (scaled_mantissa_opp (-y)). rewrite (canonic_exponent_opp (-x)), (canonic_exponent_opp (-y)). apply Ropp_le_cancel. rewrite 2!opp_F2R. -apply (rounding_monotone_pos (Zrounding_opp rnd) (-y) (-x)). +apply (round_monotone_pos (Zround_opp rnd) (-y) (-x)). rewrite <- Ropp_0. now apply Ropp_lt_contravar. now apply Ropp_le_contravar. @@ -733,7 +733,7 @@ exact Hy. apply bpow_ge_0. (* x = 0 *) rewrite Hx. -rewrite rounding_0. +rewrite round_0. apply F2R_ge_0_compat. simpl. rewrite <- (Zrnd_Z2R rnd 0). @@ -743,71 +743,71 @@ now rewrite <- Hx. apply bpow_ge_0. Qed. -Theorem rounding_monotone_l : - forall rnd x y, generic_format x -> (x <= y)%R -> (x <= rounding rnd y)%R. +Theorem round_monotone_l : + forall rnd x y, generic_format x -> (x <= y)%R -> (x <= round rnd y)%R. Proof. intros rnd x y Hx Hxy. -rewrite <- (rounding_generic rnd x Hx). -now apply rounding_monotone. +rewrite <- (round_generic rnd x Hx). +now apply round_monotone. Qed. -Theorem rounding_monotone_r : - forall rnd x y, generic_format y -> (x <= y)%R -> (rounding rnd x <= y)%R. +Theorem round_monotone_r : + forall rnd x y, generic_format y -> (x <= y)%R -> (round rnd x <= y)%R. Proof. intros rnd x y Hy Hxy. -rewrite <- (rounding_generic rnd y Hy). -now apply rounding_monotone. +rewrite <- (round_generic rnd y Hy). +now apply round_monotone. Qed. -Theorem rounding_abs_abs : +Theorem round_abs_abs : forall P : R -> R -> Prop, - ( forall rnd x, P x (rounding rnd x) ) -> - forall rnd x, P (Rabs x) (Rabs (rounding rnd x)). + ( forall rnd x, P x (round rnd x) ) -> + forall rnd x, P (Rabs x) (Rabs (round rnd x)). Proof. intros P HP rnd x. destruct (Rle_or_lt 0 x) as [Hx|Hx]. (* . *) rewrite 2!Rabs_pos_eq. apply HP. -rewrite <- (rounding_0 rnd). -now apply rounding_monotone. +rewrite <- (round_0 rnd). +now apply round_monotone. exact Hx. (* . *) rewrite (Rabs_left _ Hx). rewrite Rabs_left1. pattern x at 2 ; rewrite <- Ropp_involutive. -rewrite rounding_opp. +rewrite round_opp. rewrite Ropp_involutive. apply HP. -rewrite <- (rounding_0 rnd). -apply rounding_monotone. +rewrite <- (round_0 rnd). +apply round_monotone. now apply Rlt_le. Qed. -Theorem rounding_monotone_abs_l : - forall rnd x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (rounding rnd y))%R. +Theorem round_monotone_abs_l : + forall rnd x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (round rnd y))%R. Proof. intros rnd x y. -apply rounding_abs_abs. +apply round_abs_abs. clear rnd y; intros rnd y Hy. -now apply rounding_monotone_l. +now apply round_monotone_l. Qed. -Theorem rounding_monotone_abs_r : - forall rnd x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (rounding rnd x) <= y)%R. +Theorem round_monotone_abs_r : + forall rnd x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (round rnd x) <= y)%R. Proof. intros rnd x y. -apply rounding_abs_abs. +apply round_abs_abs. clear rnd x; intros rnd x Hx. -now apply rounding_monotone_r. +now apply round_monotone_r. Qed. -Theorem rounding_DN_opp : +Theorem round_DN_opp : forall x, - rounding ZrndDN (-x) = (- rounding ZrndUP x)%R. + round rndDN (-x) = (- round rndUP x)%R. Proof. intros x. -unfold rounding. +unfold round. rewrite scaled_mantissa_opp. rewrite opp_F2R. unfold Zrnd. simpl. @@ -816,12 +816,12 @@ rewrite Zopp_involutive. now rewrite canonic_exponent_opp. Qed. -Theorem rounding_UP_opp : +Theorem round_UP_opp : forall x, - rounding ZrndUP (-x) = (- rounding ZrndDN x)%R. + round rndUP (-x) = (- round rndDN x)%R. Proof. intros x. -unfold rounding. +unfold round. rewrite scaled_mantissa_opp. rewrite opp_F2R. unfold Zrnd. simpl. @@ -830,44 +830,44 @@ rewrite Ropp_involutive. now rewrite canonic_exponent_opp. Qed. -Theorem generic_format_rounding : +Theorem generic_format_round : forall Zrnd x, - generic_format (rounding Zrnd x). + generic_format (round Zrnd x). Proof. intros rnd x. destruct (total_order_T x 0) as [[Hx|Hx]|Hx]. rewrite <- (Ropp_involutive x). -destruct (rounding_DN_or_UP rnd (- - x)) as [Hr|Hr] ; rewrite Hr. -rewrite rounding_DN_opp. +destruct (round_DN_or_UP rnd (- - x)) as [Hr|Hr] ; rewrite Hr. +rewrite round_DN_opp. apply generic_format_opp. -apply generic_format_rounding_pos. +apply generic_format_round_pos. now apply Ropp_0_gt_lt_contravar. -rewrite rounding_UP_opp. +rewrite round_UP_opp. apply generic_format_opp. -apply generic_format_rounding_pos. +apply generic_format_round_pos. now apply Ropp_0_gt_lt_contravar. rewrite Hx. -rewrite rounding_0. +rewrite round_0. apply generic_format_0. -now apply generic_format_rounding_pos. +now apply generic_format_round_pos. Qed. Theorem generic_DN_pt : forall x, - Rnd_DN_pt generic_format x (rounding ZrndDN x). + Rnd_DN_pt generic_format x (round rndDN x). Proof. intros x. split. -apply generic_format_rounding. +apply generic_format_round. split. pattern x at 2 ; rewrite <- scaled_mantissa_bpow. -unfold rounding, F2R. simpl. +unfold round, F2R. simpl. apply Rmult_le_compat_r. apply bpow_ge_0. apply Zfloor_lb. intros g Hg Hgx. -rewrite <- (rounding_generic ZrndDN _ Hg). -now apply rounding_monotone. +rewrite <- (round_generic rndDN _ Hg). +now apply round_monotone. Qed. Theorem generic_format_satisfies_any : @@ -877,29 +877,29 @@ split. (* symmetric set *) exact generic_format_0. exact generic_format_opp. -(* rounding down *) +(* round down *) intros x. -exists (rounding ZrndDN x). +exists (round rndDN x). apply generic_DN_pt. Qed. Theorem generic_UP_pt : forall x, - Rnd_UP_pt generic_format x (rounding ZrndUP x). + Rnd_UP_pt generic_format x (round rndUP x). Proof. intros x. rewrite <- (Ropp_involutive x). -rewrite rounding_UP_opp. +rewrite round_UP_opp. apply Rnd_DN_UP_pt_sym. apply generic_format_satisfies_any. apply generic_DN_pt. Qed. -Theorem rounding_DN_small_pos : +Theorem round_DN_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> - rounding ZrndDN x = R0. + round rndDN x = R0. Proof. intros x ex Hx He. rewrite <- (F2R_0 beta (canonic_exponent x)). @@ -907,11 +907,11 @@ rewrite <- mantissa_DN_small_pos with (1 := Hx) (2 := He). now rewrite <- canonic_exponent_fexp_pos with (1 := Hx). Qed. -Theorem rounding_UP_small_pos : +Theorem round_UP_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> - rounding ZrndUP x = (bpow (fexp ex)). + round rndUP x = (bpow (fexp ex)). Proof. intros x ex Hx He. rewrite <- F2R_bpow. @@ -924,21 +924,21 @@ Theorem generic_format_EM : generic_format x \/ ~generic_format x. Proof. intros x. -destruct (Req_dec (rounding ZrndDN x) x) as [Hx|Hx]. +destruct (Req_dec (round rndDN x) x) as [Hx|Hx]. left. rewrite <- Hx. -apply generic_format_rounding. +apply generic_format_round. right. intros H. apply Hx. -now apply rounding_generic. +now apply round_generic. Qed. -Theorem rounding_large_pos_ge_pow : +Theorem round_large_pos_ge_pow : forall rnd x e, - (0 < rounding rnd x)%R -> + (0 < round rnd x)%R -> (bpow e <= x)%R -> - (bpow e <= rounding rnd x)%R. + (bpow e <= round rnd x)%R. Proof. intros rnd x e Hd Hex. destruct (ln_beta beta x) as (ex, He). @@ -953,25 +953,25 @@ cut (e < ex)%Z. omega. apply <- bpow_lt. now apply Rle_lt_trans with (2 := proj2 He). destruct (Zle_or_lt ex (fexp ex)). -destruct (rounding_bounded_small_pos rnd x ex H He) as [Hr|Hr]. +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. omega. -apply (rounding_bounded_large_pos rnd x ex H He). +apply (round_bounded_large_pos rnd x ex H He). Qed. Theorem canonic_exponent_DN : forall x, - (0 < rounding ZrndDN x)%R -> - canonic_exponent (rounding ZrndDN x) = canonic_exponent x. + (0 < round rndDN x)%R -> + canonic_exponent (round rndDN x) = canonic_exponent x. Proof. intros x Hd. unfold canonic_exponent. apply f_equal. apply ln_beta_unique. -rewrite (Rabs_pos_eq (rounding ZrndDN x)). 2: now apply Rlt_le. +rewrite (Rabs_pos_eq (round rndDN x)). 2: now apply Rlt_le. destruct (ln_beta beta x) as (ex, He). simpl. assert (Hx: (0 < x)%R). @@ -980,7 +980,7 @@ apply (generic_DN_pt x). specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. split. -apply rounding_large_pos_ge_pow with (1 := Hd). +apply round_large_pos_ge_pow with (1 := Hd). apply He. apply Rle_lt_trans with (2 := proj2 He). apply (generic_DN_pt x). @@ -988,20 +988,20 @@ Qed. Theorem scaled_mantissa_DN : forall x, - (0 < rounding ZrndDN x)%R -> - scaled_mantissa (rounding ZrndDN x) = Z2R (Zfloor (scaled_mantissa x)). + (0 < round rndDN x)%R -> + scaled_mantissa (round rndDN x) = Z2R (Zfloor (scaled_mantissa x)). Proof. intros x Hd. unfold scaled_mantissa. rewrite canonic_exponent_DN with (1 := Hd). -unfold rounding, F2R. simpl. -now rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +unfold round, F2R. simpl. +now rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. Qed. Theorem generic_N_pt_DN_or_UP : forall x f, Rnd_N_pt generic_format x f -> - f = rounding ZrndDN x \/ f = rounding ZrndUP x. + f = round rndDN x \/ f = round rndUP x. Proof. intros x f Hxf. destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf). @@ -1027,7 +1027,7 @@ Proof. intros e x He Hx. pattern x at 2 ; rewrite Hx. unfold F2R at 2. simpl. -rewrite Rmult_assoc, <- bpow_add. +rewrite Rmult_assoc, <- bpow_plus. assert (H: Z2R (Zpower beta (canonic_exponent x + - fexp e)) = bpow (canonic_exponent x + - fexp e)). apply Z2R_Zpower. unfold canonic_exponent. @@ -1036,11 +1036,11 @@ generalize (not_FTZ ex). generalize (proj2 (proj2 (prop_exp _) He) (fexp ex + 1)%Z). omega. rewrite <- H. -rewrite <- mult_Z2R, Ztrunc_Z2R. +rewrite <- Z2R_mult, Ztrunc_Z2R. unfold F2R. simpl. -rewrite mult_Z2R. +rewrite Z2R_mult. rewrite H. -rewrite Rmult_assoc, <- bpow_add. +rewrite Rmult_assoc, <- bpow_plus. now ring_simplify (canonic_exponent x + - fexp e + fexp e)%Z. Qed. @@ -1131,7 +1131,7 @@ apply Rlt_le_trans with (1 := H). apply Z2R_le. apply Zceil_glb. apply Rlt_le. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Zfloor_ub. (* . *) unfold Znearest at 1. @@ -1176,7 +1176,7 @@ Theorem Rcompare_floor_ceil_mid : Proof. intros x Hx. rewrite Zceil_floor_neq with (1 := Hx). -rewrite plus_Z2R. simpl. +rewrite Z2R_plus. simpl. destruct (Rcompare_spec (x - Z2R (Zfloor x)) (/ 2)) as [H1|H1|H1] ; apply sym_eq. (* . *) apply Rcompare_Lt. @@ -1206,7 +1206,7 @@ Theorem Rcompare_ceil_floor_mid : Proof. intros x Hx. rewrite Zceil_floor_neq with (1 := Hx). -rewrite plus_Z2R. simpl. +rewrite Z2R_plus. simpl. destruct (Rcompare_spec (Z2R (Zfloor x) + 1 - x) (/ 2)) as [H1|H1|H1] ; apply sym_eq. (* . *) apply Rcompare_Lt. @@ -1229,7 +1229,7 @@ apply Rmult_lt_compat_r with (2 := H1). now apply (Z2R_lt 0 2). Qed. -Definition ZrndN := mkZrounding Znearest Znearest_monotone Znearest_Z2R. +Definition rndN := mkZround Znearest Znearest_monotone Znearest_Z2R. Theorem Znearest_N_strict : forall x, @@ -1247,7 +1247,7 @@ now elim Hx. rewrite Rabs_left1. rewrite Ropp_minus_distr. rewrite Zceil_floor_neq. -rewrite plus_Z2R. +rewrite Z2R_plus. simpl. apply Ropp_lt_cancel. apply Rplus_lt_reg_r with R1. @@ -1279,7 +1279,7 @@ now apply (Z2R_lt 0 2). destruct (Znearest_DN_or_UP x) as [H|H] ; rewrite H ; clear H. now rewrite Hx. rewrite Zceil_floor_neq. -rewrite plus_Z2R. +rewrite Z2R_plus. simpl. replace (x - (Z2R (Zfloor x) + 1))%R with (x - Z2R (Zfloor x) - 1)%R by ring. rewrite Hx. @@ -1312,17 +1312,17 @@ Qed. Theorem generic_N_pt : forall x, - Rnd_N_pt generic_format x (rounding ZrndN x). + Rnd_N_pt generic_format x (round rndN x). Proof. intros x. -set (d := rounding ZrndDN x). -set (u := rounding ZrndUP x). +set (d := round rndDN x). +set (u := round rndUP x). set (mx := scaled_mantissa x). set (bx := bpow (canonic_exponent x)). (* . *) -assert (H: (Rabs (rounding ZrndN x - x) <= Rmin (x - d) (u - x))%R). +assert (H: (Rabs (round rndN x - x) <= Rmin (x - d) (u - x))%R). pattern x at -1 ; rewrite <- scaled_mantissa_bpow. -unfold d, u, rounding, ZrndN, ZrndDN, ZrndUP, F2R. simpl. +unfold d, u, round, rndN, rndDN, rndUP, F2R. simpl. fold mx bx. rewrite <- 3!Rmult_minus_distr_r. rewrite Rabs_mult, (Rabs_pos_eq bx). 2: apply bpow_ge_0. @@ -1367,7 +1367,7 @@ apply Rle_0_minus. apply Zceil_ub. (* . *) apply Rnd_DN_UP_pt_N with d u. -now apply generic_format_rounding. +now apply generic_format_round. now apply generic_DN_pt. now apply generic_UP_pt. apply Rle_trans with (1 := H). @@ -1378,7 +1378,7 @@ Qed. End Znearest. -Section ZrndN_opp. +Section rndN_opp. Theorem Znearest_opp : forall choice x, @@ -1387,7 +1387,7 @@ Proof. intros choice x. destruct (Req_dec (Z2R (Zfloor x)) x) as [Hx|Hx]. rewrite <- Hx. -rewrite <- opp_Z2R. +rewrite <- Z2R_opp. now rewrite 2!Znearest_Z2R. unfold Znearest. replace (- x - Z2R (Zfloor (-x)))%R with (Z2R (Zceil x) - x)%R. @@ -1403,24 +1403,24 @@ now rewrite Zopp_involutive. intros _. now rewrite Zopp_involutive. unfold Zceil. -rewrite opp_Z2R. +rewrite Z2R_opp. apply Rplus_comm. Qed. -Theorem rounding_N_opp : +Theorem round_N_opp : forall choice, forall x, - rounding (ZrndN choice) (-x) = (- rounding (ZrndN (fun t => negb (choice (-t)%R))) x)%R. + round (rndN choice) (-x) = (- round (rndN (fun t => negb (choice (-t)%R))) x)%R. Proof. intros choice x. -unfold rounding, F2R. simpl. +unfold round, F2R. simpl. rewrite canonic_exponent_opp. rewrite scaled_mantissa_opp. rewrite Znearest_opp. -rewrite opp_Z2R. +rewrite Z2R_opp. now rewrite Ropp_mult_distr_l_reverse. Qed. -End ZrndN_opp. +End rndN_opp. End RND_generic. diff --git a/src/Core/Fcore_rnd.v b/src/Core/Fcore_rnd.v index 42fe50b496b8832bb158b82c4adc879b9b1a684c..bdd73e5d7e8ce4c1a81d6bccca06a83d61ba83aa 100644 --- a/src/Core/Fcore_rnd.v +++ b/src/Core/Fcore_rnd.v @@ -5,9 +5,9 @@ Section RND_prop. Open Scope R_scope. -Theorem rounding_val_of_pred : +Theorem round_val_of_pred : forall rnd : R -> R -> Prop, - rounding_pred rnd -> + round_pred rnd -> forall x, { f : R | rnd x f }. Proof. intros rnd (H1,H2) x. @@ -32,20 +32,20 @@ now apply H4. now rewrite H. Qed. -Theorem rounding_fun_of_pred : +Theorem round_fun_of_pred : forall rnd : R -> R -> Prop, - rounding_pred rnd -> + round_pred rnd -> { f : R -> R | forall x, rnd x (f x) }. Proof. intros rnd H. -exists (fun x => projT1 (rounding_val_of_pred rnd H x)). +exists (fun x => projT1 (round_val_of_pred rnd H x)). intros x. -now destruct rounding_val_of_pred as (f, H1). +now destruct round_val_of_pred as (f, H1). Qed. -Theorem rounding_unicity : +Theorem round_unicity : forall rnd : R -> R -> Prop, - rounding_pred_monotone rnd -> + round_pred_monotone rnd -> forall x f1 f2, rnd x f1 -> rnd x f2 -> @@ -59,7 +59,7 @@ Qed. Theorem Rnd_DN_pt_monotone : forall F : R -> Prop, - rounding_pred_monotone (Rnd_DN_pt F). + round_pred_monotone (Rnd_DN_pt F). Proof. intros F x y f g (Hx1,(Hx2,_)) (Hy1,(_,Hy2)) Hxy. apply Hy2. @@ -84,7 +84,7 @@ Theorem Rnd_DN_pt_unicity : f1 = f2. Proof. intros F. -apply rounding_unicity. +apply round_unicity. apply Rnd_DN_pt_monotone. Qed. @@ -100,7 +100,7 @@ Qed. Theorem Rnd_UP_pt_monotone : forall F : R -> Prop, - rounding_pred_monotone (Rnd_UP_pt F). + round_pred_monotone (Rnd_UP_pt F). Proof. intros F x y f g (Hx1,(_,Hx2)) (Hy1,(Hy2,_)) Hxy. apply Hx2. @@ -125,7 +125,7 @@ Theorem Rnd_UP_pt_unicity : f1 = f2. Proof. intros F. -apply rounding_unicity. +apply round_unicity. apply Rnd_UP_pt_monotone. Qed. @@ -437,7 +437,7 @@ Qed. Theorem Rnd_ZR_pt_monotone : forall F : R -> Prop, F 0 -> - rounding_pred_monotone (Rnd_ZR_pt F). + round_pred_monotone (Rnd_ZR_pt F). Proof. intros F F0 x y f g (Hx1, Hx2) (Hy1, Hy2) Hxy. destruct (Rle_or_lt 0 x) as [Hx|Hx]. @@ -851,7 +851,7 @@ Qed. Theorem Rnd_NG_pt_monotone : forall (F : R -> Prop) (P : R -> R -> Prop), Rnd_NG_pt_unicity_prop F P -> - rounding_pred_monotone (Rnd_NG_pt F P). + round_pred_monotone (Rnd_NG_pt F P). Proof. intros F P HP x y f g (Hf,Hx) (Hg,Hy) [Hxy|Hxy]. now apply Rnd_N_pt_monotone with F x y. @@ -1063,7 +1063,7 @@ Qed. Theorem Rnd_NA_pt_monotone : forall F : R -> Prop, F 0 -> - rounding_pred_monotone (Rnd_NA_pt F). + round_pred_monotone (Rnd_NA_pt F). Proof. intros F HF x y f g Hxf Hyg Hxy. apply (Rnd_NG_pt_monotone F _ (Rnd_NA_pt_unicity_prop F HF) x y). @@ -1121,9 +1121,9 @@ intros x Hx. now apply Rnd_NA_pt_idempotent with F. Qed. -Theorem rounding_pred_pos_imp_rnd : +Theorem round_pred_pos_imp_rnd : forall P : R -> R -> Prop, - rounding_pred_monotone P -> + round_pred_monotone P -> P 0 0 -> forall x f, P x f -> 0 <= x -> 0 <= f. Proof. @@ -1131,9 +1131,9 @@ intros P HP HP0 x f Hxf Hx. now apply (HP 0 x). Qed. -Theorem rounding_pred_rnd_imp_pos : +Theorem round_pred_rnd_imp_pos : forall P : R -> R -> Prop, - rounding_pred_monotone P -> + round_pred_monotone P -> P 0 0 -> forall x f, P x f -> 0 < f -> 0 < x. Proof. @@ -1144,9 +1144,9 @@ apply Rlt_not_le with (1 := Hf). now apply (HP x 0). Qed. -Theorem rounding_pred_neg_imp_rnd : +Theorem round_pred_neg_imp_rnd : forall P : R -> R -> Prop, - rounding_pred_monotone P -> + round_pred_monotone P -> P 0 0 -> forall x f, P x f -> x <= 0 -> f <= 0. Proof. @@ -1154,9 +1154,9 @@ intros P HP HP0 x f Hxf Hx. now apply (HP x 0). Qed. -Theorem rounding_pred_rnd_imp_neg : +Theorem round_pred_rnd_imp_neg : forall P : R -> R -> Prop, - rounding_pred_monotone P -> + round_pred_monotone P -> P 0 0 -> forall x f, P x f -> f < 0 -> x < 0. Proof. @@ -1266,7 +1266,7 @@ Qed. Inductive satisfies_any (F : R -> Prop) := Satisfies_any : F 0 -> ( forall x : R, F x -> F (-x) ) -> - rounding_pred_total (Rnd_DN_pt F) -> satisfies_any F. + round_pred_total (Rnd_DN_pt F) -> satisfies_any F. Theorem satisfies_any_eq : forall F1 F2 : R -> Prop, @@ -1297,7 +1297,7 @@ Qed. Theorem satisfies_any_imp_DN : forall F : R -> Prop, satisfies_any F -> - rounding_pred (Rnd_DN_pt F). + round_pred (Rnd_DN_pt F). Proof. intros F (_,_,Hrnd). split. @@ -1308,7 +1308,7 @@ Qed. Theorem satisfies_any_imp_UP : forall F : R -> Prop, satisfies_any F -> - rounding_pred (Rnd_UP_pt F). + round_pred (Rnd_UP_pt F). Proof. intros F Hany. split. @@ -1325,7 +1325,7 @@ Qed. Theorem satisfies_any_imp_ZR : forall F : R -> Prop, satisfies_any F -> - rounding_pred (Rnd_ZR_pt F). + round_pred (Rnd_ZR_pt F). Proof. intros F Hany. split. @@ -1366,7 +1366,7 @@ Theorem satisfies_any_imp_NG : forall (F : R -> Prop) (P : R -> R -> Prop), satisfies_any F -> NG_existence_prop F P -> - rounding_pred_total (Rnd_NG_pt F P). + round_pred_total (Rnd_NG_pt F P). Proof. intros F P Hany HP x. destruct (proj1 (satisfies_any_imp_DN F Hany) x) as (d, Hd). @@ -1507,11 +1507,11 @@ Qed. Theorem satisfies_any_imp_NA : forall F : R -> Prop, satisfies_any F -> - rounding_pred (Rnd_NA_pt F). + round_pred (Rnd_NA_pt F). Proof. intros F Hany. split. -assert (H : rounding_pred_total (Rnd_NG_pt F (fun a b => (Rabs a <= Rabs b)%R))). +assert (H : round_pred_total (Rnd_NG_pt F (fun a b => (Rabs a <= Rabs b)%R))). apply satisfies_any_imp_NG. apply Hany. intros x d u Hf Hd Hu. diff --git a/src/Core/Fcore_rnd_ne.v b/src/Core/Fcore_rnd_ne.v index 1a8b652d3349d8af87f5124642d299cd0491d700..33cc2d58c5e8ab9a400ee07a196678b2517cc7e3 100644 --- a/src/Core/Fcore_rnd_ne.v +++ b/src/Core/Fcore_rnd_ne.v @@ -30,8 +30,8 @@ Definition DN_UP_parity_pos_prop := ~ format x -> canonic xd -> canonic xu -> - F2R xd = rounding beta fexp ZrndDN x -> - F2R xu = rounding beta fexp ZrndUP x -> + F2R xd = round beta fexp rndDN x -> + F2R xu = round beta fexp rndUP x -> Zeven (Fnum xu) = negb (Zeven (Fnum xd)). Definition DN_UP_parity_prop := @@ -39,8 +39,8 @@ Definition DN_UP_parity_prop := ~ format x -> canonic xd -> canonic xu -> - F2R xd = rounding beta fexp ZrndDN x -> - F2R xu = rounding beta fexp ZrndUP x -> + F2R xd = round beta fexp rndDN x -> + F2R xu = round beta fexp rndUP x -> Zeven (Fnum xu) = negb (Zeven (Fnum xd)). Theorem DN_UP_parity_aux : @@ -73,9 +73,9 @@ rewrite <- Ropp_involutive. now apply generic_format_opp. now apply canonic_opp. now apply canonic_opp. -rewrite rounding_DN_opp, <- opp_F2R. +rewrite round_DN_opp, <- opp_F2R. now apply f_equal. -rewrite rounding_UP_opp, <- opp_F2R. +rewrite round_UP_opp, <- opp_F2R. now apply f_equal. Qed. @@ -98,7 +98,7 @@ assert (Hd3 : Fnum xd = Z0). apply F2R_eq_0_reg with beta (Fexp xd). change (F2R xd = R0). rewrite Hxd. -apply rounding_DN_small_pos with (1 := Hex) (2 := Hxe). +apply round_DN_small_pos with (1 := Hex) (2 := Hxe). assert (Hu3 : xu = Float beta (1 * Zpower beta (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))). apply canonic_unicity with (1 := Hu). apply (f_equal fexp). @@ -110,13 +110,13 @@ rewrite F2R_bpow. apply sym_eq. rewrite Hxu. apply sym_eq. -apply rounding_UP_small_pos with (1 := Hex) (2 := Hxe). +apply round_UP_small_pos with (1 := Hex) (2 := Hxe). now eapply prop_exp. rewrite Hd3, Hu3. rewrite Zmult_1_l. simpl. destruct strong_fexp as [H|H]. -apply Zodd_Zpower with (2 := H). +apply Zeven_Zpower_odd with (2 := H). apply Zle_minus_le_0. now eapply prop_exp. rewrite (proj2 (H ex)). @@ -146,7 +146,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 (rounding_bounded_large_pos beta fexp ZrndUP x ex). +now apply (round_bounded_large_pos beta fexp rndUP x ex). (* - xu = bpow ex *) assert (Hu3: xu = Float beta (1 * Zpower beta (ex - fexp (ex + 1))) (fexp (ex + 1))). apply canonic_unicity with (1 := Hu). @@ -162,10 +162,10 @@ exact Hxe2. assert (Hd3: xd = Float beta (Zpower beta (ex - fexp ex) - 1) (fexp ex)). assert (H: F2R xd = F2R (Float beta (Zpower beta (ex - fexp ex) - 1) (fexp ex))). unfold F2R. simpl. -rewrite minus_Z2R. +rewrite Z2R_minus. unfold Rminus. rewrite Rmult_plus_distr_r. -rewrite Z2R_Zpower, <- bpow_add. +rewrite Z2R_Zpower, <- bpow_plus. ring_simplify (ex - fexp ex + fexp ex)%Z. rewrite Hu2, Hud. unfold ulp, canonic_exponent. @@ -193,7 +193,7 @@ rewrite Bool.negb_involutive. rewrite (Zeven_Zpower beta (ex - fexp ex)). 2: omega. destruct strong_fexp. rewrite H. -apply Zodd_Zpower with (2 := H). +apply Zeven_Zpower_odd with (2 := H). now apply Zle_minus_le_0. apply Zeven_Zpower. specialize (H ex). @@ -212,7 +212,7 @@ rewrite Zeven_plus. now apply eqb_sym. apply sym_eq. apply eq_Z2R. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Rmult_eq_reg_r with (bpow (fexp ex)). rewrite H. simpl. ring. @@ -238,7 +238,7 @@ apply DN_UP_parity_generic_pos. Qed. Theorem Rnd_NE_pt_total : - rounding_pred_total Rnd_NE_pt. + round_pred_total Rnd_NE_pt. Proof. apply satisfies_any_imp_NG. now apply generic_format_satisfies_any. @@ -281,7 +281,7 @@ now apply generic_UP_pt. Qed. Theorem Rnd_NE_pt_monotone : - rounding_pred_monotone Rnd_NE_pt. + round_pred_monotone Rnd_NE_pt. Proof. apply Rnd_NG_pt_monotone. intros x d u Hd Hdn Hu Hun (cd, (Hd1, Hd2)) (cu, (Hu1, Hu2)). @@ -305,26 +305,26 @@ apply Rnd_UP_pt_unicity with (1 := Hu). now apply generic_UP_pt. Qed. -Theorem Rnd_NE_pt_rounding : - rounding_pred Rnd_NE_pt. +Theorem Rnd_NE_pt_round : + round_pred Rnd_NE_pt. split. apply Rnd_NE_pt_total. apply Rnd_NE_pt_monotone. Qed. -Definition ZrndNE := ZrndN (fun x => negb (Zeven (Zfloor x))). +Definition rndNE := rndN (fun x => negb (Zeven (Zfloor x))). Theorem generic_NE_pt_pos : forall x, (0 < x)%R -> - Rnd_NE_pt x (rounding beta fexp ZrndNE x). + Rnd_NE_pt x (round beta fexp rndNE x). Proof. intros x Hx. split. now apply generic_N_pt. unfold NE_prop. set (mx := scaled_mantissa beta fexp x). -set (xr := rounding beta fexp ZrndNE x). +set (xr := round beta fexp rndNE x). destruct (Req_dec (mx - Z2R (Zfloor mx)) (/2)) as [Hm|Hm]. (* midpoint *) left. @@ -336,33 +336,33 @@ unfold Fcore_generic_fmt.canonic. simpl. apply f_equal. apply (generic_N_pt beta fexp prop_exp _ x). simpl. -unfold xr, rounding, Zrnd. simpl. +unfold xr, round, Zrnd. simpl. unfold 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 (rounding beta fexp ZrndDN x))) = true). -destruct (Rle_or_lt (rounding beta fexp ZrndDN x) 0) as [Hr|Hr]. +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]. rewrite (Rle_antisym _ _ Hr). unfold scaled_mantissa. rewrite Rmult_0_l. change R0 with (Z2R 0). now rewrite (Ztrunc_Z2R 0). -erewrite <- rounding_0. -apply rounding_monotone ; try easy. +erewrite <- round_0. +apply round_monotone ; try easy. now apply Rlt_le. rewrite scaled_mantissa_DN ; try easy. now rewrite Ztrunc_Z2R. (* . odd floor *) -change (Zeven (Ztrunc (scaled_mantissa beta fexp (rounding beta fexp ZrndUP x))) = true). +change (Zeven (Ztrunc (scaled_mantissa beta fexp (round beta fexp rndUP 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 := rounding_bounded_large_pos _ _ ZrndUP _ _ He Hex). +assert (Hu := round_bounded_large_pos _ _ rndUP _ _ He Hex). assert (Hfc: Zceil mx = (Zfloor mx + 1)%Z). apply Zceil_floor_neq. intros H. @@ -377,9 +377,9 @@ destruct (proj2 Hu) as [Hu'|Hu']. (* ... u <> bpow *) unfold scaled_mantissa. rewrite canonic_exponent_fexp_pos with (1 := conj (proj1 Hu) Hu'). -unfold rounding, F2R. simpl. +unfold round, F2R. simpl. rewrite canonic_exponent_fexp_pos with (1 := Hex). -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. rewrite Ztrunc_Z2R. fold mx. rewrite Hfc. @@ -388,7 +388,7 @@ now rewrite Zeven_plus, Hmx. rewrite Hu'. unfold scaled_mantissa, canonic_exponent. rewrite ln_beta_bpow. -rewrite <- bpow_add, <- Z2R_Zpower. +rewrite <- bpow_plus, <- Z2R_Zpower. rewrite Ztrunc_Z2R. case_eq (Zeven beta) ; intros Hr. destruct strong_fexp as [Hs|Hs]. @@ -403,15 +403,15 @@ rewrite Zeven_plus. apply eqb_true. unfold mx. replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower beta (ex - fexp ex)). -rewrite Zodd_Zpower with (2 := Hr). +rewrite Zeven_Zpower_odd with (2 := Hr). easy. omega. apply eq_Z2R. rewrite Z2R_Zpower. 2: omega. apply Rmult_eq_reg_r with (bpow (fexp ex)). unfold Zminus. -rewrite bpow_add. -rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l, Rmult_1_r. +rewrite bpow_plus. +rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l, Rmult_1_r. pattern (fexp ex) ; rewrite <- canonic_exponent_fexp_pos with (1 := Hex). now apply sym_eq. apply Rgt_not_eq. @@ -429,17 +429,17 @@ intros g Hg. destruct (Req_dec x g) as [Hxg|Hxg]. rewrite <- Hxg. apply sym_eq. -apply rounding_generic. +apply round_generic. rewrite Hxg. apply Hg. -set (d := rounding beta fexp ZrndDN x). -set (u := rounding beta fexp ZrndUP x). +set (d := round beta fexp rndDN x). +set (u := round beta fexp rndUP x). apply Rnd_N_pt_unicity with (d := d) (u := u) (4 := Hg). now apply generic_DN_pt. now apply generic_UP_pt. 2: now apply generic_N_pt. rewrite <- (scaled_mantissa_bpow beta fexp x). -unfold d, u, rounding, F2R. simpl. fold mx. +unfold d, u, round, F2R. simpl. fold mx. rewrite <- 2!Rmult_minus_distr_r. intros H. apply Rmult_eq_reg_r in H. @@ -459,13 +459,13 @@ apply Rgt_not_eq. apply bpow_gt_0. Qed. -Theorem rounding_NE_opp : +Theorem round_NE_opp : forall x, - rounding beta fexp ZrndNE (-x) = (- rounding beta fexp ZrndNE x)%R. + round beta fexp rndNE (-x) = (- round beta fexp rndNE x)%R. Proof. -intros x; unfold ZrndNE. -rewrite rounding_N_opp. -unfold rounding. +intros x; unfold rndNE. +rewrite round_N_opp. +unfold round. apply f_equal; apply f_equal; apply f_equal2; trivial. unfold Zrnd; simpl. generalize ((scaled_mantissa beta fexp x)); clear x; intros x. @@ -485,7 +485,7 @@ Qed. Theorem generic_NE_pt : forall x, - Rnd_NE_pt x (rounding beta fexp ZrndNE x). + Rnd_NE_pt x (round beta fexp rndNE x). Proof. intros x. destruct (total_order_T x 0) as [[Hx|Hx]|Hx]. @@ -500,10 +500,10 @@ apply opp_F2R. now apply canonic_opp. simpl. now rewrite Zeven_opp. -rewrite <- rounding_NE_opp. +rewrite <- round_NE_opp. apply generic_NE_pt_pos. now apply Ropp_0_gt_lt_contravar. -rewrite Hx, rounding_0. +rewrite Hx, round_0. apply Rnd_NG_pt_refl. apply generic_format_0. now apply generic_NE_pt_pos. diff --git a/src/Core/Fcore_ulp.v b/src/Core/Fcore_ulp.v index 57d87610ec6331cb2ef85c6e5c38780c27fdae6c..52005d9a3aa2d766ab6d56d552f702fdccc04119 100644 --- a/src/Core/Fcore_ulp.v +++ b/src/Core/Fcore_ulp.v @@ -86,13 +86,13 @@ Qed. Theorem ulp_DN_UP : forall x, ~ F x -> - rounding beta fexp ZrndUP x = (rounding beta fexp ZrndDN x + ulp x)%R. + round beta fexp rndUP x = (round beta fexp rndDN x + ulp x)%R. Proof. intros x Fx. -unfold rounding, Zrnd, ulp. simpl. +unfold round, Zrnd, ulp. simpl. unfold F2R. simpl. rewrite Zceil_floor_neq. -rewrite plus_Z2R. simpl. +rewrite Z2R_plus. simpl. ring. intros H. apply Fx. @@ -115,7 +115,7 @@ unfold ulp, F2R. simpl. pattern (bpow (canonic_exponent beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_plus_distr_r. change 1%R with (Z2R 1). -rewrite <- plus_Z2R. +rewrite <- Z2R_plus. change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exponent beta fexp x)) <= bpow e)%R. apply F2R_p1_le_bpow. apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x). @@ -146,7 +146,7 @@ unfold ulp, F2R. simpl. pattern (bpow (canonic_exponent beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_plus_distr_r. change 1%R with (Z2R 1). -rewrite <- plus_Z2R. +rewrite <- Z2R_plus. change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exponent beta fexp x)) <= bpow ex)%R. apply F2R_p1_le_bpow. apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x). @@ -158,14 +158,14 @@ now apply Rlt_le. apply Heps. Qed. -Theorem rounding_DN_succ : +Theorem round_DN_succ : forall x, (0 < x)%R -> F x -> forall eps, (0 <= eps < ulp x)%R -> - rounding beta fexp ZrndDN (x + eps) = x. + round beta fexp rndDN (x + eps) = x. Proof. intros x Zx Fx eps Heps. pattern x at 2 ; rewrite Fx. -unfold rounding. +unfold round. unfold scaled_mantissa, Zrnd. simpl. unfold canonic_exponent at 1 2. rewrite ln_beta_succ ; trivial. @@ -183,18 +183,18 @@ apply Rmult_lt_compat_r. apply bpow_gt_0. now apply Rplus_lt_compat_l. rewrite Rmult_plus_distr_r. -rewrite plus_Z2R. +rewrite Z2R_plus. apply Rplus_le_compat. pattern x at 1 3 ; rewrite Fx. unfold F2R. simpl. rewrite Rmult_assoc. -rewrite <- bpow_add. +rewrite <- bpow_plus. rewrite Zplus_opp_r. rewrite Rmult_1_r. rewrite Zfloor_Z2R. apply Rle_refl. unfold ulp. -rewrite <- bpow_add. +rewrite <- bpow_plus. rewrite Zplus_opp_r. apply Rle_refl. apply Rmult_le_pos. @@ -221,11 +221,11 @@ rewrite canonic_exponent_fexp with (1 := Ex). unfold F2R. simpl. rewrite Rmult_plus_distr_r. rewrite Rmult_assoc. -rewrite <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. change (bpow 0) with (Z2R 1). -rewrite <- plus_Z2R. +rewrite <- Z2R_plus. rewrite Ztrunc_Z2R. -rewrite plus_Z2R. +rewrite Z2R_plus. rewrite Rmult_plus_distr_r. now rewrite Rmult_1_l. rewrite Rabs_pos_eq. @@ -260,29 +260,29 @@ now apply Rlt_le. now apply Rlt_le. Qed. -Theorem rounding_UP_succ : +Theorem round_UP_succ : forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp x)%R -> - rounding beta fexp ZrndUP (x + eps) = (x + ulp x)%R. + round beta fexp rndUP (x + eps) = (x + ulp x)%R. Proof. intros x Zx Fx eps (Heps1,[Heps2|Heps2]). assert (Heps: (0 <= eps < ulp x)%R). split. now apply Rlt_le. exact Heps2. -assert (Hd := rounding_DN_succ x Zx Fx eps Heps). +assert (Hd := round_DN_succ x Zx Fx eps Heps). rewrite ulp_DN_UP. rewrite Hd. unfold ulp, canonic_exponent. now rewrite ln_beta_succ. intros Fs. -rewrite rounding_generic in Hd. +rewrite round_generic in Hd. apply Rgt_not_eq with (2 := Hd). pattern x at 2 ; rewrite <- Rplus_0_r. now apply Rplus_lt_compat_l. exact Fs. rewrite Heps2. -apply rounding_generic. +apply round_generic. now apply generic_format_succ. Qed. @@ -300,9 +300,9 @@ replace y with (x+(y-x))%R by ring. absurd (x < y)%R. 2: apply H. apply Rle_not_lt; apply Req_le. -rewrite <- rounding_DN_succ with (eps:=(y-x)%R); try easy. +rewrite <- round_DN_succ with (eps:=(y-x)%R); try easy. ring_simplify (x+(y-x))%R. -apply sym_eq; now apply rounding_generic. +apply sym_eq; now apply round_generic. split; trivial. apply Rlt_le; now apply Rlt_Rminus. Qed. @@ -310,30 +310,30 @@ Qed. Theorem ulp_error : forall Zrnd x, - (Rabs (rounding beta fexp Zrnd x - x) < ulp x)%R. + (Rabs (round beta fexp Zrnd x - x) < ulp x)%R. Proof. intros Zrnd x. destruct (generic_format_EM beta fexp prop_exp x) as [Hx|Hx]. (* x = rnd x *) -rewrite rounding_generic with (1 := Hx). +rewrite round_generic with (1 := Hx). unfold Rminus. rewrite Rplus_opp_r, Rabs_R0. apply bpow_gt_0. (* x <> rnd x *) -destruct (rounding_DN_or_UP beta fexp Zrnd x) as [H|H] ; rewrite H ; clear H. +destruct (round_DN_or_UP beta fexp Zrnd x) as [H|H] ; rewrite H ; clear H. (* . *) rewrite Rabs_left1. rewrite Ropp_minus_distr. -apply Rplus_lt_reg_r with (rounding beta fexp ZrndDN x). +apply Rplus_lt_reg_r with (round beta fexp rndDN x). rewrite <- ulp_DN_UP with (1 := Hx). ring_simplify. -assert (Hu: (x <= rounding beta fexp ZrndUP x)%R). +assert (Hu: (x <= round beta fexp rndUP x)%R). apply (generic_UP_pt beta fexp prop_exp x). destruct Hu as [Hu|Hu]. exact Hu. elim Hx. rewrite Hu. -now apply generic_format_rounding. +now apply generic_format_round. apply Rle_minus. apply (generic_DN_pt beta fexp prop_exp x). (* . *) @@ -341,25 +341,25 @@ rewrite Rabs_pos_eq. rewrite ulp_DN_UP with (1 := Hx). apply Rplus_lt_reg_r with (x - ulp x)%R. ring_simplify. -assert (Hd: (rounding beta fexp ZrndDN x <= x)%R). +assert (Hd: (round beta fexp rndDN x <= x)%R). apply (generic_DN_pt beta fexp prop_exp x). destruct Hd as [Hd|Hd]. exact Hd. elim Hx. rewrite <- Hd. -now apply generic_format_rounding. +now apply generic_format_round. apply Rle_0_minus. apply (generic_UP_pt beta fexp prop_exp x). Qed. Theorem ulp_half_error : forall choice x, - (Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * ulp x)%R. + (Rabs (round beta fexp (rndN choice) x - x) <= /2 * ulp x)%R. Proof. intros choice x. destruct (generic_format_EM beta fexp prop_exp x) as [Hx|Hx]. (* x = rnd x *) -rewrite rounding_generic. +rewrite round_generic. unfold Rminus. rewrite Rplus_opp_r, Rabs_R0. apply Rmult_le_pos. @@ -369,7 +369,7 @@ now apply (Z2R_lt 0 2). apply bpow_ge_0. exact Hx. (* x <> rnd x *) -set (d := rounding beta fexp ZrndDN x). +set (d := round beta fexp rndDN x). destruct (generic_N_pt beta fexp prop_exp choice x) as (Hr1, Hr2). destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. (* . rnd(x) = rndd(x) *) @@ -387,7 +387,7 @@ right. field. apply Rle_minus. apply (generic_DN_pt beta fexp prop_exp x). (* . rnd(x) = rndu(x) *) -assert (Hu: (d + ulp x)%R = rounding beta fexp ZrndUP x). +assert (Hu: (d + ulp x)%R = round beta fexp rndUP x). unfold d. now rewrite <- ulp_DN_UP. apply Rle_trans with (Rabs (d + ulp x - x)). @@ -436,8 +436,8 @@ Qed. Theorem ulp_DN_pt_eq : forall x, - (0 < rounding beta fexp ZrndDN x)%R -> - ulp (rounding beta fexp ZrndDN x) = ulp x. + (0 < round beta fexp rndDN x)%R -> + ulp (round beta fexp rndDN x) = ulp x. Proof. intros x Hd. unfold ulp. @@ -448,13 +448,13 @@ Qed. Theorem ulp_error_f : (forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) -> forall Zrnd x, - (rounding beta fexp Zrnd x <> 0)%R -> - (Rabs (rounding beta fexp Zrnd x - x) < ulp (rounding beta fexp Zrnd x))%R. + (round beta fexp Zrnd x <> 0)%R -> + (Rabs (round beta fexp Zrnd x - x) < ulp (round beta fexp Zrnd x))%R. Proof. intros Hf Zrnd x Hfx. -case (rounding_DN_or_UP beta fexp Zrnd x); intros Hx. +case (round_DN_or_UP beta fexp Zrnd x); intros Hx. (* *) -case (Rle_or_lt 0 (rounding beta fexp ZrndDN x)). +case (Rle_or_lt 0 (round beta fexp rndDN x)). intros H; destruct H. rewrite Hx at 2. rewrite ulp_DN_pt_eq; trivial. @@ -462,49 +462,49 @@ apply ulp_error. rewrite Hx in Hfx; contradict Hfx; auto with real. intros H. apply Rlt_le_trans with (1:=ulp_error _ _). -rewrite <- (ulp_opp x), <- (ulp_opp (rounding beta fexp Zrnd x)). +rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp Zrnd x)). apply ulp_monotone; trivial. apply Ropp_0_gt_lt_contravar; apply Rlt_gt. case (Rle_or_lt 0 x); trivial. intros H1; contradict H. apply Rle_not_lt. -apply rounding_monotone_l; trivial. +apply round_monotone_l; trivial. apply generic_format_0. apply Ropp_le_contravar; rewrite Hx. apply (generic_DN_pt beta fexp prop_exp x). (* *) -rewrite Hx; case (Rle_or_lt 0 (rounding beta fexp ZrndUP x)). +rewrite Hx; case (Rle_or_lt 0 (round beta fexp rndUP x)). intros H; destruct H. apply Rlt_le_trans with (1:=ulp_error _ _). apply ulp_monotone; trivial. case (Rle_or_lt x 0); trivial. intros H1; contradict H. apply Rle_not_lt. -apply rounding_monotone_r; trivial. +apply round_monotone_r; trivial. apply generic_format_0. apply (generic_UP_pt beta fexp prop_exp x). rewrite Hx in Hfx; contradict Hfx; auto with real. intros H. -rewrite <- (ulp_opp (rounding beta fexp ZrndUP x)). -rewrite <- rounding_DN_opp. +rewrite <- (ulp_opp (round beta fexp rndUP x)). +rewrite <- round_DN_opp. rewrite ulp_DN_pt_eq; trivial. -replace (rounding beta fexp ZrndUP x - x)%R with (-((rounding beta fexp ZrndDN (-x) - (-x))))%R. +replace (round beta fexp rndUP x - x)%R with (-((round beta fexp rndDN (-x) - (-x))))%R. rewrite Rabs_Ropp. apply ulp_error. -rewrite rounding_DN_opp; ring. -rewrite rounding_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. +rewrite round_DN_opp; ring. +rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. Qed. Theorem ulp_half_error_f : (forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) -> forall choice x, - (rounding beta fexp (ZrndN choice) x <> 0)%R -> - (Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * ulp (rounding beta fexp (ZrndN choice) x))%R. + (round beta fexp (rndN choice) x <> 0)%R -> + (Rabs (round beta fexp (rndN choice) x - x) <= /2 * ulp (round beta fexp (rndN choice) x))%R. Proof. intros Hf choice x Hfx. -case (rounding_DN_or_UP beta fexp (ZrndN choice) x); intros Hx. +case (round_DN_or_UP beta fexp (rndN choice) x); intros Hx. (* *) -case (Rle_or_lt 0 (rounding beta fexp ZrndDN x)). +case (Rle_or_lt 0 (round beta fexp rndDN x)). intros H; destruct H. rewrite Hx at 2. rewrite ulp_DN_pt_eq; trivial. @@ -514,18 +514,18 @@ intros H. apply Rle_trans with (1:=ulp_half_error _ _). apply Rmult_le_compat_l. auto with real. -rewrite <- (ulp_opp x), <- (ulp_opp (rounding beta fexp (ZrndN choice) x)). +rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp (rndN choice) x)). apply ulp_monotone; trivial. apply Ropp_0_gt_lt_contravar; apply Rlt_gt. case (Rle_or_lt 0 x); trivial. intros H1; contradict H. apply Rle_not_lt. -apply rounding_monotone_l; trivial. +apply round_monotone_l; trivial. apply generic_format_0. apply Ropp_le_contravar; rewrite Hx. apply (generic_DN_pt beta fexp prop_exp x). (* *) -case (Rle_or_lt 0 (rounding beta fexp ZrndUP x)). +case (Rle_or_lt 0 (round beta fexp rndUP x)). intros H; destruct H. apply Rle_trans with (1:=ulp_half_error _ _). apply Rmult_le_compat_l. @@ -534,20 +534,20 @@ apply ulp_monotone; trivial. case (Rle_or_lt x 0); trivial. intros H1; contradict H. apply Rle_not_lt. -apply rounding_monotone_r; trivial. +apply round_monotone_r; trivial. apply generic_format_0. rewrite Hx; apply (generic_UP_pt beta fexp prop_exp x). rewrite Hx in Hfx; contradict Hfx; auto with real. intros H. -rewrite Hx at 2; rewrite <- (ulp_opp (rounding beta fexp ZrndUP x)). -rewrite <- rounding_DN_opp. +rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp rndUP x)). +rewrite <- round_DN_opp. rewrite ulp_DN_pt_eq; trivial. pattern x at 1 2; rewrite <- Ropp_involutive. -rewrite rounding_N_opp. +rewrite round_N_opp. unfold Rminus. rewrite <- Ropp_plus_distr, Rabs_Ropp. apply ulp_half_error. -rewrite rounding_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. +rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. Qed. Definition pred x := @@ -578,7 +578,7 @@ unfold ulp, F2R. simpl. pattern (bpow (canonic_exponent beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_minus_distr_r. change 1%R with (Z2R 1). -rewrite <- minus_Z2R. +rewrite <- Z2R_minus. change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exponent beta fexp x)))%R. apply bpow_le_F2R_m1; trivial. now rewrite <- Fx. @@ -614,11 +614,11 @@ rewrite canonic_exponent_fexp with (1 := Ex). unfold F2R. simpl. rewrite Rmult_minus_distr_r. rewrite Rmult_assoc. -rewrite <- bpow_add, Zplus_opp_r, Rmult_1_r. +rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. change (bpow 0) with (Z2R 1). -rewrite <- minus_Z2R. +rewrite <- Z2R_minus. rewrite Ztrunc_Z2R. -rewrite minus_Z2R. +rewrite Z2R_minus. rewrite Rmult_minus_distr_r. now rewrite Rmult_1_l. rewrite Rabs_pos_eq. @@ -667,9 +667,9 @@ case (Zle_lt_or_eq _ _ He); clear He; intros He. assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R. unfold f; rewrite Hx. unfold F2R; simpl. -rewrite minus_Z2R, Z2R_Zpower. +rewrite Z2R_minus, Z2R_Zpower. rewrite Rmult_minus_distr_r, Rmult_1_l. -rewrite <- bpow_add. +rewrite <- bpow_plus. now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. omega. rewrite H. @@ -696,7 +696,7 @@ now destruct beta. simpl. unfold Zpower_pos; simpl. now rewrite Zmult_1_r. -rewrite <- bpow_add. +rewrite <- bpow_plus. replace (1+(e-2))%Z with (e-1)%Z by ring. now right. rewrite <- Rplus_0_r. @@ -810,7 +810,7 @@ now destruct beta. simpl. unfold Zpower_pos; simpl. now rewrite Zmult_1_r. -rewrite <- bpow_add. +rewrite <- bpow_plus. replace (1+(e-2))%Z with (e-1)%Z by ring. now right. rewrite <- Rplus_0_r, Hxe. @@ -880,13 +880,13 @@ apply Rle_0_minus. now apply ulp_le_pos. Qed. -Theorem rounding_UP_pred : +Theorem round_UP_pred : forall x, (0 < pred x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x) )%R -> - rounding beta fexp ZrndUP (pred x + eps) = x. + round beta fexp rndUP (pred x + eps) = x. Proof. intros x Hx Fx eps Heps. -rewrite rounding_UP_succ; trivial. +rewrite round_UP_succ; trivial. apply pred_ulp; trivial. apply Rlt_trans with (1:=Hx). apply pred_lt. @@ -897,10 +897,10 @@ apply pred_lt. Qed. -Theorem rounding_DN_pred : +Theorem round_DN_pred : forall x, (0 < pred x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x))%R -> - rounding beta fexp ZrndDN (x - eps) = pred x. + round beta fexp rndDN (x - eps) = pred x. Proof. intros x Hpx Fx eps Heps. assert (Hx:(0 < x)%R). @@ -910,7 +910,7 @@ replace (x-eps)%R with (pred x + (ulp (pred x)-eps))%R. 2: pattern x at 3; rewrite <- (pred_ulp x); trivial. 2: ring. 2: now apply Rgt_not_eq. -rewrite rounding_DN_succ; trivial. +rewrite round_DN_succ; trivial. now apply format_pred. split. apply Rle_0_minus. @@ -959,8 +959,8 @@ intros Hy3. contradict Hy2. (* -rewrite <- rounding_DN_pred with y (Rmin y (ulp (pred y))). -apply rounding_monotone_l; trivial. +rewrite <- round_DN_pred with y (Rmin y (ulp (pred y))). +apply round_monotone_l; trivial. apply generic_format_0.*) @@ -978,10 +978,10 @@ apply Rlt_trans with (1:=proj1 H); easy. now apply Rgt_not_eq. (* *) replace x with (y-(y-x))%R by ring. -rewrite <- rounding_DN_pred with (eps:=(y-x)%R); try easy. +rewrite <- round_DN_pred with (eps:=(y-x)%R); try easy. ring_simplify (y-(y-x))%R. apply Req_le. -apply sym_eq; now apply rounding_generic. +apply sym_eq; now apply round_generic. split; trivial. now apply Rlt_Rminus. now apply Rlt_le. diff --git a/src/Prop/Fprop_div_sqrt_error.v b/src/Prop/Fprop_div_sqrt_error.v index 32beafa6cb739e0ee1878a0bcb53990d8eb68325..f2bfebdbc4a801c9d7314b6283adfdcdceff3ef6 100644 --- a/src/Prop/Fprop_div_sqrt_error.v +++ b/src/Prop/Fprop_div_sqrt_error.v @@ -51,22 +51,22 @@ Qed. Theorem div_error_FLX : forall Zrnd x y, format x -> format y -> - format (x - rounding beta (FLX_exp prec) Zrnd (x/y) * y)%R. + format (x - round beta (FLX_exp prec) Zrnd (x/y) * y)%R. Proof. intros 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 (rounding beta (FLX_exp prec) Zrnd (x/y)) 0); intros Hr. +case (Req_dec (round beta (FLX_exp prec) Zrnd (x/y)) 0); intros Hr. rewrite Hr; ring_simplify (x-0*y)%R; assumption. assert (Zx: x <> R0). contradict Hr. rewrite Hr. unfold Rdiv. -now rewrite Rmult_0_l, rounding_0. +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 (rounding beta (FLX_exp prec) Zrnd (x / y))) as (fr,(Hr1,Hr2)). -apply generic_format_rounding. +destruct (format_nx (round beta (FLX_exp prec) Zrnd (x / y))) as (fr,(Hr1,Hr2)). +apply generic_format_round. now apply FLX_exp_correct. unfold Rminus; apply format_add with fx (Fopp beta (Fmult beta fr fy)); trivial. now rewrite Fopp_F2R,mult_F2R, <- Hr1, <- Hy1. @@ -101,8 +101,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 + - (rounding beta (FLX_exp prec) Zrnd (x / y) * y))%R with - (y * (-(rounding beta (FLX_exp prec) Zrnd (x / y) - x/y)))%R. +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. 2: field; assumption. rewrite Rabs_mult. apply Rlt_le_trans with (Rabs y * bpow (Fexp fr))%R. @@ -118,7 +118,7 @@ exact Hr. 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. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. rewrite Hy2; unfold canonic_exponent, FLX_exp. @@ -131,26 +131,26 @@ Variable Hp1 : Zlt 1 prec. Theorem sqrt_error_N : forall x, format x -> - format (x - Rsqr (rounding beta (FLX_exp prec) (ZrndN choice) (sqrt x)))%R. + format (x - Rsqr (round beta (FLX_exp prec) (rndN choice) (sqrt x)))%R. Proof. intros x Hx. destruct (total_order_T x 0) as [[Hxz|Hxz]|Hxz]. unfold sqrt. destruct (Rcase_abs x). -rewrite rounding_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, rounding_0. +rewrite Hxz, sqrt_0, round_0. unfold Rsqr. rewrite Rmult_0_l, Rminus_0_r. apply generic_format_0. -case (Req_dec (rounding beta (FLX_exp prec) (ZrndN choice) (sqrt x)) 0); intros Hr. +case (Req_dec (round beta (FLX_exp prec) (rndN 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 (rounding beta (FLX_exp prec) (ZrndN choice) (sqrt x))) as (fr,(Hr1,Hr2)). -apply generic_format_rounding. +destruct (format_nx (round beta (FLX_exp prec) (rndN choice) (sqrt x))) as (fr,(Hr1,Hr2)). +apply generic_format_round. now apply FLX_exp_correct. unfold Rminus; apply format_add with fx (Fopp beta (Fmult beta fr fr)); trivial. unfold Rsqr; now rewrite Fopp_F2R,mult_F2R, <- Hr1. @@ -231,7 +231,7 @@ right; unfold ulp; apply f_equal. rewrite Hr2, <- Hr1; trivial. rewrite Rmult_assoc, Rmult_comm. replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring. -rewrite bpow_add, Rmult_assoc. +rewrite bpow_plus, Rmult_assoc. apply Rmult_lt_compat_l. apply bpow_gt_0. apply Rmult_lt_reg_l with 2%R. @@ -266,7 +266,7 @@ intros H1. absurd (Rabs (F2R fr) < bpow (es - 1))%R. apply Rle_not_lt. rewrite <- Hr1. -apply rounding_monotone_abs_l. +apply round_monotone_abs_l. now apply FLX_exp_correct. apply generic_format_bpow. unfold FLX_exp; omega. diff --git a/src/Prop/Fprop_mult_error.v b/src/Prop/Fprop_mult_error.v index 99fa844d588f1321dd57012aefbed84c569c6197..a2680f21206ed136f4e95b13634453e9fa6dd869 100644 --- a/src/Prop/Fprop_mult_error.v +++ b/src/Prop/Fprop_mult_error.v @@ -16,17 +16,17 @@ Theorem mult_error_FLX_aux: forall rnd, forall x y, format x -> format y -> - (rounding beta (FLX_exp prec) rnd (x * y) - (x * y) <> 0)%R -> + (round beta (FLX_exp prec) rnd (x * y) - (x * y) <> 0)%R -> exists f:float beta, - (F2R f = rounding beta (FLX_exp prec) rnd (x * y) - (x * y))%R + (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. intros rnd x y Hx Hy Hz. -set (f := (rounding beta (FLX_exp prec) rnd (x * y))). +set (f := (round beta (FLX_exp prec) rnd (x * y))). destruct (Req_dec (x * y) 0) as [Hxy0|Hxy0]. contradict Hz. rewrite Hxy0. -rewrite rounding_0. +rewrite round_0. ring. destruct (ln_beta beta (x * y)) as (exy, Hexy). specialize (Hexy Hxy0). @@ -52,7 +52,7 @@ cut (exy - 1 < ex + ey)%Z. omega. apply <- (bpow_lt beta). apply Rle_lt_trans with (1 := proj1 Hexy). rewrite Rabs_mult. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_0_lt_compat. apply Rabs_pos. apply Rabs_pos. @@ -68,7 +68,7 @@ cut ((ex - 1) + (ey - 1) < exy)%Z. omega. apply <- (bpow_lt beta). apply Rle_lt_trans with (2 := proj2 Hexy). rewrite Rabs_mult. -rewrite bpow_add. +rewrite bpow_plus. apply Rmult_le_compat. apply bpow_ge_0. apply bpow_ge_0. @@ -82,7 +82,7 @@ rewrite Hx at 6. rewrite Hy at 6. rewrite <- mult_F2R. simpl. -unfold f, rounding, Rminus. +unfold f, round, Rminus. rewrite opp_F2R, Rplus_comm, <- plus_F2R. unfold Fplus. simpl. now rewrite Zle_imp_le_bool with (1 := Hc2). @@ -118,10 +118,10 @@ Theorem mult_error_FLX : forall rnd, forall x y, format x -> format y -> - format (rounding beta (FLX_exp prec) rnd (x * y) - (x * y))%R. + format (round beta (FLX_exp prec) rnd (x * y) - (x * y))%R. Proof. intros rnd x y Hx Hy. -destruct (Req_dec (rounding beta (FLX_exp prec) rnd (x * y) - x * y) 0) as [Hr0|Hr0]. +destruct (Req_dec (round beta (FLX_exp prec) rnd (x * y) - x * y) 0) as [Hr0|Hr0]. rewrite Hr0. apply generic_format_0. destruct (mult_error_FLX_aux rnd x y Hx Hy Hr0) as ((m,e),(H1,(H2,H3))). @@ -150,29 +150,29 @@ Theorem mult_error_FLT : forall x y, format x -> format y -> (x*y = 0)%R \/ (bpow (emin + 2*prec - 1) <= Rabs (x * y))%R -> - format (rounding beta (FLT_exp emin prec) rnd (x * y) - (x * y))%R. + format (round beta (FLT_exp emin prec) rnd (x * y) - (x * y))%R. Proof. clear Hpemin. intros rnd x y Hx Hy Hxy. -set (f := (rounding beta (FLT_exp emin prec) rnd (x * y))). +set (f := (round beta (FLT_exp emin prec) rnd (x * y))). destruct (Req_dec (f - x * y) 0) as [Hr0|Hr0]. rewrite Hr0. apply generic_format_0. destruct Hxy as [Hxy|Hxy]. unfold f. rewrite Hxy. -rewrite rounding_0. +rewrite round_0. ring_simplify (0 - 0)%R. apply generic_format_0. destruct (mult_error_FLX_aux beta prec Hp 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_rounding_FLX beta emin). +rewrite <- (FLT_round_FLX beta emin). assumption. apply Rle_trans with (2:=Hxy). apply -> bpow_le. omega. -rewrite <- (FLT_rounding_FLX beta emin) in H1. +rewrite <- (FLT_round_FLX beta emin) in H1. 2:apply Rle_trans with (2:=Hxy). 2:apply -> bpow_le; omega. unfold f; rewrite <- H1. @@ -190,7 +190,7 @@ assert (Hxy0:(x*y <> 0)%R). contradict Hr0. unfold f. rewrite Hr0. -rewrite rounding_0. +rewrite round_0. ring. assert (Hx0: (x <> 0)%R). contradict Hxy0. @@ -206,7 +206,7 @@ assert (emin + 2 * prec -1 < ex + ey)%Z. 2: omega. apply <- (bpow_lt beta). apply Rle_lt_trans with (1:=Hxy). -rewrite Rabs_mult, bpow_add. +rewrite Rabs_mult, bpow_plus. apply Rmult_le_0_lt_compat; try apply Rabs_pos. apply Ex. apply Ey. diff --git a/src/Prop/Fprop_plus_error.v b/src/Prop/Fprop_plus_error.v index 2188c87500e574785ab1cfdedf40a9a19b3272ca..98c88d18a44edb7e9aa2e5aed47bbc35cc6cd5f0 100644 --- a/src/Prop/Fprop_plus_error.v +++ b/src/Prop/Fprop_plus_error.v @@ -9,33 +9,33 @@ Notation bpow e := (bpow beta e). Variable fexp : Z -> Z. Hypothesis prop_exp : valid_exp fexp. -Theorem rounding_repr_same_exp : +Theorem round_repr_same_exp : forall rnd m e, exists m', - rounding beta fexp rnd (F2R (Float beta m e)) = F2R (Float beta m' e). + round beta fexp rnd (F2R (Float beta m e)) = F2R (Float beta m' e). Proof. intros rnd m e. set (e' := canonic_exponent beta fexp (F2R (Float beta m e))). -unfold rounding, scaled_mantissa. fold e'. +unfold round, scaled_mantissa. fold e'. destruct (Zle_or_lt e' e) as [He|He]. exists m. unfold F2R at 2. simpl. -rewrite Rmult_assoc, <- bpow_add. +rewrite Rmult_assoc, <- bpow_plus. rewrite <- Z2R_Zpower. 2: omega. -rewrite <- mult_Z2R, Zrnd_Z2R. +rewrite <- Z2R_mult, Zrnd_Z2R. unfold F2R. simpl. -rewrite mult_Z2R. +rewrite Z2R_mult. rewrite Rmult_assoc. rewrite Z2R_Zpower. 2: omega. -rewrite <- bpow_add. +rewrite <- bpow_plus. apply (f_equal (fun v => Z2R m * bpow v)%R). ring. exists ((Zrnd rnd (Z2R m * bpow (e - e'))) * Zpower beta (e' - e))%Z. unfold F2R. simpl. -rewrite mult_Z2R. +rewrite Z2R_mult. rewrite Z2R_Zpower. 2: omega. rewrite 2!Rmult_assoc. -rewrite <- 2!bpow_add. +rewrite <- 2!bpow_plus. apply (f_equal (fun v => _ * bpow v)%R). ring. Qed. @@ -49,13 +49,13 @@ Theorem plus_error_aux : forall x y, (canonic_exponent beta fexp x <= canonic_exponent beta fexp y)%Z -> format x -> format y -> - format (rounding beta fexp (ZrndN choice) (x + y) - (x + y))%R. + format (round beta fexp (rndN choice) (x + y) - (x + y))%R. Proof. intros x y. set (ex := canonic_exponent beta fexp x). set (ey := canonic_exponent beta fexp y). intros He Hx Hy. -destruct (Req_dec (rounding beta fexp (ZrndN choice) (x + y) - (x + y)) R0) as [H0|H0]. +destruct (Req_dec (round beta fexp (rndN choice) (x + y) - (x + y)) R0) as [H0|H0]. rewrite H0. apply generic_format_0. set (mx := Ztrunc (scaled_mantissa beta fexp x)). @@ -69,7 +69,7 @@ unfold Fplus. simpl. now rewrite Zle_imp_le_bool with (1 := He). (* *) rewrite Hxy. -destruct (rounding_repr_same_exp (ZrndN choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy'). +destruct (round_repr_same_exp (rndN choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy'). rewrite Hxy'. assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R = F2R @@ -94,7 +94,7 @@ Qed. Theorem plus_error : forall x y, format x -> format y -> - format (rounding beta fexp (ZrndN choice) (x + y) - (x + y))%R. + format (round beta fexp (rndN choice) (x + y) - (x + y))%R. Proof. intros x y Hx Hy. destruct (Zle_or_lt (canonic_exponent beta fexp x) (canonic_exponent beta fexp y)). @@ -117,12 +117,12 @@ Notation format := (generic_format beta fexp). Hypothesis not_FTZ : forall e, (fexp (fexp e + 1) <= fexp e)%Z. -Theorem rounding_plus_eq_zero_aux : +Theorem round_plus_eq_zero_aux : forall rnd x y, (canonic_exponent beta fexp x <= canonic_exponent beta fexp y)%Z -> format x -> format y -> (0 <= x + y)%R -> - rounding beta fexp rnd (x + y) = R0 -> + round beta fexp rnd (x + y) = R0 -> (x + y = 0)%R. Proof. intros rnd x y He Hx Hy Hp Hxy. @@ -141,7 +141,7 @@ rewrite <- plus_F2R. unfold Fplus. simpl. now rewrite Zle_bool_refl. rewrite H in Hxy. -rewrite rounding_generic in Hxy. +rewrite round_generic in Hxy. now rewrite <- H in Hxy. apply generic_format_canonic_exponent. rewrite <- H. @@ -149,20 +149,20 @@ unfold canonic_exponent. rewrite ln_beta_unique with (1 := Hexy). apply Zle_refl. (* . *) -elim Rle_not_lt with (1 := rounding_monotone beta _ prop_exp rnd _ _ (proj1 Hexy)). +elim Rle_not_lt with (1 := round_monotone beta _ prop_exp rnd _ _ (proj1 Hexy)). rewrite (Rabs_pos_eq _ Hp). rewrite Hxy. -rewrite rounding_generic. +rewrite round_generic. apply bpow_gt_0. apply generic_format_bpow. ring_simplify (exy - 1 + 1)%Z. omega. Qed. -Theorem rounding_plus_eq_zero : +Theorem round_plus_eq_zero : forall rnd x y, format x -> format y -> - rounding beta fexp rnd (x + y) = R0 -> + round beta fexp rnd (x + y) = R0 -> (x + y = 0)%R. Proof. intros rnd x y Hx Hy. @@ -170,27 +170,27 @@ destruct (Rle_or_lt R0 (x + y)) as [H1|H1]. (* . *) revert H1. destruct (Zle_or_lt (canonic_exponent beta fexp x) (canonic_exponent beta fexp y)) as [H2|H2]. -now apply rounding_plus_eq_zero_aux. +now apply round_plus_eq_zero_aux. rewrite Rplus_comm. -apply rounding_plus_eq_zero_aux ; try easy. +apply round_plus_eq_zero_aux ; try easy. now apply Zlt_le_weak. (* . *) revert H1. rewrite <- (Ropp_involutive (x + y)), Ropp_plus_distr, <- Ropp_0. intros H1. -rewrite rounding_opp. +rewrite round_opp. intros Hxy. apply f_equal. -cut (rounding beta fexp (Zrounding_opp rnd) (- x + - y) = 0)%R. +cut (round beta fexp (Zround_opp rnd) (- x + - y) = 0)%R. cut (0 <= -x + -y)%R. destruct (Zle_or_lt (canonic_exponent beta fexp (-x)) (canonic_exponent beta fexp (-y))) as [H2|H2]. -apply rounding_plus_eq_zero_aux ; try apply generic_format_opp ; easy. +apply round_plus_eq_zero_aux ; try apply generic_format_opp ; easy. rewrite Rplus_comm. -apply rounding_plus_eq_zero_aux ; try apply generic_format_opp ; try easy. +apply round_plus_eq_zero_aux ; try apply generic_format_opp ; try easy. now apply Zlt_le_weak. apply Rlt_le. now apply Ropp_lt_cancel. -rewrite <- (Ropp_involutive (rounding _ _ _ _)). +rewrite <- (Ropp_involutive (round _ _ _ _)). rewrite Hxy. apply Ropp_involutive. Qed. diff --git a/src/Prop/Fprop_relative.v b/src/Prop/Fprop_relative.v index d49c3a1592de3fce2424d52bda880d22730d1538..16181eca4a3411dd908876ed004687421959d135 100644 --- a/src/Prop/Fprop_relative.v +++ b/src/Prop/Fprop_relative.v @@ -12,9 +12,9 @@ Hypothesis prop_exp : valid_exp fexp. Theorem generic_relative_error_lt_conversion : forall rnd x b, (0 < b)%R -> - (Rabs (rounding beta fexp rnd x - x) < b * Rabs x)%R -> + (Rabs (round beta fexp rnd x - x) < b * Rabs x)%R -> exists eps, - (Rabs eps < b)%R /\ rounding beta fexp rnd x = (x * (1 + eps))%R. + (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R. Proof. intros rnd x b Hb0 Hxb. destruct (Req_dec x 0) as [Hx0|Hx0]. @@ -23,9 +23,9 @@ exists R0. split. now rewrite Rabs_R0. rewrite Hx0, Rmult_0_l. -apply rounding_0. +apply round_0. (* *) -exists ((rounding beta fexp rnd x - x) / x)%R. +exists ((round beta fexp rnd x - x) / x)%R. split. 2: now field. unfold Rdiv. rewrite Rabs_mult. @@ -38,9 +38,9 @@ Qed. Theorem generic_relative_error_le_conversion : forall rnd x b, (0 <= b)%R -> - (Rabs (rounding beta fexp rnd x - x) <= b * Rabs x)%R -> + (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R -> exists eps, - (Rabs eps <= b)%R /\ rounding beta fexp rnd x = (x * (1 + eps))%R. + (Rabs eps <= b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R. Proof. intros rnd x b Hb0 Hxb. destruct (Req_dec x 0) as [Hx0|Hx0]. @@ -49,9 +49,9 @@ exists R0. split. now rewrite Rabs_R0. rewrite Hx0, Rmult_0_l. -apply rounding_0. +apply round_0. (* *) -exists ((rounding beta fexp rnd x - x) / x)%R. +exists ((round beta fexp rnd x - x) / x)%R. split. 2: now field. unfold Rdiv. rewrite Rabs_mult. @@ -62,7 +62,7 @@ rewrite Rinv_l with (1 := Hx0). now rewrite Rabs_R1, Rmult_1_r. Qed. -Variable rnd : Zrounding. +Variable rnd : Zround. Variable emin p : Z. Hypothesis Hmin : forall k, (emin < k)%Z -> (p <= k - fexp k)%Z. @@ -70,7 +70,7 @@ Hypothesis Hmin : forall k, (emin < k)%Z -> (p <= k - fexp k)%Z. Theorem generic_relative_error : forall x, (bpow emin <= Rabs x)%R -> - (Rabs (rounding beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R. + (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R. Proof. intros x Hx. apply Rlt_le_trans with (ulp beta fexp x)%R. @@ -85,7 +85,7 @@ destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. -rewrite <- bpow_add. +rewrite <- bpow_plus. apply -> bpow_le. assert (emin < ex)%Z. apply <- bpow_lt. @@ -102,7 +102,7 @@ Theorem generic_relative_error_ex : forall x, (bpow emin <= Rabs x)%R -> exists eps, - (Rabs eps < bpow (-p + 1))%R /\ rounding beta fexp rnd x = (x * (1 + eps))%R. + (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R. Proof. intros x Hx. apply generic_relative_error_lt_conversion. @@ -113,7 +113,7 @@ Qed. Theorem generic_relative_error_F2R : forall m, let x := F2R (Float beta m emin) in (x <> 0)%R -> - (Rabs (rounding beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R. + (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R. Proof. intros m x Hx. apply generic_relative_error. @@ -129,7 +129,7 @@ Theorem generic_relative_error_F2R_ex : forall m, let x := F2R (Float beta m emin) in (x <> 0)%R -> exists eps, - (Rabs eps < bpow (-p + 1))%R /\ rounding beta fexp rnd x = (x * (1 + eps))%R. + (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R. Proof. intros m x Hx. apply generic_relative_error_lt_conversion. @@ -141,7 +141,7 @@ Theorem generic_relative_error_2 : (0 < p)%Z -> forall x, (bpow emin <= Rabs x)%R -> - (Rabs (rounding beta fexp rnd x - x) < bpow (-p + 1) * Rabs (rounding beta fexp rnd x))%R. + (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R. Proof. intros Hp x Hx. apply Rlt_le_trans with (ulp beta fexp x)%R. @@ -160,19 +160,19 @@ apply <- bpow_lt. apply Rle_lt_trans with (2 := proj2 He). exact Hx. apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. -rewrite <- bpow_add. +rewrite <- bpow_plus. apply -> bpow_le. generalize (Hmin ex). omega. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. -apply rounding_abs_abs. +apply round_abs_abs. exact prop_exp. clear rnd x Hx Hx' He. intros rnd x Hx. -rewrite <- (rounding_generic beta fexp rnd (bpow (ex - 1))). -now apply rounding_monotone. +rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). +now apply round_monotone. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). @@ -183,7 +183,7 @@ Theorem generic_relative_error_F2R_2 : (0 < p)%Z -> forall m, let x := F2R (Float beta m emin) in (x <> 0)%R -> - (Rabs (rounding beta fexp rnd x - x) < bpow (-p + 1) * Rabs (rounding beta fexp rnd x))%R. + (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R. Proof. intros Hp m x Hx. apply generic_relative_error_2. @@ -201,7 +201,7 @@ Variable choice : R -> bool. Theorem generic_relative_error_N : forall x, (bpow emin <= Rabs x)%R -> - (Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R. + (Rabs (round beta fexp (rndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R. Proof. intros x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. @@ -221,7 +221,7 @@ destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. -rewrite <- bpow_add. +rewrite <- bpow_plus. apply -> bpow_le. assert (emin < ex)%Z. apply <- bpow_lt. @@ -238,7 +238,7 @@ Theorem generic_relative_error_N_ex : forall x, (bpow emin <= Rabs x)%R -> exists eps, - (Rabs eps <= /2 * bpow (-p + 1))%R /\ rounding beta fexp (ZrndN choice) x = (x * (1 + eps))%R. + (Rabs eps <= /2 * bpow (-p + 1))%R /\ round beta fexp (rndN choice) x = (x * (1 + eps))%R. Proof. intros x Hx. apply generic_relative_error_le_conversion. @@ -252,12 +252,12 @@ Qed. Theorem generic_relative_error_N_F2R : forall m, let x := F2R (Float beta m emin) in - (Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R. + (Rabs (round beta fexp (rndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R. Proof. intros m x. destruct (Req_dec x 0) as [Hx|Hx]. (* . *) -rewrite Hx, rounding_0. +rewrite Hx, round_0. unfold Rminus. rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0. rewrite Rmult_0_r. @@ -275,7 +275,7 @@ Qed. Theorem generic_relative_error_N_F2R_ex : forall m, let x := F2R (Float beta m emin) in exists eps, - (Rabs eps <= /2 * bpow (-p + 1))%R /\ rounding beta fexp (ZrndN choice) x = (x * (1 + eps))%R. + (Rabs eps <= /2 * bpow (-p + 1))%R /\ round beta fexp (rndN choice) x = (x * (1 + eps))%R. Proof. intros m x. apply generic_relative_error_le_conversion. @@ -291,7 +291,7 @@ Theorem generic_relative_error_N_2 : (0 < p)%Z -> forall x, (bpow emin <= Rabs x)%R -> - (Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs (rounding beta fexp (ZrndN choice) x))%R. + (Rabs (round beta fexp (rndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs (round beta fexp (rndN choice) x))%R. Proof. intros Hp x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. @@ -315,19 +315,19 @@ apply <- bpow_lt. apply Rle_lt_trans with (2 := proj2 He). exact Hx. apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. -rewrite <- bpow_add. +rewrite <- bpow_plus. apply -> bpow_le. generalize (Hmin ex). omega. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. -apply rounding_abs_abs. +apply round_abs_abs. exact prop_exp. clear rnd x Hx Hx' He. intros rnd x Hx. -rewrite <- (rounding_generic beta fexp rnd (bpow (ex - 1))). -now apply rounding_monotone. +rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). +now apply round_monotone. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). @@ -337,12 +337,12 @@ Qed. Theorem generic_relative_error_N_F2R_2 : (0 < p)%Z -> forall m, let x := F2R (Float beta m emin) in - (Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs (rounding beta fexp (ZrndN choice) x))%R. + (Rabs (round beta fexp (rndN choice) x - x) <= /2 * bpow (-p + 1) * Rabs (round beta fexp (rndN choice) x))%R. Proof. intros Hp m x. destruct (Req_dec x 0) as [Hx|Hx]. (* . *) -rewrite Hx, rounding_0. +rewrite Hx, round_0. unfold Rminus. rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0. rewrite Rmult_0_r. @@ -364,12 +364,12 @@ Section Fprop_relative_FLT. Variable emin prec : Z. Variable Hp : Zlt 0 prec. -Variable rnd : Zrounding. +Variable rnd : Zround. Theorem relative_error_FLT_F2R : forall m, let x := F2R (Float beta m (emin + prec - 1)) in (x <> 0)%R -> - (Rabs (rounding beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. + (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. Proof. intros m x Hx. apply generic_relative_error_F2R. @@ -384,7 +384,7 @@ Qed. Theorem relative_error_FLT : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> - (Rabs (rounding beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. + (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. Proof. intros x Hx. apply generic_relative_error with (emin + prec - 1)%Z. @@ -400,7 +400,7 @@ Theorem relative_error_FLT_F2R_ex : forall m, let x := F2R (Float beta m (emin + prec - 1)) in (x <> 0)%R -> exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ rounding beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. + (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. Proof. intros m x Hx. apply generic_relative_error_lt_conversion. @@ -412,7 +412,7 @@ Theorem relative_error_FLT_ex : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ rounding beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. + (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. Proof. intros x Hx. apply generic_relative_error_lt_conversion. @@ -425,7 +425,7 @@ Variable choice : R -> bool. Theorem relative_error_N_FLT : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> - (Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. + (Rabs (round beta (FLT_exp emin prec) (rndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. Proof. intros x Hx. apply generic_relative_error_N with (emin + prec - 1)%Z. @@ -441,7 +441,7 @@ Theorem relative_error_N_FLT_ex : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> exists eps, - (Rabs eps <= /2 * bpow (-prec + 1))%R /\ rounding beta (FLT_exp emin prec) (ZrndN choice) x = (x * (1 + eps))%R. + (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (rndN choice) x = (x * (1 + eps))%R. Proof. intros x Hx. apply generic_relative_error_le_conversion. @@ -456,7 +456,7 @@ Qed. Theorem relative_error_N_FLT_2 : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> - (Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x))%R. + (Rabs (round beta (FLT_exp emin prec) (rndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (rndN choice) x))%R. Proof. intros x Hx. apply generic_relative_error_N_2 with (emin + prec - 1)%Z. @@ -471,7 +471,7 @@ Qed. Theorem relative_error_N_FLT_F2R : forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. + (Rabs (round beta (FLT_exp emin prec) (rndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. Proof. intros m x. apply generic_relative_error_N_F2R. @@ -485,7 +485,7 @@ Qed. Theorem relative_error_N_FLT_F2R_ex : forall m, let x := F2R (Float beta m (emin + prec - 1)) in exists eps, - (Rabs eps <= /2 * bpow (-prec + 1))%R /\ rounding beta (FLT_exp emin prec) (ZrndN choice) x = (x * (1 + eps))%R. + (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (rndN choice) x = (x * (1 + eps))%R. Proof. intros m x. apply generic_relative_error_le_conversion. @@ -499,7 +499,7 @@ Qed. Theorem relative_error_N_FLT_F2R_2 : forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (rounding beta (FLT_exp emin prec) (ZrndN choice) x))%R. + (Rabs (round beta (FLT_exp emin prec) (rndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (rndN choice) x))%R. Proof. intros m x. apply generic_relative_error_N_F2R_2. @@ -519,7 +519,7 @@ Theorem error_N_FLT_aux : (Rabs eps <= /2 * bpow (-prec + 1))%R /\ (Rabs eta <= /2 * bpow (emin))%R /\ (eps*eta=0)%R /\ - rounding beta (FLT_exp emin prec) (ZrndN choice) x = (x * (1 + eps) + eta)%R. + round beta (FLT_exp emin prec) (rndN choice) x = (x * (1 + eps) + eta)%R. Proof. intros x Hx2. case (Rle_or_lt (bpow (emin+prec)) x); intros Hx. @@ -538,7 +538,7 @@ apply bpow_ge_0. split;[apply Rmult_0_r|idtac]. now rewrite Rplus_0_r. (* *) -exists 0%R; exists (rounding beta (FLT_exp emin prec) (ZrndN choice) x - x)%R. +exists 0%R; exists (round beta (FLT_exp emin prec) (rndN choice) x - x)%R. split. rewrite Rabs_R0; apply Rmult_le_pos. auto with real. @@ -571,12 +571,12 @@ Section Fprop_relative_FLX. Variable prec : Z. Variable Hp : Zlt 0 prec. -Variable rnd : Zrounding. +Variable rnd : Zround. Theorem relative_error_FLX : forall x, (x <> 0)%R -> - (Rabs (rounding beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. + (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. Proof. intros x Hx. destruct (ln_beta beta x) as (ex, He). @@ -593,7 +593,7 @@ Theorem relative_error_FLX_ex : forall x, (x <> 0)%R -> exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ rounding beta (FLX_exp prec) rnd x = (x * (1 + eps))%R. + (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R. Proof. intros x Hx. apply generic_relative_error_lt_conversion. @@ -604,7 +604,7 @@ Qed. Theorem relative_error_FLX_2 : forall x, (x <> 0)%R -> - (Rabs (rounding beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs (rounding beta (FLX_exp prec) rnd x))%R. + (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs (round beta (FLX_exp prec) rnd x))%R. Proof. intros x Hx. destruct (ln_beta beta x) as (ex, He). @@ -622,12 +622,12 @@ Variable choice : R -> bool. Theorem relative_error_N_FLX : forall x, - (Rabs (rounding beta (FLX_exp prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. + (Rabs (round beta (FLX_exp prec) (rndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. Proof. intros x. destruct (Req_dec x 0) as [Hx|Hx]. (* . *) -rewrite Hx, rounding_0. +rewrite Hx, round_0. unfold Rminus. rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0. rewrite Rmult_0_r. @@ -646,7 +646,7 @@ Qed. Theorem relative_error_N_FLX_ex : forall x, exists eps, - (Rabs eps <= /2 * bpow (-prec + 1))%R /\ rounding beta (FLX_exp prec) (ZrndN choice) x = (x * (1 + eps))%R. + (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLX_exp prec) (rndN choice) x = (x * (1 + eps))%R. Proof. intros x. apply generic_relative_error_le_conversion. @@ -660,12 +660,12 @@ Qed. Theorem relative_error_N_FLX_2 : forall x, - (Rabs (rounding beta (FLX_exp prec) (ZrndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (rounding beta (FLX_exp prec) (ZrndN choice) x))%R. + (Rabs (round beta (FLX_exp prec) (rndN choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLX_exp prec) (rndN choice) x))%R. Proof. intros x. destruct (Req_dec x 0) as [Hx|Hx]. (* . *) -rewrite Hx, rounding_0. +rewrite Hx, round_0. unfold Rminus. rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0. rewrite Rmult_0_r.