Commit 21e92c6a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan Committed by Guillaume Melquiond

Add support for NaN payload.

parent 07c3c8c2
......@@ -33,7 +33,7 @@ Section AnyRadix.
Inductive full_float :=
| F754_zero : bool -> full_float
| F754_infinity : bool -> full_float
| F754_nan : full_float
| F754_nan : bool -> positive -> full_float
| F754_finite : bool -> positive -> Z -> full_float.
Definition FF2R beta x :=
......@@ -67,16 +67,20 @@ Definition bounded m e :=
Definition valid_binary x :=
match x with
| F754_finite _ m e => bounded m e
| F754_nan _ pl => (Z_of_nat' (S (digits2_Pnat pl)) <? prec)%Z
| _ => true
end.
(** Basic type used for representing binary FP numbers.
Note that there is exactly one such object per FP datum.
NaNs do not have any payload. They cannot be distinguished. *)
Definition nan_pl := {pl | (Z_of_nat' (S (digits2_Pnat pl)) <? prec)%Z = true}.
Inductive binary_float :=
| B754_zero : bool -> binary_float
| B754_infinity : bool -> binary_float
| B754_nan : binary_float
| B754_nan : bool -> nan_pl -> binary_float
| B754_finite : bool ->
forall (m : positive) (e : Z), bounded m e = true -> binary_float.
......@@ -85,7 +89,7 @@ Definition FF2B x :=
| F754_finite s m e => B754_finite s m e
| F754_infinity s => fun _ => B754_infinity s
| F754_zero s => fun _ => B754_zero s
| F754_nan => fun _ => B754_nan
| F754_nan b pl => fun H => B754_nan b (exist _ pl H)
end.
Definition B2FF x :=
......@@ -93,7 +97,7 @@ Definition B2FF x :=
| B754_finite s m e _ => F754_finite s m e
| B754_infinity s => F754_infinity s
| B754_zero s => F754_zero s
| B754_nan => F754_nan
| B754_nan b (exist pl _) => F754_nan b pl
end.
Definition radix2 := Build_radix 2 (refl_equal true).
......@@ -108,30 +112,30 @@ Theorem FF2R_B2FF :
forall x,
FF2R radix2 (B2FF x) = B2R x.
Proof.
now intros [sx|sx| |sx mx ex Hx].
now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx].
Qed.
Theorem B2FF_FF2B :
forall x Hx,
B2FF (FF2B x Hx) = x.
Proof.
now intros [sx|sx| |sx mx ex] Hx.
now intros [sx|sx|sx plx|sx mx ex] Hx.
Qed.
Theorem valid_binary_B2FF :
forall x,
valid_binary (B2FF x) = true.
Proof.
now intros [sx|sx| |sx mx ex Hx].
now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx].
Qed.
Theorem FF2B_B2FF :
forall x H,
FF2B (B2FF x) H = x.
Proof.
intros [sx|sx| |sx mx ex Hx] H ; try easy.
apply f_equal.
apply eqbool_irrelevance.
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] H ; try easy.
simpl. apply f_equal, f_equal, eqbool_irrelevance.
apply f_equal, eqbool_irrelevance.
Qed.
Theorem FF2B_B2FF_valid :
......@@ -146,7 +150,7 @@ Theorem B2R_FF2B :
forall x Hx,
B2R (FF2B x Hx) = FF2R radix2 x.
Proof.
now intros [sx|sx| |sx mx ex] Hx.
now intros [sx|sx|sx plx|sx mx ex] Hx.
Qed.
Theorem match_FF2B :
......@@ -154,17 +158,17 @@ Theorem match_FF2B :
match FF2B x Hx return T with
| B754_zero sx => fz sx
| B754_infinity sx => fi sx
| B754_nan => fn
| B754_nan b (exist p _) => fn b p
| B754_finite sx mx ex _ => ff sx mx ex
end =
match x with
| F754_zero sx => fz sx
| F754_infinity sx => fi sx
| F754_nan => fn
| F754_nan b p => fn b p
| F754_finite sx mx ex => ff sx mx ex
end.
Proof.
now intros T fz fi fn ff [sx|sx| |sx mx ex] Hx.
now intros T fz fi fn ff [sx|sx|sx plx|sx mx ex] Hx.
Qed.
Theorem canonic_canonic_mantissa :
......@@ -189,7 +193,7 @@ Theorem generic_format_B2R :
forall x,
generic_format radix2 fexp (B2R x).
Proof.
intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0.
intros [sx|sx|sx plx|sx mx ex Hx] ; try apply generic_format_0.
simpl.
apply generic_format_canonic.
apply canonic_canonic_mantissa.
......@@ -210,7 +214,7 @@ Theorem B2FF_inj :
B2FF x = B2FF y ->
x = y.
Proof.
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] [sy|sy|sy [ply Hply]|sy my ey Hy] ; try easy.
(* *)
intros H.
now inversion H.
......@@ -221,11 +225,18 @@ now inversion H.
intros H.
inversion H.
clear H.
revert Hplx.
rewrite H2.
intros Hx.
apply f_equal, f_equal, eqbool_irrelevance.
(* *)
intros H.
inversion H.
clear H.
revert Hx.
rewrite H2, H3.
intros Hx.
apply f_equal.
apply eqbool_irrelevance.
apply f_equal, eqbool_irrelevance.
Qed.
Definition is_finite_strict f :=
......@@ -299,37 +310,71 @@ Theorem is_finite_FF_B2FF :
forall x,
is_finite_FF (B2FF x) = is_finite x.
Proof.
now intros [| |? []|].
Qed.
Definition is_nan f :=
match f with
| B754_nan _ _ => true
| _ => false
end.
Definition is_nan_FF f :=
match f with
| F754_nan _ _ => true
| _ => false
end.
Theorem is_nan_FF2B :
forall x Hx,
is_nan (FF2B x Hx) = is_nan_FF x.
Proof.
now intros [| | |].
Qed.
Definition Bopp x :=
Theorem is_nan_FF_B2FF :
forall x,
is_nan_FF (B2FF x) = is_nan x.
Proof.
now intros [| |? []|].
Qed.
Definition Bopp opp_nan x :=
match x with
| B754_nan => x
| B754_nan sx plx =>
let '(sres, plres) := opp_nan sx plx in B754_nan sres plres
| B754_infinity sx => B754_infinity (negb sx)
| B754_finite sx mx ex Hx => B754_finite (negb sx) mx ex Hx
| B754_zero sx => B754_zero (negb sx)
end.
Theorem Bopp_involutive :
forall x, Bopp (Bopp x) = x.
forall opp_nan x,
is_nan x = false ->
Bopp opp_nan (Bopp opp_nan x) = x.
Proof.
now intros [sx|sx| |sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive.
now intros opp_nan [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive.
Qed.
Theorem B2R_Bopp :
forall x,
B2R (Bopp x) = (- B2R x)%R.
forall opp_nan x,
B2R (Bopp opp_nan x) = (- B2R x)%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; apply sym_eq ; try apply Ropp_0.
intros opp_nan [sx|sx|sx plx|sx mx ex Hx]; apply sym_eq ; try apply Ropp_0.
simpl. destruct opp_nan. apply Ropp_0.
simpl.
rewrite <- F2R_opp.
now case sx.
Qed.
Theorem is_finite_Bopp: forall x,
is_finite (Bopp x) = is_finite x.
Theorem is_finite_Bopp :
forall opp_nan x,
is_finite (Bopp opp_nan x) = is_finite x.
Proof.
now intros [| | |].
intros opp_nan [| | |] ; try easy.
intros s pl.
simpl.
now case opp_nan.
Qed.
Theorem bounded_lt_emax :
......@@ -367,7 +412,7 @@ Theorem abs_B2R_lt_emax :
forall x,
(Rabs (B2R x) < bpow radix2 emax)%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
intros [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
rewrite <- F2R_Zabs, abs_cond_Zopp.
now apply bounded_lt_emax.
Qed.
......@@ -644,7 +689,7 @@ Definition binary_round_aux mode sx mx ex lx :=
match shr_m mrs'' with
| Z0 => F754_zero sx
| Zpos m => if Zle_bool e'' (emax - prec) then F754_finite sx m e'' else binary_overflow mode sx
| _ => F754_nan (* dummy *)
| _ => F754_nan false xH (* dummy *)
end.
Theorem binary_round_aux_correct :
......@@ -826,7 +871,7 @@ Qed.
Definition Bsign x :=
match x with
| B754_nan => false
| B754_nan s _ => s
| B754_zero s => s
| B754_infinity s => s
| B754_finite s _ _ _ => s
......@@ -834,7 +879,7 @@ Definition Bsign x :=
Definition sign_FF x :=
match x with
| F754_nan => false
| F754_nan s _ => s
| F754_zero s => s
| F754_infinity s => s
| F754_finite s _ _ => s
......@@ -844,7 +889,7 @@ Theorem Bsign_FF2B :
forall x H,
Bsign (FF2B x H) = sign_FF x.
Proof.
now intros [sx|sx| |sx mx ex] H.
now intros [sx|sx|sx plx|sx mx ex] H.
Qed.
(** Multiplication *)
......@@ -902,15 +947,15 @@ apply Rlt_bool_false.
now apply F2R_ge_0_compat.
Qed.
Definition Bmult m x y :=
Definition Bmult mult_nan m x y :=
let f pl := B754_nan (fst pl) (snd pl) in
match x, y with
| B754_nan, _ => x
| _, B754_nan => y
| B754_nan _ _, _ | _, B754_nan _ _ => f (mult_nan x y)
| B754_infinity sx, B754_infinity sy => B754_infinity (xorb sx sy)
| B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy)
| B754_finite sx _ _ _, B754_infinity sy => B754_infinity (xorb sx sy)
| B754_infinity _, B754_zero _ => B754_nan
| B754_zero _, B754_infinity _ => B754_nan
| B754_infinity _, B754_zero _ => f (mult_nan x y)
| B754_zero _, B754_infinity _ => f (mult_nan x y)
| B754_finite sx _ _ _, B754_zero sy => B754_zero (xorb sx sy)
| B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy)
| B754_zero sx, B754_zero sy => B754_zero (xorb sx sy)
......@@ -919,14 +964,14 @@ Definition Bmult m x y :=
end.
Theorem Bmult_correct :
forall m x y,
forall mult_nan m x y,
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 emax) then
B2R (Bmult m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\
is_finite (Bmult m x y) = andb (is_finite x) (is_finite y)
B2R (Bmult mult_nan m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\
is_finite (Bmult mult_nan m x y) = andb (is_finite x) (is_finite y)
else
B2FF (Bmult m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
B2FF (Bmult mult_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ;
intros mult_nan m [sx|sx|sx plx|sx mx ex Hx] [sy|sy|sy ply|sy my ey Hy] ;
try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ split ; apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ).
simpl.
case Bmult_correct_aux.
......@@ -940,15 +985,15 @@ intros H2.
now rewrite B2FF_FF2B.
Qed.
Definition Bmult_FF m x y :=
Definition Bmult_FF mult_nan m x y :=
let f pl := F754_nan (fst pl) (snd pl) in
match x, y with
| F754_nan, _ => x
| _, F754_nan => y
| F754_nan _ _, _ | _, F754_nan _ _ => f (mult_nan x y)
| F754_infinity sx, F754_infinity sy => F754_infinity (xorb sx sy)
| F754_infinity sx, F754_finite sy _ _ => F754_infinity (xorb sx sy)
| F754_finite sx _ _, F754_infinity sy => F754_infinity (xorb sx sy)
| F754_infinity _, F754_zero _ => F754_nan
| F754_zero _, F754_infinity _ => F754_nan
| F754_infinity _, F754_zero _ => f (mult_nan x y)
| F754_zero _, F754_infinity _ => f (mult_nan x y)
| F754_finite sx _ _, F754_zero sy => F754_zero (xorb sx sy)
| F754_zero sx, F754_finite sy _ _ => F754_zero (xorb sx sy)
| F754_zero sx, F754_zero sy => F754_zero (xorb sx sy)
......@@ -957,14 +1002,20 @@ Definition Bmult_FF m x y :=
end.
Theorem B2FF_Bmult :
forall mult_nan mult_nan_ff,
forall m x y,
B2FF (Bmult m x y) = Bmult_FF m (B2FF x) (B2FF y).
mult_nan_ff (B2FF x) (B2FF y) = (let '(sr, exist plr _) := mult_nan x y in (sr, plr)) ->
B2FF (Bmult mult_nan m x y) = Bmult_FF mult_nan_ff m (B2FF x) (B2FF y).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
intros mult_nan mult_nan_ff m x y Hmult_nan.
unfold Bmult_FF. rewrite Hmult_nan.
destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Hx], y as [sy|sy|sy [ply Hply]|sy my ey Hy] ;
simpl; try match goal with |- context [mult_nan ?x ?y] =>
destruct (mult_nan x y) as [? []] end;
try easy.
apply B2FF_FF2B.
Qed.
Definition shl_align mx ex ex' :=
match (ex' - ex)%Z with
| Zneg d => (shift_pos d mx, ex')
......@@ -1129,12 +1180,12 @@ now apply F2R_lt_0_compat.
Qed.
(** Addition *)
Definition Bplus m x y :=
Definition Bplus plus_nan m x y :=
let f pl := B754_nan (fst pl) (snd pl) in
match x, y with
| B754_nan, _ => x
| _, B754_nan => y
| B754_nan _ _, _ | _, B754_nan _ _ => f (plus_nan x y)
| B754_infinity sx, B754_infinity sy =>
if Bool.eqb sx sy then x else B754_nan
if Bool.eqb sx sy then x else f (plus_nan x y)
| B754_infinity _, _ => x
| _, B754_infinity _ => y
| B754_zero sx, B754_zero sy =>
......@@ -1149,16 +1200,16 @@ Definition Bplus m x y :=
end.
Theorem Bplus_correct :
forall m x y,
forall plus_nan m x y,
is_finite x = true ->
is_finite y = true ->
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x + B2R y))) (bpow radix2 emax) then
B2R (Bplus m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\
is_finite (Bplus m x y) = true
B2R (Bplus plus_nan m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\
is_finite (Bplus plus_nan m x y) = true
else
(B2FF (Bplus m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
(B2FF (Bplus plus_nan m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
Proof with auto with typeclass_instances.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy.
intros plus_nan m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy.
(* *)
rewrite Rplus_0_r, round_0, Rabs_R0, Rlt_bool_true...
simpl.
......@@ -1279,26 +1330,25 @@ now apply f_equal.
apply Sz.
Qed.
Definition Bminus m x y := Bplus m x (Bopp y).
Definition Bminus minus_nan m x y := Bplus minus_nan m x (Bopp pair y).
Theorem Bminus_correct :
forall m x y,
forall minus_nan m x y,
is_finite x = true ->
is_finite y = true ->
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x - B2R y))) (bpow radix2 emax) then
B2R (Bminus m x y) = round radix2 fexp (round_mode m) (B2R x - B2R y) /\
is_finite (Bminus m x y) = true
B2R (Bminus minus_nan m x y) = round radix2 fexp (round_mode m) (B2R x - B2R y) /\
is_finite (Bminus minus_nan m x y) = true
else
(B2FF (Bminus m x y) = binary_overflow m (Bsign x) /\ Bsign x = negb (Bsign y)).
(B2FF (Bminus minus_nan m x y) = binary_overflow m (Bsign x) /\ Bsign x = negb (Bsign y)).
Proof with auto with typeclass_instances.
intros m x y Fx Fy.
replace (negb (Bsign y)) with (Bsign (Bopp y)).
intros m minus_nan x y Fx Fy.
replace (negb (Bsign y)) with (Bsign (Bopp pair y)).
unfold Rminus.
rewrite <- B2R_Bopp.
erewrite <- B2R_Bopp.
apply Bplus_correct.
exact Fx.
now rewrite is_finite_Bopp.
now destruct y as [ | | | ].
rewrite is_finite_Bopp. auto. now destruct y as [ | | | ].
Qed.
(** Division *)
......@@ -1322,7 +1372,7 @@ Lemma Bdiv_correct_aux :
let '(mz, ez, lz) := Fdiv_core_binary (Zpos mx) ex (Zpos my) ey in
match mz with
| Zpos mz => binary_round_aux m (xorb sx sy) mz ez lz
| _ => F754_nan (* dummy *)
| _ => F754_nan false xH (* dummy *)
end in
valid_binary z = true /\
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x / y))) (bpow radix2 emax) then
......@@ -1412,35 +1462,35 @@ apply Rinv_0_lt_compat.
now apply F2R_gt_0_compat.
Qed.
Definition Bdiv m x y :=
Definition Bdiv div_nan m x y :=
let f pl := B754_nan (fst pl) (snd pl) in
match x, y with
| B754_nan, _ => x
| _, B754_nan => y
| B754_infinity sx, B754_infinity sy => B754_nan
| B754_nan _ _, _ | _, B754_nan _ _ => f (div_nan x y)
| B754_infinity sx, B754_infinity sy => f (div_nan x y)
| B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy)
| B754_finite sx _ _ _, B754_infinity sy => B754_zero (xorb sx sy)
| B754_infinity sx, B754_zero sy => B754_infinity (xorb sx sy)
| B754_zero sx, B754_infinity sy => B754_zero (xorb sx sy)
| B754_finite sx _ _ _, B754_zero sy => B754_infinity (xorb sx sy)
| B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy)
| B754_zero sx, B754_zero sy => B754_nan
| B754_zero sx, B754_zero sy => f (div_nan x y)
| B754_finite sx mx ex _, B754_finite sy my ey _ =>
FF2B _ (proj1 (Bdiv_correct_aux m sx mx ex sy my ey))
end.
Theorem Bdiv_correct :
forall m x y,
forall div_nan m x y,
B2R y <> R0 ->
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then
B2R (Bdiv m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\
is_finite (Bdiv m x y) = is_finite x
B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\
is_finite (Bdiv div_nan m x y) = is_finite x
else
B2FF (Bdiv m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
B2FF (Bdiv div_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
Proof.
intros m x [sy|sy| |sy my ey Hy] Zy ; try now elim Zy.
intros div_nan m x [sy|sy|sy ply|sy my ey Hy] Zy ; try now elim Zy.
revert x.
unfold Rdiv.
intros [sx|sx| |sx mx ex Hx] ;
intros [sx|sx|sx plx|sx mx ex Hx] ;
try ( rewrite Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ split ; apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ).
simpl.
case Bdiv_correct_aux.
......@@ -1479,7 +1529,7 @@ Lemma Bsqrt_correct_aux :
let '(mz, ez, lz) := Fsqrt_core_binary (Zpos mx) ex in
match mz with
| Zpos mz => binary_round_aux m false mz ez lz
| _ => F754_nan (* dummy *)
| _ => F754_nan false xH (* dummy *)
end in
valid_binary z = true /\
FF2R radix2 z = round radix2 fexp (round_mode m) (sqrt x) /\
......@@ -1584,23 +1634,24 @@ now case mz.
apply sqrt_ge_0.
Qed.
Definition Bsqrt m x :=
Definition Bsqrt sqrt_nan m x :=
let f pl := B754_nan (fst pl) (snd pl) in
match x with
| B754_nan => x
| B754_nan sx plx => f (sqrt_nan x)
| B754_infinity false => x
| B754_infinity true => B754_nan
| B754_finite true _ _ _ => B754_nan
| B754_infinity true => f (sqrt_nan x)
| B754_finite true _ _ _ => f (sqrt_nan x)
| B754_zero _ => x
| B754_finite sx mx ex Hx =>
FF2B _ (proj1 (Bsqrt_correct_aux m mx ex Hx))
end.
Theorem Bsqrt_correct :
forall m x,
B2R (Bsqrt m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)) /\
is_finite (Bsqrt m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end.
forall sqrt_nan m x,
B2R (Bsqrt sqrt_nan m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)) /\
is_finite (Bsqrt sqrt_nan m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end.
Proof.
intros m [sx|[|]| |sx mx ex Hx] ; try ( now simpl ; rewrite sqrt_0, round_0 ; auto with typeclass_instances ).
intros sqrt_nan m [sx|[|]| |sx mx ex Hx] ; try ( now simpl ; rewrite sqrt_0, round_0 ; auto with typeclass_instances ).
simpl.
case Bsqrt_correct_aux.
intros H1 (H2, H3).
......
......@@ -172,7 +172,7 @@ Definition bits_of_binary_float (x : binary_float) :=
match x with
| B754_zero sx => join_bits sx 0 0
| B754_infinity sx => join_bits sx 0 (Zpower 2 ew - 1)
| B754_nan => join_bits false (Zpower 2 mw - 1) (Zpower 2 ew - 1)
| B754_nan sx (exist plx _) => join_bits sx (Zpos plx) (Zpower 2 ew - 1)
| B754_finite sx mx ex _ =>
if Zle_bool (Zpower 2 mw) (Zpos mx) then
join_bits sx (Zpos mx - Zpower 2 mw) (ex - emin + 1)
......@@ -184,7 +184,7 @@ Definition split_bits_of_binary_float (x : binary_float) :=
match x with
| B754_zero sx => (sx, 0, 0)%Z
| B754_infinity sx => (sx, 0, Zpower 2 ew - 1)%Z
| B754_nan => (false, Zpower 2 mw - 1, Zpower 2 ew - 1)%Z
| B754_nan sx (exist plx _) => (sx, Zpos plx, Zpower 2 ew - 1)%Z
| B754_finite sx mx ex _ =>
if Zle_bool (Zpower 2 mw) (Zpos mx) then
(sx, Zpos mx - Zpower 2 mw, ex - emin + 1)%Z
......@@ -196,8 +196,16 @@ Theorem split_bits_of_binary_float_correct :
forall x,
split_bits (bits_of_binary_float x) = split_bits_of_binary_float x.
Proof.
intros [sx|sx| |sx mx ex Hx] ;
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] ;
try ( simpl ; apply split_join_bits ; split ; try apply Zle_refl ; try apply Zlt_pred ; trivial ; omega ).
simpl. apply split_join_bits; split; try (zify; omega).
destruct (digits2_Pnat_correct plx).
rewrite Zpower_nat_Z in H0.
eapply Zlt_le_trans. apply H0.
change 2%Z with (radix_val radix2). apply Zpower_le.
rewrite Z.ltb_lt in Hplx.
unfold prec in *. zify; omega.
(* *)
unfold bits_of_binary_float, split_bits_of_binary_float.
assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z).
destruct (andb_prop _ _ Hx) as (Hx', _).
......@@ -246,14 +254,18 @@ Definition binary_float_of_bits_aux x :=
match mx with
| Z0 => F754_zero sx
| Zpos px => F754_finite sx px emin
| Zneg _ => F754_nan (* dummy *)
| Zneg _ => F754_nan false xH (* dummy *)
end
else if Zeq_bool ex (Zpower 2 ew - 1) then
if Zeq_bool mx 0 then F754_infinity sx else F754_nan
match mx with
| Z0 => F754_infinity sx
| Zpos plx => F754_nan sx plx
| Zneg _ => F754_nan false xH (* dummy *)
end
else
match (mx + Zpower 2 mw)%Z with
| Zpos px => F754_finite sx px (ex + emin - 1)
| _ => F754_nan (* dummy *)
| _ => F754_nan false xH (* dummy *)
end.
Lemma binary_float_of_bits_aux_correct :
......@@ -292,9 +304,20 @@ cut (0 < emax)%Z. clear -H Hew ; omega.
apply (Zpower_gt_0 radix2).
clear -Hew ; omega.
apply bpow_gt_0.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
case Zeq_bool_spec ; intros He2.
now case Zeq_bool.
case_eq (x mod 2 ^ mw)%Z; try easy.
(* nan *)
intros plx Eqplx. apply Z.ltb_lt.
rewrite Z_of_nat_S_digits2_Pnat.
assert (forall a b, a <= b -> a < b+1)%Z by (intros; omega). apply H. clear H.
apply Zdigits_le_Zpower. simpl.
rewrite <- Eqplx. edestruct Z_mod_lt; eauto.
change 2%Z with (radix_val radix2).
apply Z.lt_gt, Zpower_gt_0. omega.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
case_eq (x mod 2^mw + 2^mw)%Z ; try easy.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
(* normal *)
intros px Hm.