Commit 9540d864 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Started a formalization of IEEE-754 binary floating-point numbers.

parent 9e7452d5
Require Import Fcore.
Require Import Fcalc_digits.
Section Binary.
Variable prec emax : Z.
Let fexp := FLT_exp (1 - (emax + prec)) prec.
Definition bounded_prec m e :=
Zeq_bool (fexp (Z_of_nat (S (digits2_Pnat m)) + e)) e.
Definition bounded m e :=
andb (bounded_prec m e) (Zle_bool e emax).
Inductive binary_float :=
| B754_zero : bool -> binary_float
| B754_infinity : bool -> binary_float
| B754_nan : binary_float
| B754_finite : bool ->
forall (m : positive) (e : Z), bounded m e = true -> binary_float.
Definition radix2 := Build_radix 2 (refl_equal true).
Definition B2R f :=
match f with
| B754_finite s m e _ => F2R (Float radix2 ((if s then Zneg else Zpos) m) e)
| _ => R0
end.
Theorem canonic_bounded_prec :
forall (sx : bool) mx ex,
bounded_prec mx ex = true ->
canonic radix2 fexp (Float radix2 ((if sx then Zneg else Zpos) mx) ex).
Proof.
intros sx mx ex H.
assert (Hx := Zeq_bool_eq _ _ H). clear H.
apply sym_eq.
simpl.
pattern ex at 2 ; rewrite <- Hx.
apply (f_equal fexp).
rewrite ln_beta_F2R_digits.
rewrite <- digits_abs.
rewrite Z_of_nat_S_digits2_Pnat.
now case sx.
now case sx.
Qed.
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.
simpl.
apply generic_format_canonic.
apply canonic_bounded_prec.
now destruct (andb_prop _ _ Hx) as (H, _).
Qed.
Definition is_finite_strict f :=
match f with
| B754_finite _ _ _ _ => true
| _ => false
end.
Theorem binary_unicity :
forall x y : binary_float,
is_finite_strict x = true ->
is_finite_strict y = true ->
B2R x = B2R y ->
x = y.
Proof.
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
simpl.
intros _ _ Heq.
assert (Hs: sx = sy).
(* *)
revert Heq. clear.
case sx ; case sy ; try easy ;
intros Heq ; apply False_ind ; revert Heq.
apply Rlt_not_eq.
apply Rlt_trans with R0.
now apply F2R_lt_0_compat.
now apply F2R_gt_0_compat.
apply Rgt_not_eq.
apply Rgt_trans with R0.
now apply F2R_gt_0_compat.
now apply F2R_lt_0_compat.
assert (mx = my /\ ex = ey).
(* *)
refine (_ (canonic_unicity _ fexp _ _ _ _ Heq)).
rewrite Hs.
now case sy ; intro H ; injection H ; split.
apply canonic_bounded_prec.
exact (proj1 (andb_prop _ _ Hx)).
apply canonic_bounded_prec.
exact (proj1 (andb_prop _ _ Hy)).
(* *)
revert Hx.
rewrite Hs, (proj1 H), (proj2 H).
intros Hx.
apply f_equal.
apply eqbool_irrelevance.
Qed.
Definition is_finite f :=
match f with
| B754_finite _ _ _ _ => true
| B754_zero _ => true
| _ => false
end.
Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA.
Definition round_mode m :=
match m with
| mode_NE => rndNE
| mode_ZR => rndZR
| mode_DN => rndDN
| mode_UP => rndUP
| mode_NA => rndNA
end.
Definition Bplus m x y :=
match x, y with
| B754_nan, _ => x
| _, B754_nan => y
| B754_infinity sx, B754_infinity sy =>
if Bool.eqb sx sy then x else B754_nan
| B754_infinity _, _ => x
| _, B754_infinity _ => y
| B754_zero sx, B754_zero sy =>
if Bool.eqb sx sy then x else
match m with mode_DN => B754_zero true | _ => B754_zero false end
| B754_zero _, _ => y
| _, B754_zero _ => x
| B754_finite sx mx ex Hx, B754_finite sy my ey Hy =>
B754_nan
end.
Theorem Bplus_finite :
forall m x y,
is_finite x = true ->
is_finite y = true ->
B2R (Bplus m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y)%R.
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy ; intros _ _.
(* *)
rewrite Rplus_0_r, round_0.
simpl.
case (Bool.eqb sx sy) ; try easy.
now case m.
(* *)
rewrite Rplus_0_l.
apply sym_eq.
apply round_generic.
apply generic_format_B2R.
(* *)
rewrite Rplus_0_r.
apply sym_eq.
apply round_generic.
apply generic_format_B2R.
(* *)
Admitted.
End Binary.
......@@ -23,6 +23,7 @@ FILES = \
Prop/Fprop_div_sqrt_error.v \
Prop/Fprop_Sterbenz.v \
Appli/Fappli_Axpy.v \
Appli/Fappli_IEEE.v \
Appli/Fappli_sqrt_FLT_ne.v
EXTRA_DIST = $(FILES)
......
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