Removing and renaming

NEWS

@@ -6,6 +6,7 @@ TODO
  - changed named, generalized and added lemmas in Fcore_ulp
  - defined a predecessor and successor on both positive, negative and
    zero values (the previous pred has been renamed pred_pos)
+ - removed some hypotheses on lemmas of Fprop_relative
  - More examples have been added
      * Average: proof on Sterbenz's average and correctly-rounded average
 TODO

examples/Double_round_beta_odd.v

@@ -280,7 +280,7 @@ destruct (Rle_or_lt rx2 0) as [Nprx2|Prx2].
     now apply bpow_le. }
 (* 0 < rx2 *)
 assert (Hl2 : ln_beta rx2 = ln_beta x :> Z).
-{ now rewrite Hrx2r; apply ln_beta_round_DN; [|rewrite <- Hrx2r]. }
+{ now rewrite Hrx2r; apply ln_beta_DN; [|rewrite <- Hrx2r]. }
 assert (Hr12 : round beta fexp1 (Znearest choice1) rx2 = rx1).
 { unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
   rewrite Hl2; fold ex1.
@@ -467,7 +467,7 @@ destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1].
       [lra|apply bpow_ge_0|lra|apply bpow_lt]. }
 (* 0 < rx1 *)
 assert (Hl1 : ln_beta rx1 = ln_beta x :> Z).
-{ now apply ln_beta_round_DN. }
+{ now apply ln_beta_DN. }
 assert (Hl2 : ln_beta rx2c = ln_beta x :> Z).
 { apply ln_beta_unique; rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
   replace rx2c with (rx1 + (/ 2 * bpow ex1 + / 2 * bpow ex2));
@@ -1902,7 +1902,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
     - now apply Rlt_le. }
   assert (Hlr : ln_beta x = ln_beta rd :> Z).
   { apply eq_sym.
-      apply ln_beta_round_DN; [exact Vfexp1|].
+      apply ln_beta_DN; [exact Vfexp1|].
       exact Prd. }
   destruct (midpoint_beta_odd_remains_pos rd Prd (fexp1 (ln_beta x))
                                           (fexp2 (ln_beta x)))

src/Appli/Fappli_double_round.v

@@ -2715,7 +2715,7 @@ destruct (Req_dec a 0) as [Za|Nza].
 - (* a <> 0 *)
   assert (Pa : 0 < a); [lra|].
   assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)).
-  { unfold a; apply ln_beta_round_DN.
+  { unfold a; apply ln_beta_DN.
     - exact Vfexp1.
     - now fold a. }
   assert (Hl' : 0 < - (u2 * a) + b * b).
@@ -3143,7 +3143,7 @@ destruct (Req_dec a 0) as [Za|Nza].
 - (* a <> 0 *)
   assert (Pa : 0 < a); [lra|].
   assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)).
-  { unfold a; apply ln_beta_round_DN.
+  { unfold a; apply ln_beta_DN.
     - exact Vfexp1.
     - now fold a. }
   assert (Hl' : 0 < - (u2 * a) + b * b).

src/Appli/Fappli_rnd_odd.v

@@ -536,7 +536,7 @@ Lemma ln_beta_d:  (0< F2R d)%R ->
     (ln_beta beta (F2R d) = ln_beta beta x :>Z).
 Proof with auto with typeclass_instances.
 intros Y.
-rewrite d_eq; apply ln_beta_round_DN...
+rewrite d_eq; apply ln_beta_DN...
 now rewrite <- d_eq.
 Qed.
 

src/Core/Fcore_generic_fmt.v

@@ -1015,7 +1015,7 @@ Qed.
 
 End monotone.
 
-Theorem round_abs_abs' :
+Theorem round_abs_abs :
   forall P : R -> R -> Prop,
   ( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) ->
   forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
@@ -1043,18 +1043,6 @@ apply round_le...
 now apply Rlt_le.
 Qed.
 
-(* TODO: remove *)
-Theorem round_abs_abs :
-  forall P : R -> R -> Prop,
-  ( forall rnd (Hr : Valid_rnd rnd) x, P x (round rnd x) ) ->
-  forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
-Proof.
-intros P HP.
-apply round_abs_abs'.
-intros.
-now apply HP.
-Qed.
-
 Theorem round_bounded_large :
   forall rnd {Hr : Valid_rnd rnd} x ex,
   (fexp ex < ex)%Z ->
@@ -1064,7 +1052,7 @@ Proof with auto with typeclass_instances.
 intros rnd Hr x ex He.
 apply round_abs_abs...
 clear rnd Hr x.
-intros rnd' Hr x.
+intros rnd' Hr x _.
 apply round_bounded_large_pos...
 Qed.
 
@@ -1076,7 +1064,7 @@ Proof.
 intros rnd Hr x ex H1 H2.
 generalize Rabs_R0.
 rewrite <- H2 at 1.
-apply (round_abs_abs' (fun t rt => forall (ex : Z),
+apply (round_abs_abs (fun t rt => forall (ex : Z),
 (bpow (ex - 1) <= t < bpow ex)%R ->
 rt = 0%R -> (ex <= fexp ex)%Z)); trivial.
 clear; intros rnd Hr x Hx.
@@ -1496,7 +1484,7 @@ right.
 now rewrite Zmax_l with (1 := Zlt_le_weak _ _ He).
 Qed.
 
-Theorem ln_beta_round_DN : (* TODO ln_beta_DN  ??? SB ???*)
+Theorem ln_beta_DN :
   forall x,
   (0 < round Zfloor x)%R ->
   (ln_beta beta (round Zfloor x) = ln_beta beta x :> Z).
@@ -1513,7 +1501,6 @@ now apply Rgt_not_eq.
 now apply Rlt_le.
 Qed.
 
-(* TODO: remove *)
 Theorem canonic_exp_DN :
   forall x,
   (0 < round Zfloor x)%R ->
@@ -1521,7 +1508,7 @@ Theorem canonic_exp_DN :
 Proof.
 intros x Hd.
 apply (f_equal fexp).
-now apply ln_beta_round_DN.
+now apply ln_beta_DN.
 Qed.
 
 Theorem scaled_mantissa_DN :
@@ -2312,7 +2299,7 @@ intros x Gx.
 apply generic_format_abs_inv.
 apply generic_format_abs in Gx.
 revert rnd valid_rnd x Gx.
-refine (round_abs_abs' _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _).
+refine (round_abs_abs _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _).
 intros rnd valid_rnd x [Hx|Hx] Gx.
 (* x > 0 *)
 generalize (ln_beta_generic_gt _ x (Rgt_not_eq _ _ Hx) Gx).

src/Prop/Fprop_div_sqrt_error.v

@@ -95,9 +95,6 @@ intros e; apply Zle_refl.
 now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1.
 (* *)
 destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)).
-apply Rmult_integral_contrapositive_currified.
-exact Zx.
-now apply Rinv_neq_0_compat.
 rewrite Heps2.
 rewrite <- Rabs_Ropp.
 replace (-(x + - (x / y * (1 + eps) * y)))%R with (x * eps)%R by now field.

src/Prop/Fprop_relative.v

@@ -35,7 +35,7 @@ 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 ->
   (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
   exists eps,
@@ -62,19 +62,6 @@ 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 ->
@@ -149,6 +136,7 @@ Proof with auto with typeclass_instances.
 intros x Hx.
 apply relative_error_lt_conversion...
 apply bpow_gt_0.
+intros _.
 now apply relative_error.
 Qed.
 
@@ -167,28 +155,17 @@ 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
   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_lt_conversion'...
+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,
@@ -220,7 +197,7 @@ apply bpow_ge_0.
 generalize He.
 apply round_abs_abs...
 clear rnd valid_rnd x Hx Hx' He.
-intros rnd valid_rnd x Hx.
+intros rnd valid_rnd x _ Hx.
 rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
 now apply round_le.
 apply generic_format_bpow.
@@ -377,7 +354,7 @@ apply bpow_ge_0.
 generalize He.
 apply round_abs_abs...
 clear rnd valid_rnd x Hx Hx' He.
-intros rnd valid_rnd x Hx.
+intros rnd valid_rnd x _ Hx.
 rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
 now apply round_le.
 apply generic_format_bpow.
@@ -428,17 +405,6 @@ Qed.
 Variable rnd : R -> Z.
 Context { valid_rnd : Valid_rnd rnd }.
 
-(* TODO: remove *)
-Theorem relative_error_FLT_F2R_emin :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (x <> 0)%R ->
-  (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
-Proof with auto with typeclass_instances.
-intros m x Hx.
-apply relative_error_F2R_emin...
-apply relative_error_FLT_aux.
-Qed.
-
 Theorem relative_error_FLT :
   forall x,
   (bpow (emin + prec - 1) <= Rabs x)%R ->
@@ -449,7 +415,7 @@ apply relative_error with (emin + prec - 1)%Z...
 apply relative_error_FLT_aux.
 Qed.
 
-Theorem relative_error_FLT_F2R_emin' :
+Theorem relative_error_FLT_F2R_emin :
   forall m, let x := F2R (Float beta m emin) in
   (x <> 0)%R ->
   (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
@@ -472,26 +438,13 @@ now exists (Float beta m emin).
 now apply relative_error_FLT.
 Qed.
 
-Theorem relative_error_FLT_F2R_emin_ex' :
+Theorem relative_error_FLT_F2R_emin_ex :
   forall m, let x := F2R (Float beta m emin) in
   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_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_lt_conversion'...
+apply relative_error_lt_conversion...
 apply bpow_gt_0.
 now apply relative_error_FLT_F2R_emin.
 Qed.
@@ -506,7 +459,7 @@ Proof with auto with typeclass_instances.
 intros x Hx.
 apply relative_error_lt_conversion...
 apply bpow_gt_0.
-now apply relative_error_FLT.
+intros _; now apply relative_error_FLT.
 Qed.
 
 Variable choice : Z -> bool.
@@ -548,7 +501,7 @@ apply relative_error_N_round with (emin + prec - 1)%Z...
 apply relative_error_FLT_aux.
 Qed.
 
-Theorem relative_error_N_FLT_F2R_emin' :
+Theorem relative_error_N_FLT_F2R_emin :
   forall m, let x := F2R (Float beta m emin) in
   (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
 Proof with auto with typeclass_instances.
@@ -573,17 +526,7 @@ now exists (Float beta m emin).
 now apply relative_error_N_FLT.
 Qed.
 
-(* TODO: remove *)
-Theorem relative_error_N_FLT_F2R_emin :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
-Proof with auto with typeclass_instances.
-intros m x.
-apply relative_error_N_F2R_emin...
-apply relative_error_FLT_aux.
-Qed.
-
-Theorem relative_error_N_FLT_F2R_emin_ex' :
+Theorem relative_error_N_FLT_F2R_emin_ex :
   forall m, let x := F2R (Float beta m emin) in
   exists eps,
   (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
@@ -594,26 +537,11 @@ apply Rmult_le_pos.
 apply Rlt_le.
 apply (RinvN_pos 1).
 apply bpow_ge_0.
-now apply relative_error_N_FLT_F2R_emin'.
-Qed.
-
-(* TODO: remove *)
-Theorem relative_error_N_FLT_F2R_emin_ex :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  exists eps,
-  (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
-Proof with auto with typeclass_instances.
-intros m x.
-apply relative_error_le_conversion...
-apply Rlt_le.
-apply Rmult_lt_0_compat.
-apply Rinv_0_lt_compat.
-now apply (Z2R_lt 0 2).
-apply bpow_gt_0.
 now apply relative_error_N_FLT_F2R_emin.
 Qed.
 
-Theorem relative_error_N_FLT_round_F2R_emin' :
+
+Theorem relative_error_N_FLT_round_F2R_emin :
   forall m, let x := F2R (Float beta m emin) in
   (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
 Proof with auto with typeclass_instances.
@@ -639,16 +567,6 @@ apply relative_error_N_round with (emin := (emin + prec - 1)%Z)...
 apply relative_error_FLT_aux.
 Qed.
 
-(* TODO: remove *)
-Theorem relative_error_N_FLT_round_F2R_emin :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
-Proof with auto with typeclass_instances.
-intros m x.
-apply relative_error_N_round_F2R_emin...
-apply relative_error_FLT_aux.
-Qed.
-
 Lemma error_N_FLT_aux :
   forall x,
   (0 < x)%R ->
@@ -771,28 +689,17 @@ apply He.
 Qed.
 
 (** 1+#&epsilon;# property in any rounding in FLX *)
-Theorem relative_error_FLX_ex' :
+Theorem relative_error_FLX_ex :
   forall x,
   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_lt_conversion'...
+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 ->