Commit f941b6f5 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Renaming and all that

parent 1d4375f4
......@@ -518,6 +518,21 @@ apply Rgt_not_eq.
apply radix_pos.
Qed.
Lemma rnd_0_or_ge_FLT_z: forall x y e,
generic_format beta (FLT_exp emin prec) x
-> generic_format beta (FLT_exp emin prec) y
-> x = 0%R \/ (bpow e <= Rabs x)%R
-> (x = 0%R -> (y = 0 \/ bpow (e - prec) <= Rabs y)%R)
-> (round beta (FLT_exp emin prec) rnd (x+y) = 0)%R \/
(bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R.
Proof with auto with typeclass_instances.
intros x y e Fx Fy H1 H2; case H1.
intros H3; rewrite H3, Rplus_0_l.
rewrite round_generic...
intros H3.
now apply rnd_0_or_ge_FLT.
Qed.
Lemma rnd_0_or_ge_FLX: forall x y e,
generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y ->
(bpow e <= Rabs x)%R ->
......
......@@ -34,7 +34,7 @@ Notation format := (generic_format beta fexp).
Theorem generic_format_plus :
forall x y,
format x -> format y ->
(Rabs (x + y) < bpow (Zmin (mag beta x) (mag beta y)))%R ->
(Rabs (x + y) <= bpow (Zmin (mag beta x) (mag beta y)))%R ->
format (x + y)%R.
Proof.
intros x y Fx Fy Hxy.
......@@ -45,6 +45,7 @@ destruct (Req_dec x R0) as [Zx|Zx].
now rewrite Zx, Rplus_0_l.
destruct (Req_dec y R0) as [Zy|Zy].
now rewrite Zy, Rplus_0_r.
destruct Hxy as [Hxy|Hxy].
revert Hxy.
destruct (mag beta x) as (ex, Ex). simpl.
specialize (Ex Zx).
......@@ -83,6 +84,12 @@ apply Zmin_r.
apply monotone_exp.
apply Zlt_le_weak.
now apply Zgt_lt.
apply generic_format_abs_inv.
rewrite Hxy.
apply generic_format_bpow.
apply valid_exp.
case (Zmin_spec (mag beta x) (mag beta y)); intros (H1,H2);
rewrite H2; now apply mag_generic_gt.
Qed.
Theorem generic_format_plus_weak :
......@@ -97,16 +104,16 @@ now rewrite Zx, Rplus_0_l.
destruct (Req_dec y R0) as [Zy|Zy].
now rewrite Zy, Rplus_0_r.
apply generic_format_plus ; try assumption.
apply Rle_lt_trans with (1 := Hxy).
apply Rle_trans with (1 := Hxy).
unfold Rmin.
destruct (Rle_dec (Rabs x) (Rabs y)) as [Hxy'|Hxy'].
rewrite Zmin_l.
destruct (mag beta x) as (ex, Hx).
now apply Hx.
apply Rlt_le; now apply Hx.
now apply mag_le_abs.
rewrite Zmin_r.
destruct (mag beta y) as (ex, Hy).
now apply Hy.
apply Rlt_le; now apply Hy.
apply mag_le_abs.
exact Zy.
apply Rlt_le.
......
......@@ -961,7 +961,6 @@ Hypothesis precisionGe3 : (3 <= prec)%Z.
Variable choice : Z -> bool.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis emin_neg: (emin <= 0)%Z.
Hypothesis Even_radix: (Even beta).
Notation format := (generic_format beta (FLT_exp emin prec)).
Notation round_flt :=(round beta (FLT_exp emin prec) (Znearest choice)).
......@@ -1293,17 +1292,17 @@ simpl (Fmult _ _ _).
destruct (round_repr_same_exp beta (FLT_exp emin prec)
ZnearestE (Ztrunc (scaled_mantissa beta (FLT_exp emin prec) a) *
Ztrunc (scaled_mantissa beta (FLT_exp emin prec) b))
(canonic_exp beta (FLT_exp emin prec) a +
canonic_exp beta (FLT_exp emin prec) b)) as (n,Hn).
(cexp beta (FLT_exp emin prec) a +
cexp beta (FLT_exp emin prec) b)) as (n,Hn).
rewrite Hn; clear Hn.
rewrite <- F2R_minus, Fminus_same_exp.
intros K.
eapply Rle_trans with (2:=F2R_ge _ K).
simpl (Fexp _).
apply bpow_le.
unfold canonic_exp, FLT_exp.
destruct (ln_beta beta a) as (ea,Ha).
destruct (ln_beta beta b) as (eb,Hb).
unfold cexp, FLT_exp.
destruct (mag beta a) as (ea,Ha).
destruct (mag beta b) as (eb,Hb).
apply Zle_trans with ((ea-prec)+(eb-prec))%Z.
replace ((ea-prec)+(eb-prec))%Z with ((-1+(ea+eb))+(1-2*prec))%Z by ring.
rewrite <- Z.add_sub_assoc.
......@@ -1471,21 +1470,21 @@ simpl.
apply Zle_trans with (FLT_exp emin prec (emin +3*prec-1)).
unfold FLT_exp.
rewrite Z.max_l; omega.
apply canonic_exp_ge_bpow...
apply cexp_ge_bpow...
apply Rle_trans with (2:=H).
apply bpow_le; omega.
simpl.
apply Zle_trans with (FLT_exp emin prec (emin +2*prec+1)).
unfold FLT_exp.
rewrite Z.max_l; omega.
apply canonic_exp_ge_bpow...
apply cexp_ge_bpow...
apply Rle_trans with (2:=Hy).
apply bpow_le; omega.
simpl.
apply Zle_trans with (FLT_exp emin prec (emin +2*prec-1)).
unfold FLT_exp.
rewrite Z.max_l; omega.
apply canonic_exp_ge_bpow...
apply cexp_ge_bpow...
case (mult_error_FLT_ge a x (emin+4*prec-3)); try assumption.
intros Z; contradict Zu2.
unfold u2, u1; easy.
......
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