diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v index 6400304be79d4bdd3b4d4ed2749b981b2b8004db..81a2b2d671e3a7e9e8dbfb3e9893699cd3c77573 100644 --- a/src/Appli/Fappli_IEEE.v +++ b/src/Appli/Fappli_IEEE.v @@ -39,7 +39,7 @@ Inductive full_float := Definition FF2R beta x := match x with | F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e) - | _ => R0 + | _ => 0%R end. End AnyRadix. @@ -104,7 +104,7 @@ Definition B2FF x := Definition B2R f := match f with | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e) - | _ => R0 + | _ => 0%R end. Theorem FF2R_B2FF : @@ -1714,7 +1714,7 @@ Definition Bdiv div_nan m x y := Theorem Bdiv_correct : forall div_nan m x y, - B2R y <> R0 -> + B2R y <> 0%R -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\ is_finite (Bdiv div_nan m x y) = is_finite x /\ diff --git a/src/Core/Fcore_FLT.v b/src/Core/Fcore_FLT.v index 8034feede1fb065862ed54b3188d40155336c449..2258b1d9b721fe68931bb530eb9d7117363716a8 100644 --- a/src/Core/Fcore_FLT.v +++ b/src/Core/Fcore_FLT.v @@ -187,7 +187,7 @@ Qed. (** Links between FLT and FIX (underflow) *) Theorem canonic_exp_FLT_FIX : - forall x, x <> R0 -> + forall x, x <> 0%R -> (Rabs x < bpow (emin + prec))%R -> canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x. Proof. diff --git a/src/Core/Fcore_FTZ.v b/src/Core/Fcore_FTZ.v index 2ebc7851897b21c9c29d4bf328e4e60666d1ba3e..a2fab00b3a93ce2c25a28d564e3c9d227934976c 100644 --- a/src/Core/Fcore_FTZ.v +++ b/src/Core/Fcore_FTZ.v @@ -217,7 +217,7 @@ Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. Definition Zrnd_FTZ x := - if Rle_bool R1 (Rabs x) then rnd x else Z0. + if Rle_bool 1 (Rabs x) then rnd x else Z0. Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ. Proof with auto with typeclass_instances. @@ -270,7 +270,7 @@ Proof. intros x Hx. unfold round, scaled_mantissa, canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. -assert (Hx0: x <> R0). +assert (Hx0: x <> 0%R). intros Hx0. apply Rle_not_lt with (1 := Hx). rewrite Hx0, Rabs_R0. @@ -286,7 +286,7 @@ rewrite Rle_bool_true. apply refl_equal. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))). -change R1 with (bpow 0). +change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FLX_exp prec ex)). rewrite bpow_plus. apply Rmult_le_compat_r. @@ -320,7 +320,7 @@ rewrite Rle_bool_false. apply F2R_0. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))). -change R1 with (bpow 0). +change 1%R with (bpow 0). rewrite <- (Zplus_opp_r (FTZ_exp ex)). rewrite bpow_plus. apply Rmult_lt_compat_r. diff --git a/src/Core/Fcore_Raux.v b/src/Core/Fcore_Raux.v index 75e3841beb5798e5e619238cb1e69068c9cabf39..1276494c9753cabfb73421ca206b960da134a200 100644 --- a/src/Core/Fcore_Raux.v +++ b/src/Core/Fcore_Raux.v @@ -1456,7 +1456,7 @@ Definition bpow e := match e with | Zpos p => Z2R (Zpower_pos r p) | Zneg p => Rinv (Z2R (Zpower_pos r p)) - | Z0 => R1 + | Z0 => 1%R end. Theorem Z2R_Zpower_pos : @@ -1875,7 +1875,7 @@ apply bpow_ge_0. Qed. Theorem ln_beta_mult_bpow : - forall x e, x <> R0 -> + forall x e, x <> 0%R -> (ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z. Proof. intros x e Zx. @@ -1898,7 +1898,7 @@ Qed. Theorem ln_beta_le_bpow : forall x e, - x <> R0 -> + x <> 0%R -> (Rabs x < bpow e)%R -> (ln_beta x <= e)%Z. Proof. diff --git a/src/Core/Fcore_float_prop.v b/src/Core/Fcore_float_prop.v index 8199ede6244b72cd04f8463ee895d997a24575ab..a183bf0a8b661d7a2b95be0fe7e235078873b777 100644 --- a/src/Core/Fcore_float_prop.v +++ b/src/Core/Fcore_float_prop.v @@ -136,7 +136,7 @@ Qed. (** Sign facts *) Theorem F2R_0 : forall e : Z, - F2R (Float beta 0 e) = R0. + F2R (Float beta 0 e) = 0%R. Proof. intros e. unfold F2R. simpl. @@ -145,7 +145,7 @@ Qed. Theorem F2R_eq_0_reg : forall m e : Z, - F2R (Float beta m e) = R0 -> + F2R (Float beta m e) = 0%R -> m = Z0. Proof. intros m e H. diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v index 21e518900a576c449bdad102d9b444fa15048b07..1d10b61e6005dcee507f93756269a78d172034f6 100644 --- a/src/Core/Fcore_generic_fmt.v +++ b/src/Core/Fcore_generic_fmt.v @@ -252,7 +252,7 @@ apply Rmult_1_r. Qed. Theorem scaled_mantissa_0 : - scaled_mantissa 0 = R0. + scaled_mantissa 0 = 0%R. Proof. apply Rmult_0_l. Qed. @@ -667,7 +667,7 @@ Theorem round_bounded_small_pos : forall x ex, (ex <= fexp ex)%Z -> (bpow (ex - 1) <= x < bpow ex)%R -> - round x = R0 \/ round x = bpow (fexp ex). + round x = 0%R \/ round x = bpow (fexp ex). Proof. intros x ex He Hx. unfold round, scaled_mantissa. @@ -751,7 +751,7 @@ now apply sym_eq. Qed. Theorem round_0 : - round 0 = R0. + round 0 = 0%R. Proof. unfold round, scaled_mantissa. rewrite Rmult_0_l. @@ -762,8 +762,8 @@ Qed. Theorem exp_small_round_0_pos : forall x ex, - (bpow (ex - 1) <= x < bpow ex)%R -> - round x =R0 -> (ex <= fexp ex)%Z . + (bpow (ex - 1) <= x < bpow ex)%R -> + round x = 0%R -> (ex <= fexp ex)%Z . Proof. intros x ex H H1. case (Zle_or_lt ex (fexp ex)); trivial; intros V. @@ -771,7 +771,7 @@ contradict H1. apply Rgt_not_eq. apply Rlt_le_trans with (bpow (ex-1)). apply bpow_gt_0. -apply (round_bounded_large_pos); assumption. +apply (round_bounded_large_pos); assumption. Qed. Theorem generic_format_round_pos : @@ -931,7 +931,7 @@ rewrite <- Ropp_0. now apply Ropp_lt_contravar. now apply Ropp_le_contravar. (* . 0 <= y *) -apply Rle_trans with R0. +apply Rle_trans with 0%R. apply F2R_le_0_compat. simpl. rewrite <- (Zrnd_Z2R rnd 0). apply Zrnd_le... @@ -1020,7 +1020,7 @@ Qed. Theorem exp_small_round_0 : forall rnd {Hr : Valid_rnd rnd} x ex, (bpow (ex - 1) <= Rabs x < bpow ex)%R -> - round rnd x =R0 -> (ex <= fexp ex)%Z . + round rnd x = 0%R -> (ex <= fexp ex)%Z . Proof. intros rnd Hr x ex H1 H2. generalize Rabs_R0. @@ -1296,7 +1296,7 @@ Theorem round_DN_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> - round Zfloor x = R0. + round Zfloor x = 0%R. Proof. intros x ex Hx He. rewrite <- (F2R_0 beta (canonic_exp x)). @@ -1552,7 +1552,7 @@ Qed. Lemma canonic_exp_le_bpow : forall (x : R) (e : Z), - x <> R0 -> + x <> 0%R -> (Rabs x < bpow e)%R -> (canonic_exp x <= fexp e)%Z. Proof. @@ -1578,7 +1578,7 @@ Context { valid_rnd : Valid_rnd rnd }. Theorem ln_beta_round_ge : forall x, - round rnd x <> R0 -> + round rnd x <> 0%R -> (ln_beta beta x <= ln_beta beta (round rnd x))%Z. Proof with auto with typeclass_instances. intros x. @@ -1597,7 +1597,7 @@ Qed. Theorem canonic_exp_round_ge : forall x, - round rnd x <> R0 -> + round rnd x <> 0%R -> (canonic_exp x <= canonic_exp (round rnd x))%Z. Proof with auto with typeclass_instances. intros x Zr. @@ -1807,7 +1807,7 @@ rewrite Zceil_floor_neq. rewrite Z2R_plus. simpl. apply Ropp_lt_cancel. -apply Rplus_lt_reg_l with R1. +apply Rplus_lt_reg_l with 1%R. replace (1 + -/2)%R with (/2)%R by field. now replace (1 + - (Z2R (Zfloor x) + 1 - x))%R with (x - Z2R (Zfloor x))%R by ring. apply Rlt_not_eq. @@ -1866,7 +1866,7 @@ rewrite Z2R_abs, Z2R_minus. replace (Z2R (Znearest x) - Z2R n)%R with (- (x - Z2R (Znearest x)) + (x - Z2R n))%R by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). simpl. -replace R1 with (/2 + /2)%R by field. +replace 1%R with (/2 + /2)%R by field. apply Rplus_le_lt_compat with (2 := Hd). rewrite Rabs_Ropp. apply Znearest_N. diff --git a/src/Core/Fcore_ulp.v b/src/Core/Fcore_ulp.v index c1c88893dde9623f6a6bee5d7fa98d260516aaf7..add7adb2aec4653ea3e8077e27fb385190d16651 100644 --- a/src/Core/Fcore_ulp.v +++ b/src/Core/Fcore_ulp.v @@ -1514,7 +1514,7 @@ now apply pred_pos_plus_ulp. Qed. Theorem pred_ulp_0 : - pred (ulp 0) = R0. + pred (ulp 0) = 0%R. Proof. rewrite pred_eq_pos. 2: apply ulp_ge_0. diff --git a/src/Prop/Fprop_div_sqrt_error.v b/src/Prop/Fprop_div_sqrt_error.v index 9d29001d625f5dd56bb9f22fb611624f13d66c6c..c56d1debfd1aad02e855696514dd514a2d35b3dd 100644 --- a/src/Prop/Fprop_div_sqrt_error.v +++ b/src/Prop/Fprop_div_sqrt_error.v @@ -103,7 +103,7 @@ apply Rlt_le_trans with (Rabs x * 1)%R. apply Rmult_lt_compat_l. now apply Rabs_pos_lt. apply Rlt_le_trans with (1 := Heps1). -change R1 with (bpow 0). +change 1%R with (bpow 0). apply bpow_le. generalize (prec_gt_0 prec). clear ; omega. diff --git a/src/Prop/Fprop_plus_error.v b/src/Prop/Fprop_plus_error.v index 7842014a86e97cd6ce5a917f858de678f4f11f06..38c7bb0e726e7438be445bdbd9c8dc2853bed14d 100644 --- a/src/Prop/Fprop_plus_error.v +++ b/src/Prop/Fprop_plus_error.v @@ -158,7 +158,7 @@ Lemma round_plus_eq_zero_aux : (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z -> format x -> format y -> (0 <= x + y)%R -> - round beta fexp rnd (x + y) = R0 -> + round beta fexp rnd (x + y) = 0%R -> (x + y = 0)%R. Proof with auto with typeclass_instances. intros x y He Hx Hy Hp Hxy. @@ -203,11 +203,11 @@ Context { valid_rnd : Valid_rnd rnd }. Theorem round_plus_eq_zero : forall x y, format x -> format y -> - round beta fexp rnd (x + y) = R0 -> + round beta fexp rnd (x + y) = 0%R -> (x + y = 0)%R. Proof with auto with typeclass_instances. intros x y Hx Hy. -destruct (Rle_or_lt R0 (x + y)) as [H1|H1]. +destruct (Rle_or_lt 0 (x + y)) as [H1|H1]. (* . *) revert H1. destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2]. diff --git a/src/Prop/Fprop_relative.v b/src/Prop/Fprop_relative.v index 585b71da940d0068d045f1f11789f7ce7723f90e..7e673c2eb090521fe89b8560cb762dbb3c0d377b 100644 --- a/src/Prop/Fprop_relative.v +++ b/src/Prop/Fprop_relative.v @@ -44,7 +44,7 @@ Proof with auto with typeclass_instances. intros x b Hb0 Hxb. destruct (Req_dec x 0) as [Hx0|Hx0]. (* *) -exists R0. +exists 0%R. split. now rewrite Rabs_R0. rewrite Hx0, Rmult_0_l. @@ -71,7 +71,7 @@ Proof with auto with typeclass_instances. intros x b Hb0 Hxb. destruct (Req_dec x 0) as [Hx0|Hx0]. (* *) -exists R0. +exists 0%R. split. now rewrite Rabs_R0. rewrite Hx0, Rmult_0_l. @@ -650,7 +650,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]]. { apply (Rmult_le_reg_l 2 _ _ Rlt_0_2). rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|]. apply Rgt_not_eq, Rlt_gt, Rlt_0_2. } - exists R0; exists R0; rewrite Zx; split; [|split; [|split]]. + exists 0%R; exists 0%R; rewrite Zx; split; [|split; [|split]]. { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. } { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. } { now rewrite Rmult_0_l. }