Renamed theorem generic_format_canonic_exponent and weakened its hypothesis.

src/Calc/Fcalc_round.v

@@ -594,10 +594,8 @@ set (k := (fexp (digits beta m + e) - e)%Z).
 case Zlt_bool_spec ; intros Hk.
 (* *)
 unfold truncate_aux.
-destruct (Z_eq_dec (m / beta ^ k) 0) as [Hd|Hd].
-rewrite Hd, F2R_0.
-apply generic_format_0.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros Hd.
 unfold canonic_exponent.
 rewrite ln_beta_F2R_digits with (1 := Hd).
 rewrite digits_shr with (1 := Hm).
@@ -617,7 +615,7 @@ apply Zlt_le_weak.
 now apply Zgt_lt.
 (* *)
 destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
 unfold canonic_exponent.
 rewrite ln_beta_F2R_digits.
 2: now apply Zgt_not_eq.
@@ -781,14 +779,11 @@ split.
 apply refl_equal.
 inversion_clear H1.
 rewrite H.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros Zm.
 unfold canonic_exponent.
-rewrite ln_beta_F2R_digits.
+rewrite ln_beta_F2R_digits with (1 := Zm).
 now apply Zlt_le_weak.
-apply sym_not_eq.
-apply Zlt_not_eq.
-rewrite H in Hx.
-apply F2R_gt_0_reg with (1 := Hx).
 (* x = 0 *)
 assert (Hm: m = Z0).
 cut (m <= 0 < m + 1)%Z. omega.
@@ -1089,7 +1084,7 @@ exact H2.
 rewrite H2 in H1.
 inversion_clear H1.
 rewrite H.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
 unfold canonic_exponent.
 omega.
 Qed.

src/Core/Fcore_FLT.v

@@ -61,10 +61,8 @@ clear prec_gt_0_.
 intros x ((mx, ex), (H1, (H2, H3))).
 simpl in H2, H3.
 rewrite H1.
-destruct (Z_eq_dec mx 0) as [Zmx|Zmx].
-rewrite Zmx, F2R_0.
-apply generic_format_0.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros Zmx.
 unfold canonic_exponent, FLT_exp.
 rewrite ln_beta_F2R with (1 := Zmx).
 apply Zmax_lub with (2 := H3).
@@ -152,9 +150,11 @@ Theorem FLX_generic_format_FLT :
   forall x : R,
   generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
 Proof.
+clear prec_gt_0_.
 intros x Hx.
 unfold generic_format in Hx; rewrite Hx.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 rewrite <- Hx.
 unfold canonic_exponent, FLX_exp, FLT_exp.
 apply Zle_max_l.
@@ -194,9 +194,11 @@ Theorem FIX_generic_format_FLT :
   generic_format beta FLT_exp x ->
   generic_format beta (FIX_exp emin) x.
 Proof.
+clear prec_gt_0_.
 intros x Hx.
 rewrite Hx.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 rewrite <- Hx.
 apply Zle_max_r.
 Qed.

src/Core/Fcore_FLX.v

@@ -150,10 +150,8 @@ clear prec_gt_0_.
 intros x ((mx,ex),(H1,H2)).
 simpl in H2.
 rewrite H1.
-destruct (Z_eq_dec mx 0) as [Zmx|Zmx].
-rewrite Zmx, F2R_0.
-apply generic_format_0.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros Zmx.
 unfold canonic_exponent, FLX_exp.
 rewrite ln_beta_F2R with (1 := Zmx).
 apply Zplus_le_reg_r with (prec - ex)%Z.

src/Core/Fcore_FTZ.v

@@ -80,7 +80,7 @@ rewrite Hx4.
 apply generic_format_0.
 specialize (Hx2 Hx4).
 rewrite Hx1.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
 unfold canonic_exponent, FTZ_exp.
 rewrite <- Hx1.
 destruct (ln_beta beta x) as (ex, Hx6).

src/Core/Fcore_generic_fmt.v

@@ -99,26 +99,26 @@ now rewrite Zmult_1_l.
 omega.
 Qed.
 
-Theorem generic_format_canonic_exponent :
+Theorem generic_format_F2R :
   forall m e,
-  (canonic_exponent (F2R (Float beta m e)) <= e)%Z ->
+  ( m <> 0 -> canonic_exponent (F2R (Float beta m e)) <= e )%Z ->
   generic_format (F2R (Float beta m e)).
 Proof.
 intros m e.
+destruct (Z_eq_dec m 0) as [Zm|Zm].
+intros _.
+rewrite Zm, F2R_0.
+apply generic_format_0.
 unfold generic_format, scaled_mantissa.
 set (e' := canonic_exponent (F2R (Float beta m e))).
 intros He.
+specialize (He Zm).
 unfold F2R at 3. simpl.
-assert (H: (Z2R m * bpow e * bpow (- e') = Z2R (m * Zpower beta (e + -e')))%R).
-rewrite Rmult_assoc, <- bpow_plus, Z2R_mult.
-rewrite Z2R_Zpower.
-apply refl_equal.
+rewrite  F2R_change_exp with (1 := He).
+apply F2R_eq_compat.
+rewrite Rmult_assoc, <- bpow_plus, <- Z2R_Zpower, <- Z2R_mult.
+now rewrite Ztrunc_Z2R.
 now apply Zle_left.
-rewrite H, Ztrunc_Z2R.
-unfold F2R. simpl.
-rewrite <- H.
-rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
-now rewrite Rmult_1_r.
 Qed.
 
 Theorem canonic_opp :

src/Core/Fcore_ulp.v

@@ -670,7 +670,8 @@ rewrite <- bpow_plus.
 now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring.
 omega.
 rewrite H.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 apply Zeq_le.
 apply canonic_exponent_fexp.
 rewrite <- H.

src/Prop/Fprop_Sterbenz.v

@@ -66,7 +66,8 @@ unfold canonic_exponent.
 now rewrite ln_beta_unique with (1 := Ey).
 rewrite Hx, Hy.
 rewrite <- plus_F2R.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 case_eq (Fplus beta fx fy).
 intros mxy exy Pxy.
 rewrite <- Pxy, plus_F2R, <- Hx, <- Hy.

src/Prop/Fprop_div_sqrt_error.v

@@ -42,7 +42,8 @@ intros x y fx fy Hx Hy H1 H2.
 case (Req_dec (x+y) 0); intros H.
 rewrite H; apply generic_format_0.
 rewrite Hx, Hy, <- plus_F2R.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 case_eq (Fplus beta fx fy).
 intros mz ez Hz.
 rewrite <- Hz.

src/Prop/Fprop_mult_error.v

@@ -150,8 +150,7 @@ rewrite Hr0.
 apply generic_format_0.
 destruct (mult_error_FLX_aux x y Hx Hy Hr0) as ((m,e),(H1,(H2,H3))).
 rewrite <- H1.
-apply generic_format_canonic_exponent; simpl.
-simpl in H2; assumption.
+now apply generic_format_F2R.
 Qed.
 
 End Fprop_mult_error.
@@ -203,7 +202,8 @@ rewrite <- (FLT_round_FLX beta emin) in H1.
 2:apply Rle_trans with (2:=Hxy).
 2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega.
 unfold f; rewrite <- H1.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 simpl in H2, H3.
 unfold canonic_exponent, FLT_exp.
 case (Zmax_spec (ln_beta beta (F2R (Float beta m e)) - prec) emin);

src/Prop/Fprop_plus_error.v

@@ -106,7 +106,8 @@ assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex
   F2R (Float beta (mxy - (mx + my * beta ^ (ey - ex))) ex)).
 now rewrite <- minus_F2R, Fminus_same_exp.
 rewrite H.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 apply monotone_exp.
 rewrite <- H, <- Hxy', <- Hxy.
 apply ln_beta_monotone_abs.
@@ -171,7 +172,8 @@ now rewrite <- plus_F2R, Fplus_same_exp.
 rewrite H in Hxy.
 rewrite round_generic in Hxy...
 now rewrite <- H in Hxy.
-apply generic_format_canonic_exponent.
+apply generic_format_F2R.
+intros _.
 rewrite <- H.
 unfold canonic_exponent.
 rewrite ln_beta_unique with (1 := Hexy).