Added facts on rounding large values.

src/Flocq_Raux.v

@@ -554,29 +554,38 @@ apply epow_unique with (2 := H1).
 exact H2.
 Qed.
 
-Lemma Zpower_pos_lt: forall b z, (0 < b)%Z -> (0 < Zpower_pos b z)%Z.
-intros; apply lt_Z2R.
-simpl; rewrite Zpower_pos_powerRZ.
+Lemma Zpower_pos_gt_0 :
+  forall b p, (0 < b)%Z ->
+  (0 < Zpower_pos b p)%Z.
+Proof.
+intros b p Hb.
+apply lt_Z2R.
+rewrite Zpower_pos_powerRZ.
 apply powerRZ_lt.
-apply Rle_lt_trans with (Z2R 0).
-right; reflexivity.
-now apply Z2R_lt.
+now apply (Z2R_lt 0).
 Qed.
 
-Lemma Zpower_lt: forall b z, (0 < b)%Z -> (0 < z)%Z -> (0 < Zpower b z)%Z.
-intros.
-destruct z; unfold Zpower; auto with zarith.
-now apply Zpower_pos_lt.
-absurd (0 <= Zneg p)%Z; auto with zarith.
+Lemma Zpower_gt_0 :
+  forall b p,
+  (0 < b)%Z -> (0 < p)%Z ->
+  (0 < Zpower b p)%Z.
+Proof.
+intros b p Hb Hz.
+unfold Zpower.
+destruct p ; try easy.
+now apply Zpower_pos_gt_0.
 Qed.
 
-Lemma vNum_gt_1: forall prec, (0 < prec)%Z -> (1 < radix_val r ^ prec)%Z.
+Lemma Zpower_gt_1 :
+  forall p,
+  (0 < p)%Z ->
+  (1 < Zpower (radix_val r) p)%Z.
+Proof.
 intros.
 apply lt_Z2R.
-rewrite Z2R_Zpower; auto with zarith.
-apply Rle_lt_trans with (epow 0%Z).
-right; reflexivity.
-now apply -> epow_lt.
+rewrite Z2R_Zpower.
+now apply -> (epow_lt 0).
+now apply Zlt_le_weak.
 Qed.
 
 End pow.

src/Flocq_rnd_FLT.v

@@ -81,7 +81,7 @@ exists (Float beta 1 (prec+emin)).
 split.
 unfold F2R; simpl; auto with real.
 simpl.
-now apply vNum_gt_1.
+now apply Zpower_gt_1.
 unfold F2R; apply Rmult_le_compat_r.
 apply epow_ge_0.
 rewrite <- Z2R_Zpower; auto with zarith.

src/Flocq_rnd_FLX.v

@@ -42,7 +42,7 @@ split.
 unfold F2R. simpl.
 now rewrite Rmult_0_l.
 simpl.
-apply Zpower_lt.
+apply Zpower_gt_0.
 now apply Zlt_le_trans with (2 := radix_prop beta).
 exact Hp.
 specialize (Hx2 Hx3).

src/Flocq_rnd_generic.v

@@ -537,7 +537,7 @@ intros ep _.
 simpl.
 apply (Z2R_le 1).
 apply (Zlt_le_succ 0).
-apply Zpower_pos_lt.
+apply Zpower_pos_gt_0.
 now apply Zlt_le_trans with (2 := radix_prop beta).
 intros ep Hp. now elim Hp.
 apply Rmult_le_compat_r.
@@ -620,7 +620,7 @@ assert (bpow (fexp ex) = F2R (Float beta 1 (fexp ex))).
 unfold F2R. simpl.
 now rewrite Rmult_1_l.
 destruct (F2R_prec_normalize beta 1 (fexp ex) (fexp ex) ((fexp ex + 1) - fexp (fexp ex + 1))) as (m, H0).
-apply vNum_gt_1.
+apply Zpower_gt_1.
 generalize (proj1 (proj2 (prop_exp ex) He)).
 omega.
 rewrite <- H.
@@ -682,4 +682,68 @@ apply epow_ge_0.
 exact Hgp.
 Qed.
 
+Theorem Rnd_DN_pt_large_pos :
+  forall x xd ex,
+  (bpow (ex - 1)%Z <= x < bpow ex)%R ->
+  (fexp ex < ex)%Z ->
+  Rnd_DN_pt generic_format x xd ->
+  (bpow (ex - 1)%Z <= xd)%R.
+Proof.
+intros x xd ex Hx He (_, (_, Hd)).
+apply Hd with (2 := proj1 Hx).
+exists (Float beta (Zpower (radix_val beta) ((ex - 1) - fexp ex)) (fexp ex)).
+unfold F2R. simpl.
+split.
+(* . *)
+rewrite Z2R_Zpower.
+rewrite <- epow_add.
+apply f_equal.
+ring.
+omega.
+(* . *)
+intros H.
+apply f_equal.
+apply sym_eq.
+apply ln_beta_unique.
+rewrite Rabs_pos_eq.
+split.
+apply Rle_refl.
+apply -> epow_lt.
+apply Zlt_pred.
+apply epow_ge_0.
+Qed.
+
+Theorem Rnd_UP_pt_large_pos :
+  forall x xu ex,
+  (bpow (ex - 1)%Z <= x < bpow ex)%R ->
+  (fexp ex < ex)%Z ->
+  Rnd_UP_pt generic_format x xu ->
+  (xu <= bpow ex)%R.
+Proof.
+intros x xu ex Hx He (((dm, de), (Hu1, Hu2)), (Hu3, Hu4)).
+apply Hu4 with (2 := (Rlt_le _ _ (proj2 Hx))).
+exists (Float beta (Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
+unfold F2R. simpl.
+split.
+(* . *)
+rewrite Z2R_Zpower.
+rewrite <- epow_add.
+apply f_equal.
+ring.
+generalize (proj1 (prop_exp _) He).
+omega.
+(* . *)
+intros H.
+apply f_equal.
+apply sym_eq.
+apply ln_beta_unique.
+rewrite Rabs_pos_eq.
+split.
+ring_simplify (ex + 1 - 1)%Z.
+apply Rle_refl.
+apply -> epow_lt.
+apply Zlt_succ.
+apply epow_ge_0.
+Qed.
+
 End RND_generic.