From 9d8706aa0442788ae0f97ee0d49906762dd697ed Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 24 Dec 2011 08:55:21 +0000 Subject: [PATCH] Prove that a representable number, once rounded (whatever the format/direction), is still representable. --- src/Core/Fcore_generic_fmt.v | 83 ++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v index 1a6d053..c42bceb 100644 --- a/src/Core/Fcore_generic_fmt.v +++ b/src/Core/Fcore_generic_fmt.v @@ -338,6 +338,30 @@ now apply Rle_lt_trans with (2 := Ex). now rewrite (proj2 (proj2 (valid_exp _) He)). Qed. +Theorem ln_beta_generic_gt : + forall x, (x <> 0)%R -> + generic_format x -> + (canonic_exp x < ln_beta beta x)%Z. +Proof. +intros x Zx Gx. +apply Znot_ge_lt. +unfold canonic_exp. +destruct (ln_beta beta x) as (ex,Ex) ; simpl. +specialize (Ex Zx). +intros H. +apply Zge_le in H. +generalize (scaled_mantissa_small x ex (proj2 Ex) H). +contradict Zx. +rewrite Gx. +replace (Ztrunc (scaled_mantissa x)) with Z0. +apply F2R_0. +cut (Zabs (Ztrunc (scaled_mantissa x)) < 1)%Z. +clear ; zify ; omega. +apply lt_Z2R. +rewrite Z2R_abs. +now rewrite <- scaled_mantissa_generic. +Qed. + Theorem mantissa_DN_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> @@ -2025,6 +2049,65 @@ apply He. now apply ln_beta_gt_bpow. Qed. +Variable rnd : R -> Z. +Context { valid_rnd : Valid_rnd rnd }. + +Theorem generic_round_generic : + forall x, + generic_format fexp1 x -> + generic_format fexp1 (round fexp2 rnd x). +Proof with auto with typeclass_instances. +intros x Gx. +apply generic_format_abs_inv. +apply generic_format_abs in Gx. +revert rnd valid_rnd x Gx. +refine (round_abs_abs' _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _). +intros rnd valid_rnd x [Hx|Hx] Gx. +(* x > 0 *) +generalize (ln_beta_generic_gt _ x (Rgt_not_eq _ _ Hx) Gx). +unfold canonic_exp. +destruct (ln_beta beta x) as (ex,Ex) ; simpl. +specialize (Ex (Rgt_not_eq _ _ Hx)). +intros He'. +rewrite Rabs_pos_eq in Ex by now apply Rlt_le. +destruct (Zle_or_lt ex (fexp2 ex)) as [He|He]. +(* - x near 0 for fexp2 *) +destruct (round_bounded_small_pos fexp2 rnd x ex He Ex) as [Hr|Hr]. +rewrite Hr. +apply generic_format_0. +rewrite Hr. +apply generic_format_bpow'... +apply Zlt_le_weak. +apply valid_exp_large with ex... +(* - x large for fexp2 *) +destruct (Zle_or_lt (canonic_exp fexp2 x) (canonic_exp fexp1 x)) as [He''|He'']. +(* - - round fexp2 x is representable for fexp1 *) +rewrite round_generic... +rewrite Gx. +apply generic_format_F2R. +fold (round fexp1 Ztrunc x). +intros Zx. +unfold canonic_exp at 1. +rewrite ln_beta_round_ZR... +contradict Zx. +apply F2R_eq_0_reg with (1 := Zx). +(* - - round fexp2 x has too many digits for fexp1 *) +destruct (round_bounded_large_pos fexp2 rnd x ex He Ex) as (Hr1,[Hr2|Hr2]). +apply generic_format_F2R. +intros Zx. +fold (round fexp2 rnd x). +unfold canonic_exp at 1. +rewrite ln_beta_unique_pos with (1 := conj Hr1 Hr2). +rewrite <- ln_beta_unique_pos with (1 := Ex). +now apply Zlt_le_weak. +rewrite Hr2. +apply generic_format_bpow'... +now apply Zlt_le_weak. +(* x = 0 *) +rewrite <- Hx, round_0... +apply generic_format_0. +Qed. + End Inclusion. End Generic. -- GitLab