Commit 38e7d780 authored by BOLDO Sylvie's avatar BOLDO Sylvie

WIP discri

parent e70bebc3
......@@ -233,4 +233,63 @@ apply Ex.
apply Ey.
Qed.
Theorem mult_error_FLT_ge_bpow :
forall x y e,
format x -> format y ->
(emin <= e + prec)%Z ->
(bpow (e+2*prec-1) <= Rabs (x * y))%R ->
(round beta (FLT_exp emin prec) rnd (x * y) - (x * y) <> 0)%R ->
(bpow e <= Rabs (round beta (FLT_exp emin prec) rnd (x * y) - (x * y)))%R.
Proof with auto with typeclass_instances.
intros x y e.
set (f := (round beta (FLT_exp emin prec) rnd (x * y))).
intros Hx Hy He Hxy Hr0.
destruct (Req_dec (x * y) 0) as [Hxy'|Hxy'].
contradict Hr0.
unfold f.
rewrite Hxy'.
rewrite round_0...
ring.
assert (Y:(bpow (emin + prec - 1) <= Rabs (x * y))%R).
apply Rle_trans with (2:=Hxy); apply bpow_le.
omega.
(* *)
destruct (mult_error_FLX_aux beta prec rnd x y) as ((m,i),(H1,(H2,H3))).
now apply generic_format_FLX_FLT with emin.
now apply generic_format_FLX_FLT with emin.
rewrite <- (round_FLT_FLX beta emin); assumption.
rewrite <- (round_FLT_FLX beta emin) in H1; try assumption.
fold f in H1.
rewrite <- H1.
rewrite <- F2R_abs.
apply Rle_trans with (bpow i).
apply bpow_le; simpl in H3; rewrite H3.
unfold Generic_fmt.cexp, FLX_exp.
destruct (mag beta x) as (ex,Hex).
destruct (mag beta y) as (ey,Hey); simpl.
assert (e+2*prec-1 < ex+ey)%Z; try omega.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=Hxy).
rewrite Rabs_mult, bpow_plus.
apply Rmult_lt_compat.
apply Rabs_pos.
apply Rabs_pos.
apply Hex.
contradict Hxy'; rewrite Hxy'; ring.
apply Hey.
contradict Hxy'; rewrite Hxy'; ring.
apply bpow_le_F2R.
apply gt_0_F2R with beta i.
fold (Fabs beta (Float beta m i)).
rewrite F2R_abs, H1.
now apply Rabs_pos_lt.
Qed.
End Fprop_mult_error_FLT.
......@@ -754,14 +754,52 @@ rewrite inj_abs; omega.
Qed.
Lemma Fulp_ulp: forall f, Fbounded b f ->
Lemma Fulp_ulp_aux: forall f, Fcanonic beta b f ->
Fulp b beta (Z.abs_nat p) f
= ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).
Proof.
Admitted.
intros f H.
case (Req_dec (FtoR beta f) 0); intros Zf.
(* f = 0 *)
rewrite Zf, ulp_FLT_small.
2: unfold Prec_gt_0; omega.
2: rewrite Rabs_R0; apply bpow_gt_0.
rewrite Fulp_zero.
apply sym_eq, bpow_powerRZ.
apply is_Fzero_rep2 with beta; try assumption.
apply radix_gt_1.
(* f <> 0 *)
rewrite ulp_neq_0; try assumption.
replace (FtoR beta f) with (F2R (Float beta (Float.Fnum f) (Float.Fexp f))).
rewrite <- pff_canonic_is_canonic; try assumption.
simpl; rewrite CanonicFulp; try assumption.
unfold FtoR; simpl; rewrite bpow_powerRZ; ring.
apply radix_gt_1.
replace 1 with (Z.abs_nat 1) by easy.
apply Zabs_nat_lt; omega.
unfold F2R, FtoR; simpl.
rewrite bpow_powerRZ; easy.
Qed.
Lemma Fulp_ulp: forall f, Fbounded b f ->
Fulp b beta (Z.abs_nat p) f
= ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).
intros f H.
assert (Y1: (1 < beta)%Z) by apply radix_gt_1.
assert (Y2:Z.abs_nat p <> 0).
apply notEqLt.
replace 0 with (Z.abs_nat 0) by easy.
apply Zabs_nat_lt; omega.
rewrite FulpComp with (q:=Fnormalize beta b (Z.abs_nat p) f); try assumption.
rewrite <- FnormalizeCorrect with beta b (Z.abs_nat p) f; try assumption.
apply Fulp_ulp_aux.
apply FnormalizeCanonic; try assumption.
replace 1 with (Z.abs_nat 1) by easy.
apply Zabs_nat_lt; omega.
apply FnormalizeBounded; try assumption.
apply sym_eq, FnormalizeCorrect; try assumption.
Qed.
End Equiv.
......
This diff is collapsed.
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