Commit 0417a82b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Change some R0 to 0%R.

parent f91c2225
......@@ -134,7 +134,7 @@ Qed.
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec (f : float beta) :
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(x <> 0%R -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
FLXN_format x.
Theorem generic_format_FLXN :
......
......@@ -34,7 +34,7 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Inductive FTZ_format (x : R) : Prop :=
FTZ_spec (f : float beta) :
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(x <> 0%R -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z ->
FTZ_format x.
......@@ -189,7 +189,8 @@ apply Zle_refl.
omega.
Qed.
Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1).
Theorem ulp_FTZ_0 :
ulp beta FTZ_exp 0 = bpow (emin+prec-1).
Proof with auto with typeclass_instances.
unfold ulp; rewrite Req_bool_true; trivial.
case (negligible_exp_spec FTZ_exp).
......@@ -300,7 +301,7 @@ Qed.
Theorem round_FTZ_small :
forall x : R,
(Rabs x < bpow (emin + prec - 1))%R ->
round beta FTZ_exp Zrnd_FTZ x = R0.
round beta FTZ_exp Zrnd_FTZ x = 0%R.
Proof with auto with typeclass_instances.
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
......
......@@ -178,7 +178,7 @@ Qed.
Lemma generic_format_F2R' :
forall (x : R) (f : float beta),
F2R f = x ->
(x <> R0 -> (cexp x <= Fexp f)%Z) ->
(x <> 0%R -> (cexp x <= Fexp f)%Z) ->
generic_format x.
Proof.
intros x f H1 H2.
......@@ -2129,7 +2129,7 @@ Context { valid_exp2 : Valid_exp fexp2 }.
Theorem generic_inclusion_mag :
forall x,
( x <> R0 -> (fexp2 (mag beta x) <= fexp1 (mag beta x))%Z ) ->
( x <> 0%R -> (fexp2 (mag beta x) <= fexp1 (mag beta x))%Z ) ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof.
......
......@@ -97,7 +97,7 @@ Definition ulp x := match Req_bool x 0 with
end.
Lemma ulp_neq_0 :
forall x, x <> R0 ->
forall x, x <> 0%R ->
ulp x = bpow (cexp beta fexp x).
Proof.
intros x Hx.
......@@ -821,7 +821,7 @@ Proof.
intros x Zx Fx Hx.
replace (ulp (x - ulp x)) with (ulp x).
ring.
assert (H : x <> R0) by now apply Rgt_not_eq.
assert (H : x <> 0%R) by now apply Rgt_not_eq.
assert (H' : x <> bpow (cexp beta fexp x)).
unfold cexp ; intros M.
case_eq (mag beta x); intros ex Hex T.
......
......@@ -379,7 +379,7 @@ Definition build_nan (x : { x | is_nan x = true }) :=
proj1_sig x.
Theorem B2R_build_nan :
forall x, B2R (build_nan x) = R0.
forall x, B2R (build_nan x) = 0%R.
Proof.
now intros [[| | |] H].
Qed.
......
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