Commit 80196ef0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use float arguments for Fdiv and Fsqrt.

parent 7d4b2df1
...@@ -80,9 +80,8 @@ apply sym_eq, F2R_Zabs. ...@@ -80,9 +80,8 @@ apply sym_eq, F2R_Zabs.
Qed. Qed.
Definition sqrt (x : float beta) := Definition sqrt (x : float beta) :=
let (m, e) := x in if Zlt_bool 0 (Fnum x) then
if Zlt_bool 0 m then let '(m', e', l) := truncate beta fexp (Fsqrt beta fexp x) in
let '(m', e', l) := truncate beta fexp (Fsqrt beta fexp m e) in
Float beta (choice false m' l) e' Float beta (choice false m' l) e'
else Float beta 0 0. else Float beta 0 0.
...@@ -90,10 +89,10 @@ Theorem sqrt_correct : ...@@ -90,10 +89,10 @@ Theorem sqrt_correct :
forall x : float beta, forall x : float beta,
round beta fexp rnd (R_sqrt.sqrt (F2R x)) = F2R (sqrt x). round beta fexp rnd (R_sqrt.sqrt (F2R x)) = F2R (sqrt x).
Proof. Proof.
intros [m e]. intros x.
unfold sqrt. unfold sqrt.
case Zlt_bool_spec ; intros Hm. case Zlt_bool_spec ; intros Hm.
generalize (Fsqrt_correct beta fexp m e Hm). generalize (Fsqrt_correct beta fexp x (F2R_gt_0 _ _ Hm)).
destruct Fsqrt as [[m' e'] l]. destruct Fsqrt as [[m' e'] l].
intros [Hs1 Hs2]. intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l). rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l).
...@@ -101,7 +100,7 @@ destruct truncate as [[m'' e''] l']. ...@@ -101,7 +100,7 @@ destruct truncate as [[m'' e''] l'].
now rewrite Rlt_bool_false by apply sqrt_ge_0. now rewrite Rlt_bool_false by apply sqrt_ge_0.
now rewrite Rabs_pos_eq by apply sqrt_ge_0. now rewrite Rabs_pos_eq by apply sqrt_ge_0.
now left. now left.
destruct (Req_dec (F2R (Float beta m e)) 0) as [Hz|Hz]. destruct (Req_dec (F2R x) 0) as [Hz|Hz].
rewrite Hz, sqrt_0, F2R_0. rewrite Hz, sqrt_0, F2R_0.
now apply round_0. now apply round_0.
unfold R_sqrt.sqrt. unfold R_sqrt.sqrt.
...@@ -159,12 +158,10 @@ now elim Hy0. ...@@ -159,12 +158,10 @@ now elim Hy0.
Qed. Qed.
Definition div (x y : float beta) := Definition div (x y : float beta) :=
let (mx, ex) := x in if Zeq_bool (Fnum x) 0 then Float beta 0 0
let (my, ey) := y in
if Zeq_bool mx 0 then Float beta 0 0
else else
let '(m, e, l) := truncate beta fexp (Fdiv beta fexp (Zabs mx) ex (Zabs my) ey) in let '(m, e, l) := truncate beta fexp (Fdiv beta fexp (Fabs _ x) (Fabs _ y)) in
let s := xorb (Zlt_bool mx 0) (Zlt_bool my 0) in let s := xorb (Zlt_bool (Fnum x) 0) (Zlt_bool (Fnum y) 0) in
Float beta (cond_Zopp s (choice s m l)) e. Float beta (cond_Zopp s (choice s m l)) e.
Theorem div_correct : Theorem div_correct :
...@@ -172,41 +169,43 @@ Theorem div_correct : ...@@ -172,41 +169,43 @@ Theorem div_correct :
F2R y <> 0%R -> F2R y <> 0%R ->
round beta fexp rnd (F2R x / F2R y) = F2R (div x y). round beta fexp rnd (F2R x / F2R y) = F2R (div x y).
Proof. Proof.
intros [mx ex] [my ey] Hy. intros x y Hy.
unfold div. unfold div.
case Zeq_bool_spec ; intros Hm. case Zeq_bool_spec ; intros Hm.
rewrite Hm, 2!F2R_0. destruct x as [mx ex].
unfold Rdiv. simpl in Hm.
rewrite Rmult_0_l. rewrite Hm, 2!F2R_0.
now apply round_0. unfold Rdiv.
assert (Hx: (0 < Zabs mx)%Z) by now apply Z.abs_pos. rewrite Rmult_0_l.
assert (Hy': (0 < Zabs my)%Z). now apply round_0.
apply Z.abs_pos. assert (0 < F2R (Fabs _ x))%R as Hx.
destruct x as [mx ex].
now apply F2R_gt_0, Z.abs_pos.
assert (0 < F2R (Fabs _ y))%R as Hy'.
destruct y as [my ey].
apply F2R_gt_0, Z.abs_pos.
contradict Hy. contradict Hy.
rewrite Hy. rewrite Hy.
apply F2R_0. apply F2R_0.
generalize (Fdiv_correct beta fexp (Zabs mx) ex (Zabs my) ey Hx Hy'). generalize (Fdiv_correct beta fexp (Fabs _ x) (Fabs _ y) Hx Hy').
destruct Fdiv as [[m e] l]. destruct Fdiv as [[m e] l].
intros [Hs1 Hs2]. intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l). rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l).
destruct truncate as [[m' e'] l']. - destruct truncate as [[m' e'] l'].
apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))). apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
rewrite Rsgn_div. rewrite Rsgn_div.
apply f_equal2 ; apply Rsgn_F2R. apply f_equal2 ; apply Rsgn_F2R.
contradict Hm. contradict Hm.
apply eq_0_F2R with (1 := Hm). apply eq_0_F2R with (1 := Hm).
exact Hy. exact Hy.
unfold Rdiv. - unfold Rdiv.
rewrite Rabs_mult, Rabs_Rinv. rewrite Rabs_mult, Rabs_Rinv by exact Hy.
rewrite <- 2!F2R_Zabs. now rewrite <- 2!F2R_abs.
exact Hs2. - left.
exact Hy. rewrite <- cexp_abs.
left. unfold Rdiv.
rewrite <- cexp_abs. rewrite Rabs_mult, Rabs_Rinv by exact Hy.
unfold Rdiv. now rewrite <- 2!F2R_abs.
rewrite Rabs_mult, Rabs_Rinv.
now rewrite <- 2!F2R_Zabs.
exact Hy.
Qed. Qed.
End Compute. End Compute.
...@@ -116,20 +116,24 @@ destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2'']. ...@@ -116,20 +116,24 @@ destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2''].
now constructor. now constructor.
Qed. Qed.
Definition Fdiv m1 e1 m2 e2 := Definition Fdiv (x y : float beta) :=
let (m1, e1) := x in
let (m2, e2) := y in
let e' := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in let e' := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in
let e := Zmin (Zmin (fexp e') (fexp (e' + 1))) (e1 - e2) in let e := Zmin (Zmin (fexp e') (fexp (e' + 1))) (e1 - e2) in
let '(m, l) := Fdiv_core m1 e1 m2 e2 e in let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
(m, e, l). (m, e, l).
Theorem Fdiv_correct : Theorem Fdiv_correct :
forall m1 e1 m2 e2, forall x y,
(0 < m1)%Z -> (0 < m2)%Z -> (0 < F2R x)%R -> (0 < F2R y)%R ->
let '(m, e, l) := Fdiv m1 e1 m2 e2 in let '(m, e, l) := Fdiv x y in
(e <= cexp beta fexp (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)))%Z /\ (e <= cexp beta fexp (F2R x / F2R y))%Z /\
inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l. inbetween_float beta m e (F2R x / F2R y) l.
Proof. Proof.
intros m1 e1 m2 e2 Hm1 Hm2. intros [m1 e1] [m2 e2] Hm1 Hm2.
apply gt_0_F2R in Hm1.
apply gt_0_F2R in Hm2.
unfold Fdiv. unfold Fdiv.
generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2). generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2).
set (e := Zminus _ _). set (e := Zminus _ _).
......
...@@ -164,20 +164,22 @@ now apply IZR_le. ...@@ -164,20 +164,22 @@ now apply IZR_le.
apply sqrt_ge_0. apply sqrt_ge_0.
Qed. Qed.
Definition Fsqrt m1 e1 := Definition Fsqrt (x : float beta) :=
let (m1, e1) := x in
let e' := (Zdigits beta m1 + e1 + 1)%Z in let e' := (Zdigits beta m1 + e1 + 1)%Z in
let e := Zmin (fexp (Z.div2 e')) (Z.div2 e1) in let e := Zmin (fexp (Z.div2 e')) (Z.div2 e1) in
let (m, l) := Fsqrt_core m1 e1 e in let '(m, l) := Fsqrt_core m1 e1 e in
(m, e, l). (m, e, l).
Theorem Fsqrt_correct : Theorem Fsqrt_correct :
forall m1 e1, forall x,
(0 < m1)%Z -> (0 < F2R x)%R ->
let '(m, e, l) := Fsqrt m1 e1 in let '(m, e, l) := Fsqrt x in
(e <= cexp beta fexp (sqrt (F2R (Float beta m1 e1))))%Z /\ (e <= cexp beta fexp (sqrt (F2R x)))%Z /\
inbetween_float beta m e (sqrt (F2R (Float beta m1 e1))) l. inbetween_float beta m e (sqrt (F2R x)) l.
Proof. Proof.
intros m1 e1 Hm1. intros [m1 e1] Hm1.
apply gt_0_F2R in Hm1.
unfold Fsqrt. unfold Fsqrt.
set (e := Zmin _ _). set (e := Zmin _ _).
assert (2 * e <= e1)%Z as He. assert (2 * e <= e1)%Z as He.
......
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