Commit 6a6fde85 authored by BOLDO Sylvie's avatar BOLDO Sylvie

TODO-- (moving, improving)

parent 9a515bc7
Version 2.5.0:
- iter_pos?
- new definition of the ulp. ulp(0) is now 0 when there is no minimal
exponent, such as in FLX, and beta^(fexp n) when there is a n such
that n <= fexp n. For instance, the value of ulp(O) is then
beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
is equivalent to the previous "unfold ulp" provided the value is
not zero.
- added several lemmas in Fcore_ulp, including generic_format_ulp
- changed ulp_le: it now works for any values. Please use ulp_le_pos
for the previous behavior.
- changed ulp_error: it now requires x to be non zero, as ulp(0)
may now be zero.
- pred has been renamed pred_pos
- defined a predecessor and successor on both positive, negative and
zero values.
- added useful lemmas about pred and succ, including
generic_format_pred, succ_le_lt, le_pred_lt, succ_pred, pred_inj,
pred_monotone, pred_UP_eq_DN.
- TODO: more examples (Average, Cody_Waite, Compute, Triangle, Division_u16)
TODO
- new definition of the ulp with a nice ulp(0)
- changed named, generalized and added lemmas in Fcore_ulp
- defined a predecessor and successor on both positive, negative and
zero values (the previous pred has been renamed pred_pos)
- More examples have been added
* Average: proof on Sterbenz's average and correctly-rounded average
TODO
* Cody_Waite
* Compute: effective FP computation inside Coq with an example of
(sqr (sqrt x)) in radix 5 and precision 3.
* Division_u16
* Triangle: Kahan's algorithm for the area of a triangle
Version 2.4.0:
......
......@@ -5,48 +5,7 @@ Require Import Fourier.
Open Scope R_scope.
Section av1.
(* TODO: bouger lemmes! *)
Lemma Fnum_ge_0_compat: forall (beta : radix) (f : float beta),
0 <= F2R f -> (0 <= Fnum f)%Z.
Proof.
intros beta f H.
case (Zle_or_lt 0 (Fnum f)); trivial.
intros H1; contradict H.
apply Rlt_not_le.
now apply F2R_lt_0_compat.
Qed.
Lemma Fnum_le_0_compat: forall (beta : radix) (f : float beta),
F2R f <= 0 -> (Fnum f <= 0)%Z.
Proof.
intros beta f H.
case (Zle_or_lt (Fnum f) 0); trivial.
intros H1; contradict H.
apply Rlt_not_le.
now apply F2R_gt_0_compat.
Qed.
Lemma Rmin_opp: forall x y, Rmin (-x) (-y) = - Rmax x y.
Proof.
intros x y.
apply Rmax_case_strong; intros H.
rewrite Rmin_left; trivial.
now apply Ropp_le_contravar.
rewrite Rmin_right; trivial.
now apply Ropp_le_contravar.
Qed.
Lemma Rmax_opp: forall x y, Rmax (-x) (-y) = - Rmin x y.
Proof.
intros x y.
apply Rmin_case_strong; intros H.
rewrite Rmax_left; trivial.
now apply Ropp_le_contravar.
rewrite Rmax_right; trivial.
now apply Ropp_le_contravar.
Qed.
Lemma Rmin_Rmax_overflow: forall x y z M, Rabs x <= M -> Rabs y <= M ->
Rmin x y <= z <= Rmax x y -> Rabs z <= M.
......
......@@ -2814,21 +2814,6 @@ destruct (Req_dec a 0) as [Za|Nza].
+ now apply Rle_trans with x.
Qed.
(* TODO --> Fcore_Raux *)
Lemma sqrt_neg : forall x, x <= 0 -> sqrt x = 0.
Proof.
intros x Npx.
destruct (Req_dec x 0) as [Zx|Nzx].
- (* x = 0 *)
rewrite Zx.
exact sqrt_0.
- (* x < 0 *)
unfold sqrt.
destruct Rcase_abs.
+ reflexivity.
+ casetype False.
now apply Nzx, Rle_antisym; [|apply Rge_le].
Qed.
Lemma double_round_sqrt :
forall fexp1 fexp2 : Z -> Z,
......
......@@ -244,6 +244,25 @@ now apply F2R_eq_0_reg with (Fexp f).
Qed.
Lemma Fnum_ge_0_compat: forall (f : float beta),
(0 <= F2R f)%R -> (0 <= Fnum f)%Z.
Proof.
intros f H.
case (Zle_or_lt 0 (Fnum f)); trivial.
intros H1; contradict H.
apply Rlt_not_le.
now apply F2R_lt_0_compat.
Qed.
Lemma Fnum_le_0_compat: forall (f : float beta),
(F2R f <= 0)%R -> (Fnum f <= 0)%Z.
Proof.
intros f H.
case (Zle_or_lt (Fnum f) 0); trivial.
intros H1; contradict H.
apply Rlt_not_le.
now apply F2R_gt_0_compat.
Qed.
(** Floats and bpow *)
Theorem F2R_bpow :
......
......@@ -1496,7 +1496,7 @@ right.
now rewrite Zmax_l with (1 := Zlt_le_weak _ _ He).
Qed.
Theorem ln_beta_round_DN : (* TODO ln_beta_DN *)
Theorem ln_beta_round_DN : (* TODO ln_beta_DN ??? SB ???*)
forall x,
(0 < round Zfloor x)%R ->
(ln_beta beta (round Zfloor x) = ln_beta beta x :> Z).
......
......@@ -84,6 +84,12 @@ Qed.
(** Definition and basic properties about the ulp *)
(** Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal
exponent, such as in FLX, and beta^(fexp n) when there is a n such
that n <= fexp n. For instance, the value of ulp(O) is then
beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
is equivalent to the previous "unfold ulp" provided the value is
not zero. *)
Definition ulp x := match Req_bool x 0 with
| true => match negligible_exp with
......@@ -1209,19 +1215,21 @@ apply Ropp_lt_contravar.
now apply Heps.
Qed.
(* TODO: Rmin -> Rle_bool x 0 *)
Theorem round_DN_plus_eps:
forall x, F x ->
forall eps, (0 <= eps < Rmin (ulp x) (ulp (pred (-x))))%R ->
forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x)
else (ulp (pred (-x))))%R ->
round beta fexp Zfloor (x + eps) = x.
Proof.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
apply round_DN_plus_eps_pos; try assumption.
split; try apply Heps.
apply Rlt_le_trans with (1:=proj2 Heps).
apply Rmin_l.
rewrite Rle_bool_true in Heps; trivial.
now apply Heps.
(* *)
rewrite Rle_bool_false in Heps; trivial.
rewrite <- (Ropp_involutive (x+eps)).
pattern x at 2; rewrite <- (Ropp_involutive x).
rewrite round_DN_opp.
......@@ -1232,8 +1240,7 @@ now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
split.
apply Rplus_lt_reg_l with eps; ring_simplify.
apply Rlt_le_trans with (1:=proj2 Heps).
apply Rmin_r.
apply Heps.
apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify.
apply Heps.
unfold pred.
......@@ -1246,20 +1253,20 @@ now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
Qed.
(* TODO: Rmin -> Rle_bool x 0 *)
Theorem round_UP_plus_eps :
forall x, F x ->
forall eps, (0 < eps <= Rmin (ulp x) (ulp (pred (-x))))%R ->
forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x)
else (ulp (pred (-x))))%R ->
round beta fexp Zceil (x + eps) = (succ x)%R.
Proof with auto with typeclass_instances.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
rewrite succ_eq_pos; try assumption.
apply round_UP_plus_eps_pos; try assumption.
split; try apply Heps.
apply Rle_trans with (1:=proj2 Heps).
apply Rmin_l.
rewrite Rle_bool_true in Heps; trivial.
apply round_UP_plus_eps_pos; assumption.
(* *)
rewrite Rle_bool_false in Heps; trivial.
rewrite <- (Ropp_involutive (x+eps)).
rewrite <- (Ropp_involutive (succ x)).
rewrite round_UP_opp.
......@@ -1273,8 +1280,7 @@ now apply generic_format_opp.
now apply generic_format_opp, generic_format_succ.
split.
apply Rplus_le_reg_l with eps; ring_simplify.
apply Rle_trans with (1:=proj2 Heps).
apply Rmin_r.
apply Heps.
unfold pred; rewrite Ropp_involutive.
apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify.
apply Heps.
......@@ -1632,94 +1638,71 @@ now apply Ropp_0_gt_lt_contravar.
Qed.
(* TODO: Rmin -> Rle_bool x 0 *)
Theorem round_UP_pred_plus_eps :
forall x, F x ->
forall eps, (0 < eps <= Rmin (ulp x) (ulp (pred x)))%R ->
forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x)
else (ulp (pred x)))%R ->
round beta fexp Zceil (pred x + eps) = x.
Proof.
intros x Fx eps Heps.
rewrite round_UP_plus_eps.
now apply succ_pred.
now apply generic_format_pred.
unfold pred at 3.
unfold pred at 4.
rewrite Ropp_involutive, pred_succ.
rewrite ulp_opp.
now rewrite Rmin_comm.
generalize Heps; case (Rle_bool_spec x 0); intros H1 H2.
rewrite Rle_bool_false; trivial.
case H1; intros H1'.
apply Rlt_le_trans with (2:=H1).
apply pred_lt_id.
now apply Rlt_not_eq.
rewrite H1'; unfold pred, succ.
rewrite Ropp_0; rewrite Rle_bool_true;[idtac|now right].
rewrite Rplus_0_l.
rewrite <- Ropp_0; apply Ropp_lt_contravar.
apply Rlt_le_trans with (1:=proj1 H2).
apply Rle_trans with (1:=proj2 H2).
rewrite Ropp_0, H1'.
now right.
rewrite Rle_bool_true; trivial.
now apply pred_ge_0.
now apply generic_format_opp.
Qed.
(* TODO: Rmin -> Rle_bool x 0 *)
Theorem round_DN_minus_eps:
forall x, F x ->
forall eps, (0 < eps <= Rmin (ulp x) (ulp (pred x)))%R ->
forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x)
else (ulp (pred x)))%R ->
round beta fexp Zfloor (x - eps) = pred x.
Proof.
intros x Fx eps Heps.
(* *)
assert ( (0 < x /\ x - pred x = ulp (pred x))
\/ (x < 0)
\/ ( x = 0 /\ pred x = - ulp 0))%R.
case (Rle_or_lt 0 x); intros Zx.
case Zx; intros Zx'.
left; split; try assumption.
rewrite pred_eq_pos; try assumption.
pattern x at 1; rewrite <- (pred_pos_plus_ulp x); try assumption.
ring.
right; right; split.
now rewrite Zx'.
rewrite <- Zx'.
rewrite pred_eq_pos.
unfold pred_pos; rewrite Req_bool_false.
ring.
apply Rlt_not_eq, bpow_gt_0.
now apply Req_le_sym.
right; left; assumption.
(* *)
case H;[intros (H1,H2); clear H|idtac].
(* . *)
replace (x-eps)%R with (pred x + (x-pred x-eps))%R by ring.
rewrite H2.
apply round_DN_plus_eps_pos.
now apply pred_ge_0.
now apply generic_format_pred.
split.
apply Rplus_le_reg_l with eps; ring_simplify.
apply Rle_trans with (1:=proj2 Heps).
apply Rmin_r.
apply Rplus_lt_reg_l with (eps-ulp(pred x))%R; ring_simplify.
apply Heps.
clear H; intros H; case H;[intros H1|intros (H1,H2)]; clear H.
(* . *)
replace (x-eps)%R with (-(-x+eps))%R by ring.
rewrite round_DN_opp.
unfold pred; apply f_equal.
pattern (-x)%R at 1; rewrite <- (pred_succ (-x)).
apply round_UP_pred_plus_eps_pos.
apply Rlt_trans with (-x)%R.
now apply Ropp_0_gt_lt_contravar.
apply succ_gt_id.
now apply Rgt_not_eq, Ropp_0_gt_lt_contravar.
apply round_UP_pred_plus_eps.
now apply generic_format_succ, generic_format_opp.
rewrite pred_succ, ulp_opp.
split;[apply Heps|idtac].
apply Rle_trans with (1:=proj2 Heps).
apply Rmin_l.
rewrite pred_succ.
rewrite ulp_opp.
generalize Heps; case (Rle_bool_spec x 0); intros H1 H2.
rewrite Rle_bool_false; trivial.
case H1; intros H1'.
apply Rlt_le_trans with (-x)%R.
now apply Ropp_0_gt_lt_contravar.
apply succ_ge_id.
rewrite H1', Ropp_0, succ_eq_pos;[idtac|now right].
rewrite Rplus_0_l.
apply Rlt_le_trans with (1:=proj1 H2).
rewrite H1' in H2; apply H2.
rewrite Rle_bool_true.
now rewrite succ_opp, ulp_opp.
rewrite succ_opp.
rewrite <- Ropp_0; apply Ropp_le_contravar.
now apply pred_ge_0.
now apply generic_format_opp.
now apply generic_format_opp.
(* . *)
rewrite H1.
unfold Rminus; rewrite Rplus_0_l.
rewrite round_DN_opp.
rewrite <- (Rplus_0_l eps).
rewrite round_UP_plus_eps_pos.
rewrite H1 in H2; rewrite H2; ring.
now apply Req_le_sym.
apply generic_format_0.
split; try apply Heps.
apply Rle_trans with (1:=proj2 Heps).
rewrite H1; apply Rmin_l.
Qed.
(** Error of a rounding, expressed in number of ulps *)
......
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