Commit 631bf464 authored by BOLDO Sylvie's avatar BOLDO Sylvie

FLT rounding

parent 16850d38
......@@ -180,6 +180,12 @@ repeat rewrite Z2R_IZR.
apply IZR_lt.
Qed.
Lemma Z2R_lt_le: forall e1 e2, (Z2R (e1-1) < Z2R e2)%R -> (Z2R e1 <= Z2R e2)%R.
intros.
apply Z2R_le.
assert (e1 -1 < e2)%Z; auto with zarith.
now apply lt_Z2R.
Qed.
Lemma Z2R_neq :
forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R.
......@@ -189,6 +195,13 @@ repeat rewrite Z2R_IZR.
apply IZR_neq.
Qed.
Lemma Rabs_Z2R: forall z, Rabs (Z2R z) = Z2R (Zabs z).
intros.
repeat rewrite Z2R_IZR.
apply Rabs_Zabs.
Qed.
End Z2R.
......@@ -198,6 +211,13 @@ Record radix := { radix_val : Z ; radix_prop : (2 <= radix_val )%Z }.
Variable r: radix.
Lemma radix_pos: (0 < Z2R (radix_val r))%R.
destruct r; simpl.
apply Rle_lt_trans with (Z2R 0).
right; reflexivity.
apply Z2R_lt; auto with zarith.
Qed.
Definition epow e :=
match e with
| Zpos p => Z2R (Zpower_pos (radix_val r) p)
......@@ -273,6 +293,29 @@ unfold epow, Zpower_pos, iter_pos.
now rewrite Zmult_1_r.
Qed.
Lemma epow_add1 :
forall e : Z, (epow (e+1) = Z2R (radix_val r) * epow e)%R.
Proof.
intros.
rewrite <- epow_1.
rewrite <- epow_add.
now rewrite Zplus_comm.
Qed.
Lemma epow_opp :
forall e : Z, (epow (-e) = /epow e)%R.
Proof.
intros e; destruct e.
simpl; now rewrite Rinv_1.
now replace (-Zpos p)%Z with (Zneg p) by reflexivity.
replace (-Zneg p)%Z with (Zpos p) by reflexivity.
simpl; rewrite Rinv_involutive; trivial.
generalize (epow_gt_0 (Zpos p)).
simpl; auto with real.
Qed.
Lemma Z2R_Zpower :
forall e : Z,
(0 <= e)%Z ->
......@@ -370,7 +413,7 @@ apply -> epow_le.
now apply Zeq_le.
apply -> epow_le.
apply Zeq_le.
now apply eq_sym.
now apply sym_eq.
Qed.
Lemma epow_exp :
......@@ -466,4 +509,30 @@ now apply exp_ln.
now apply Rgt_not_eq.
Qed.
Lemma Zpower_pos_lt: forall b z, (0 < b)%Z -> (0 < Zpower_pos b z)%Z.
intros; apply lt_Z2R.
simpl; rewrite Zpower_pos_powerRZ.
apply powerRZ_lt.
apply Rle_lt_trans with (Z2R 0).
right; reflexivity.
now apply Z2R_lt.
Qed.
Lemma Zpower_lt: forall b z, (0 < b)%Z -> (0 < z)%Z -> (0 < Zpower b z)%Z.
intros.
destruct z; unfold Zpower; auto with zarith.
now apply Zpower_pos_lt.
absurd (0 <= Zneg p)%Z; auto with zarith.
Qed.
Lemma vNum_gt_1: forall prec, (0 < prec)%Z -> (1 < radix_val r ^ prec)%Z.
intros.
apply lt_Z2R.
rewrite Z2R_Zpower; auto with zarith.
apply Rle_lt_trans with (epow 0%Z).
right; reflexivity.
now apply -> epow_lt.
Qed.
End pow.
......@@ -6,239 +6,13 @@ Section RND_FIX.
Open Scope R_scope.
(*
Theorem exp_ln_powerRZ :
forall u v : Z, (0 < u)%Z -> exp (ln (IZR u) * (IZR v)) = powerRZ (IZR u) v.
admit.
Qed.
(*
Theorem exp_monotone : forall x y : R, (x <= y)%R -> (exp x <= exp y)%R.
intros x y H; case H; intros H2.
left; apply exp_increasing; auto.
right; auto with real.
Qed.*)
Definition floor_int (r : R) :=(up r-1)%Z.
Theorem floor_int_pos : forall r : R, (0 <= r)%R -> (0 <= IZR (floor_int r))%R.
Proof.
intros r H1; unfold floor_int in |- *.
generalize (archimed r); intros T; elim T; intros H3 H2; clear T.
replace 0%R with (IZR 0); auto with real; apply IZR_le.
assert (0 < up r)%Z; auto with zarith.
apply lt_IZR; apply Rle_lt_trans with r; auto with real zarith.
Qed.
Theorem floor_int_correct1 : forall r : R, (IZR (floor_int r) <= r)%R.
Proof.
intros r; unfold floor_int in |- *.
generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
apply Rplus_le_reg_l with (1 + - r)%R.
ring_simplify (1 + - r + r)%R.
apply Rle_trans with (2 := H2).
unfold Zminus; rewrite plus_IZR; right; simpl in |- *; ring.
Qed.
Theorem floor_int_correct2 : forall r : R, (r < IZR (floor_int r+1))%R.
intros r; unfold floor_int in |- *.
generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
ring_simplify (up r - 1 + 1)%Z; auto.
Qed.
Theorem floor_int_correct3 : forall r : R, (r - 1 < IZR (floor_int r))%R.
intros r; unfold floor_int in |- *.
generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
unfold Rminus, Zminus; rewrite plus_IZR; simpl in |- *; auto with real.
Qed.
*)
Variable beta : radix.
Notation bpow := (epow beta).
Variable emin prec : Z.
(*
Definition RND_DN_pos_fn (r : R) :=
match Rle_dec (powerRZ (IZR radix) (prec-1+emin)) r with
| left _ =>
let e := floor_int (ln r / ln (IZR radix) + IZR (- prec+1)) in
Float radix (floor_int (r * powerRZ (IZR radix) (- e))) e
| right _ => Float radix (floor_int (r * powerRZ (IZR radix) (-emin))) emin
end.
Variable radix_gt_0 : (0 < radix)%Z.
Lemma FLT_format_satisfies_DN_aux:
forall x : R, (0 <= x)%R -> exists f : R, Rnd_DN (FLT_format radix emin prec) x f.
Proof.
intros; exists (F2R (RND_DN_pos_fn x)); split.
exists (RND_DN_pos_fn x); split; auto; split.
unfold RND_DN_pos_fn; case (Rle_dec (powerRZ (IZR radix) (prec-1+emin)) x); simpl; intros H1.
rewrite Zabs_eq.
2: apply le_IZR; apply floor_int_pos; apply Rmult_le_pos; auto.
2: admit. (* cf apres *)
apply lt_IZR.
apply Rle_lt_trans with (1:=floor_int_correct1 _).
rewrite <- exp_ln_powerRZ; auto.
apply Rlt_le_trans with (x *
(exp (-ln x) * exp (ln (IZR radix) * IZR (prec))))%R.
apply Rmult_lt_compat_l; auto with real.
apply Rlt_le_trans with (2:=H1); auto with real zarith.
admit. (* cf apres *)
rewrite <- exp_plus.
apply exp_increasing.
apply Rmult_lt_reg_l with (/ln (IZR radix))%R.
admit.
apply Rle_lt_trans with (IZR (- floor_int (ln x / ln (IZR radix) + IZR (- prec+1)))).
right; field.
admit.
apply Rlt_le_trans with (-(ln x / ln (IZR radix) - IZR (prec)))%R.
2: right; field.
2: admit.
rewrite Ropp_Ropp_IZR.
apply Ropp_lt_contravar.
apply Rle_lt_trans with (2:= floor_int_correct3 _).
rewrite plus_IZR; rewrite Ropp_Ropp_IZR; simpl; right; ring.
rewrite exp_Ropp; rewrite exp_ln; auto.
2: admit.
rewrite exp_ln_powerRZ.
admit.
auto.
rewrite Zabs_eq.
2: apply le_IZR; apply floor_int_pos; apply Rmult_le_pos; auto.
2: admit. (* cf apres *)
apply lt_IZR.
apply Rle_lt_trans with (1:=floor_int_correct1 _).
apply Rlt_le_trans with (powerRZ (IZR radix) (prec - 1 + emin)* powerRZ (IZR radix) (- emin))%R.
apply Rmult_lt_compat_r.
admit.
auto with real.
rewrite <- powerRZ_add; auto with real.
(* apply Rle_ powerRZ.*)
admit.
admit.
unfold RND_DN_pos_fn; case (Rle_dec (powerRZ (IZR radix) (prec-1+emin)) x);
simpl; auto with zarith; intros H1.
assert (emin-1 < floor_int (ln x / ln (IZR radix) + IZR (- prec + 1)))%Z; auto with zarith.
apply lt_IZR.
apply Rle_lt_trans with (2:= floor_int_correct3 _).
apply Rplus_le_reg_l with (IZR prec).
apply Rmult_le_reg_l with (ln (IZR radix)).
admit.
apply Rle_trans with (ln x).
exp
ln
rewrite <- exp_ln_powerRZ; auto.
apply Rlt_le_trans with (x *
(exp (-ln x) * exp (ln (IZR radix) * IZR (prec))))%R.
apply Rmult_lt_compat_l; auto with real.
apply Rlt_le_trans with (2:=H1); auto with real zarith.
admit. (* cf apres *)
rewrite <- exp_plus.
apply exp_increasing.
apply Rmult_lt_reg_l with (/ln (IZR radix))%R.
admit.
apply Rle_lt_trans with (IZR (- floor_int (ln x / ln (IZR radix) + IZR (- prec+1)))).
right; field.
admit.
apply Rlt_le_trans with (-(ln x / ln (IZR radix) - IZR (prec)))%R.
2: right; field.
2: admit.
rewrite Ropp_Ropp_IZR.
apply Ropp_lt_contravar.
apply Rle_lt_trans with (2:= floor_int_correct3 _).
rewrite plus_IZR; rewrite Ropp_Ropp_IZR; simpl; right; ring.
rewrite exp_Ropp; rewrite exp_ln; auto.
2: admit.
rewrite exp_ln_powerRZ.
admit.
auto.
(ln (IZR radix) *
IZR (- (ln x / ln (IZR radix) + IZR (- Zpred prec))))
apply Rle_lt_trans with (x *
powerRZ (IZR radix)
(- floor_int (ln x / ln (IZR radix) + IZR (- Zpred prec)))
rewrite powerRZ_add; auto with real zarith.
rewrite Zpower_powerRZ; rewrite <- Rabsolu_Zabs.
unfold FLT_format.
Theorem FLT_format_satisfies_DN : satisfies_DN (FLT_format radix emin prec).
Proof.
unfold satisfies_DN.
intros.
Theorem FLT_format_satisfies_DN_UP :
satisfies_DN_UP (FLT_format radix emin prec).
Proof.
intros.
assert (Hdn: satisfies_DN (FLT_format radix emin prec)) by admit.
apply satisfies_DN_imp_UP.
intros x (f,(Hx,(Hm,He))).
exists (Float radix (-(Fnum f))%Z (Fexp f)).
repeat split.
rewrite Hx.
unfold F2R.
simpl.
rewrite Ropp_Ropp_IZR.
now rewrite Ropp_mult_distr_l_reverse.
simpl.
now rewrite Zabs_Zopp.
exact He.
exact Hdn.
Qed.
Variable radix_gt_0 : (0 < radix)%Z.
Lemma powerRZ_radix_ge_0 :
forall e : Z, (0 <= powerRZ (IZR radix) e)%R.
Proof.
intros.
apply powerRZ_le.
change R0 with (IZR 0).
apply IZR_lt.
exact radix_gt_0.
Qed.
Lemma powerRZ_radix_gt_0 :
forall e : Z, (0 < powerRZ (IZR radix) e)%R.
Proof.
intros.
apply powerRZ_lt.
change R0 with (IZR 0).
apply IZR_lt.
exact radix_gt_0.
Qed.
Lemma IZR_radix_neq_0 :
IZR radix <> R0.
Proof.
apply Rgt_not_eq.
change R0 with (IZR 0).
apply IZR_lt.
exact radix_gt_0.
Qed.
*)
Variable emin : Z.
Theorem FIX_format_satisfies_any :
satisfies_any (FIX_format beta emin).
......
Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_float_prop.
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_FIX.
Require Import Flocq_rnd_FLX.
Section RND_FLT.
Open Scope R_scope.
Variable beta : radix.
Notation bpow := (epow beta).
Variable emin prec : Z.
Variable Hp : Zlt 0 prec.
Theorem FLT_format_satisfies_any :
satisfies_any (FLT_format beta emin prec).
elim (FIX_format_satisfies_any beta emin); intros O1 T2 r1 H1; clear T2.
elim (FLX_format_satisfies_any beta prec); trivial; intros O1' T2 r2 H2; clear T2.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
exists (Float beta 0 emin).
split.
unfold F2R.
now rewrite Rmult_0_l.
split.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply epow_gt_0.
now apply Zlt_le_weak.
apply Zeq_le.
apply refl_equal.
intros x ((m,e),(K1,K2)).
exists (Float beta (-m) e).
split.
rewrite K1.
unfold F2R.
simpl.
now rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
split.
simpl.
now rewrite Zabs_Zopp.
now simpl.
(* rounding *)
exists (fun x =>
match total_order_T 0 x with
|inleft _ => match total_order_T (bpow (prec+emin)%Z) x with
| inleft _ => r2 x
| inright _ => r1 x
end
| inright _ => match total_order_T x (-bpow (prec+emin)%Z) with
| inleft _ => r2 x
| inright _ => r1 x
end
end).
intros x.
destruct (total_order_T 0 x) as [B|B].
assert (0 <= x);[destruct B; auto with real| clear B].
(* x >= 0 *)
destruct (total_order_T (bpow (prec+emin)%Z) x) as [Hx|Hx].
(** x big *)
assert (bpow (prec + emin)%Z <= x);[destruct Hx; auto with real| clear Hx].
destruct (H2 x) as ((f,(Lf1,Lf2)),(L1,L2)).
split.
exists f.
repeat split; trivial.
apply <- (epow_le beta).
apply Rmult_le_reg_l with (bpow prec).
apply epow_gt_0.
rewrite <- epow_add.
apply Rle_trans with (F2R f).
rewrite <- Lf1.
apply L2; trivial.
exists (Float beta 1 (prec+emin)).
split.
unfold F2R; simpl; auto with real.
simpl.
now apply vNum_gt_1.
unfold F2R; apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite <- Z2R_Zpower; auto with zarith.
apply Z2R_le.
rewrite <- (Zabs_eq (Fnum f)); auto with zarith.
apply le_Z2R.
apply Rmult_le_reg_l with (bpow (Fexp f)).
apply epow_gt_0.
apply Rle_trans with 0%R.
simpl; right; ring.
apply Rle_trans with (r2 x).
now apply L2.
right; rewrite Lf1; unfold F2R; now apply Rmult_comm.
split; trivial.
intros g P1 P2.
apply L2; trivial.
destruct P1 as (f',(M1,(M2,M3))).
exists f'; split; auto.
(** x small *)
assert (x < bpow (prec + emin)%Z);[auto with real| clear Hx].
destruct (H1 x) as ((f,(Lf1,Lf2)),(L1,L2)).
split.
exists f.
repeat split; trivial.
apply lt_Z2R.
rewrite <- Rabs_Z2R.
rewrite Z2R_Zpower; auto with zarith.
apply Rmult_lt_reg_r with (bpow emin).
apply epow_gt_0.
rewrite <- epow_add.
apply Rle_lt_trans with (2:=H0).
apply Rle_trans with (2:=L1).
rewrite <- (Rabs_right (r1 x)).
right; rewrite Lf1.
unfold F2R; rewrite Rabs_mult.
rewrite (Rabs_right (bpow (Fexp f))).
now rewrite Lf2.
apply Rle_ge; apply epow_ge_0.
apply Rle_ge; now apply L2.
rewrite Lf2; auto with zarith.
split; trivial.
intros g P1 P2.
apply L2; trivial.
destruct P1 as (f',(M1,(M2,M3))).
exists (Float beta ((Fnum f'*Zpower (radix_val beta) (Fexp f'-emin))) emin); split; auto.
rewrite M1; unfold F2R; simpl.
rewrite mult_Z2R.
rewrite Z2R_Zpower; auto with zarith.
rewrite Rmult_assoc; rewrite <- epow_add.
now replace (Fexp f' - emin + emin)%Z with (Fexp f') by ring.
assert (x < 0);[auto with real| clear B].
(* x < 0 *)
destruct (total_order_T x (-bpow (prec+emin)%Z)) as [Hx|Hx].
(** x big *)
assert (x <= - bpow (prec + emin)%Z);[destruct Hx; auto with real| clear Hx].
destruct (H2 x) as ((f,(Lf1,Lf2)),(L1,L2)).
split.
exists f.
repeat split; trivial.
apply <- (epow_le beta).
apply Rmult_le_reg_l with (bpow prec).
apply epow_gt_0.
rewrite <- epow_add.
apply Ropp_le_cancel.
apply Rle_trans with (2:=H0).
apply Rle_trans with (2:=L1).
rewrite Lf1.
rewrite <- Ropp_mult_distr_l_reverse.
unfold F2R; apply Rmult_le_compat_r.
apply epow_ge_0.
apply Ropp_le_cancel.
eapply Rle_trans.
apply RRle_abs.
rewrite Rabs_Ropp; rewrite Rabs_Z2R.
rewrite Ropp_involutive.
rewrite <- Z2R_Zpower; auto with zarith.
apply Z2R_le; auto with zarith.
split; trivial.
intros g P1 P2.
apply L2; trivial.
destruct P1 as (f',(M1,(M2,M3))).
exists f'; split; auto.
(** x small *)
assert (- bpow (prec + emin)%Z < x);[auto with real| clear Hx].
destruct (H1 x) as ((f,(Lf1,Lf2)),(L1,L2)).
split.
assert (-bpow (prec + emin)%Z <= r1 x).
apply L2.
exists (Float beta (-Zpower (radix_val beta) prec)%Z emin); split.
unfold F2R; simpl.
rewrite opp_Z2R.
rewrite Z2R_Zpower; auto with zarith.
rewrite Ropp_mult_distr_l_reverse.
now rewrite <- epow_add.
now simpl.
now left.
case H3; intros I.
exists f.
repeat split; trivial.
apply lt_Z2R.
rewrite <- Rabs_Z2R.
rewrite Z2R_Zpower; auto with zarith.
apply Rmult_lt_reg_r with (bpow emin).
apply epow_gt_0.
rewrite <- epow_add.
apply Ropp_lt_cancel.
apply Rlt_le_trans with (1:=I).
apply Ropp_le_cancel; rewrite Ropp_involutive.
rewrite <- (Rabs_left1 (r1 x)).
right; rewrite Lf1.
unfold F2R; rewrite Rabs_mult.
rewrite (Rabs_right (bpow (Fexp f))).
now rewrite Lf2.
apply Rle_ge; apply epow_ge_0.
apply Rle_trans with (1:=L1); now left.
rewrite Lf2; auto with zarith.
exists (Float beta (-Zpower (radix_val beta) (prec-1)) (emin+1)).
split.
rewrite <- I.
unfold F2R; simpl.
rewrite opp_Z2R.
rewrite Z2R_Zpower; auto with zarith.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- epow_add.
now replace (prec - 1 + (emin + 1))%Z with (prec+emin)%Z by ring.
split.
simpl.
rewrite Zabs_Zopp.
rewrite Zabs_eq.
apply lt_Z2R.
repeat rewrite Z2R_Zpower; auto with zarith.
apply -> epow_lt; auto with zarith.
apply le_Z2R.
rewrite Z2R_Zpower; auto with zarith.
simpl.
apply epow_ge_0.
simpl; auto with zarith.
split; trivial.
intros g P1 P2.
apply L2; trivial.
destruct P1 as (f',(M1,(M2,M3))).
exists (Float beta ((Fnum f'*Zpower (radix_val beta) (Fexp f'-emin))) emin); split; auto.
rewrite M1; unfold F2R; simpl.
rewrite mult_Z2R.
rewrite Z2R_Zpower; auto with zarith.
rewrite Rmult_assoc; rewrite <- epow_add.
now replace (Fexp f' - emin + emin)%Z with (Fexp f') by ring.
Qed.
End RND_FLT.
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