Remove useless hypothesis from relative_error_*_ex.

src/Prop/Fprop_relative.v

@@ -35,9 +35,9 @@ Section relative_error_conversion.
 Variable rnd : R -> Z.
 Context { valid_rnd : Valid_rnd rnd }.
 
-Lemma relative_error_lt_conversion :
+Lemma relative_error_lt_conversion' :
   forall x b, (0 < b)%R ->
-  (Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
+  (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
   exists eps,
   (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
@@ -50,6 +50,7 @@ now rewrite Rabs_R0.
 rewrite Hx0, Rmult_0_l.
 apply round_0...
 (* *)
+specialize (Hxb Hx0).
 exists ((round beta fexp rnd x - x) / x)%R.
 split. 2: now field.
 unfold Rdiv.
@@ -61,6 +62,19 @@ rewrite Rinv_l with (1 := Hx0).
 now rewrite Rabs_R1, Rmult_1_r.
 Qed.
 
+(* TODO: remove *)
+Lemma relative_error_lt_conversion :
+  forall x b, (0 < b)%R ->
+  (Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
+  exists eps,
+  (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
+Proof.
+intros x b Hb0 Hxb.
+apply relative_error_lt_conversion'.
+exact Hb0.
+now intros _.
+Qed.
+
 Lemma relative_error_le_conversion :
   forall x b, (0 <= b)%R ->
   (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R ->
@@ -154,18 +168,28 @@ rewrite F2R_0, F2R_Zabs.
 now apply Rabs_pos_lt.
 Qed.
 
-Theorem relative_error_F2R_emin_ex :
+Theorem relative_error_F2R_emin_ex' :
   forall m, let x := F2R (Float beta m emin) in
-  (x <> 0)%R ->
   exists eps,
   (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
-intros m x Hx.
-apply relative_error_lt_conversion...
+intros m x.
+apply relative_error_lt_conversion'...
 apply bpow_gt_0.
 now apply relative_error_F2R_emin.
 Qed.
 
+(* TODO: remove *)
+Theorem relative_error_F2R_emin_ex :
+  forall m, let x := F2R (Float beta m emin) in
+  (x <> 0)%R ->
+  exists eps,
+  (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
+Proof with auto with typeclass_instances.
+intros m x _.
+apply relative_error_F2R_emin_ex'.
+Qed.
+
 Theorem relative_error_round :
   (0 < p)%Z ->
   forall x,
@@ -424,18 +448,28 @@ apply relative_error with (emin + prec - 1)%Z...
 apply relative_error_FLT_aux.
 Qed.
 
-Theorem relative_error_FLT_F2R_emin_ex :
+Theorem relative_error_FLT_F2R_emin_ex' :
   forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (x <> 0)%R ->
   exists eps,
   (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
-intros m x Hx.
-apply relative_error_lt_conversion...
+intros m x.
+apply relative_error_lt_conversion'...
 apply bpow_gt_0.
 now apply relative_error_FLT_F2R_emin.
 Qed.
 
+(* TODO: remove *)
+Theorem relative_error_FLT_F2R_emin_ex :
+  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
+  (x <> 0)%R ->
+  exists eps,
+  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
+Proof with auto with typeclass_instances.
+intros m x _.
+apply relative_error_FLT_F2R_emin_ex'.
+Qed.
+
 (** 1+#&epsilon;# property in any rounding in FLT *)
 Theorem relative_error_FLT_ex :
   forall x,
@@ -606,18 +640,28 @@ apply He.
 Qed.
 
 (** 1+#&epsilon;# property in any rounding in FLX *)
-Theorem relative_error_FLX_ex :
+Theorem relative_error_FLX_ex' :
   forall x,
-  (x <> 0)%R ->
   exists eps,
   (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
-intros x Hx.
-apply relative_error_lt_conversion...
+intros x.
+apply relative_error_lt_conversion'...
 apply bpow_gt_0.
 now apply relative_error_FLX.
 Qed.
 
+(* TODO: remove *)
+Theorem relative_error_FLX_ex :
+  forall x,
+  (x <> 0)%R ->
+  exists eps,
+  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R.
+Proof with auto with typeclass_instances.
+intros x _.
+apply relative_error_FLX_ex'.
+Qed.
+
 Theorem relative_error_FLX_round :
   forall x,
   (x <> 0)%R ->