Library compcert.flocq.Appli.Fappli_IEEE_bits
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2011-2013 Sylvie Boldo
Copyright (C) 2011-2013 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2011-2013 Guillaume Melquiond
IEEE-754 encoding of binary floating-point data
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_digits.
Require Import Fappli_IEEE.
Section Binary_Bits.
Implicit Arguments exist [[A] [P]].
Implicit Arguments B754_zero [[prec] [emax]].
Implicit Arguments B754_infinity [[prec] [emax]].
Implicit Arguments B754_nan [[prec] [emax]].
Implicit Arguments B754_finite [[prec] [emax]].
Require Import Fcore_digits.
Require Import Fcalc_digits.
Require Import Fappli_IEEE.
Section Binary_Bits.
Implicit Arguments exist [[A] [P]].
Implicit Arguments B754_zero [[prec] [emax]].
Implicit Arguments B754_infinity [[prec] [emax]].
Implicit Arguments B754_nan [[prec] [emax]].
Implicit Arguments B754_finite [[prec] [emax]].
Number of bits for the fraction and exponent
Variable mw ew : Z.
Hypothesis Hmw : (0 < mw)%Z.
Hypothesis Hew : (0 < ew)%Z.
Let emax := Zpower 2 (ew - 1).
Let prec := (mw + 1)%Z.
Let emin := (3 - emax - prec)%Z.
Let binary_float := binary_float prec emax.
Let Hprec : (0 < prec)%Z.
unfold prec.
apply Zle_lt_succ.
now apply Zlt_le_weak.
Qed.
Let Hm_gt_0 : (0 < 2^mw)%Z.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
Qed.
Let He_gt_0 : (0 < 2^ew)%Z.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
Qed.
Hypothesis Hmax : (prec < emax)%Z.
Definition join_bits (s : bool) m e :=
(Z.shiftl ((if s then Zpower 2 ew else 0) + e) mw + m)%Z.
Lemma join_bits_range :
∀ s m e,
(0 ≤ m < 2^mw)%Z →
(0 ≤ e < 2^ew)%Z →
(0 ≤ join_bits s m e < 2 ^ (mw + ew + 1))%Z.
Proof.
intros s m e Hm He.
unfold join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
split.
- apply (Zplus_le_compat 0 _ 0) with (2 := proj1 Hm).
rewrite <- (Zmult_0_l (2^mw)).
apply Zmult_le_compat_r.
case s.
clear -He ; omega.
now rewrite Zmult_0_l.
clear -Hm ; omega.
- apply Zlt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) × 2 ^ mw)%Z.
rewrite (Zmult_plus_distr_l _ 1).
apply Zplus_lt_compat_l.
now rewrite Zmult_1_l.
rewrite <- (Zplus_assoc mw), (Zplus_comm mw), Zpower_plus.
apply Zmult_le_compat_r.
rewrite Zpower_plus.
change (2^1)%Z with 2%Z.
case s ; clear -He ; omega.
now apply Zlt_le_weak.
easy.
clear -Hm ; omega.
clear -Hew ; omega.
now apply Zlt_le_weak.
Qed.
Definition split_bits x :=
let mm := Zpower 2 mw in
let em := Zpower 2 ew in
(Zle_bool (mm × em) x, Zmod x mm, Zmod (Zdiv x mm) em)%Z.
Theorem split_join_bits :
∀ s m e,
(0 ≤ m < Zpower 2 mw)%Z →
(0 ≤ e < Zpower 2 ew)%Z →
split_bits (join_bits s m e) = (s, m, e).
Proof.
intros s m e Hm He.
unfold split_bits, join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
apply f_equal2.
apply f_equal2.
case s.
apply Zle_bool_true.
apply Zle_0_minus_le.
ring_simplify.
apply Zplus_le_0_compat.
apply Zmult_le_0_compat.
apply He.
now apply Zlt_le_weak.
apply Hm.
apply Zle_bool_false.
apply Zplus_lt_reg_l with (2^mw × (-e))%Z.
replace (2 ^ mw × - e + ((0 + e) × 2 ^ mw + m))%Z with (m × 1)%Z by ring.
rewrite <- Zmult_plus_distr_r.
apply Zlt_le_trans with (2^mw × 1)%Z.
now apply Zmult_lt_compat_r.
apply Zmult_le_compat_l.
clear -He. omega.
now apply Zlt_le_weak.
rewrite Zplus_comm.
rewrite Z_mod_plus_full.
now apply Zmod_small.
rewrite Z_div_plus_full_l.
rewrite Zdiv_small with (1 := Hm).
rewrite Zplus_0_r.
case s.
replace (2^ew + e)%Z with (e + 1 × 2^ew)%Z by ring.
rewrite Z_mod_plus_full.
now apply Zmod_small.
now apply Zmod_small.
now apply Zgt_not_eq.
Qed.
Theorem join_split_bits :
∀ x,
(0 ≤ x < Zpower 2 (mw + ew + 1))%Z →
let '(s, m, e) := split_bits x in
join_bits s m e = x.
Proof.
intros x Hx.
unfold split_bits, join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
pattern x at 4 ; rewrite Z_div_mod_eq_full with x (2^mw)%Z.
apply (f_equal (fun v ⇒ (v + _)%Z)).
rewrite Zmult_comm.
apply f_equal.
pattern (x / (2^mw))%Z at 2 ; rewrite Z_div_mod_eq_full with (x / (2^mw))%Z (2^ew)%Z.
apply (f_equal (fun v ⇒ (v + _)%Z)).
replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw × 2 ^ ew) x then 1 else 0)%Z.
case Zle_bool.
now rewrite Zmult_1_r.
now rewrite Zmult_0_r.
rewrite Zdiv_Zdiv.
apply sym_eq.
case Zle_bool_spec ; intros Hs.
apply Zle_antisym.
cut (x / (2^mw × 2^ew) < 2)%Z. clear ; omega.
apply Zdiv_lt_upper_bound.
try apply Hx. now apply Zmult_lt_0_compat.
rewrite <- Zpower_exp ; try ( apply Zle_ge ; apply Zlt_le_weak ; assumption ).
change 2%Z at 1 with (Zpower 2 1).
rewrite <- Zpower_exp.
now rewrite Zplus_comm.
discriminate.
apply Zle_ge.
now apply Zplus_le_0_compat ; apply Zlt_le_weak.
apply Zdiv_le_lower_bound.
try apply Hx. now apply Zmult_lt_0_compat.
now rewrite Zmult_1_l.
apply Zdiv_small.
now split.
now apply Zlt_le_weak.
now apply Zlt_le_weak.
now apply Zgt_not_eq.
now apply Zgt_not_eq.
Qed.
Theorem split_bits_inj :
∀ x y,
(0 ≤ x < Zpower 2 (mw + ew + 1))%Z →
(0 ≤ y < Zpower 2 (mw + ew + 1))%Z →
split_bits x = split_bits y →
x = y.
Proof.
intros x y Hx Hy.
generalize (join_split_bits x Hx) (join_split_bits y Hy).
destruct (split_bits x) as ((sx, mx), ex).
destruct (split_bits y) as ((sy, my), ey).
intros Jx Jy H. revert Jx Jy.
inversion_clear H.
intros Jx Jy.
now rewrite <- Jx.
Qed.
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 sx (exist plx _) ⇒ join_bits sx (Zpos plx) (Zpower 2 ew - 1)
| B754_finite sx mx ex _ ⇒
let m := (Zpos mx - Zpower 2 mw)%Z in
if Zle_bool 0 m then
join_bits sx m (ex - emin + 1)
else
join_bits sx (Zpos mx) 0
end.
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 sx (exist plx _) ⇒ (sx, Zpos plx, Zpower 2 ew - 1)%Z
| B754_finite sx mx ex _ ⇒
let m := (Zpos mx - Zpower 2 mw)%Z in
if Zle_bool 0 m then
(sx, m, ex - emin + 1)%Z
else
(sx, Zpos mx, 0)%Z
end.
Theorem split_bits_of_binary_float_correct :
∀ x,
split_bits (bits_of_binary_float x) = split_bits_of_binary_float x.
Proof.
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 Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx.
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', _).
unfold canonic_mantissa in Hx'.
rewrite Zpos_digits2_pos in Hx'.
generalize (Zeq_bool_eq _ _ Hx').
unfold FLT_exp.
unfold emin.
clear ; zify ; omega.
case Zle_bool_spec ; intros H ;
[ apply → Z.le_0_sub in H | apply → Z.lt_sub_0 in H ] ;
apply split_join_bits ; try now split.
split.
clear -He_gt_0 H ; omega.
cut (Zpos mx < 2 × 2^mw)%Z. clear ; omega.
replace (2 × 2^mw)%Z with (2^prec)%Z.
apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
apply Hf.
unfold prec.
rewrite Zplus_comm.
apply Zpower_exp ; apply Zle_ge.
discriminate.
now apply Zlt_le_weak.
split.
generalize (proj1 Hf).
clear ; omega.
destruct (andb_prop _ _ Hx) as (_, Hx').
unfold emin.
replace (2^ew)%Z with (2 × emax)%Z.
generalize (Zle_bool_imp_le _ _ Hx').
clear ; omega.
apply sym_eq.
rewrite (Zsucc_pred ew).
unfold Zsucc.
rewrite Zplus_comm.
apply Zpower_exp ; apply Zle_ge.
discriminate.
now apply Zlt_0_le_0_pred.
Qed.
Theorem bits_of_binary_float_range:
∀ x, (0 ≤ bits_of_binary_float x < 2^(mw+ew+1))%Z.
Proof.
unfold bits_of_binary_float.
intros [sx|sx|sx [pl pl_range]|sx mx ex H].
- apply join_bits_range ; now split.
- apply join_bits_range.
now split.
clear -He_gt_0 ; omega.
- apply Z.ltb_lt in pl_range.
apply join_bits_range.
split.
easy.
apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)).
apply Z.lt_succ_r.
now rewrite <- Zdigits2_Zdigits.
clear -He_gt_0 ; omega.
- unfold bounded in H.
apply Bool.andb_true_iff in H ; destruct H as [A B].
apply Z.leb_le in B.
unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
case Zle_bool_spec ; intros H.
+ apply join_bits_range.
× split.
clear -H ; omega.
rewrite Zpos_digits2_pos in A.
cut (Zpos mx < 2 ^ prec)%Z.
unfold prec.
rewrite Zpower_plus by (clear -Hmw ; omega).
change (2^1)%Z with 2%Z.
clear ; omega.
apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
clear -A ; zify ; omega.
× split.
unfold emin ; clear -A ; zify ; omega.
replace ew with ((ew - 1) + 1)%Z by ring.
rewrite Zpower_plus by (clear - Hew ; omega).
unfold emin, emax in ×.
change (2^1)%Z with 2%Z.
clear -B ; omega.
+ apply → Z.lt_sub_0 in H.
apply join_bits_range ; now split.
Qed.
Definition binary_float_of_bits_aux x :=
let '(sx, mx, ex) := split_bits x in
if Zeq_bool ex 0 then
match mx with
| Z0 ⇒ F754_zero sx
| Zpos px ⇒ F754_finite sx px emin
| Zneg _ ⇒ F754_nan false xH
end
else if Zeq_bool ex (Zpower 2 ew - 1) then
match mx with
| Z0 ⇒ F754_infinity sx
| Zpos plx ⇒ F754_nan sx plx
| Zneg _ ⇒ F754_nan false xH
end
else
match (mx + Zpower 2 mw)%Z with
| Zpos px ⇒ F754_finite sx px (ex + emin - 1)
| _ ⇒ F754_nan false xH
end.
Lemma binary_float_of_bits_aux_correct :
∀ x,
valid_binary prec emax (binary_float_of_bits_aux x) = true.
Proof.
intros x.
unfold binary_float_of_bits_aux, split_bits.
case Zeq_bool_spec ; intros He1.
case_eq (x mod 2^mw)%Z ; try easy.
intros px Hm.
assert (Zdigits radix2 (Zpos px) ≤ mw)%Z.
apply Zdigits_le_Zpower.
simpl.
rewrite <- Hm.
eapply Z_mod_lt.
now apply Zlt_gt.
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exp.
fold emin.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
apply sym_eq.
apply Zmax_right.
clear -H Hprec.
unfold prec ; omega.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold emin, prec.
apply Zlt_not_le.
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.
case_eq (x mod 2 ^ mw)%Z; try easy.
intros plx Eqplx. apply Z.ltb_lt.
rewrite Zpos_digits2_pos.
assert (∀ 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.
intros px Hm.
assert (prec = Zdigits radix2 (Zpos px)).
rewrite Zdigits_ln_beta. 2: discriminate.
apply sym_eq.
apply ln_beta_unique.
rewrite <- Z2R_abs.
unfold Zabs.
replace (prec - 1)%Z with mw by ( unfold prec ; ring ).
rewrite <- Z2R_Zpower with (1 := Zlt_le_weak _ _ Hmw).
rewrite <- Z2R_Zpower. 2: now apply Zlt_le_weak.
rewrite <- Hm.
split.
apply Z2R_le.
change (radix2^mw)%Z with (0 + 2^mw)%Z.
apply Zplus_le_compat_r.
eapply Z_mod_lt.
now apply Zlt_gt.
apply Z2R_lt.
unfold prec.
rewrite Zpower_exp. 2: now apply Zle_ge ; apply Zlt_le_weak. 2: discriminate.
rewrite <- Zplus_diag_eq_mult_2.
apply Zplus_lt_compat_r.
eapply Z_mod_lt.
now apply Zlt_gt.
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exp.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
rewrite <- H.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
replace (prec + (ex + emin - 1) - prec)%Z with (ex + emin - 1)%Z by ring.
apply sym_eq.
apply Zmax_left.
revert He1.
fold ex.
cut (0 ≤ ex)%Z.
unfold emin.
clear ; intros H1 H2 ; omega.
eapply Z_mod_lt.
apply Zlt_gt.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
rewrite <- H.
apply Zlt_not_le.
unfold emin.
apply Zplus_lt_reg_r with (emax - 1)%Z.
ring_simplify.
revert He2.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
cut (ex < 2^ew)%Z.
replace (2^ew)%Z with (2 × emax)%Z.
clear ; intros H1 H2 ; omega.
replace ew with (1 + (ew - 1))%Z by ring.
rewrite Zpower_exp.
apply refl_equal.
discriminate.
clear -Hew ; omega.
eapply Z_mod_lt.
apply Zlt_gt.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
apply bpow_gt_0.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
Qed.
Definition binary_float_of_bits x :=
FF2B prec emax _ (binary_float_of_bits_aux_correct x).
Theorem binary_float_of_bits_of_binary_float :
∀ x,
binary_float_of_bits (bits_of_binary_float x) = x.
Proof.
intros x.
apply B2FF_inj.
unfold binary_float_of_bits.
rewrite B2FF_FF2B.
unfold binary_float_of_bits_aux.
rewrite split_bits_of_binary_float_correct.
destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Bx].
apply refl_equal.
simpl.
rewrite Zeq_bool_false.
now rewrite Zeq_bool_true.
cut (1 < 2^ew)%Z. clear ; omega.
now apply (Zpower_gt_1 radix2).
simpl.
rewrite Zeq_bool_false.
rewrite Zeq_bool_true; auto.
cut (1 < 2^ew)%Z. clear ; omega.
now apply (Zpower_gt_1 radix2).
unfold split_bits_of_binary_float.
case Zle_bool_spec ; intros Hm.
rewrite Zeq_bool_false.
rewrite Zeq_bool_false.
now ring_simplify (Zpos mx - 2 ^ mw + 2 ^ mw)%Z (ex - emin + 1 + emin - 1)%Z.
destruct (andb_prop _ _ Bx) as (_, H1).
generalize (Zle_bool_imp_le _ _ H1).
unfold emin.
replace (2^ew)%Z with (2 × emax)%Z.
clear ; omega.
replace ew with (1 + (ew - 1))%Z by ring.
rewrite Zpower_exp.
apply refl_equal.
discriminate.
clear -Hew ; omega.
destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Zpos_digits2_pos.
unfold FLT_exp, emin.
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
rewrite Zeq_bool_true. 2: apply refl_equal.
simpl.
apply f_equal.
destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Zpos_digits2_pos.
unfold FLT_exp, emin, prec.
apply → Z.lt_sub_0 in Hm.
generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm).
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
Qed.
Theorem bits_of_binary_float_of_bits :
∀ x,
(0 ≤ x < 2^(mw+ew+1))%Z →
bits_of_binary_float (binary_float_of_bits x) = x.
Proof.
intros x Hx.
unfold binary_float_of_bits, bits_of_binary_float.
set (Cx := binary_float_of_bits_aux_correct x).
clearbody Cx.
rewrite match_FF2B.
revert Cx.
generalize (join_split_bits x Hx).
unfold binary_float_of_bits_aux.
case_eq (split_bits x).
intros (sx, mx) ex Sx.
assert (Bm: (0 ≤ mx < 2^mw)%Z).
inversion_clear Sx.
apply Z_mod_lt.
now apply Zlt_gt.
case Zeq_bool_spec ; intros He1.
case_eq mx.
intros Hm Jx _.
now rewrite He1 in Jx.
intros px Hm Jx _.
rewrite Zle_bool_false.
now rewrite <- He1.
apply <- Z.lt_sub_0.
now rewrite <- Hm.
intros px Hm _ _.
apply False_ind.
apply Zle_not_lt with (1 := proj1 Bm).
now rewrite Hm.
case Zeq_bool_spec ; intros He2.
case_eq mx; intros Hm.
now rewrite He2.
now rewrite He2.
intros. zify; omega.
case_eq (mx + 2 ^ mw)%Z.
intros Hm.
apply False_ind.
clear -Bm Hm ; omega.
intros p Hm Jx Cx.
rewrite <- Hm.
rewrite Zle_bool_true.
now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z.
now ring_simplify.
intros p Hm.
apply False_ind.
clear -Bm Hm ; zify ; omega.
Qed.
End Binary_Bits.
Hypothesis Hmw : (0 < mw)%Z.
Hypothesis Hew : (0 < ew)%Z.
Let emax := Zpower 2 (ew - 1).
Let prec := (mw + 1)%Z.
Let emin := (3 - emax - prec)%Z.
Let binary_float := binary_float prec emax.
Let Hprec : (0 < prec)%Z.
unfold prec.
apply Zle_lt_succ.
now apply Zlt_le_weak.
Qed.
Let Hm_gt_0 : (0 < 2^mw)%Z.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
Qed.
Let He_gt_0 : (0 < 2^ew)%Z.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
Qed.
Hypothesis Hmax : (prec < emax)%Z.
Definition join_bits (s : bool) m e :=
(Z.shiftl ((if s then Zpower 2 ew else 0) + e) mw + m)%Z.
Lemma join_bits_range :
∀ s m e,
(0 ≤ m < 2^mw)%Z →
(0 ≤ e < 2^ew)%Z →
(0 ≤ join_bits s m e < 2 ^ (mw + ew + 1))%Z.
Proof.
intros s m e Hm He.
unfold join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
split.
- apply (Zplus_le_compat 0 _ 0) with (2 := proj1 Hm).
rewrite <- (Zmult_0_l (2^mw)).
apply Zmult_le_compat_r.
case s.
clear -He ; omega.
now rewrite Zmult_0_l.
clear -Hm ; omega.
- apply Zlt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) × 2 ^ mw)%Z.
rewrite (Zmult_plus_distr_l _ 1).
apply Zplus_lt_compat_l.
now rewrite Zmult_1_l.
rewrite <- (Zplus_assoc mw), (Zplus_comm mw), Zpower_plus.
apply Zmult_le_compat_r.
rewrite Zpower_plus.
change (2^1)%Z with 2%Z.
case s ; clear -He ; omega.
now apply Zlt_le_weak.
easy.
clear -Hm ; omega.
clear -Hew ; omega.
now apply Zlt_le_weak.
Qed.
Definition split_bits x :=
let mm := Zpower 2 mw in
let em := Zpower 2 ew in
(Zle_bool (mm × em) x, Zmod x mm, Zmod (Zdiv x mm) em)%Z.
Theorem split_join_bits :
∀ s m e,
(0 ≤ m < Zpower 2 mw)%Z →
(0 ≤ e < Zpower 2 ew)%Z →
split_bits (join_bits s m e) = (s, m, e).
Proof.
intros s m e Hm He.
unfold split_bits, join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
apply f_equal2.
apply f_equal2.
case s.
apply Zle_bool_true.
apply Zle_0_minus_le.
ring_simplify.
apply Zplus_le_0_compat.
apply Zmult_le_0_compat.
apply He.
now apply Zlt_le_weak.
apply Hm.
apply Zle_bool_false.
apply Zplus_lt_reg_l with (2^mw × (-e))%Z.
replace (2 ^ mw × - e + ((0 + e) × 2 ^ mw + m))%Z with (m × 1)%Z by ring.
rewrite <- Zmult_plus_distr_r.
apply Zlt_le_trans with (2^mw × 1)%Z.
now apply Zmult_lt_compat_r.
apply Zmult_le_compat_l.
clear -He. omega.
now apply Zlt_le_weak.
rewrite Zplus_comm.
rewrite Z_mod_plus_full.
now apply Zmod_small.
rewrite Z_div_plus_full_l.
rewrite Zdiv_small with (1 := Hm).
rewrite Zplus_0_r.
case s.
replace (2^ew + e)%Z with (e + 1 × 2^ew)%Z by ring.
rewrite Z_mod_plus_full.
now apply Zmod_small.
now apply Zmod_small.
now apply Zgt_not_eq.
Qed.
Theorem join_split_bits :
∀ x,
(0 ≤ x < Zpower 2 (mw + ew + 1))%Z →
let '(s, m, e) := split_bits x in
join_bits s m e = x.
Proof.
intros x Hx.
unfold split_bits, join_bits.
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
pattern x at 4 ; rewrite Z_div_mod_eq_full with x (2^mw)%Z.
apply (f_equal (fun v ⇒ (v + _)%Z)).
rewrite Zmult_comm.
apply f_equal.
pattern (x / (2^mw))%Z at 2 ; rewrite Z_div_mod_eq_full with (x / (2^mw))%Z (2^ew)%Z.
apply (f_equal (fun v ⇒ (v + _)%Z)).
replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw × 2 ^ ew) x then 1 else 0)%Z.
case Zle_bool.
now rewrite Zmult_1_r.
now rewrite Zmult_0_r.
rewrite Zdiv_Zdiv.
apply sym_eq.
case Zle_bool_spec ; intros Hs.
apply Zle_antisym.
cut (x / (2^mw × 2^ew) < 2)%Z. clear ; omega.
apply Zdiv_lt_upper_bound.
try apply Hx. now apply Zmult_lt_0_compat.
rewrite <- Zpower_exp ; try ( apply Zle_ge ; apply Zlt_le_weak ; assumption ).
change 2%Z at 1 with (Zpower 2 1).
rewrite <- Zpower_exp.
now rewrite Zplus_comm.
discriminate.
apply Zle_ge.
now apply Zplus_le_0_compat ; apply Zlt_le_weak.
apply Zdiv_le_lower_bound.
try apply Hx. now apply Zmult_lt_0_compat.
now rewrite Zmult_1_l.
apply Zdiv_small.
now split.
now apply Zlt_le_weak.
now apply Zlt_le_weak.
now apply Zgt_not_eq.
now apply Zgt_not_eq.
Qed.
Theorem split_bits_inj :
∀ x y,
(0 ≤ x < Zpower 2 (mw + ew + 1))%Z →
(0 ≤ y < Zpower 2 (mw + ew + 1))%Z →
split_bits x = split_bits y →
x = y.
Proof.
intros x y Hx Hy.
generalize (join_split_bits x Hx) (join_split_bits y Hy).
destruct (split_bits x) as ((sx, mx), ex).
destruct (split_bits y) as ((sy, my), ey).
intros Jx Jy H. revert Jx Jy.
inversion_clear H.
intros Jx Jy.
now rewrite <- Jx.
Qed.
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 sx (exist plx _) ⇒ join_bits sx (Zpos plx) (Zpower 2 ew - 1)
| B754_finite sx mx ex _ ⇒
let m := (Zpos mx - Zpower 2 mw)%Z in
if Zle_bool 0 m then
join_bits sx m (ex - emin + 1)
else
join_bits sx (Zpos mx) 0
end.
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 sx (exist plx _) ⇒ (sx, Zpos plx, Zpower 2 ew - 1)%Z
| B754_finite sx mx ex _ ⇒
let m := (Zpos mx - Zpower 2 mw)%Z in
if Zle_bool 0 m then
(sx, m, ex - emin + 1)%Z
else
(sx, Zpos mx, 0)%Z
end.
Theorem split_bits_of_binary_float_correct :
∀ x,
split_bits (bits_of_binary_float x) = split_bits_of_binary_float x.
Proof.
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 Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx.
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', _).
unfold canonic_mantissa in Hx'.
rewrite Zpos_digits2_pos in Hx'.
generalize (Zeq_bool_eq _ _ Hx').
unfold FLT_exp.
unfold emin.
clear ; zify ; omega.
case Zle_bool_spec ; intros H ;
[ apply → Z.le_0_sub in H | apply → Z.lt_sub_0 in H ] ;
apply split_join_bits ; try now split.
split.
clear -He_gt_0 H ; omega.
cut (Zpos mx < 2 × 2^mw)%Z. clear ; omega.
replace (2 × 2^mw)%Z with (2^prec)%Z.
apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
apply Hf.
unfold prec.
rewrite Zplus_comm.
apply Zpower_exp ; apply Zle_ge.
discriminate.
now apply Zlt_le_weak.
split.
generalize (proj1 Hf).
clear ; omega.
destruct (andb_prop _ _ Hx) as (_, Hx').
unfold emin.
replace (2^ew)%Z with (2 × emax)%Z.
generalize (Zle_bool_imp_le _ _ Hx').
clear ; omega.
apply sym_eq.
rewrite (Zsucc_pred ew).
unfold Zsucc.
rewrite Zplus_comm.
apply Zpower_exp ; apply Zle_ge.
discriminate.
now apply Zlt_0_le_0_pred.
Qed.
Theorem bits_of_binary_float_range:
∀ x, (0 ≤ bits_of_binary_float x < 2^(mw+ew+1))%Z.
Proof.
unfold bits_of_binary_float.
intros [sx|sx|sx [pl pl_range]|sx mx ex H].
- apply join_bits_range ; now split.
- apply join_bits_range.
now split.
clear -He_gt_0 ; omega.
- apply Z.ltb_lt in pl_range.
apply join_bits_range.
split.
easy.
apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)).
apply Z.lt_succ_r.
now rewrite <- Zdigits2_Zdigits.
clear -He_gt_0 ; omega.
- unfold bounded in H.
apply Bool.andb_true_iff in H ; destruct H as [A B].
apply Z.leb_le in B.
unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
case Zle_bool_spec ; intros H.
+ apply join_bits_range.
× split.
clear -H ; omega.
rewrite Zpos_digits2_pos in A.
cut (Zpos mx < 2 ^ prec)%Z.
unfold prec.
rewrite Zpower_plus by (clear -Hmw ; omega).
change (2^1)%Z with 2%Z.
clear ; omega.
apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
clear -A ; zify ; omega.
× split.
unfold emin ; clear -A ; zify ; omega.
replace ew with ((ew - 1) + 1)%Z by ring.
rewrite Zpower_plus by (clear - Hew ; omega).
unfold emin, emax in ×.
change (2^1)%Z with 2%Z.
clear -B ; omega.
+ apply → Z.lt_sub_0 in H.
apply join_bits_range ; now split.
Qed.
Definition binary_float_of_bits_aux x :=
let '(sx, mx, ex) := split_bits x in
if Zeq_bool ex 0 then
match mx with
| Z0 ⇒ F754_zero sx
| Zpos px ⇒ F754_finite sx px emin
| Zneg _ ⇒ F754_nan false xH
end
else if Zeq_bool ex (Zpower 2 ew - 1) then
match mx with
| Z0 ⇒ F754_infinity sx
| Zpos plx ⇒ F754_nan sx plx
| Zneg _ ⇒ F754_nan false xH
end
else
match (mx + Zpower 2 mw)%Z with
| Zpos px ⇒ F754_finite sx px (ex + emin - 1)
| _ ⇒ F754_nan false xH
end.
Lemma binary_float_of_bits_aux_correct :
∀ x,
valid_binary prec emax (binary_float_of_bits_aux x) = true.
Proof.
intros x.
unfold binary_float_of_bits_aux, split_bits.
case Zeq_bool_spec ; intros He1.
case_eq (x mod 2^mw)%Z ; try easy.
intros px Hm.
assert (Zdigits radix2 (Zpos px) ≤ mw)%Z.
apply Zdigits_le_Zpower.
simpl.
rewrite <- Hm.
eapply Z_mod_lt.
now apply Zlt_gt.
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exp.
fold emin.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
apply sym_eq.
apply Zmax_right.
clear -H Hprec.
unfold prec ; omega.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold emin, prec.
apply Zlt_not_le.
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.
case_eq (x mod 2 ^ mw)%Z; try easy.
intros plx Eqplx. apply Z.ltb_lt.
rewrite Zpos_digits2_pos.
assert (∀ 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.
intros px Hm.
assert (prec = Zdigits radix2 (Zpos px)).
rewrite Zdigits_ln_beta. 2: discriminate.
apply sym_eq.
apply ln_beta_unique.
rewrite <- Z2R_abs.
unfold Zabs.
replace (prec - 1)%Z with mw by ( unfold prec ; ring ).
rewrite <- Z2R_Zpower with (1 := Zlt_le_weak _ _ Hmw).
rewrite <- Z2R_Zpower. 2: now apply Zlt_le_weak.
rewrite <- Hm.
split.
apply Z2R_le.
change (radix2^mw)%Z with (0 + 2^mw)%Z.
apply Zplus_le_compat_r.
eapply Z_mod_lt.
now apply Zlt_gt.
apply Z2R_lt.
unfold prec.
rewrite Zpower_exp. 2: now apply Zle_ge ; apply Zlt_le_weak. 2: discriminate.
rewrite <- Zplus_diag_eq_mult_2.
apply Zplus_lt_compat_r.
eapply Z_mod_lt.
now apply Zlt_gt.
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exp.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
rewrite <- H.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
replace (prec + (ex + emin - 1) - prec)%Z with (ex + emin - 1)%Z by ring.
apply sym_eq.
apply Zmax_left.
revert He1.
fold ex.
cut (0 ≤ ex)%Z.
unfold emin.
clear ; intros H1 H2 ; omega.
eapply Z_mod_lt.
apply Zlt_gt.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
rewrite <- H.
apply Zlt_not_le.
unfold emin.
apply Zplus_lt_reg_r with (emax - 1)%Z.
ring_simplify.
revert He2.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
cut (ex < 2^ew)%Z.
replace (2^ew)%Z with (2 × emax)%Z.
clear ; intros H1 H2 ; omega.
replace ew with (1 + (ew - 1))%Z by ring.
rewrite Zpower_exp.
apply refl_equal.
discriminate.
clear -Hew ; omega.
eapply Z_mod_lt.
apply Zlt_gt.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
apply bpow_gt_0.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
Qed.
Definition binary_float_of_bits x :=
FF2B prec emax _ (binary_float_of_bits_aux_correct x).
Theorem binary_float_of_bits_of_binary_float :
∀ x,
binary_float_of_bits (bits_of_binary_float x) = x.
Proof.
intros x.
apply B2FF_inj.
unfold binary_float_of_bits.
rewrite B2FF_FF2B.
unfold binary_float_of_bits_aux.
rewrite split_bits_of_binary_float_correct.
destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Bx].
apply refl_equal.
simpl.
rewrite Zeq_bool_false.
now rewrite Zeq_bool_true.
cut (1 < 2^ew)%Z. clear ; omega.
now apply (Zpower_gt_1 radix2).
simpl.
rewrite Zeq_bool_false.
rewrite Zeq_bool_true; auto.
cut (1 < 2^ew)%Z. clear ; omega.
now apply (Zpower_gt_1 radix2).
unfold split_bits_of_binary_float.
case Zle_bool_spec ; intros Hm.
rewrite Zeq_bool_false.
rewrite Zeq_bool_false.
now ring_simplify (Zpos mx - 2 ^ mw + 2 ^ mw)%Z (ex - emin + 1 + emin - 1)%Z.
destruct (andb_prop _ _ Bx) as (_, H1).
generalize (Zle_bool_imp_le _ _ H1).
unfold emin.
replace (2^ew)%Z with (2 × emax)%Z.
clear ; omega.
replace ew with (1 + (ew - 1))%Z by ring.
rewrite Zpower_exp.
apply refl_equal.
discriminate.
clear -Hew ; omega.
destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Zpos_digits2_pos.
unfold FLT_exp, emin.
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
rewrite Zeq_bool_true. 2: apply refl_equal.
simpl.
apply f_equal.
destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Zpos_digits2_pos.
unfold FLT_exp, emin, prec.
apply → Z.lt_sub_0 in Hm.
generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm).
generalize (Zdigits radix2 (Zpos mx)).
clear.
intros ; zify ; omega.
Qed.
Theorem bits_of_binary_float_of_bits :
∀ x,
(0 ≤ x < 2^(mw+ew+1))%Z →
bits_of_binary_float (binary_float_of_bits x) = x.
Proof.
intros x Hx.
unfold binary_float_of_bits, bits_of_binary_float.
set (Cx := binary_float_of_bits_aux_correct x).
clearbody Cx.
rewrite match_FF2B.
revert Cx.
generalize (join_split_bits x Hx).
unfold binary_float_of_bits_aux.
case_eq (split_bits x).
intros (sx, mx) ex Sx.
assert (Bm: (0 ≤ mx < 2^mw)%Z).
inversion_clear Sx.
apply Z_mod_lt.
now apply Zlt_gt.
case Zeq_bool_spec ; intros He1.
case_eq mx.
intros Hm Jx _.
now rewrite He1 in Jx.
intros px Hm Jx _.
rewrite Zle_bool_false.
now rewrite <- He1.
apply <- Z.lt_sub_0.
now rewrite <- Hm.
intros px Hm _ _.
apply False_ind.
apply Zle_not_lt with (1 := proj1 Bm).
now rewrite Hm.
case Zeq_bool_spec ; intros He2.
case_eq mx; intros Hm.
now rewrite He2.
now rewrite He2.
intros. zify; omega.
case_eq (mx + 2 ^ mw)%Z.
intros Hm.
apply False_ind.
clear -Bm Hm ; omega.
intros p Hm Jx Cx.
rewrite <- Hm.
rewrite Zle_bool_true.
now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z.
now ring_simplify.
intros p Hm.
apply False_ind.
clear -Bm Hm ; zify ; omega.
Qed.
End Binary_Bits.
Specialization for IEEE single precision operations
Section B32_Bits.
Implicit Arguments B754_nan [[prec] [emax]].
Definition binary32 := binary_float 24 128.
Let Hprec : (0 < 24)%Z.
apply refl_equal.
Qed.
Let Hprec_emax : (24 < 128)%Z.
apply refl_equal.
Qed.
Definition default_nan_pl32 : bool × nan_pl 24 :=
(false, exist _ (iter_nat xO 22 xH) (refl_equal true)).
Definition unop_nan_pl32 (f : binary32) : bool × nan_pl 24 :=
match f with
| B754_nan s pl ⇒ (s, pl)
| _ ⇒ default_nan_pl32
end.
Definition binop_nan_pl32 (f1 f2 : binary32) : bool × nan_pl 24 :=
match f1, f2 with
| B754_nan s1 pl1, _ ⇒ (s1, pl1)
| _, B754_nan s2 pl2 ⇒ (s2, pl2)
| _, _ ⇒ default_nan_pl32
end.
Definition b32_opp := Bopp 24 128 pair.
Definition b32_plus := Bplus _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_minus := Bminus _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_mult := Bmult _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_div := Bdiv _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_sqrt := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32.
Definition b32_of_bits : Z → binary32 := binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _).
Definition bits_of_b32 : binary32 → Z := bits_of_binary_float 23 8.
End B32_Bits.
Implicit Arguments B754_nan [[prec] [emax]].
Definition binary32 := binary_float 24 128.
Let Hprec : (0 < 24)%Z.
apply refl_equal.
Qed.
Let Hprec_emax : (24 < 128)%Z.
apply refl_equal.
Qed.
Definition default_nan_pl32 : bool × nan_pl 24 :=
(false, exist _ (iter_nat xO 22 xH) (refl_equal true)).
Definition unop_nan_pl32 (f : binary32) : bool × nan_pl 24 :=
match f with
| B754_nan s pl ⇒ (s, pl)
| _ ⇒ default_nan_pl32
end.
Definition binop_nan_pl32 (f1 f2 : binary32) : bool × nan_pl 24 :=
match f1, f2 with
| B754_nan s1 pl1, _ ⇒ (s1, pl1)
| _, B754_nan s2 pl2 ⇒ (s2, pl2)
| _, _ ⇒ default_nan_pl32
end.
Definition b32_opp := Bopp 24 128 pair.
Definition b32_plus := Bplus _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_minus := Bminus _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_mult := Bmult _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_div := Bdiv _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_sqrt := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32.
Definition b32_of_bits : Z → binary32 := binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _).
Definition bits_of_b32 : binary32 → Z := bits_of_binary_float 23 8.
End B32_Bits.
Specialization for IEEE double precision operations
Section B64_Bits.
Implicit Arguments B754_nan [[prec] [emax]].
Definition binary64 := binary_float 53 1024.
Let Hprec : (0 < 53)%Z.
apply refl_equal.
Qed.
Let Hprec_emax : (53 < 1024)%Z.
apply refl_equal.
Qed.
Definition default_nan_pl64 : bool × nan_pl 53 :=
(false, exist _ (iter_nat xO 51 xH) (refl_equal true)).
Definition unop_nan_pl64 (f : binary64) : bool × nan_pl 53 :=
match f with
| B754_nan s pl ⇒ (s, pl)
| _ ⇒ default_nan_pl64
end.
Definition binop_nan_pl64 (pl1 pl2 : binary64) : bool × nan_pl 53 :=
match pl1, pl2 with
| B754_nan s1 pl1, _ ⇒ (s1, pl1)
| _, B754_nan s2 pl2 ⇒ (s2, pl2)
| _, _ ⇒ default_nan_pl64
end.
Definition b64_opp := Bopp 53 1024 pair.
Definition b64_plus := Bplus _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_minus := Bminus _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_mult := Bmult _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_div := Bdiv _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_sqrt := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64.
Definition b64_of_bits : Z → binary64 := binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _).
Definition bits_of_b64 : binary64 → Z := bits_of_binary_float 52 11.
End B64_Bits.
Implicit Arguments B754_nan [[prec] [emax]].
Definition binary64 := binary_float 53 1024.
Let Hprec : (0 < 53)%Z.
apply refl_equal.
Qed.
Let Hprec_emax : (53 < 1024)%Z.
apply refl_equal.
Qed.
Definition default_nan_pl64 : bool × nan_pl 53 :=
(false, exist _ (iter_nat xO 51 xH) (refl_equal true)).
Definition unop_nan_pl64 (f : binary64) : bool × nan_pl 53 :=
match f with
| B754_nan s pl ⇒ (s, pl)
| _ ⇒ default_nan_pl64
end.
Definition binop_nan_pl64 (pl1 pl2 : binary64) : bool × nan_pl 53 :=
match pl1, pl2 with
| B754_nan s1 pl1, _ ⇒ (s1, pl1)
| _, B754_nan s2 pl2 ⇒ (s2, pl2)
| _, _ ⇒ default_nan_pl64
end.
Definition b64_opp := Bopp 53 1024 pair.
Definition b64_plus := Bplus _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_minus := Bminus _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_mult := Bmult _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_div := Bdiv _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_sqrt := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64.
Definition b64_of_bits : Z → binary64 := binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _).
Definition bits_of_b64 : binary64 → Z := bits_of_binary_float 52 11.
End B64_Bits.