Commit a35bdb83 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Made proofs about Fdiv_core a bit more reusable.

parent 5e6b5904
......@@ -163,7 +163,7 @@ Definition div (x y : float beta) :=
let (my, ey) := y in
if Zeq_bool mx 0 then Float beta 0 0
else
let '(m, e, l) := truncate beta fexp (Fdiv_core beta fexp (Zabs mx) ex (Zabs my) ey) in
let '(m, e, l) := truncate beta fexp (Fdiv beta fexp (Zabs mx) ex (Zabs my) ey) in
let s := xorb (Zlt_bool mx 0) (Zlt_bool my 0) in
Float beta (cond_Zopp s (choice s m l)) e.
......@@ -185,8 +185,8 @@ assert (Hy': (0 < Zabs my)%Z).
contradict Hy.
rewrite Hy.
apply F2R_0.
generalize (Fdiv_core_correct beta fexp (Zabs mx) ex (Zabs my) ey Hx Hy').
destruct Fdiv_core as [[m e] l].
generalize (Fdiv_correct beta fexp (Zabs mx) ex (Zabs my) ey Hx Hy').
destruct Fdiv as [[m e] l].
intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m e l).
destruct truncate as [[m' e'] l'].
......
......@@ -40,122 +40,113 @@ The algorithm performs the following steps:
Complexity is fine as long as p1 <= 2p and p2 <= p.
*)
Definition Fdiv_core m1 e1 m2 e2 :=
let d1 := Zdigits beta m1 in
let d2 := Zdigits beta m2 in
let e' := (d1 + e1 - (d2 + e2))%Z in
let e := Zmin (Zmin (fexp e') (fexp (e' + 1))) (e1 - e2) in
let m := (m1 * Zpower beta (e1 - e2 - e))%Z in
let '(q, r) := Zdiv_eucl m m2 in
(q, e, new_location m2 r loc_Exact).
Lemma mag_div_F2R :
forall m1 e1 m2 e2,
(0 < m1)%Z -> (0 < m2)%Z ->
let e := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in
(e <= mag beta (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) <= e + 1)%Z.
Proof.
intros m1 e1 m2 e2 Hm1 Hm2.
rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq.
rewrite <- (mag_F2R_Zdigits beta m2 e2) by now apply Zgt_not_eq.
apply mag_div.
now apply F2R_neq_0, Zgt_not_eq.
now apply F2R_neq_0, Zgt_not_eq.
Qed.
Definition Fdiv_core m1 e1 m2 e2 e :=
let (m1', m2') :=
if Zle_bool e (e1 - e2)%Z
then (m1 * Zpower beta (e1 - e2 - e), m2)%Z
else (m1, m2 * Zpower beta (e - (e1 - e2)))%Z in
let '(q, r) := Zdiv_eucl m1' m2' in
(q, new_location m2' r loc_Exact).
Theorem Fdiv_core_correct :
forall m1 e1 m2 e2,
forall m1 e1 m2 e2 e,
(0 < m1)%Z -> (0 < m2)%Z ->
let '(m, e, l) := Fdiv_core m1 e1 m2 e2 in
(e <= cexp beta fexp (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)))%Z /\
let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
Proof.
intros m1 e1 m2 e2 Hm1 Hm2.
intros m1 e1 m2 e2 e Hm1 Hm2.
unfold Fdiv_core.
set (d1 := Zdigits beta m1).
set (d2 := Zdigits beta m2).
set (e := (d1 + e1 - (d2 + e2))%Z).
set (e' := Zmin (Zmin (fexp e) (fexp (e + 1))) (e1 - e2)).
set (m' := (m1 * Zpower beta (e1 - e2 - e'))%Z).
assert (bpow (e - 1) < F2R (Float beta m1 e1) / F2R (Float beta m2 e2) < bpow (e + 1))%R as Hd.
{ unfold e, d1, d2.
rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq.
rewrite <- (mag_F2R_Zdigits beta m2 e2) by now apply Zgt_not_eq.
destruct mag as [e1' He1].
destruct mag as [e2' He2].
simpl.
assert (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R as H1.
{ rewrite Rabs_pos_eq in He1.
now apply He1, F2R_neq_0, Zgt_not_eq.
now apply Rlt_le, F2R_gt_0. }
assert (bpow (e2' - 1) <= F2R (Float beta m2 e2) < bpow e2')%R as H2.
{ rewrite Rabs_pos_eq in He2.
now apply He2, F2R_neq_0, Zgt_not_eq.
now apply Rlt_le, F2R_gt_0. }
split.
- replace (e1' - e2' - 1)%Z with (e1' - 1 + -e2')%Z by ring.
rewrite bpow_plus, bpow_opp.
apply Rle_lt_trans with (F2R (Float beta m1 e1) * / bpow e2')%R.
apply Rmult_le_compat_r with (2 := proj1 H1).
apply Rlt_le, Rinv_0_lt_compat, bpow_gt_0.
apply Rmult_lt_compat_l.
now apply F2R_gt_0.
apply Rinv_lt with (2 := proj2 H2).
now apply F2R_gt_0.
- replace (e1' - e2' + 1)%Z with (e1' + -(e2' - 1))%Z by ring.
rewrite bpow_plus, bpow_opp.
apply Rle_lt_trans with (F2R (Float beta m1 e1) * / bpow (e2' - 1))%R.
apply Rmult_le_compat_l.
now apply F2R_ge_0, Zlt_le_weak.
apply Rinv_le with (2 := proj1 H2).
apply bpow_gt_0.
apply Rmult_lt_compat_r with (2 := proj2 H1).
apply Rinv_0_lt_compat, bpow_gt_0. }
assert (F2R (Float beta m1 e1) = F2R (Float beta m' (e' + e2))) as Hf1.
unfold m'.
replace (e1 - e2 - e')%Z with (e1 - (e' + e2))%Z by ring.
apply F2R_change_exp.
cut (e' <= e1 - e2)%Z. clear ; omega.
apply Z.le_min_r.
generalize (Z_div_mod m' m2 (Zlt_gt _ _ Hm2)).
destruct (Zdiv_eucl m' m2) as (q, r).
match goal with |- context [if ?b then ?b1 else ?b2] => set (m12 := if b then b1 else b2) end.
case_eq m12 ; intros m1' m2' Hm.
assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * bpow e)%R /\ (0 < m2')%Z) as [Hf Hm2'].
{ unfold F2R, Zminus ; simpl.
destruct (Zle_bool e (e1 - e2)) eqn:He' ; injection Hm ; intros ; subst.
- split ; try easy.
apply Zle_bool_imp_le in He'.
rewrite mult_IZR, IZR_Zpower by omega.
unfold Zminus ; rewrite 2!bpow_plus, 2!bpow_opp.
field.
repeat split ; try apply Rgt_not_eq, bpow_gt_0.
now apply IZR_neq, Zgt_not_eq.
- apply Z.leb_gt in He'.
split ; cycle 1.
{ apply Z.mul_pos_pos with (1 := Hm2).
apply Zpower_gt_0 ; omega. }
rewrite mult_IZR, IZR_Zpower by omega.
unfold Zminus ; rewrite bpow_plus, bpow_opp, bpow_plus, bpow_opp.
field.
repeat split ; try apply Rgt_not_eq, bpow_gt_0.
now apply IZR_neq, Zgt_not_eq. }
clearbody m12 ; clear Hm Hm1 Hm2.
generalize (Z_div_mod m1' m2' (Z.lt_gt _ _ Hm2')).
destruct (Zdiv_eucl m1' m2') as (q, r).
intros (Hq, Hr).
split.
- apply Zle_trans with (1 := Zle_min_l _ _).
unfold cexp.
assert (e <= mag beta (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) <= e + 1)%Z as [H1 H2].
{ destruct Hd as [Hd1 Hd2].
assert (0 < F2R (Float beta m1 e1) / F2R (Float beta m2 e2))%R as H.
apply Rmult_lt_0_compat.
now apply F2R_gt_0.
now apply Rinv_0_lt_compat, F2R_gt_0.
split.
- apply mag_ge_bpow.
rewrite Rabs_pos_eq ; now apply Rlt_le.
- apply mag_le_bpow.
now apply Rgt_not_eq.
rewrite Rabs_pos_eq.
exact Hd2.
now apply Rlt_le. }
destruct (Zle_lt_or_eq _ _ H1) as [H|H].
+ replace (fexp (mag _ _)) with (fexp (e + 1)).
apply Zle_min_r.
clear -H1 H2 H ; apply f_equal ; omega.
+ replace (fexp (mag _ _)) with (fexp e).
apply Zle_min_l.
clear -H1 H2 H ; apply f_equal ; omega.
- rewrite Hf1.
rewrite Hf.
unfold inbetween_float, F2R. simpl.
rewrite bpow_plus, plus_IZR.
rewrite Hq, plus_IZR, mult_IZR.
replace ((IZR m2 * IZR q + IZR r) * (bpow e' * bpow e2) / (IZR m2 * bpow e2))%R
with ((IZR q + IZR r / IZR m2) * bpow e')%R.
rewrite Hq, 2!plus_IZR, mult_IZR.
apply inbetween_mult_compat.
apply bpow_gt_0.
destruct (Z_lt_le_dec 1 m2) as [Hm2''|Hm2''].
replace 1%R with (IZR m2 * /IZR m2)%R.
apply new_location_correct ; try easy.
apply Rinv_0_lt_compat.
now apply IZR_lt.
now constructor.
apply Rinv_r.
apply Rgt_not_eq.
now apply IZR_lt.
assert (r = 0 /\ m2 = 1)%Z by (clear -Hr Hm2'' ; omega).
rewrite (proj1 H), (proj2 H).
unfold Rdiv.
rewrite Rmult_0_l, Rplus_0_r.
now constructor.
field.
split ; apply Rgt_not_eq.
apply bpow_gt_0.
now apply IZR_lt.
apply bpow_gt_0.
destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2''].
- replace 1%R with (IZR m2' * /IZR m2')%R.
apply new_location_correct ; try easy.
apply Rinv_0_lt_compat.
now apply IZR_lt.
constructor.
field.
now apply IZR_neq, Zgt_not_eq.
field.
now apply IZR_neq, Zgt_not_eq.
- assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; omega).
unfold Rdiv.
rewrite Rmult_1_l, Rplus_0_r, Rinv_1, Rmult_1_r.
now constructor.
Qed.
Definition Fdiv m1 e1 m2 e2 :=
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 '(m, l) := Fdiv_core m1 e1 m2 e2 e in
(m, e, l).
Theorem Fdiv_correct :
forall m1 e1 m2 e2,
(0 < m1)%Z -> (0 < m2)%Z ->
let '(m, e, l) := Fdiv m1 e1 m2 e2 in
(e <= cexp beta fexp (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)))%Z /\
inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
Proof.
intros m1 e1 m2 e2 Hm1 Hm2.
unfold Fdiv.
generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2).
set (e := Zminus _ _).
set (e' := Zmin (Zmin (fexp e) (fexp (e + 1))) (e1 - e2)).
intros [H1 H2].
generalize (Fdiv_core_correct m1 e1 m2 e2 e' Hm1 Hm2).
destruct Fdiv_core as [m' l].
apply conj.
apply Zle_trans with (1 := Zle_min_l _ _).
unfold cexp.
destruct (Zle_lt_or_eq _ _ H1) as [H|H].
- replace (fexp (mag _ _)) with (fexp (e + 1)).
apply Zle_min_r.
clear -H1 H2 H ; apply f_equal ; omega.
- replace (fexp (mag _ _)) with (fexp e).
apply Zle_min_l.
clear -H1 H2 H ; apply f_equal ; omega.
Qed.
End Fcalc_div.
......@@ -1816,23 +1816,23 @@ Lemma Bdiv_correct_aux :
z = binary_overflow m (xorb sx sy).
Proof.
intros m sx mx ex sy my ey.
assert (Fdiv_core_binary (Zpos mx) ex (Zpos my) ey = Fdiv_core radix2 fexp (Zpos mx) ex (Zpos my) ey) as ->.
{ unfold Fdiv_core, Fdiv_core_binary.
rewrite 2!Zdigits2_Zdigits.
rewrite (Z.min_l _ (fexp _)).
change 2%Z with (radix_val radix2).
set (e' := Zmin _ _).
unfold Fdiv_core_binary.
rewrite 2!Zdigits2_Zdigits.
match goal with |- context [Zmin ?m1 ?m2] => set (e' := Zmin m1 m2) end.
generalize (Fdiv_core_correct radix2 (Zpos mx) ex (Zpos my) ey e' eq_refl eq_refl).
unfold Fdiv_core.
rewrite Zle_bool_true by apply Zle_min_r.
match goal with |- context [Zfast_div_eucl ?m _] => set (mx' := m) end.
assert (mx' = Zpos mx * Zpower radix2 (ex - ey - e'))%Z as <-.
{ unfold mx'.
destruct (ex - ey - e')%Z as [|p|p].
rewrite Zmult_1_r.
now rewrite Zfast_div_eucl_correct.
rewrite Z.shiftl_mul_pow2 by easy.
now rewrite Zfast_div_eucl_correct.
now rewrite Zfast_div_eucl_correct.
apply FLT_exp_monotone, Z.le_succ_diag_r. }
refine (_ (Fdiv_core_correct radix2 fexp (Zpos mx) ex (Zpos my) ey _ _)) ; try easy.
destruct (Fdiv_core radix2 fexp (Zpos mx) ex (Zpos my) ey) as ((mz, ez), lz).
intros (Pz, Bz).
simpl.
now rewrite Zmult_1_r.
now rewrite Z.shiftl_mul_pow2.
easy. }
clearbody mx'.
rewrite Zfast_div_eucl_correct.
destruct Zdiv_eucl as [q r].
intros Bz.
assert (xorb sx sy = Rlt_bool (F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) *
/ F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey)) 0) as ->.
{ apply eq_sym.
......@@ -1886,7 +1886,10 @@ apply binary_round_aux_correct'.
now apply F2R_neq_0 ; case sy.
- rewrite <- cexp_abs, Rabs_mult, Rabs_Rinv.
rewrite 2!F2R_cond_Zopp, 2!abs_cond_Ropp, <- Rabs_Rinv.
now rewrite <- Rabs_mult, cexp_abs.
rewrite <- Rabs_mult, cexp_abs.
apply Zle_trans with (1 := Zle_min_l _ _).
apply FLT_exp_monotone.
now apply mag_div_F2R.
now apply F2R_neq_0.
now apply F2R_neq_0 ; case sy.
Qed.
......
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