Commit 43d3a42b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove trailing whitespaces.

parent 75ceaaca
......@@ -113,31 +113,30 @@ Version 2.0.0:
. generic_relative_error_F2R_ex -> relative_error_F2R_emin_ex
. generic_relative_error_2 -> relative_error_round
. generic_relative_error_F2R_2 -> relative_error_round_F2R_emin
. generic_relative_error_N -> relative_error_N
. generic_relative_error_N -> relative_error_N
. generic_relative_error_N_ex -> relative_error_N_ex
. generic_relative_error_N_F2R -> relative_error_N_F2R_emin
. generic_relative_error_N_F2R_ex -> relative_error_N_F2R_emin_ex
. generic_relative_error_N_2 -> relative_error_N_round
. generic_relative_error_N_F2R_2 -> relative_error_N_round_F2R_emin
. relative_error_FLT_F2R -> relative_error_FLT_F2R_emin
. relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
. relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
. relative_error_N_FLT_2 -> relative_error_N_FLT_round
. relative_error_N_FLT_F2R -> relative_error_N_FLT_F2R_emin
. relative_error_N_FLT_F2R_ex -> relative_error_N_FLT_F2R_emin_ex
. relative_error_N_FLT_F2R_2 -> relative_error_N_FLT_round_F2R_emin
. relative_error_FLX_2 -> relative_error_FLX_round
. relative_error_N_FLX_2 -> relative_error_N_FLX_round
. canonic_bounded_prec -> canonic_canonic_mantissa
. canonic_bounded_prec -> canonic_canonic_mantissa
. B2R_lt_emax -> abs_B2R_lt_emax
. binary_unicity -> B2FF_inj
. finite_binary_unicity -> B2R_inj
. binary_round_sign_correct -> binary_round_aux_correct
. shl_correct -> shl_align_correct
. snd_shl -> snd_shl_align
. shl_fexp_correct -> shl_align_fexp_correct
. snd_shl -> snd_shl_align
. shl_fexp_correct -> shl_align_fexp_correct
. binary_round_sign_shl_correct -> binary_round_correct
Version 1.4.0:
- improved efficiency of IEEE-754 addition
- fixed compilation with Coq 8.3
......
......@@ -49,7 +49,7 @@ Section Binary.
(** prec is the number of bits of the mantissa including the implicit one
emax is the exponent of the infinities
Typically p=24 and emax = 128 in single precision *)
Variable prec emax : Z.
Variable prec emax : Z.
Context (prec_gt_0_ : Prec_gt_0 prec).
Hypothesis Hmax : (prec < emax)%Z.
......@@ -70,7 +70,7 @@ Definition valid_binary x :=
| _ => true
end.
(** Basic type used for representing binary FP numbers.
(** 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. *)
Inductive binary_float :=
......
......@@ -39,7 +39,7 @@ The algorithm performs the following steps:
- Shift dividend mantissa so that it has at least p2 + p digits.
- Perform the Euclidean division.
- Compute the position according to the division remainder.
Complexity is fine as long as p1 <= 2p and p2 <= p.
*)
......
......@@ -1589,7 +1589,7 @@ rewrite <- Ropp_mult_distr_l_reverse.
now rewrite <- Z2R_opp.
Qed.
(** Another well-used function for having the logarithm of a real number x to the base #&beta;# *)
(** Another well-used function for having the logarithm of a real number x to the base #&beta;# *)
Record ln_beta_prop x := {
ln_beta_val :> Z ;
_ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R
......
......@@ -408,7 +408,7 @@ apply Zle_0_nat.
easy.
destruct n as [|n|n] ; try easy.
now rewrite 3!ZOmod_0_r.
Qed.
Qed.
Theorem ZOdiv_plus_pow_digit :
forall u v n, (0 <= u * v)%Z ->
......
......@@ -400,7 +400,7 @@ Theorem abs_lt_bpow_prec:
forall prec,
(forall e, (e - prec <= fexp e)%Z) ->
(* OK with FLX, FLT and FTZ *)
forall x,
forall x,
(Rabs x < bpow (prec + canonic_exp x))%R.
intros prec Hp x.
case (Req_dec x 0); intros Hxz.
......
......@@ -55,9 +55,9 @@ now rewrite canonic_exp_abs.
Qed.
Theorem ulp_le_id:
forall x,
forall x,
(0 < x)%R ->
F x ->
F x ->
(ulp x <= x)%R.
Proof.
intros x Zx Fx.
......@@ -74,9 +74,9 @@ now rewrite <- Fx.
Qed.
Theorem ulp_le_abs:
forall x,
forall x,
(x <> 0)%R ->
F x ->
F x ->
(ulp x <= Rabs x)%R.
Proof.
intros x Zx Fx.
......@@ -493,7 +493,7 @@ rewrite round_DN_opp; ring.
rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
Qed.
Theorem ulp_half_error_f :
Theorem ulp_half_error_f :
forall { Hm : Monotone_exp fexp },
forall choice x,
(round beta fexp (Znearest choice) x <> 0)%R ->
......@@ -590,7 +590,7 @@ now rewrite Rmult_1_l.
Qed.
Lemma generic_format_pred_1:
forall x, (0 < x)%R -> F x ->
forall x, (0 < x)%R -> F x ->
x <> bpow (ln_beta beta x - 1) ->
F (x - ulp x).
Proof.
......@@ -649,7 +649,7 @@ omega.
Qed.
Lemma generic_format_pred_2 :
forall x, (0 < x)%R -> F x ->
forall x, (0 < x)%R -> F x ->
let e := ln_beta_val beta x (ln_beta beta x) in
x = bpow (e - 1) ->
F (x - bpow (fexp (e - 1))).
......@@ -657,7 +657,7 @@ Proof.
intros x Zx Fx e Hx.
pose (f:=(x - bpow (fexp (e - 1)))%R).
fold f.
assert (He:(fexp (e-1) <= e-1)%Z).
assert (He:(fexp (e-1) <= e-1)%Z).
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hx; assumption.
case (Zle_lt_or_eq _ _ He); clear He; intros He.
......@@ -713,7 +713,7 @@ ring.
Qed.
Theorem generic_format_pred :
forall x, (0 < x)%R -> F x ->
forall x, (0 < x)%R -> F x ->
F (pred x).
Proof.
intros x Zx Fx.
......@@ -724,7 +724,7 @@ now apply generic_format_pred_1.
Qed.
Lemma pred_plus_ulp_1 :
forall x, (0 < x)%R -> F x ->
forall x, (0 < x)%R -> F x ->
x <> bpow (ln_beta beta x - 1) ->
((x - ulp x) + ulp (x-ulp x) = x)%R.
Proof.
......@@ -771,7 +771,7 @@ now rewrite <- Fx.
Qed.
Lemma pred_plus_ulp_2 :
forall x, (0 < x)%R -> F x ->
forall x, (0 < x)%R -> F x ->
let e := ln_beta_val beta x (ln_beta beta x) in
x = bpow (e - 1) ->
(x - bpow (fexp (e-1)) <> 0)%R ->
......@@ -780,7 +780,7 @@ Proof.
intros x Zx Fx e Hxe Zp.
replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))).
ring.
assert (He:(fexp (e-1) <= e-1)%Z).
assert (He:(fexp (e-1) <= e-1)%Z).
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hxe; assumption.
case (Zle_lt_or_eq _ _ He); clear He; intros He.
......@@ -837,7 +837,7 @@ now apply pred_plus_ulp_1.
Qed.
Theorem pred_lt_id :
forall x,
forall x,
(pred x < x)%R.
Proof.
intros.
......@@ -858,7 +858,7 @@ apply bpow_gt_0.
Qed.
Theorem pred_ge_0 :
forall x,
forall x,
(0 < x)%R -> F x -> (0 <= pred x)%R.
intros x Zx Fx.
unfold pred.
......@@ -924,7 +924,7 @@ Lemma le_pred_lt_aux :
(0 < x < y)%R ->
(x <= pred y)%R.
Proof with auto with typeclass_instances.
intros x y Hx Hy H.
intros x y Hx Hy H.
assert (Zy:(0 < y)%R).
apply Rlt_trans with (1:=proj1 H).
apply H.
......
......@@ -54,7 +54,7 @@ rewrite <- Fexp_Fplus, Hz.
apply Zle_refl.
Qed.
Theorem ex_Fexp_canonic: forall fexp, forall x, generic_format beta fexp x
Theorem ex_Fexp_canonic: forall fexp, forall x, generic_format beta fexp x
-> exists fx:float beta, (x=F2R fx)%R /\ Fexp fx = canonic_exp beta fexp x.
intros fexp x; unfold generic_format.
exists (Float beta (Ztrunc (scaled_mantissa beta fexp x)) (canonic_exp beta fexp x)).
......@@ -176,7 +176,7 @@ apply generic_format_round...
unfold Rminus; apply generic_format_plus_prec with fx (Fopp beta (Fmult beta fr fr)); trivial.
intros e; apply Zle_refl.
unfold Rsqr; now rewrite F2R_opp,F2R_mult, <- Hr1.
(* *)
(* *)
apply Rle_lt_trans with x.
apply Rabs_minus_le.
apply Rle_0_sqr.
......@@ -248,7 +248,7 @@ apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R.
rewrite <- Hr1.
apply ulp_half_error_f...
right; unfold ulp; apply f_equal.
rewrite Hr2, <- Hr1; trivial.
rewrite Hr2, <- Hr1; trivial.
rewrite Rmult_assoc, Rmult_comm.
replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring.
rewrite bpow_plus, Rmult_assoc.
......
......@@ -40,7 +40,7 @@ Lemma mult_error_FLX_aux:
forall x y,
format x -> format y ->
(round beta (FLX_exp prec) rnd (x * y) - (x * y) <> 0)%R ->
exists f:float beta,
exists f:float beta,
(F2R f = round beta (FLX_exp prec) rnd (x * y) - (x * y))%R
/\ (canonic_exp beta (FLX_exp prec) (F2R f) <= Fexp f)%Z
/\ (Fexp f = cexp x + cexp y)%Z.
......
......@@ -525,15 +525,15 @@ Lemma error_N_FLT_aux :
forall x,
(0 < x)%R ->
exists eps, exists eta,
(Rabs eps <= /2 * bpow (-prec + 1))%R /\
(Rabs eta <= /2 * bpow (emin))%R /\
(Rabs eps <= /2 * bpow (-prec + 1))%R /\
(Rabs eta <= /2 * bpow (emin))%R /\
(eps*eta=0)%R /\
round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps) + eta)%R.
Proof.
intros x Hx2.
case (Rle_or_lt (bpow (emin+prec)) x); intros Hx.
(* *)
destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice x
destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice x
as (eps,(Heps1,Heps2)).
now apply FLT_exp_valid.
intros; unfold FLT_exp.
......
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