Made ln_beta total.

src/Flocq_Raux.v

@@ -470,10 +470,10 @@ now rewrite <- opp_Z2R.
 Qed.
 
 Lemma ln_beta :
-  forall x : R, (0 < x)%R ->
-  {e | (epow (e - 1)%Z <= x < epow e)%R}.
+  forall x : R,
+  {e | (0 < x)%R -> (epow (e - 1)%Z <= x < epow e)%R}.
 Proof.
-intros x Hx.
+intros x.
 set (fact := ln (Z2R (radix_val r))).
 (* . *)
 assert (0 < fact)%R.
@@ -489,6 +489,7 @@ generalize (radix_prop r).
 omega.
 (* . *)
 exists (up (ln x / fact))%Z.
+intros Hx.
 rewrite 2!epow_exp.
 fold fact.
 pattern x at 2 3 ; replace x with (exp (ln x / fact * fact)).
@@ -544,14 +545,17 @@ apply Zle_antisym ;
 Qed.
 
 Lemma ln_beta_unique :
-  forall (x : R) (e : Z) (Hx : (0 < x)%R),
+  forall (x : R) (e : Z),
   (epow (e - 1) <= x < epow e)%R ->
-  projT1 (ln_beta x Hx) = e.
+  projT1 (ln_beta x) = e.
 Proof.
-intros x e1 Hx H1.
-destruct (ln_beta x Hx) as (e2, H2).
-apply epow_unique with (2 := H1).
-exact H2.
+intros x e1 Hx1.
+destruct (ln_beta x) as (e2, Hx2).
+apply epow_unique with (2 := Hx1).
+simpl.
+apply Hx2.
+apply Rlt_le_trans with (2 := proj1 Hx1).
+apply epow_gt_0.
 Qed.
 
 Lemma Zpower_pos_gt_0 :

src/Flocq_rnd_FIX.v

@@ -38,25 +38,14 @@ Proof.
 split.
 (* . *)
 intros ((xm, xe), (Hx1, Hx2)).
-destruct (Req_dec x 0) as [Hx3|Hx3].
-exists (Float beta 0 emin).
-repeat split.
-unfold F2R. simpl.
-now rewrite Rmult_0_l.
-specialize (Hx2 Hx3).
-exists (Float beta xm emin).
-repeat split.
 rewrite Hx1.
-apply (f_equal (fun e => F2R (Float beta xm e))).
-simpl in Hx2.
-now unfold FIX_exp in Hx2.
+eexists ; repeat split.
+now rewrite Hx2.
 (* . *)
 intros ((xm, xe), (Hx1, Hx2)).
-exists (Float beta xm (FIX_exp xe)).
-split.
-unfold FIX_exp.
-now rewrite <- Hx2.
-now intros Hx3.
+rewrite Hx1.
+eexists ; repeat split.
+now rewrite Hx2.
 Qed.
 
 Theorem FIX_format_satisfies_any :

src/Flocq_rnd_FLT.v

@@ -63,14 +63,11 @@ apply Zpower_gt_0.
 now apply Zlt_le_trans with (2 := radix_prop beta).
 exact Hp.
 apply Zle_refl.
-specialize (Hx2 Hx3).
-exists (Float beta xm xe).
-split.
-exact Hx1.
-simpl.
-destruct (ln_beta beta (Rabs x) (Rabs_pos_lt x Hx3)) as (ex, Hx4).
+rewrite Hx1.
+eexists ; repeat split.
+destruct (ln_beta beta (Rabs x)) as (ex, Hx4).
 simpl in Hx2.
-split.
+specialize (Hx4 (Rabs_pos_lt x Hx3)).
 apply lt_Z2R.
 rewrite Z2R_Zpower.
 apply Rmult_lt_reg_r with (bpow (ex - prec)%Z).
@@ -95,14 +92,12 @@ apply Zle_max_r.
 intros ((xm, xe), (Hx1, (Hx2, Hx3))).
 destruct (Req_dec x 0) as [Hx4|Hx4].
 rewrite Hx4.
-exists (Float beta 0 0).
-split.
+exists (Float beta 0 _) ; repeat split.
 unfold F2R. simpl.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
-destruct (ln_beta beta (Rabs x) (Rabs_pos_lt _ Hx4)) as (ex, Hx5).
 simpl in Hx2, Hx3.
+destruct (ln_beta beta (Rabs x)) as (ex, Hx5).
+specialize (Hx5 (Rabs_pos_lt _ Hx4)).
 assert (Hx6 : x = F2R (Float beta (xm * Zpower (radix_val beta) (xe - FLT_exp ex)) (FLT_exp ex))).
 rewrite Hx1.
 unfold F2R. simpl.
@@ -133,7 +128,6 @@ now apply Zlt_le_weak.
 exact Hx3.
 rewrite Hx6.
 eexists ; repeat split.
-intros H.
 simpl.
 apply f_equal.
 apply sym_eq.

src/Flocq_rnd_FLX.v

@@ -45,13 +45,12 @@ simpl.
 apply Zpower_gt_0.
 now apply Zlt_le_trans with (2 := radix_prop beta).
 exact Hp.
-specialize (Hx2 Hx3).
-exists (Float beta xm xe).
-split.
-exact Hx1.
+rewrite Hx1.
+eexists ; repeat split.
 simpl.
-destruct (ln_beta beta (Rabs x) (Rabs_pos_lt x Hx3)) as (ex, Hx4).
+destruct (ln_beta beta (Rabs x)) as (ex, Hx4).
 simpl in Hx2.
+specialize (Hx4 (Rabs_pos_lt x Hx3)).
 apply lt_Z2R.
 rewrite Z2R_Zpower.
 apply Rmult_lt_reg_r with (bpow (ex - prec)%Z).
@@ -69,14 +68,12 @@ now apply Zlt_le_weak.
 intros ((xm, xe), (Hx1, Hx2)).
 destruct (Req_dec x 0) as [Hx3|Hx3].
 rewrite Hx3.
-exists (Float beta 0 0).
-split.
+exists (Float beta 0 _) ; repeat split.
 unfold F2R. simpl.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
-destruct (ln_beta beta (Rabs x) (Rabs_pos_lt _ Hx3)) as (ex, Hx4).
 simpl in Hx2.
+destruct (ln_beta beta (Rabs x)) as (ex, Hx4).
+specialize (Hx4 (Rabs_pos_lt _ Hx3)).
 destruct (F2R_prec_normalize beta xm xe (ex - 1) prec Hx2) as (mx, Hx5).
 rewrite <- Hx1.
 exact (proj1 Hx4).
@@ -84,7 +81,6 @@ rewrite Hx1.
 replace (ex - 1 - (prec - 1))%Z with (ex - prec)%Z in Hx5 by ring.
 rewrite Hx5.
 eexists ; repeat split.
-intros H.
 change (Fexp (Float beta mx (ex - prec))) with (FLX_exp ex).
 apply f_equal.
 apply sym_eq.

src/Flocq_rnd_generic.v

@@ -22,8 +22,7 @@ Variable prop_exp : valid_exp.
 
 Definition generic_format (x : R) :=
   exists f : float beta,
-  x = F2R f /\ forall (H : x <> R0),
-  Fexp f = fexp (projT1 (ln_beta beta _ (Rabs_pos_lt _ H))).
+  x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))).
 
 Theorem generic_DN_pt_large_pos_ge_pow :
   forall x ex,
@@ -84,12 +83,10 @@ now apply generic_DN_pt_large_pos_ge_pow.
 split.
 (* - . rounded *)
 eexists ; split ; [ reflexivity | idtac ].
-intros He9.
 simpl.
 apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.
-clear He9.
 rewrite Rabs_right.
 split.
 exact Hbl.
@@ -141,7 +138,6 @@ destruct (Rle_or_lt g R0) as [Hg3|Hg3].
 apply Rle_trans with (2 := Hbl).
 apply Rle_trans with (1 := Hg3).
 apply epow_ge_0.
-specialize (Hg2 (Rgt_not_eq _ _ Hg3)).
 apply Rnot_lt_le.
 intros Hrg.
 assert (bpow (ex - 1)%Z <= g < bpow ex)%R.
@@ -179,12 +175,9 @@ cutrewrite (up (x * bpow (- fexp ex)%Z) = 1%Z).
 unfold F2R. simpl.
 rewrite Rmult_0_l.
 split.
-exists (Float beta Z0 (fexp ex)).
-split.
+exists (Float beta Z0 _) ; repeat split.
 unfold F2R. simpl.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
 split.
 apply Rle_trans with (2 := Hx1).
 apply epow_ge_0.
@@ -192,8 +185,8 @@ apply epow_ge_0.
 intros g ((gm, ge), (Hg1, Hg2)) Hgx.
 apply Rnot_lt_le.
 intros Hg3.
-specialize (Hg2 (Rgt_not_eq _ _ Hg3)).
-destruct (ln_beta beta g Hg3) as (ge', Hg4).
+destruct (ln_beta beta g) as (ge', Hg4).
+specialize (Hg4 Hg3).
 generalize Hg4. intros Hg5.
 rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in Hg5.
 rewrite ln_beta_unique with (1 := Hg5) in Hg2.
@@ -313,8 +306,7 @@ split.
 (* - . rounded *)
 destruct (Rle_lt_or_eq_dec _ _ Hbl) as [Hbl2|Hbl2].
 (* - . . not a radix power *)
-eexists ; split ; [ reflexivity | idtac ].
-intros Hr.
+eexists ; repeat split.
 simpl.
 apply f_equal.
 apply sym_eq.
@@ -348,7 +340,6 @@ cut (0 <= ex - fexp (ex + 1))%Z. 2: omega.
 case (ex - fexp (ex + 1))%Z ; trivial.
 intros ep H.
 now elim H.
-intros H.
 apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.
@@ -369,9 +360,9 @@ apply Rnot_lt_le.
 intros Hg3.
 assert (Hg4 : (g < 0)%R).
 now apply Rle_lt_trans with (1 := Hgx).
-specialize (Hg2 (Rlt_not_eq _ _ Hg4)).
-destruct (ln_beta beta (Rabs g) (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))) as (ge', Hge).
+destruct (ln_beta beta (Rabs g)) as (ge', Hge).
 simpl in Hg2.
+specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))).
 apply Rlt_not_le with (1 := Hg3).
 rewrite Hg1.
 unfold F2R. simpl.
@@ -425,7 +416,6 @@ clear.
 case (fexp ex - fexp (fexp ex + 1))%Z ; trivial.
 intros ep Hp.
 now elim Hp.
-intros H.
 apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.
@@ -452,9 +442,9 @@ apply Rnot_lt_le.
 intros Hg3.
 assert (Hg4 : (g < 0)%R).
 now apply Rle_lt_trans with (1 := Hgx).
-specialize (Hg2 (Rlt_not_eq _ _ Hg4)).
-destruct (ln_beta beta (Rabs g) (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))) as (ge', Hge).
+destruct (ln_beta beta (Rabs g)) as (ge', Hge).
 simpl in Hg2.
+specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))).
 rewrite (Rabs_left _ Hg4) in Hge.
 assert (Hge' : (ge' <= fexp ex)%Z).
 cut (ge' - 1 < fexp ex)%Z. omega.
@@ -530,66 +520,51 @@ Theorem generic_format_satisfies_any :
 Proof.
 refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
 (* symmetric set *)
-exists (Float beta 0 0).
-split.
+exists (Float beta 0 _) ; repeat split.
 unfold F2R. simpl.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
 intros x ((m,e),(H1,H2)).
-exists (Float beta (-m) e).
-split.
-rewrite H1.
-apply opp_F2R.
-intros H3.
-simpl in H2.
-assert (H4 := Ropp_neq_0_compat _ H3).
-rewrite Ropp_involutive in H4.
-rewrite (H2 H4).
-clear H2.
-destruct (ln_beta beta (Rabs x)) as (ex, H5).
-simpl.
-apply f_equal.
-apply sym_eq.
-apply ln_beta_unique.
-now rewrite Rabs_Ropp.
+exists (Float beta (-m) _) ; repeat split.
+rewrite H1 at 1.
+rewrite Rabs_Ropp.
+rewrite opp_F2R.
+apply (f_equal (fun v => F2R (Float beta (- m) v))).
+exact H2.
 (* rounding down *)
-assert (Hxx : forall x, (0 > x)%R -> (0 < -x)%R).
-intros.
-now apply Ropp_0_gt_lt_contravar.
 exists (fun x =>
   match total_order_T 0 x with
   | inleft (left Hx) =>
-    let e := fexp (projT1 (ln_beta beta _ Hx)) in
+    let e := fexp (projT1 (ln_beta beta x)) in
     F2R (Float beta (up (x * bpow (Zopp e)) - 1) e)
   | inleft (right _) => R0
   | inright Hx =>
-    let e := fexp (projT1 (ln_beta beta _ (Hxx _ Hx))) in
+    let e := fexp (projT1 (ln_beta beta (-x))) in
     F2R (Float beta (up (x * bpow (Zopp e)) - 1) e)
   end).
 intros x.
 destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
 (* positive *)
-destruct (ln_beta beta x Hx) as (ex, Hx').
+destruct (ln_beta beta x) as (ex, Hx').
 simpl.
-now apply generic_DN_pt_pos.
+apply generic_DN_pt_pos.
+now apply Hx'.
 (* zero *)
 split.
-exists (Float beta 0 0).
-split.
-unfold F2R.
+exists (Float beta 0 _) ; repeat split.
+unfold F2R. simpl.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
 rewrite <- Hx.
 split.
 apply Rle_refl.
 intros g _ H.
 exact H.
 (* negative *)
-destruct (ln_beta beta (- x) (Hxx x Hx)) as (ex, Hx').
+destruct (ln_beta beta (- x)) as (ex, Hx').
 simpl.
-now apply generic_DN_pt_neg.
+apply generic_DN_pt_neg.
+apply Hx'.
+rewrite <- Ropp_0.
+now apply Ropp_lt_contravar.
 Qed.
 
 Theorem generic_DN_pt_small_pos :
@@ -600,12 +575,9 @@ Theorem generic_DN_pt_small_pos :
 Proof.
 intros x ex Hx He.
 split.
-exists (Float beta 0 0).
+exists (Float beta 0 _) ; repeat split.
 unfold F2R. simpl.
-split.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
 split.
 apply Rle_trans with (2 := proj1 Hx).
 apply epow_ge_0.
@@ -613,9 +585,9 @@ apply epow_ge_0.
 intros g ((gm, ge), (Hg1, Hg2)) Hgx.
 apply Rnot_lt_le.
 intros Hg3.
-specialize (Hg2 (Rgt_not_eq _ _ Hg3)).
-destruct (ln_beta beta (Rabs g) (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))) as (eg, Hg4).
+destruct (ln_beta beta (Rabs g)) as (eg, Hg4).
 simpl in Hg2.
+specialize (Hg4 (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))).
 rewrite Rabs_right in Hg4.
 apply Rle_not_lt with (1 := Hgx).
 rewrite Hg1.
@@ -656,7 +628,6 @@ split.
 rewrite H.
 eexists ; repeat split.
 simpl.
-intros H1.
 apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.
@@ -682,9 +653,9 @@ apply Rgt_not_eq.
 apply Rlt_le_trans with (2 := Hgx).
 apply Rlt_le_trans with (2 := proj1 Hx).
 apply epow_gt_0.
-specialize (Hg2 H0).
-destruct (ln_beta beta (Rabs g) (Rabs_pos_lt g H0)) as (eg, Hg3).
+destruct (ln_beta beta (Rabs g)) as (eg, Hg3).
 simpl in Hg2.
+specialize (Hg3 (Rabs_pos_lt g H0)).
 apply Rnot_lt_le.
 intros Hgp.
 apply Rlt_not_le with (1 := Hgp).
@@ -727,7 +698,6 @@ ring.
 generalize (proj1 (prop_exp _) He).
 omega.
 (* . *)
-intros H.
 apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.

src/Flocq_ulp.v

@@ -14,11 +14,7 @@ Variable fexp : Z -> Z.
 
 Variable prop_exp : valid_exp fexp.
 
-Definition ulp x :=
-  match Req_EM_T x 0 with
-  | left _ => R0
-  | right Hx => F2R (Float beta 1 (fexp (projT1 (ln_beta beta (Rabs x) (Rabs_pos_lt _ Hx)))))
-  end.
+Definition ulp x := F2R (Float beta 1 (fexp (projT1 (ln_beta beta (Rabs x))))).
 
 Definition F := generic_format beta fexp.
 
@@ -29,12 +25,9 @@ intros x Fx Hx.
 elim Fx.
 rewrite Hx.
 clear.
-exists (Float beta 0 0).
-split.
+exists (Float beta 0 _) ; repeat split.
 unfold F2R. simpl.
 now rewrite Rmult_0_l.
-intros H.
-now elim H.
 Qed.
 
 Theorem ulp_pred_succ_pt :
@@ -48,8 +41,9 @@ destruct (Req_EM_T x 0) as [Hx1|Hx1].
 now elim zero_not_in_format with x.
 destruct (Rdichotomy x 0 Hx1) as [Hx2|Hx2].
 (* negative *)
-destruct (ln_beta beta (Rabs x) (Rabs_pos_lt x Hx1)) as (ex, Hx3).
+destruct (ln_beta beta (Rabs x)) as (ex, Hx3).
 simpl.
+specialize (Hx3 (Rabs_pos_lt x Hx1)).
 destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
 (* . negative big *)
 admit.
@@ -71,8 +65,9 @@ now eapply generic_format_satisfies_any.
 rewrite Ropp_0.
 now apply generic_DN_pt_small_pos with ex.
 (* positive *)
-destruct (ln_beta beta (Rabs x) (Rabs_pos_lt x Hx1)) as (ex, Hx3).
+destruct (ln_beta beta (Rabs x)) as (ex, Hx3).
 simpl.
+specialize (Hx3 (Rabs_pos_lt x Hx1)).
 rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx2)) in Hx3.
 destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
 (* . positive big *)