Commit 5120bc45 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Made canonic floats explicit for generic format.

parent dd74b2f2
......@@ -40,20 +40,20 @@ split.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
rewrite Hx1.
eexists ; repeat split.
exact Hx2.
now apply generic_format_canonic.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
rewrite Hx1.
intros H.
rewrite H.
eexists ; repeat split.
exact Hx2.
Qed.
Theorem FIX_format_satisfies_any :
satisfies_any FIX_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp _)).
exact FIX_format_generic.
intros x.
apply iff_sym.
apply FIX_format_generic.
exact FIX_exp_correct.
Qed.
......
......@@ -58,56 +58,48 @@ intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta x) as (ex, Hx5).
simpl.
specialize (Hx5 Hx4).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now eexists.
now rewrite <- Hx1.
rewrite Hx1, (F2R_change_exp beta emin).
now eexists.
exact Hx3.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
simpl.
split.
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
now apply Zlt_le_weak.
apply Zle_refl.
rewrite Hx1.
eexists ; repeat split.
destruct (ln_beta beta x) as (ex, Hx4).
simpl in Hx2.
specialize (Hx4 Hx3).
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 <- bpow_lt.
apply Rle_lt_trans with (1 := proj1 Hx5).
rewrite Hx1.
apply F2R_lt_bpow.
simpl.
now ring_simplify (prec + xe - xe)%Z.
(* . *)
unfold generic_format.
set (ex := canonic_exponent beta FLT_exp x).
set (mx := Ztrunc (x * bpow (- ex))).
intros Hx.
rewrite Hx.
eexists ; repeat split ; simpl.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow (ex - prec)).
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
apply bpow_gt_0.
rewrite <- bpow_add.
replace (prec + (ex - prec))%Z with ex by ring.
apply Rle_lt_trans with (Z2R (Zabs xm) * bpow xe)%R.
rewrite Hx2.
apply Rmult_le_compat_l.
apply (Z2R_le 0).
apply Zabs_pos.
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
rewrite <- abs_F2R.
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
unfold canonic_exponent in ex.
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
apply -> bpow_le.
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
apply Zle_max_l.
replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x).
exact (proj2 Hx4).
rewrite Hx1.
apply abs_F2R.
now apply Zlt_le_weak.
rewrite Hx2.
apply Zle_max_r.
Qed.
......@@ -122,28 +114,20 @@ exact FLT_exp_correct.
Qed.
Theorem FLT_canonic_FLX :
forall x : R,
forall x, x <> R0 ->
(bpow (emin + prec - 1) <= Rabs x)%R ->
forall f : float beta,
( canonic beta FLT_exp x f <-> canonic beta (FLX_exp prec) x f ).
canonic_exponent beta FLT_exp x = canonic_exponent beta (FLX_exp prec) x.
Proof.
intros x Hx f.
unfold canonic.
replace (FLT_exp (projT1 (ln_beta beta x))) with (FLX_exp prec (projT1 (ln_beta beta x))).
apply iff_refl.
unfold FLX_exp, FLT_exp.
apply sym_eq.
intros x Hx0 Hx.
unfold canonic_exponent.
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
simpl.
assert (emin + prec - 1 < ex)%Z. 2: omega.
unfold FLX_exp. simpl.
specialize (He Hx0).
cut (emin + prec - 1 < ex)%Z. omega.
apply <- (bpow_lt beta).
apply Rle_lt_trans with (1 := Hx).
apply He.
intros H.
elim Rlt_not_le with (2 := Hx).
rewrite H, Rabs_R0.
apply bpow_gt_0.
Qed.
Theorem FLT_generic_format_FLX :
......@@ -152,10 +136,11 @@ Theorem FLT_generic_format_FLX :
( generic_format beta FLT_exp x <-> generic_format beta (FLX_exp prec) x ).
Proof.
intros x Hx.
assert (Hc := FLT_canonic_FLX x Hx).
split ; intros (f, Hf) ; exists f.
now apply -> Hc.
now apply <- Hc.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ; apply generic_format_0.
unfold generic_format.
now rewrite (FLT_canonic_FLX x Hx0 Hx).
Qed.
Theorem FLT_format_FLX :
......@@ -164,22 +149,21 @@ Theorem FLT_format_FLX :
( FLT_format x <-> FLX_format beta prec x ).
Proof.
intros x Hx1.
assert (Hc := FLT_canonic_FLX x Hx1).
apply iff_trans with (1 := FLT_format_generic x).
apply iff_trans with (1 := FLT_generic_format_FLX x Hx1).
apply iff_sym.
now apply FLX_format_generic.
Qed.
Theorem FLT_exp_FIX :
Theorem FLT_canonic_FIX :
forall x, x <> R0 ->
(Rabs x < bpow (emin + prec))%R ->
FLT_exp (projT1 (ln_beta beta x)) = FIX_exp emin (projT1 (ln_beta beta x)).
canonic_exponent beta FLT_exp x = canonic_exponent beta (FIX_exp emin) x.
Proof.
intros x Hx0 Hx.
unfold FIX_exp, FLT_exp.
rewrite Zmax_right.
apply refl_equal.
unfold canonic_exponent.
apply Zmax_right.
unfold FIX_exp.
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 < emin + prec)%Z. omega.
......@@ -188,15 +172,35 @@ apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.
Theorem FLT_canonic_FIX :
forall x : R, x <> R0 ->
(Rabs x < bpow (emin + prec))%R ->
forall f : float beta,
( canonic beta FLT_exp x f <-> canonic beta (FIX_exp emin) x f ).
Theorem FLT_generic_format_FIX :
forall x : R,
(Rabs x <= bpow (emin + prec))%R ->
( generic_format beta FLT_exp x <-> generic_format beta (FIX_exp emin) x ).
Proof.
intros x Hx0 Hx f.
unfold canonic.
now rewrite FLT_exp_FIX.
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ; apply generic_format_0.
destruct Hx as [Hx|Hx].
unfold generic_format.
now rewrite (FLT_canonic_FIX x Hx0 Hx).
(* extra case *)
rewrite <- (Rabs_pos_eq (bpow (emin + prec))) in Hx. 2: apply bpow_ge_0.
assert (H1: generic_format beta FLT_exp (bpow (emin + prec))).
rewrite <- F2R_bpow.
apply generic_format_canonic_exponent.
unfold generic_format, canonic_exponent, FLT_exp.
rewrite F2R_bpow, ln_beta_bpow.
apply Zmax_lub ; omega.
assert (H2: generic_format beta (FIX_exp emin) (bpow (emin + prec))).
rewrite <- F2R_bpow.
apply generic_format_canonic_exponent.
unfold generic_format, canonic_exponent, FIX_exp.
omega.
destruct Rabs_eq_Rabs with (1 := Hx) as [H|H] ;
rewrite H ; clear H ;
split ; intros _ ;
try apply generic_format_opp ; easy.
Qed.
Theorem FLT_format_FIX :
......@@ -204,54 +208,11 @@ Theorem FLT_format_FIX :
(Rabs x <= bpow (emin + prec))%R ->
( FLT_format x <-> FIX_format beta emin x ).
Proof.
intros x Hx.
split.
(* . *)
intros ((xm, xe), (H1, (H2, H3))).
rewrite H1, (F2R_change_exp beta emin).
now eexists.
exact H3.
(* . *)
destruct Hx as [Hx|Hx].
(* . . *)
intros ((xm, xe), (H1, H2)).
rewrite H1.
eexists ; repeat split.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow xe).
apply bpow_gt_0.
rewrite H1, abs_F2R in Hx.
apply Rlt_le_trans with (1 := Hx).
rewrite <- bpow_add.
apply -> bpow_le.
rewrite Zplus_comm, <- H2.
apply Zle_refl.
now apply Zlt_le_weak.
now apply Zeq_le.
(* . . *)
assert (Ha: forall x, FLT_format (Rabs x) -> FLT_format x).
clear.
intros x Ha.
unfold Rabs in Ha.
destruct (Rcase_abs x) as [Hx|Hx].
apply <- FLT_format_generic.
rewrite <- (Ropp_involutive x).
apply generic_format_sym.
now apply -> FLT_format_generic.
exact Ha.
(* . . *)
intros _.
apply Ha.
rewrite Hx.
exists (Float beta 1 (emin + prec)).
split.
apply sym_eq.
apply Rmult_1_l.
simpl.
split.
now apply Zpower_gt_1.
omega.
intros x Hx1.
apply iff_trans with (1 := FLT_format_generic x).
apply iff_trans with (1 := FLT_generic_format_FIX x Hx1).
apply iff_sym.
now apply FIX_format_generic.
Qed.
Theorem Rnd_NE_pt_FLT :
......
......@@ -111,7 +111,9 @@ apply FIX_format_generic.
assert (Hf: FLX_exp (projT1 (ln_beta beta x)) = FIX_exp (ex - prec) (projT1 (ln_beta beta x))).
unfold FIX_exp, FLX_exp.
now rewrite ln_beta_unique with (1 := Hx2).
split ; apply generic_format_fun_eq ; now rewrite Hf.
split ;
unfold generic_format, canonic_exponent ;
now rewrite Hf.
Qed.
Theorem FLX_format_satisfies_any :
......
......@@ -58,20 +58,21 @@ destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
specialize (Hx2 Hx4).
unfold generic_format, canonic, FTZ_exp.
rewrite Hx1.
apply generic_format_canonic_exponent.
unfold canonic_exponent, FTZ_exp.
rewrite <- Hx1.
destruct (ln_beta beta x) as (ex, Hx6).
simpl.
specialize (Hx6 Hx4).
generalize (Zlt_cases (ex - prec) emin).
case (Zlt_bool (ex - prec) emin) ; intros H1.
elim (Rlt_not_ge _ _ (proj2 Hx6)).
apply Rle_ge.
rewrite Hx1.
elim (Rlt_not_le _ _ (proj2 Hx6)).
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
rewrite <- bpow_add.
apply -> bpow_le.
omega.
rewrite abs_F2R.
rewrite Hx1, abs_F2R.
unfold F2R. simpl.
apply Rmult_le_compat.
apply bpow_ge_0.
......@@ -81,11 +82,16 @@ now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
now apply -> bpow_le.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec (proj2 Hx2)).
now eexists.
now rewrite <- Hx1.
cut (ex - 1 < prec + xe)%Z. omega.
apply <- (bpow_lt beta).
apply Rle_lt_trans with (1 := proj1 Hx6).
rewrite Hx1.
apply F2R_lt_bpow.
simpl.
ring_simplify (prec + xe - xe)%Z.
apply Hx2.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
intros Hx.
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
split.
......@@ -95,15 +101,15 @@ split.
intros H.
now elim H.
apply Zle_refl.
unfold generic_format, canonic_exponent, FTZ_exp in Hx.
destruct (ln_beta beta x) as (ex, Hx4).
simpl in Hx2.
simpl in Hx.
specialize (Hx4 Hx3).
unfold FTZ_exp in Hx2.
generalize (Zlt_cases (ex - prec) emin) Hx2. clear Hx2.
generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx.
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
elim Rlt_not_ge with (1 := proj2 Hx4).
apply Rle_ge.
rewrite Hx1, abs_F2R.
rewrite Hx2, abs_F2R.
rewrite <- (Rmult_1_l (bpow ex)).
unfold F2R. simpl.
apply Rmult_le_compat.
......@@ -112,29 +118,24 @@ apply bpow_ge_0.
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow xe).
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
apply bpow_gt_0.
rewrite Rmult_0_l.
change (0 < F2R (Float beta (Zabs xm) xe))%R.
rewrite <- abs_F2R, <- Hx1.
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
rewrite <- abs_F2R, <- Hx2.
now apply Rabs_pos_lt.
apply -> bpow_le.
omega.
exists (Float beta xm xe).
split.
exact Hx1.
split.
intros _.
split.
rewrite Hx2.
eexists ; repeat split ; simpl.
apply le_Z2R.
rewrite Z2R_Zpower.
apply Rmult_le_reg_r with (bpow (ex - prec)).
apply bpow_gt_0.
rewrite <- bpow_add.
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
rewrite <- Hx2.
change (bpow (ex - 1) <= F2R (Float beta (Zabs xm) xe))%R.
rewrite <- abs_F2R, <- Hx1.
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
rewrite <- abs_F2R, <- Hx2.
apply Hx4.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
......@@ -144,13 +145,10 @@ apply Rmult_lt_reg_r with (bpow (ex - prec)).
apply bpow_gt_0.
rewrite <- bpow_add.
replace (prec + (ex - prec))%Z with ex by ring.
rewrite <- Hx2.
change (F2R (Float beta (Zabs xm) xe) < bpow ex)%R.
rewrite <- abs_F2R, <- Hx1.
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
rewrite <- abs_F2R, <- Hx2.
apply Hx4.
now apply Zlt_le_weak.
simpl.
rewrite Hx2.
now apply Zge_le.
Qed.
......
This diff is collapsed.
......@@ -19,38 +19,38 @@ Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition NE_prop (_ : R) f :=
exists g : float beta, canonic f g /\ Zeven (Fnum g).
exists g : float beta, f = F2R g /\ canonic g /\ Zeven (Fnum g).
Definition Rnd_NE_pt :=
Rnd_NG_pt format NE_prop.
Definition DN_UP_parity_pos_prop :=
forall x xd xu cd cu,
forall x xd xu,
(0 < x)%R ->
~ format x ->
canonic xd cd ->
canonic xu cu ->
Rnd_DN_pt format x xd ->
Rnd_UP_pt format x xu ->
Zodd (Fnum cd + Fnum cu).
canonic xd ->
canonic xu ->
Rnd_DN_pt format x (F2R xd) ->
Rnd_UP_pt format x (F2R xu) ->
Zodd (Fnum xd + Fnum xu).
Definition DN_UP_parity_prop :=
forall x xd xu cd cu,
forall x xd xu,
~ format x ->
canonic xd cd ->
canonic xu cu ->
Rnd_DN_pt format x xd ->
Rnd_UP_pt format x xu ->
Zodd (Fnum cd + Fnum cu).
canonic xd ->
canonic xu ->
Rnd_DN_pt format x (F2R xd) ->
Rnd_UP_pt format x (F2R xu) ->
Zodd (Fnum xd + Fnum xu).
Theorem DN_UP_parity_aux :
DN_UP_parity_pos_prop ->
DN_UP_parity_prop.
Proof.
intros Hpos x xd xu cd cu Hfx Hd Hu Hxd Hxu.
intros Hpos x xd xu Hfx Hd Hu Hxd Hxu.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
(* . *)
exact (Hpos x xd xu cd cu Hx Hfx Hd Hu Hxd Hxu).
exact (Hpos x xd xu Hx Hfx Hd Hu Hxd Hxu).
elim Hfx.
rewrite <- Hx.
apply generic_format_0.
......@@ -58,26 +58,28 @@ apply generic_format_0.
assert (Hx': (0 < -x)%R).
apply Ropp_lt_cancel.
now rewrite Ropp_involutive, Ropp_0.
destruct cd as (md, ed).
destruct cu as (mu, eu).
replace (Fnum (Float beta md ed) + Fnum (Float beta mu eu))%Z
with (-1 * ((Fnum (Float beta (-mu) ed) + Fnum (Float beta (-md) eu))))%Z
destruct xd as (md, ed).
destruct xu as (mu, eu).
simpl.
replace (md + mu)%Z
with (-1 * ((Fnum (Float beta (-mu) eu)) + Fnum (Float beta (-md) ed)))%Z
by (unfold Fnum ; ring).
apply Zodd_mult_Zodd.
now apply (Zodd_pred 0).
apply (Hpos (-x)%R (-xu)%R (-xd)%R (Float beta (-mu) eu) (Float beta (-md) ed)).
exact Hx'.
apply (Hpos (-x)%R _ _ Hx').
intros H.
apply Hfx.
rewrite <- (Ropp_involutive x).
now apply generic_format_sym.
now apply canonic_sym.
now apply canonic_sym.
rewrite <- Ropp_involutive.
now apply generic_format_opp.
now apply canonic_opp.
now apply canonic_opp.
apply Rnd_UP_DN_pt_sym.
apply generic_format_sym.
apply generic_format_opp.
rewrite <- opp_F2R.
now rewrite 2!Ropp_involutive.
apply Rnd_DN_UP_pt_sym.
apply generic_format_sym.
apply generic_format_opp.
rewrite <- opp_F2R.
now rewrite 2!Ropp_involutive.
Qed.
......@@ -89,30 +91,30 @@ Hypothesis strong_fexp : Zodd (radix_val beta) \/ forall e,
Theorem DN_UP_parity_generic_pos :
DN_UP_parity_pos_prop.
Proof.
intros x xd xu cd cu H0x Hfx Hd Hu Hxd Hxu.
intros x xd xu H0x Hfx Hd Hu Hxd Hxu.
destruct (ln_beta beta x) as (ex, Hexa).
specialize (Hexa (Rgt_not_eq _ _ H0x)).
generalize Hexa. intros Hex.
rewrite (Rabs_pos_eq _ (Rlt_le _ _ H0x)) in Hex.
destruct (Zle_or_lt ex (fexp ex)) as [Hxe|Hxe].
(* small x *)
assert (Hd3 : Fnum cd = Z0).
apply F2R_eq_0_reg with beta (Fexp cd).
change (F2R cd = R0).
rewrite <- (proj1 Hd).
assert (Hd3 : Fnum xd = Z0).
apply F2R_eq_0_reg with beta (Fexp xd).
change (F2R xd = R0).
apply Rnd_DN_pt_unicity with (1 := Hxd).
now apply generic_DN_pt_small_pos with (2 := Hex).
assert (Hu3 : cu = Float beta (1 * Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
assert (Hu3 : xu = Float beta (1 * Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
apply canonic_unicity with (1 := Hu).
replace xu with (bpow (fexp ex)).
split.
rewrite <- F2R_bpow.
apply F2R_change_exp.
apply (f_equal fexp).
rewrite <- F2R_change_exp.
now rewrite F2R_bpow, ln_beta_bpow.
now eapply valid_fexp.
simpl.
now rewrite ln_beta_bpow.
rewrite <- F2R_change_exp.
rewrite F2R_bpow.
apply sym_eq.
apply Rnd_UP_pt_unicity with (2 := Hxu).
now apply generic_UP_pt_small_pos.
now eapply valid_fexp.
rewrite Hd3, Hu3.
rewrite Zmult_1_l.
simpl.
......@@ -124,7 +126,7 @@ rewrite (proj2 (H ex)).
now rewrite Zminus_diag.
exact Hxe.
(* large x *)
assert (Hd4: (bpow (ex - 1) <= Rabs xd < bpow ex)%R).
assert (Hd4: (bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R).
rewrite Rabs_pos_eq.
split.
apply Hxd.
......@@ -138,7 +140,7 @@ apply Hxd.
apply generic_format_0.
now apply Rlt_le.
assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now eapply valid_fexp.
destruct (total_order_T (bpow ex) xu) as [[Hu2|Hu2]|Hu2].
destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2].
(* - xu > bpow ex *)
elim (Rlt_not_le _ _ Hu2).
apply Rnd_UP_pt_monotone with (generic_format beta fexp) x (bpow ex).
......@@ -151,23 +153,21 @@ apply Rle_refl.
easy.
now apply Rlt_le.
(* - xu = bpow ex *)
assert (Hu3: cu = Float beta (1 * Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
assert (Hu3: xu = Float beta (1 * Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
apply canonic_unicity with (1 := Hu).
rewrite <- Hu2.
split.
apply (f_equal fexp).
rewrite <- F2R_change_exp.
now rewrite F2R_bpow, ln_beta_bpow.
now eapply valid_fexp.
rewrite <- Hu2.
apply sym_eq.
rewrite <- F2R_change_exp.
apply F2R_bpow.
exact Hxe2.
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_bpow.
assert (Hd3: cd = Float beta (Zpower (radix_val beta) (ex - fexp ex) - 1) (fexp ex)).
apply canonic_unicity with (1 := Hd).
generalize (ulp_pred_succ_pt beta _ valid_fexp x xd xu Hfx Hxd Hxu).
assert (Hd3: xd = Float beta (Zpower (radix_val beta) (ex - fexp ex) - 1) (fexp ex)).
assert (H: F2R xd = F2R (Float beta (Zpower (radix_val beta) (ex - fexp ex) - 1) (fexp ex))).
generalize (ulp_pred_succ_pt beta _ valid_fexp x (F2R xd) (F2R xu) Hfx Hxd Hxu).
intros Hud.
split.
unfold F2R. simpl.
rewrite minus_Z2R.
unfold Rminus.
......@@ -175,7 +175,7 @@ rewrite Rmult_plus_distr_r.
rewrite Z2R_Zpower, <- bpow_add.
ring_simplify (ex - fexp ex + fexp ex)%Z.
rewrite Hu2, Hud.
unfold ulp.
unfold ulp, canonic_exponent.