Split format definitions.

src/Flocq_rnd_FIX.v

@@ -19,11 +19,22 @@ Definition FIX_format (x : R) :=
 Definition FIX_RoundingModeP (rnd : R -> R):=
   Rounding_for_Format FIX_format rnd.
 
-Theorem FIX_format_satisfies_any :
-  satisfies_any FIX_format.
+Definition FIX_exp (e : Z) := emin.
+
+Theorem FIX_exp_correct : valid_exp FIX_exp.
+Proof.
+intros k.
+unfold FIX_exp.
+split ; intros H.
+now apply Zlt_le_weak.
+split.
+apply Zle_refl.
+now intros _ _.
+Qed.
+
+Theorem FIX_format_generic :
+  forall x : R, generic_format beta FIX_exp x <-> FIX_format x.
 Proof.
-pose (fexp (e : Z) := emin).
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
 split.
 (* . *)
 intros ((xm, xe), (Hx1, Hx2)).
@@ -38,23 +49,23 @@ repeat split.
 rewrite Hx1.
 apply (f_equal (fun e => F2R (Float beta xm e))).
 simpl in Hx2.
-unfold fexp in Hx2.
-apply Hx2.
+now unfold FIX_exp in Hx2.
 (* . *)
 intros ((xm, xe), (Hx1, Hx2)).
-exists (Float beta xm (fexp xe)).
+exists (Float beta xm (FIX_exp xe)).
 split.
-unfold fexp.
+unfold FIX_exp.
 now rewrite <- Hx2.
 now intros Hx3.
-(* . *)
-intros k.
-unfold fexp.
-split ; intros H.
-now apply Zlt_le_weak.
-split.
-apply Zle_refl.
-now intros _ _.
+Qed.
+
+Theorem FIX_format_satisfies_any :
+  satisfies_any FIX_format.
+Proof.
+pose (fexp (e : Z) := emin).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
+exact FIX_format_generic.
+exact FIX_exp_correct.
 Qed.
 
 End RND_FIX.

src/Flocq_rnd_FLX.v

@@ -21,11 +21,18 @@ Definition FLX_format (x : R) :=
 Definition FLX_RoundingModeP (rnd : R -> R):=
   Rounding_for_Format FLX_format rnd.
 
-Theorem FLX_format_satisfies_any :
-  satisfies_any FLX_format.
+Definition FLX_exp (e : Z) := (e - prec)%Z.
+
+Theorem FLX_exp_correct : valid_exp FLX_exp.
+Proof.
+intros k.
+unfold FLX_exp.
+repeat split ; intros ; omega.
+Qed.
+
+Theorem FLX_format_generic :
+  forall x : R, generic_format beta FLX_exp x <-> FLX_format x.
 Proof.
-pose (fexp e := (e - prec)%Z).
-refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
 split.
 (* . *)
 intros ((xm, xe), (Hx1, Hx2)).
@@ -51,7 +58,7 @@ apply Rmult_lt_reg_r with (bpow (ex - prec)%Z).
 apply epow_gt_0.
 rewrite <- epow_add.
 replace (prec + (ex - prec))%Z with ex by ring.
-change (ex - prec)%Z with (fexp ex).
+change (ex - prec)%Z with (FLX_exp ex).
 rewrite <- Hx2.
 replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x).
 exact (proj2 Hx4).
@@ -78,16 +85,21 @@ 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 (fexp ex).
+change (Fexp (Float beta mx (ex - prec))) with (FLX_exp ex).
 apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.
 rewrite <- Hx5.
 now rewrite <- Hx1.
-(* . *)
-intros k.
-unfold fexp.
-repeat split ; intros ; omega.
+Qed.
+
+Theorem FLX_format_satisfies_any :
+  satisfies_any FLX_format.
+Proof.
+pose (fexp e := (e - prec)%Z).
+refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta fexp _)).
+exact FLX_format_generic.
+exact FLX_exp_correct.
 Qed.
 
 End RND_FIX.

src/Flocq_rnd_generic.v

@@ -11,12 +11,14 @@ Notation bpow := (epow beta).
 
 Variable fexp : Z -> Z.
 
-Variable valid_fexp :
- forall k : Z,
- ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\
- ( (k <= fexp k)%Z ->
-   (fexp (fexp k + 1) <= fexp k)%Z /\
-   forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ).
+Definition valid_exp :=
+  forall k : Z,
+  ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\
+  ( (k <= fexp k)%Z ->
+    (fexp (fexp k + 1) <= fexp k)%Z /\
+    forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ).
+
+Variable prop_exp : valid_exp.
 
 Definition generic_format (x : R) :=
   exists f : float beta,
@@ -237,7 +239,7 @@ apply Rle_trans with (bpow ge).
 apply -> epow_le.
 simpl in Hg2.
 rewrite Hg2.
-rewrite (proj2 (proj2 (valid_fexp ex) He1) ge').
+rewrite (proj2 (proj2 (prop_exp ex) He1) ge').
 exact He1.
 apply Zle_trans with (2 := He1).
 cut (ge' - 1 < ex)%Z. omega.
@@ -370,7 +372,7 @@ apply Rle_lt_trans with (1 := Hbr).
 exact Hx.
 (* - . . a radix power *)
 rewrite <- Hbl2.
-generalize (proj1 (valid_fexp _) He1).
+generalize (proj1 (prop_exp _) He1).
 clear.
 intros He2.
 exists (Float beta (- Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
@@ -449,7 +451,7 @@ rewrite Ropp_mult_distr_l_reverse.
 rewrite Rmult_1_l.
 (* - . rounded *)
 split.
-destruct (proj2 (valid_fexp _) He1) as (He2, _).
+destruct (proj2 (prop_exp _) He1) as (He2, _).
 exists (Float beta (- Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
 unfold F2R. simpl.
 split.
@@ -500,7 +502,7 @@ apply <- epow_lt.
 apply Rle_lt_trans with (1 := proj1 Hge).
 apply Ropp_lt_cancel.
 now rewrite Ropp_involutive.
-rewrite (proj2 (proj2 (valid_fexp _) He1) _ Hge') in Hg2.
+rewrite (proj2 (proj2 (prop_exp _) He1) _ Hge') in Hg2.
 rewrite <- Hg2 in Hge'.
 apply Rlt_not_le with (1 := proj2 Hge).
 rewrite Hg1.