Commit 3e0176c2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid using R0 and R1.

parent d47e4c8f
...@@ -39,7 +39,7 @@ Inductive full_float := ...@@ -39,7 +39,7 @@ Inductive full_float :=
Definition FF2R beta x := Definition FF2R beta x :=
match x with match x with
| F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e) | F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e)
| _ => R0 | _ => 0%R
end. end.
End AnyRadix. End AnyRadix.
...@@ -104,7 +104,7 @@ Definition B2FF x := ...@@ -104,7 +104,7 @@ Definition B2FF x :=
Definition B2R f := Definition B2R f :=
match f with match f with
| B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e) | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
| _ => R0 | _ => 0%R
end. end.
Theorem FF2R_B2FF : Theorem FF2R_B2FF :
...@@ -1714,7 +1714,7 @@ Definition Bdiv div_nan m x y := ...@@ -1714,7 +1714,7 @@ Definition Bdiv div_nan m x y :=
Theorem Bdiv_correct : Theorem Bdiv_correct :
forall div_nan m x y, 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 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) /\ 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 /\ is_finite (Bdiv div_nan m x y) = is_finite x /\
......
...@@ -187,7 +187,7 @@ Qed. ...@@ -187,7 +187,7 @@ Qed.
(** Links between FLT and FIX (underflow) *) (** Links between FLT and FIX (underflow) *)
Theorem canonic_exp_FLT_FIX : Theorem canonic_exp_FLT_FIX :
forall x, x <> R0 -> forall x, x <> 0%R ->
(Rabs x < bpow (emin + prec))%R -> (Rabs x < bpow (emin + prec))%R ->
canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x. canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
Proof. Proof.
......
...@@ -217,7 +217,7 @@ Variable rnd : R -> Z. ...@@ -217,7 +217,7 @@ Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }. Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_FTZ x := 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. Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
...@@ -270,7 +270,7 @@ Proof. ...@@ -270,7 +270,7 @@ Proof.
intros x Hx. intros x Hx.
unfold round, scaled_mantissa, canonic_exp. unfold round, scaled_mantissa, canonic_exp.
destruct (ln_beta beta x) as (ex, He). simpl. destruct (ln_beta beta x) as (ex, He). simpl.
assert (Hx0: x <> R0). assert (Hx0: x <> 0%R).
intros Hx0. intros Hx0.
apply Rle_not_lt with (1 := Hx). apply Rle_not_lt with (1 := Hx).
rewrite Hx0, Rabs_R0. rewrite Hx0, Rabs_R0.
...@@ -286,7 +286,7 @@ rewrite Rle_bool_true. ...@@ -286,7 +286,7 @@ rewrite Rle_bool_true.
apply refl_equal. apply refl_equal.
rewrite Rabs_mult. rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))). 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 <- (Zplus_opp_r (FLX_exp prec ex)).
rewrite bpow_plus. rewrite bpow_plus.
apply Rmult_le_compat_r. apply Rmult_le_compat_r.
...@@ -320,7 +320,7 @@ rewrite Rle_bool_false. ...@@ -320,7 +320,7 @@ rewrite Rle_bool_false.
apply F2R_0. apply F2R_0.
rewrite Rabs_mult. rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))). 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 <- (Zplus_opp_r (FTZ_exp ex)).
rewrite bpow_plus. rewrite bpow_plus.
apply Rmult_lt_compat_r. apply Rmult_lt_compat_r.
......
...@@ -1456,7 +1456,7 @@ Definition bpow e := ...@@ -1456,7 +1456,7 @@ Definition bpow e :=
match e with match e with
| Zpos p => Z2R (Zpower_pos r p) | Zpos p => Z2R (Zpower_pos r p)
| Zneg p => Rinv (Z2R (Zpower_pos r p)) | Zneg p => Rinv (Z2R (Zpower_pos r p))
| Z0 => R1 | Z0 => 1%R
end. end.
Theorem Z2R_Zpower_pos : Theorem Z2R_Zpower_pos :
...@@ -1875,7 +1875,7 @@ apply bpow_ge_0. ...@@ -1875,7 +1875,7 @@ apply bpow_ge_0.
Qed. Qed.
Theorem ln_beta_mult_bpow : 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. (ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z.
Proof. Proof.
intros x e Zx. intros x e Zx.
...@@ -1898,7 +1898,7 @@ Qed. ...@@ -1898,7 +1898,7 @@ Qed.
Theorem ln_beta_le_bpow : Theorem ln_beta_le_bpow :
forall x e, forall x e,
x <> R0 -> x <> 0%R ->
(Rabs x < bpow e)%R -> (Rabs x < bpow e)%R ->
(ln_beta x <= e)%Z. (ln_beta x <= e)%Z.
Proof. Proof.
......
...@@ -136,7 +136,7 @@ Qed. ...@@ -136,7 +136,7 @@ Qed.
(** Sign facts *) (** Sign facts *)
Theorem F2R_0 : Theorem F2R_0 :
forall e : Z, forall e : Z,
F2R (Float beta 0 e) = R0. F2R (Float beta 0 e) = 0%R.
Proof. Proof.
intros e. intros e.
unfold F2R. simpl. unfold F2R. simpl.
...@@ -145,7 +145,7 @@ Qed. ...@@ -145,7 +145,7 @@ Qed.
Theorem F2R_eq_0_reg : Theorem F2R_eq_0_reg :
forall m e : Z, forall m e : Z,
F2R (Float beta m e) = R0 -> F2R (Float beta m e) = 0%R ->
m = Z0. m = Z0.
Proof. Proof.
intros m e H. intros m e H.
......
...@@ -252,7 +252,7 @@ apply Rmult_1_r. ...@@ -252,7 +252,7 @@ apply Rmult_1_r.
Qed. Qed.
Theorem scaled_mantissa_0 : Theorem scaled_mantissa_0 :
scaled_mantissa 0 = R0. scaled_mantissa 0 = 0%R.
Proof. Proof.
apply Rmult_0_l. apply Rmult_0_l.
Qed. Qed.
...@@ -667,7 +667,7 @@ Theorem round_bounded_small_pos : ...@@ -667,7 +667,7 @@ Theorem round_bounded_small_pos :
forall x ex, forall x ex,
(ex <= fexp ex)%Z -> (ex <= fexp ex)%Z ->
(bpow (ex - 1) <= x < bpow ex)%R -> (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. Proof.
intros x ex He Hx. intros x ex He Hx.
unfold round, scaled_mantissa. unfold round, scaled_mantissa.
...@@ -751,7 +751,7 @@ now apply sym_eq. ...@@ -751,7 +751,7 @@ now apply sym_eq.
Qed. Qed.
Theorem round_0 : Theorem round_0 :
round 0 = R0. round 0 = 0%R.
Proof. Proof.
unfold round, scaled_mantissa. unfold round, scaled_mantissa.
rewrite Rmult_0_l. rewrite Rmult_0_l.
...@@ -762,8 +762,8 @@ Qed. ...@@ -762,8 +762,8 @@ Qed.
Theorem exp_small_round_0_pos : Theorem exp_small_round_0_pos :
forall x ex, forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R -> (bpow (ex - 1) <= x < bpow ex)%R ->
round x =R0 -> (ex <= fexp ex)%Z . round x = 0%R -> (ex <= fexp ex)%Z .
Proof. Proof.
intros x ex H H1. intros x ex H H1.
case (Zle_or_lt ex (fexp ex)); trivial; intros V. case (Zle_or_lt ex (fexp ex)); trivial; intros V.
...@@ -771,7 +771,7 @@ contradict H1. ...@@ -771,7 +771,7 @@ contradict H1.
apply Rgt_not_eq. apply Rgt_not_eq.
apply Rlt_le_trans with (bpow (ex-1)). apply Rlt_le_trans with (bpow (ex-1)).
apply bpow_gt_0. apply bpow_gt_0.
apply (round_bounded_large_pos); assumption. apply (round_bounded_large_pos); assumption.
Qed. Qed.
Theorem generic_format_round_pos : Theorem generic_format_round_pos :
...@@ -931,7 +931,7 @@ rewrite <- Ropp_0. ...@@ -931,7 +931,7 @@ rewrite <- Ropp_0.
now apply Ropp_lt_contravar. now apply Ropp_lt_contravar.
now apply Ropp_le_contravar. now apply Ropp_le_contravar.
(* . 0 <= y *) (* . 0 <= y *)
apply Rle_trans with R0. apply Rle_trans with 0%R.
apply F2R_le_0_compat. simpl. apply F2R_le_0_compat. simpl.
rewrite <- (Zrnd_Z2R rnd 0). rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_le... apply Zrnd_le...
...@@ -1020,7 +1020,7 @@ Qed. ...@@ -1020,7 +1020,7 @@ Qed.
Theorem exp_small_round_0 : Theorem exp_small_round_0 :
forall rnd {Hr : Valid_rnd rnd} x ex, forall rnd {Hr : Valid_rnd rnd} x ex,
(bpow (ex - 1) <= Rabs x < bpow ex)%R -> (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. Proof.
intros rnd Hr x ex H1 H2. intros rnd Hr x ex H1 H2.
generalize Rabs_R0. generalize Rabs_R0.
...@@ -1296,7 +1296,7 @@ Theorem round_DN_small_pos : ...@@ -1296,7 +1296,7 @@ Theorem round_DN_small_pos :
forall x ex, forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R -> (bpow (ex - 1) <= x < bpow ex)%R ->
(ex <= fexp ex)%Z -> (ex <= fexp ex)%Z ->
round Zfloor x = R0. round Zfloor x = 0%R.
Proof. Proof.
intros x ex Hx He. intros x ex Hx He.
rewrite <- (F2R_0 beta (canonic_exp x)). rewrite <- (F2R_0 beta (canonic_exp x)).
...@@ -1552,7 +1552,7 @@ Qed. ...@@ -1552,7 +1552,7 @@ Qed.
Lemma canonic_exp_le_bpow : Lemma canonic_exp_le_bpow :
forall (x : R) (e : Z), forall (x : R) (e : Z),
x <> R0 -> x <> 0%R ->
(Rabs x < bpow e)%R -> (Rabs x < bpow e)%R ->
(canonic_exp x <= fexp e)%Z. (canonic_exp x <= fexp e)%Z.
Proof. Proof.
...@@ -1578,7 +1578,7 @@ Context { valid_rnd : Valid_rnd rnd }. ...@@ -1578,7 +1578,7 @@ Context { valid_rnd : Valid_rnd rnd }.
Theorem ln_beta_round_ge : Theorem ln_beta_round_ge :
forall x, forall x,
round rnd x <> R0 -> round rnd x <> 0%R ->
(ln_beta beta x <= ln_beta beta (round rnd x))%Z. (ln_beta beta x <= ln_beta beta (round rnd x))%Z.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
intros x. intros x.
...@@ -1597,7 +1597,7 @@ Qed. ...@@ -1597,7 +1597,7 @@ Qed.
Theorem canonic_exp_round_ge : Theorem canonic_exp_round_ge :
forall x, forall x,
round rnd x <> R0 -> round rnd x <> 0%R ->
(canonic_exp x <= canonic_exp (round rnd x))%Z. (canonic_exp x <= canonic_exp (round rnd x))%Z.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
intros x Zr. intros x Zr.
...@@ -1807,7 +1807,7 @@ rewrite Zceil_floor_neq. ...@@ -1807,7 +1807,7 @@ rewrite Zceil_floor_neq.
rewrite Z2R_plus. rewrite Z2R_plus.
simpl. simpl.
apply Ropp_lt_cancel. 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. 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. now replace (1 + - (Z2R (Zfloor x) + 1 - x))%R with (x - Z2R (Zfloor x))%R by ring.
apply Rlt_not_eq. apply Rlt_not_eq.
...@@ -1866,7 +1866,7 @@ rewrite Z2R_abs, Z2R_minus. ...@@ -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. 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 _ _). apply Rle_lt_trans with (1 := Rabs_triang _ _).
simpl. 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). apply Rplus_le_lt_compat with (2 := Hd).
rewrite Rabs_Ropp. rewrite Rabs_Ropp.
apply Znearest_N. apply Znearest_N.
......
...@@ -1514,7 +1514,7 @@ now apply pred_pos_plus_ulp. ...@@ -1514,7 +1514,7 @@ now apply pred_pos_plus_ulp.
Qed. Qed.
Theorem pred_ulp_0 : Theorem pred_ulp_0 :
pred (ulp 0) = R0. pred (ulp 0) = 0%R.
Proof. Proof.
rewrite pred_eq_pos. rewrite pred_eq_pos.
2: apply ulp_ge_0. 2: apply ulp_ge_0.
......
...@@ -103,7 +103,7 @@ apply Rlt_le_trans with (Rabs x * 1)%R. ...@@ -103,7 +103,7 @@ apply Rlt_le_trans with (Rabs x * 1)%R.
apply Rmult_lt_compat_l. apply Rmult_lt_compat_l.
now apply Rabs_pos_lt. now apply Rabs_pos_lt.
apply Rlt_le_trans with (1 := Heps1). apply Rlt_le_trans with (1 := Heps1).
change R1 with (bpow 0). change 1%R with (bpow 0).
apply bpow_le. apply bpow_le.
generalize (prec_gt_0 prec). generalize (prec_gt_0 prec).
clear ; omega. clear ; omega.
......
...@@ -158,7 +158,7 @@ Lemma round_plus_eq_zero_aux : ...@@ -158,7 +158,7 @@ Lemma round_plus_eq_zero_aux :
(canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z -> (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
format x -> format y -> format x -> format y ->
(0 <= x + y)%R -> (0 <= x + y)%R ->
round beta fexp rnd (x + y) = R0 -> round beta fexp rnd (x + y) = 0%R ->
(x + y = 0)%R. (x + y = 0)%R.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
intros x y He Hx Hy Hp Hxy. intros x y He Hx Hy Hp Hxy.
...@@ -203,11 +203,11 @@ Context { valid_rnd : Valid_rnd rnd }. ...@@ -203,11 +203,11 @@ Context { valid_rnd : Valid_rnd rnd }.
Theorem round_plus_eq_zero : Theorem round_plus_eq_zero :
forall x y, forall x y,
format x -> format y -> format x -> format y ->
round beta fexp rnd (x + y) = R0 -> round beta fexp rnd (x + y) = 0%R ->
(x + y = 0)%R. (x + y = 0)%R.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
intros x y Hx Hy. 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. revert H1.
destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2]. destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2].
......
...@@ -44,7 +44,7 @@ Proof with auto with typeclass_instances. ...@@ -44,7 +44,7 @@ Proof with auto with typeclass_instances.
intros x b Hb0 Hxb. intros x b Hb0 Hxb.
destruct (Req_dec x 0) as [Hx0|Hx0]. destruct (Req_dec x 0) as [Hx0|Hx0].
(* *) (* *)
exists R0. exists 0%R.
split. split.
now rewrite Rabs_R0. now rewrite Rabs_R0.
rewrite Hx0, Rmult_0_l. rewrite Hx0, Rmult_0_l.
...@@ -71,7 +71,7 @@ Proof with auto with typeclass_instances. ...@@ -71,7 +71,7 @@ Proof with auto with typeclass_instances.
intros x b Hb0 Hxb. intros x b Hb0 Hxb.
destruct (Req_dec x 0) as [Hx0|Hx0]. destruct (Req_dec x 0) as [Hx0|Hx0].
(* *) (* *)
exists R0. exists 0%R.
split. split.
now rewrite Rabs_R0. now rewrite Rabs_R0.
rewrite Hx0, Rmult_0_l. rewrite Hx0, Rmult_0_l.
...@@ -650,7 +650,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]]. ...@@ -650,7 +650,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
{ apply (Rmult_le_reg_l 2 _ _ Rlt_0_2). { apply (Rmult_le_reg_l 2 _ _ Rlt_0_2).
rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|]. rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|].
apply Rgt_not_eq, Rlt_gt, Rlt_0_2. } 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 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. } { now rewrite Rmult_0_l. }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment