Commit 7342fe42 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Specified handling of infinities for free.

parent 6ce3ff3a
......@@ -142,21 +142,22 @@ rewrite opp_F2R.
now case sx.
Qed.
Theorem abs_B2R_lt_emax :
forall x,
(Rabs (B2R x) < bpow radix2 (emax + prec))%R.
Theorem bounded_lt_emax :
forall mx ex,
bounded mx ex = true ->
(F2R (Float radix2 (Zpos mx) ex) < bpow radix2 (emax + prec))%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
intros mx ex Hx.
destruct (andb_prop _ _ Hx) as (H1,H2).
generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1.
generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2.
replace (Rabs (F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex))) with (Rabs (F2R (Float radix2 (Zpos mx) ex))).
2: rewrite 2!abs_F2R ; now case sx.
generalize (ln_beta_F2R_digits radix2 (Zpos mx) ex).
destruct (ln_beta radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex).
unfold ln_beta_val.
intros H.
apply Rlt_le_trans with (bpow radix2 e').
change (Zpos mx) with (Zabs (Zpos mx)).
rewrite <- abs_F2R.
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
......@@ -171,6 +172,15 @@ intros.
omega.
Qed.
Theorem B2R_lt_emax :
forall x,
(Rabs (B2R x) < bpow radix2 (emax + prec))%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
rewrite abs_F2R, abs_cond_Zopp.
now apply bounded_lt_emax.
Qed.
Theorem bounded_canonic_lt_emax :
forall mx ex,
canonic radix2 fexp (Float radix2 (Zpos mx) ex) ->
......@@ -241,10 +251,12 @@ Theorem binary_round_sign_correct :
forall mode x mx ex lx,
inbetween_float radix2 (Zpos mx) ex (Rabs x) lx ->
(ex <= fexp (digits radix2 (Zpos mx) + ex))%Z ->
(Rabs (round radix2 fexp (round_mode mode) x) < bpow radix2 (emax + prec))%R ->
B2R (binary_round_sign mode (Rlt_bool x 0) mx ex lx) = round radix2 fexp (round_mode mode) x.
if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) x)) (bpow radix2 (emax + prec)) then
B2R (binary_round_sign mode (Rlt_bool x 0) mx ex lx) = round radix2 fexp (round_mode mode) x
else
binary_round_sign mode (Rlt_bool x 0) mx ex lx = B754_infinity (Rlt_bool x 0).
Proof.
intros m x mx ex lx Bx Ex Hx.
intros m x mx ex lx Bx Ex.
unfold binary_round_sign.
refine (_ (round_trunc_sign_any_correct _ _ fexp_correct (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))).
refine (_ (truncate_correct_partial _ _ fexp_correct _ _ _ _ _ Bx Ex)).
......@@ -276,12 +288,15 @@ assert (Br: inbetween_float radix2 m1' e1 (Rabs (round radix2 fexp (round_mode m
now apply inbetween_Exact.
destruct m1' as [|m1'|m1'].
(* . m1' = 0 *)
rewrite Rlt_bool_true.
generalize (truncate_0 radix2 fexp e1 loc_Exact).
destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
intros Hm2.
rewrite Hm2. simpl.
apply sym_eq.
case Rlt_bool ; apply F2R_0.
rewrite abs_F2R, abs_cond_Zopp, F2R_0.
apply bpow_gt_0.
(* . 0 < m1' *)
assert (He: (e1 <= fexp (digits radix2 (Zpos m1') + e1))%Z).
rewrite <- ln_beta_F2R_digits, <- Hr, ln_beta_abs.
......@@ -308,14 +323,22 @@ destruct m2 as [|m2|m2].
elim Rgt_not_eq with (2 := H3).
rewrite F2R_0.
now apply F2R_gt_0_compat.
rewrite F2R_cond_Zopp, H3, abs_cond_Ropp, abs_F2R.
simpl Zabs.
case (Sumbool.sumbool_of_bool (bounded m2 e2)) ; intros Hb.
rewrite Rlt_bool_true.
simpl.
now rewrite 2!F2R_cond_Zopp, H3.
rewrite bounded_canonic_lt_emax in Hb.
discriminate Hb.
apply F2R_cond_Zopp.
now apply bounded_lt_emax.
rewrite Rlt_bool_false.
apply refl_equal.
apply Rnot_lt_le.
intros Hx.
revert Hb.
rewrite bounded_canonic_lt_emax with (2 := Hx).
discriminate.
unfold canonic.
now rewrite <- H3.
now rewrite <- H3, <- Hr.
elim Rgt_not_eq with (2 := H3).
apply Rlt_trans with R0.
now apply F2R_lt_0_compat.
......@@ -341,6 +364,14 @@ exact inbetween_int_UP_sign.
exact inbetween_int_NA_sign.
Qed.
Definition Bsign x :=
match x with
| B754_nan => false
| B754_zero s => s
| B754_infinity s => s
| B754_finite s _ _ _ => s
end.
Definition Bmult m x y :=
match x, y with
| B754_nan, _ => x
......@@ -357,13 +388,15 @@ Definition Bmult m x y :=
binary_round_sign m (xorb sx sy) (Pmult mx my) (ex + ey) loc_Exact
end.
Theorem B2R_mult :
Theorem Bmult_correct :
forall m x y,
(Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y)%R) < bpow radix2 (emax + prec))%R ->
B2R (Bmult m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y)%R.
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 (emax + prec)) then
B2R (Bmult m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y)
else
Bmult m x y = B754_infinity (xorb (Bsign x) (Bsign y)).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ;
try ( intros ; apply sym_eq ; try rewrite Rmult_0_r ; try rewrite Rmult_0_l ; apply round_0 ).
try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ apply refl_equal | apply bpow_gt_0 ] ).
simpl.
rewrite <- mult_F2R.
simpl Fmult.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment