Commit 71a3cfec authored by Guillaume Melquiond's avatar Guillaume Melquiond

New release.

parent 56ce444c
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.3) with a Reals theory
You will need the Coq proof assistant (>= 8.4) with a Reals theory
compiled in.
The .tar.gz file is distributed with a working set of configure files. They
......
Version 2.2.0:
- added theorems about rounding to odd and double rounding
- improved handling of special values of IEEE-754 arithmetic
Version 2.1.0:
- ensured compatibility with both Coq 8.3 and 8.4
- improved support for rounding toward and away from zero
......
......@@ -66,6 +66,11 @@ install:
EXTRA_DIST = \
configure
REMOVE_FROM_DIST = \
src/Appli/Fappli_Axpy.v \
src/Appli/Fappli_Muller.v \
src/Translate/
dist: $(EXTRA_DIST)
PACK=@PACKAGE_TARNAME@-@PACKAGE_VERSION@
DIRS=`git ls-tree -d -r --name-only HEAD`
......@@ -74,6 +79,7 @@ dist: $(EXTRA_DIST)
mkdir $PACK
for d in $DIRS; do mkdir $PACK/$d; done
for f in $FILES $(EXTRA_DIST); do cp $f $PACK/$f; done
for f in $(REMOVE_FROM_DIST) ; do rm -rf $PACK/$f; done
git log --pretty="format:%ad %s" --date=short > $PACK/ChangeLog
cat /dev/null > $PACK/ChangeLog
rm `find $PACK -name .gitignore`
......
AC_INIT([Flocq], [2.1.0],
AC_INIT([Flocq], [2.2.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......
......@@ -308,7 +308,7 @@ https://github.com/apenwarr/redo for an implementation and some comprehensive do
\section sec-licensing Licensing
@author Guillaume Melquiond
@version 0.8
@version 0.9
@date 2012-2013
@copyright
This program is free software: you can redistribute it and/or modify
......@@ -2200,7 +2200,7 @@ static void complete_request(client_t &client, bool success)
else if (client.socket != INVALID_SOCKET)
{
char res = success ? 1 : 0;
send(client.socket, &res, 1, 0);
send(client.socket, &res, 1, MSG_NOSIGNAL);
#ifdef WINDOWS
closesocket(client.socket);
#else
......@@ -2665,7 +2665,7 @@ void client_mode(char *socket_name, string_list const &targets)
if (send(socket_fd, (char *)&job_id, sizeof(job_id), MSG_NOSIGNAL) != sizeof(job_id))
goto error;
// Send tagets.
// Send targets.
for (string_list::const_iterator i = targets.begin(),
i_end = targets.end(); i != i_end; ++i)
{
......
......@@ -62,8 +62,8 @@ now contradict H.
Qed.
Definition MinOrMax x f :=
((f = round beta (FLX_exp prec) Zfloor x)
Definition MinOrMax x f :=
((f = round beta (FLX_exp prec) Zfloor x)
\/ (f = round beta (FLX_exp prec) Zceil x)).
Theorem MinOrMax_opp: forall x f,
......@@ -84,7 +84,7 @@ Qed.
Theorem implies_DN_lt_ulp:
forall x f, format f ->
(0 < f <= x)%R ->
(Rabs (f-x) < ulp f)%R ->
(Rabs (f-x) < ulp f)%R ->
(f = round beta (FLX_exp prec) Zfloor x)%R.
intros x f Hf Hxf1 Hxf2.
apply sym_eq.
......@@ -100,7 +100,7 @@ Qed.
Theorem MinOrMax_ulp_pred:
forall x f, format f ->
(0 < f)%R ->
(Rabs (f-x) < ulp (pred beta (FLX_exp prec) f))%R ->
(Rabs (f-x) < ulp (pred beta (FLX_exp prec) f))%R ->
MinOrMax x f.
intros x f Ff Zf Hf.
case (Rlt_or_le x f); intros Hxf2.
......@@ -141,7 +141,7 @@ Qed.
Theorem implies_MinOrMax_bpow:
forall x f, format f ->
f = bpow (ln_beta beta f) ->
(Rabs (f-x) < /2* ulp f)%R ->
(Rabs (f-x) < /2* ulp f)%R ->
MinOrMax x f.
intros x f Hf1 Hf2 Hxf.
......@@ -165,18 +165,18 @@ Notation u := (round beta (FLX_exp prec) (Znearest choice) (t+y)).
(*
Axpy_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
Axpy_aux1_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fnormal?(b)(t) => radix*abs(t) <= Fpred(b)(u)
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
Axpy_aux1_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fsubnormal?(b)(t) => 1-dExp(b) <= Fexp(Fpred(b)(u))
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
=> abs(t-a*x) <= Fulp(b)(Fpred(b)(u))/4
Axpy_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fsubnormal?(b)(t) => u=t+y
......@@ -185,7 +185,7 @@ Axpy_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
Axpy_aux3 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Fsubnormal?(b)(t)
=> Fsubnormal?(b)(t)
=> -dExp(b) = Fexp(Fpred(b)(u)) => 1-dExp(b) <= Fexp(u)
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
......@@ -196,29 +196,29 @@ AxpyPos : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> abs(y1-y+a1*x1-a*x) < Fulp(b)(Fpred(b)(u))/4
=> MinOrMax?(y1+a1*x1,u)
Axpy_opt_aux1_aux1 : lemma Fnormal?(b)(t) => Fnormal?(b)(u) => 0 < u
=> Prec(b) >= 3 =>
Axpy_opt_aux1_aux1 : lemma Fnormal?(b)(t) => Fnormal?(b)(u) => 0 < u
=> Prec(b) >= 3 =>
(1+radix*(1+1/(2*abs(Fnum(u))))*(1+1/abs(Fnum(Fpred(b)(u)))))/(1-1/(2*abs(Fnum(t))))
<= 1+radix+radix^(4-Prec(b))
Axpy_opt_aux1 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 3 => Fnormal?(b)(t)
=> Prec(b) >= 3 => Fnormal?(b)(t)
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> radix*abs(t) <= Fpred(b)(u)
Axpy_opt_aux2 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 6 => Fnormal?(b)(t)
=> Prec(b) >= 6 => Fnormal?(b)(t)
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y)*radix^(1-Prec(b))/(radix+1) < Fulp(b)(Fpred(b)(u))
Axpy_opt_aux3 : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 3 => Fsubnormal?(b)(t)
=> Prec(b) >= 3 => Fsubnormal?(b)(t)
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y)*radix^(1-Prec(b))/(radix+radix/2) <= Fulp(b)(Fpred(b)(u))
Axpy_optPos : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u) => 0 < u
=> Prec(b) >= 6
=> Prec(b) >= 6
=> (radix+1+radix^(4-Prec(b)))*abs(a*x) <= abs(y)
=> abs(y1-y+a1*x1-a*x) < abs(y)*radix^(1-Prec(b))/(6*radix)
=> MinOrMax?(y1+a1*x1,u)
......@@ -235,7 +235,7 @@ Axpy_opt : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u)
=> MinOrMax?(y1+a1*x1,u)
Axpy_simpl : lemma Closest?(b)(a*x,t) => Closest?(b)(t+y,u)
=> Prec(b) >= 24 => radix=2
=> Prec(b) >= 24 => radix=2
=> (3+1/100000)*abs(a*x) <= abs(y)
=> abs(y1-y+a1*x1-a*x) < abs(y)*2^(1-Prec(b))/12
=> MinOrMax?(y1+a1*x1,u)
......
......@@ -177,7 +177,7 @@ apply round_generic...
apply sym_eq, sqrt_lem_1.
apply bpow_ge_0.
now left.
rewrite Hx at 1.
rewrite Hx at 1.
rewrite Rmult_comm; rewrite Hx at 1.
apply trans_eq with ((sqrt (Z2R beta)*sqrt (Z2R beta)) * (bpow (ln_beta beta x-1)*bpow (ln_beta beta x-1))).
ring.
......@@ -188,7 +188,7 @@ replace (x*x) with (bpow (2 * ln_beta beta x - 1)).
apply sym_eq, round_generic...
apply generic_format_bpow.
unfold FLX_exp; omega.
apply sym_eq; rewrite Hx at 1.
apply sym_eq; rewrite Hx at 1.
rewrite Rmult_comm; rewrite Hx at 1.
apply trans_eq with ((sqrt (Z2R beta)*sqrt (Z2R beta)) * (bpow (ln_beta beta x-1)*bpow (ln_beta beta x-1))).
ring.
......@@ -426,7 +426,7 @@ apply Rle_ge; auto with real.
Qed.
Lemma ulp_sqr_ulp_lt: forall u, 0 < u ->
Lemma ulp_sqr_ulp_lt: forall u, 0 < u ->
(u < sqrt (Z2R (radix_val beta)) * bpow (ln_beta beta u-1)) ->
ulp_flx (u * u) + ulp_flx u * ulp_flx u / 2 < 2 * u * ulp_flx u.
Proof with auto with typeclass_instances.
......@@ -726,7 +726,7 @@ intros Hb.
apply Rle_lt_trans with (sqrt (Z2R beta) * bpow (ln_beta beta x - 1)
- Z2R k * ulp_flx x).
unfold ulp, canonic_exp, FLX_exp.
apply Rle_trans with (bpow (ln_beta beta x - 1)
apply Rle_trans with (bpow (ln_beta beta x - 1)
*(sqrt (Z2R beta) -Z2R k * bpow (1-prec))).
rewrite <- (Rmult_1_r (bpow (ln_beta beta x - 1))) at 1.
apply Rmult_le_compat_l.
......@@ -869,7 +869,7 @@ Qed.
Theorem round_flx_sqr_sqrt_aux1:
Theorem round_flx_sqr_sqrt_aux1:
(/ 2 * bpow (ln_beta beta x) <
(2 * Z2R k + 1) * x -
(Z2R k + / 2) * (Z2R k + / 2) * bpow (ln_beta beta x - prec)) ->
......@@ -927,7 +927,7 @@ apply Rlt_le_trans with (x*x - /2*bpow (2 * ln_beta beta x - prec)).
unfold ulp, canonic_exp, FLX_exp.
apply Rplus_lt_reg_r with (-x*x).
apply Rle_lt_trans with
(- (bpow (ln_beta beta x - prec)*((2*Z2R k +1)*x -
(- (bpow (ln_beta beta x - prec)*((2*Z2R k +1)*x -
(Z2R k + / 2)* (Z2R k + / 2) * bpow (ln_beta beta x - prec)))).
right; field.
apply Rlt_le_trans with (- (bpow (ln_beta beta x - prec)*
......@@ -936,11 +936,11 @@ apply Ropp_lt_contravar.
apply Rmult_lt_compat_l.
apply bpow_gt_0.
exact V.
right; apply trans_eq with
right; apply trans_eq with
((-/2)*(bpow (ln_beta beta x - prec)*bpow (ln_beta beta x))).
ring.
rewrite <- bpow_plus.
apply trans_eq with
apply trans_eq with
((-/2)*bpow (2 * ln_beta beta x - prec)).
apply f_equal.
apply f_equal; ring.
......@@ -1002,7 +1002,7 @@ intros Hb.
apply Rle_antisym.
(* . *)
apply round_flx_sqr_sqrt_le...
(* . *)
(* . *)
assert (((radix_val beta = 2)%Z \/ (radix_val beta=3)%Z) \/ (radix_val beta=4)%Z).
generalize (radix_gt_1 beta); omega.
destruct H.
......@@ -1014,7 +1014,7 @@ omega.
apply radix_gt_0.
apply Rlt_le_trans with (x-/4*bpow (ln_beta beta x - prec)).
2: right; simpl; field.
apply Rle_lt_trans with (sqrt (Z2R beta) * bpow (ln_beta beta x - 1)
apply Rle_lt_trans with (sqrt (Z2R beta) * bpow (ln_beta beta x - 1)
- / 4 * bpow (ln_beta beta x - prec)).
2: apply Rplus_lt_compat_r; assumption.
apply Rle_trans with ((Z2R beta / 2)*bpow (ln_beta beta x-1)).
......@@ -1174,7 +1174,7 @@ Qed.
(*
Theorem round_flx_sqr_sqrt_aux: (4 < radix_val beta)%Z
Theorem round_flx_sqr_sqrt_aux: (4 < radix_val beta)%Z
(sqrt (Z2R (radix_val beta)) * bpow (ln_beta beta x-1) < x) ->
round_flx(x/z) <= 1.
Proof with auto with typeclass_instances.
......@@ -1266,7 +1266,7 @@ unfold Rdiv; apply Rmult_le_pos; try assumption.
left; apply Rinv_0_lt_compat.
apply Rlt_le_trans with (1:=H0); exact H.
(* *)
apply Rle_trans with
apply Rle_trans with
(round_flx (x / round_flx (sqrt (round_flx (x * x))))).
apply round_le...
unfold Rdiv; apply Rmult_le_compat_l; try exact Hx.
......@@ -1297,7 +1297,7 @@ apply Rle_trans with 0.
auto with real.
now apply Muller_pos.
now apply Muller_pos.
replace
replace
(x / round_flx (sqrt (round_flx (round_flx (x * x) + round_flx (y * y))))) with
(-(((-x) / round_flx (sqrt (round_flx (round_flx ((-x) * (-x)) + round_flx (y * y))))))).
rewrite round_NE_opp.
......
......@@ -17,7 +17,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
(** * Rounding to odd and its properties, including the equivalence
(** * Rounding to odd and its properties, including the equivalence
between rnd_NE and double rounding with rnd_odd and then rnd_NE *)
......@@ -30,7 +30,7 @@ Definition Zrnd_odd x := match Req_EM_T x (Z2R (Zfloor x)) with
| true => Zceil x
| false => Zfloor x
end
end.
end.
......@@ -273,7 +273,7 @@ rewrite <- H0.
repeat split; try assumption.
apply trans_eq with (negb (Zeven (Zfloor (scaled_mantissa beta fexp x)))).
2: rewrite H1; reflexivity.
apply trans_eq with (negb (Zeven (Fnum
apply trans_eq with (negb (Zeven (Fnum
(Float beta (Zfloor (scaled_mantissa beta fexp x)) (cexp x))))).
2: reflexivity.
case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)).
......@@ -389,13 +389,13 @@ Qed.
Lemma exists_even_fexp_lt: forall (c:Z->Z), forall (x:R),
(exists f:float beta, F2R f = x /\ (c (ln_beta beta x) < Fexp f)%Z) ->
exists f:float beta, F2R f =x /\ canonic beta c f /\ Zeven (Fnum f) = true.
exists f:float beta, F2R f =x /\ canonic beta c f /\ Zeven (Fnum f) = true.
Proof with auto with typeclass_instances.
intros c x (g,(Hg1,Hg2)).
exists (Float beta
exists (Float beta
(Fnum g*Z.pow (radix_val beta) (Fexp g - c (ln_beta beta x)))
(c (ln_beta beta x))).
assert (F2R (Float beta
assert (F2R (Float beta
(Fnum g*Z.pow (radix_val beta) (Fexp g - c (ln_beta beta x)))
(c (ln_beta beta x))) = x).
unfold F2R; simpl.
......@@ -458,7 +458,7 @@ Qed.
Lemma ln_beta_d: (0< F2R d)%R ->
Lemma ln_beta_d: (0< F2R d)%R ->
(ln_beta beta (F2R d) = ln_beta beta x :>Z).
Proof with auto with typeclass_instances.
intros Y.
......@@ -475,7 +475,7 @@ Qed.
Lemma format_bpow_x: (0 < F2R d)%R
Lemma format_bpow_x: (0 < F2R d)%R
-> generic_format beta fexp (bpow (ln_beta beta x)).
Proof with auto with typeclass_instances.
intros Y.
......@@ -584,7 +584,7 @@ unfold m; rewrite <- H0; field.
Qed.
Lemma ln_beta_m_0: (0 = F2R d)%R
Lemma ln_beta_m_0: (0 = F2R d)%R
-> (ln_beta beta m =ln_beta beta (F2R u)-1:>Z)%Z.
Proof with auto with typeclass_instances.
intros Y.
......@@ -634,7 +634,7 @@ Qed.
Lemma m_eq: (0 < F2R d)%R -> exists f:float beta,
Lemma m_eq: (0 < F2R d)%R -> exists f:float beta,
F2R f = m /\ (Fexp f = fexp (ln_beta beta x) -1)%Z.
Proof with auto with typeclass_instances.
intros Y.
......@@ -664,7 +664,7 @@ now rewrite Fexp_d.
rewrite Hu'2; omega.
Qed.
Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta,
Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta,
F2R f = m /\ (Fexp f = fexp (ln_beta beta (F2R u)) -1)%Z.
Proof with auto with typeclass_instances.
intros Y.
......@@ -688,7 +688,7 @@ destruct u; reflexivity.
rewrite Zplus_comm, Cu; unfold Zminus; now apply f_equal2.
Qed.
Lemma fexp_m_eq_0: (0 = F2R d)%R ->
Lemma fexp_m_eq_0: (0 = F2R d)%R ->
(fexp (ln_beta beta (F2R u)-1) < fexp (ln_beta beta (F2R u))+1)%Z.
Proof with auto with typeclass_instances.
intros Y.
......@@ -803,7 +803,7 @@ Qed.
Theorem round_odd_prop_pos:
round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
round beta fexp (Znearest choice) x.
Proof with auto with typeclass_instances.
set (o:=round beta fexpe Zrnd_odd x).
......@@ -928,7 +928,7 @@ Context { exists_NE_e : Exists_NE beta fexpe }. (* for defining rounding to odd
Hypothesis fexpe_fexp: forall e, (fexpe e <= fexp e -2)%Z.
Theorem canonizer: forall f, generic_format beta fexp f
Theorem canonizer: forall f, generic_format beta fexp f
-> exists g : float beta, f = F2R g /\ canonic beta fexp g.
Proof with auto with typeclass_instances.
intros f Hf.
......@@ -946,7 +946,7 @@ Qed.
Theorem round_odd_prop: forall x,
round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
round beta fexp (Znearest choice) x.
Proof with auto with typeclass_instances.
intros x.
......
......@@ -126,10 +126,10 @@ intros r1 r2 r3 H1 H2.
apply H1; rewrite H2; ring.
Qed.
Lemma Rmult_neq_compat_r: forall r1 r2 r3:R, (r1 <> 0)%R -> (r2 <> r3)%R
Lemma Rmult_neq_compat_r: forall r1 r2 r3:R, (r1 <> 0)%R -> (r2 <> r3)%R
-> (r2 *r1 <> r3*r1)%R.
intros r1 r2 r3 H H1 H2.
now apply H1, Rmult_eq_reg_r with r1.
now apply H1, Rmult_eq_reg_r with r1.
Qed.
......
......@@ -166,7 +166,7 @@ now apply Zle_left.
Qed.
Lemma generic_format_F2R': forall (x:R) (f:float beta),
F2R f = x -> ((x <> 0)%R ->
F2R f = x -> ((x <> 0)%R ->
(canonic_exp x <= Fexp f)%Z) ->
generic_format x.
Proof.
......@@ -794,8 +794,8 @@ Qed.
Theorem exp_small_round_0_pos :
forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R ->
forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R ->
round x =R0 -> (ex <= fexp ex)%Z .
Proof.
intros x ex H H1.
......@@ -1069,8 +1069,8 @@ apply round_bounded_large_pos...
Qed.
Theorem exp_small_round_0 :
forall rnd {Hr : Valid_rnd rnd} x ex,
(bpow (ex - 1) <= Rabs x < bpow ex)%R ->
forall rnd {Hr : Valid_rnd rnd} x ex,
(bpow (ex - 1) <= Rabs x < bpow ex)%R ->
round rnd x =R0 -> (ex <= fexp ex)%Z .
Proof.
intros rnd Hr x ex H1 H2.
......
......@@ -1140,7 +1140,7 @@ now split.
Qed.
Theorem pred_succ : forall { monotone_exp : Monotone_exp fexp },
Theorem pred_succ : forall { monotone_exp : Monotone_exp fexp },
forall x, F x -> (0 < x)%R -> pred (x + ulp x)=x.
Proof.
intros L x Fx Hx.
......@@ -1211,8 +1211,8 @@ Qed.
(** Properties of rounding to nearest and ulp *)
Theorem rnd_N_le_half_an_ulp: forall choice u v,
F u -> (0 < u)%R -> (v < u + (ulp u)/2)%R
Theorem rnd_N_le_half_an_ulp: forall choice u v,
F u -> (0 < u)%R -> (v < u + (ulp u)/2)%R
-> (round beta fexp (Znearest choice) v <= u)%R.
Proof with auto with typeclass_instances.
intros choice u v Fu Hu H.
......@@ -1247,8 +1247,8 @@ right; field.
Qed.
Theorem rnd_N_ge_half_an_ulp_pred: forall choice u v,
F u -> (0 < pred u)%R -> (u - (ulp (pred u))/2 < v)%R
Theorem rnd_N_ge_half_an_ulp_pred: forall choice u v,
F u -> (0 < pred u)%R -> (u - (ulp (pred u))/2 < v)%R
-> (u <= round beta fexp (Znearest choice) v)%R.
Proof with auto with typeclass_instances.
intros choice u v Fu Hu H.
......@@ -1300,9 +1300,9 @@ now apply Rgt_not_eq.
Qed.
Theorem rnd_N_ge_half_an_ulp: forall choice u v,
Theorem rnd_N_ge_half_an_ulp: forall choice u v,
F u -> (0 < u)%R -> (u <> bpow (ln_beta beta u - 1))%R
-> (u - (ulp u)/2 < v)%R
-> (u - (ulp u)/2 < v)%R
-> (u <= round beta fexp (Znearest choice) v)%R.
Proof with auto with typeclass_instances.
intros choice u v Fu Hupos Hu H.
......@@ -1346,10 +1346,10 @@ rewrite Hu2; assumption.
Qed.
Lemma round_N_DN_betw: forall choice x d u,
Lemma round_N_DN_betw: forall choice x d u,
Rnd_DN_pt (generic_format beta fexp) x d ->
Rnd_UP_pt (generic_format beta fexp) x u ->
(d<=x<(d+u)/2)%R ->
(d<=x<(d+u)/2)%R ->
round beta fexp (Znearest choice) x = d.
Proof with auto with typeclass_instances.
intros choice x d u Hd Hu H.
......@@ -1382,10 +1382,10 @@ apply H.
Qed.
Lemma round_N_UP_betw: forall choice x d u,
Lemma round_N_UP_betw: forall choice x d u,
Rnd_DN_pt (generic_format beta fexp) x d ->
Rnd_UP_pt (generic_format beta fexp) x u ->
((d+u)/2 < x <= u)%R ->
((d+u)/2 < x <= u)%R ->
round beta fexp (Znearest choice) x = u.
Proof with auto with typeclass_instances.
intros choice x d u Hd Hu H.
......
......@@ -27,7 +27,7 @@ Require Import Fappli_IEEE.
Section Bounds.
Definition nat_to_N (n:nat) := match n with
Definition nat_to_N (n:nat) := match n with
| 0 => N0
| (S m) => (Npos (P_of_succ_nat m))
end.
......@@ -38,16 +38,16 @@ intros; induction n; simpl; auto.
Qed.
Definition make_bound (p E:nat) := Bound
Definition make_bound (p E:nat) := Bound
(P_of_succ_nat (Peano.pred (Zabs_nat (Zpower_nat 2%Z p))))
(nat_to_N E).
Lemma make_EGivesEmin: forall p E:nat,
Lemma make_EGivesEmin: forall p E:nat,
(Z_of_N (dExp (make_bound p E)))=E.
intros; simpl; apply nat_to_N_correct.
Qed.
Lemma make_pGivesBound: forall p E:nat,
Lemma make_pGivesBound: forall p E:nat,
Zpos (vNum (make_bound p E))=(Zpower_nat 2 p).
intros.
unfold make_bound, vNum.
......@@ -97,7 +97,7 @@ End Bounds.
Section Equiv.
Variable b : Fbound.
Variable p : nat.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat 2%Z p.
Hypothesis precisionNotZero : 1 < p.
......@@ -121,7 +121,7 @@ exact H0.
Qed.
Lemma equiv_RNDs_aux2: forall r,
Lemma equiv_RNDs_aux2: forall r,
(generic_format radix2 (FLT_exp (-dExp b) p) r)
-> exists f, FtoR 2 f = r /\ Fbounded b f.
intros r Hr.
......@@ -160,7 +160,7 @@ intros H; contradict H; auto.
Qed.
Lemma equiv_RNDs_aux4: forall f, Fcanonic 2 b f -> FtoR 2 f <> 0 ->
canonic radix2 (FLT_exp (- dExp b) p)
canonic radix2 (FLT_exp (- dExp b) p)
(Float radix2 (Float.Fnum f) (Float.Fexp f)).
intros f Hf1 Hf2; unfold canonic; simpl.
assert (K:(F2R (Float radix2 (Float.Fnum f) (Float.Fexp f)) = FtoR 2 f)).
......@@ -242,7 +242,7 @@ Qed.
Lemma equiv_RNDs_aux5: forall (r:R),
(FtoR 2 (RND_EvenClosest b 2 p r)
(FtoR 2 (RND_EvenClosest b 2 p r)
= round radix2 (FLT_exp (-dExp b) p) rndNE r).
intros.
assert (Rnd_NE_pt radix2 (FLT_exp (-dExp b) p) r
......@@ -309,7 +309,7 @@ Qed.
Lemma equiv_RNDs: forall (r:R),
exists f:Float.float, (Fcanonic 2 b f /\ (EvenClosest b 2 p r f) /\
exists f:Float.float, (Fcanonic 2 b f /\ (EvenClosest b 2 p r f) /\
FtoR 2 f = round radix2 (FLT_exp (-dExp b) p) rndNE r).
intros r.
exists (RND_EvenClosest b 2 p r).
......@@ -325,7 +325,7 @@ End Equiv.
Section Equiv_instanc.
Lemma equiv_RNDs_s: forall (r:R),
exists f:Float.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\
exists f:Float.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\
FtoR 2 f = round radix2 (FLT_exp (-149) 24) rndNE r).
apply equiv_RNDs.
apply psGivesBound.
......@@ -334,7 +334,7 @@ Qed.
Lemma equiv_RNDs_d: forall (r:R),
exists f:Float.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\
exists f:Float.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\
FtoR 2 f = round radix2 (FLT_exp (-1074) 53) rndNE r).
apply equiv_RNDs.
apply pdGivesBound.
......
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