Added theorem ln_beta_Z2R_le and simplified some proofs.

src/Core/Fcore_FLT.v

@@ -58,26 +58,19 @@ Theorem generic_format_FLT :
   forall x, FLT_format x -> generic_format beta FLT_exp x.
 Proof.
 clear prec_gt_0_.
-intros x ((xm, xe), (Hx1, (Hx2, Hx3))).
-simpl in Hx2, Hx3.
-destruct (Req_dec x 0) as [Hx4|Hx4].
-rewrite Hx4.
+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.
-destruct (ln_beta beta x) as (ex, Hx5).
-specialize (Hx5 Hx4).
-rewrite Hx1.
 apply generic_format_canonic_exponent.
-rewrite <- Hx1.
-rewrite canonic_exponent_fexp with (1 := Hx5).
-unfold FLT_exp.
-apply Zmax_lub. 2: exact Hx3.
-cut (ex -1 < prec + xe)%Z. omega.
-apply (lt_bpow beta).
-apply Rle_lt_trans with (1 := proj1 Hx5).
-rewrite Hx1.
-apply F2R_lt_bpow.
-simpl.
-now ring_simplify (prec + xe - xe)%Z.
+unfold canonic_exponent, FLT_exp.
+rewrite ln_beta_F2R with (1 := Zmx).
+apply Zmax_lub with (2 := H3).
+apply Zplus_le_reg_r with (prec - ex)%Z.
+ring_simplify.
+now apply ln_beta_Z2R_le.
 Qed.
 
 Theorem FLT_format_generic :

src/Core/Fcore_FLX.v

@@ -153,27 +153,12 @@ rewrite H1.
 destruct (Z_eq_dec mx 0) as [Zmx|Zmx].
 rewrite Zmx, F2R_0.
 apply generic_format_0.
-destruct (Zle_or_lt 0 prec) as [Hprec|Hprec].
-(* *)
 apply generic_format_canonic_exponent.
 unfold canonic_exponent, FLX_exp.
 rewrite ln_beta_F2R with (1 := Zmx).
 apply Zplus_le_reg_r with (prec - ex)%Z.
 ring_simplify.
-apply bpow_lt_bpow with beta.
-destruct (ln_beta beta (Z2R mx)) as (emx,Emx). simpl.
-specialize (Emx (Z2R_neq _ _ Zmx)).
-apply Rle_lt_trans with (1 := proj1 Emx).
-rewrite <- Z2R_abs.
-rewrite <- Z2R_Zpower with (1 := Hprec).
-now apply Z2R_lt.
-(* *)
-revert H2 Hprec.
-case prec ; simpl ; try discriminate.
-intros _ H _.
-elim (Zlt_irrefl 0).
-apply Zle_lt_trans with (2 := H).
-apply Zabs_pos.
+now apply ln_beta_Z2R_le.
 Qed.
 
 Theorem FLX_format_satisfies_any :

src/Core/Fcore_Raux.v

@@ -2125,6 +2125,27 @@ apply Rle_ge.
 apply bpow_ge_0.
 Qed.
 
+Theorem ln_beta_Z2R_le :
+  forall m e,
+  m <> Z0 ->
+  (Zabs m < Zpower r e)%Z->
+  (ln_beta (Z2R m) <= e)%Z.
+Proof.
+intros m e Zm Hm.
+destruct (ln_beta (Z2R m)) as (e',E) ; simpl.
+specialize (E (Z2R_neq m 0 Zm)).
+apply bpow_lt_bpow.
+apply Rle_lt_trans with (1 := proj1 E).
+destruct (Zle_or_lt 0 e).
+rewrite <- Z2R_abs, <- Z2R_Zpower with (1 := H).
+now apply Z2R_lt.
+elim Zm.
+cut (Zabs m < 0)%Z.
+now case m.
+clear -Hm H.
+now destruct e.
+Qed.
+
 Theorem Zpower_pos_gt_0 :
   forall b p, (0 < b)%Z ->
   (0 < Zpower_pos b p)%Z.