Commit f5709f0c authored by BOLDO Sylvie's avatar BOLDO Sylvie
Browse files

Clean before release

parent b6611aaf
......@@ -1037,266 +1037,3 @@ Qed.
End Odd_prop.
(*
Section Odd_one_prec.
Variable beta : radix.
Hypothesis Even_beta: Zeven (radix_val beta)=true.
Variable choice:Z->bool.
Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis Hprec: (1 < prec)%Z.
Notation fexp:=(FLT_exp emin prec).
Notation format := (generic_format beta (FLT_exp emin prec)).
Notation cexp := (canonic_exp beta (FLT_exp emin prec)).
Theorem fexpe_add_odd: forall x y e, format x ->
Rnd_odd_pt beta fexp y e ->
(exists m:Z, y = F2R (Float beta m emin)) \/ (bpow beta (emin+prec-1)%Z <= Rabs y)%R ->
((Z2R beta*Z2R beta+1)*Rabs e <= Rabs x)%R ->
exists C:Z,
(2 <= C)%Z /\
Rnd_odd_pt beta (FLT_exp (emin-C) (prec+C)) (x + y) (x+e).
Proof with auto with typeclass_instances.
intros x y e Fx He Hy Hex.
(* . *)
case (Req_dec y 0); intros Hy'.
exists 2%Z; split.
omega.
rewrite Hy'.
replace e with 0%R.
rewrite Rplus_0_r.
split; [idtac|now left].
apply generic_format_fexpe_fexp with fexp...
intros z; unfold FLT_exp.
rewrite <- Z.sub_max_distr_r.
apply Z.max_le_compat; omega.
apply sym_eq, Rnd_odd_pt_unicity with (3:=He)...
rewrite Hy'; split.
apply generic_format_0.
now left.
(* *)
pose (C:=(ln_beta beta (x+e) - ln_beta beta e)%Z).
pose (fexpe := (FLT_exp (emin - C) (prec + C))).
exists C.
(* . *)
assert (U:(e <> 0)%R).
destruct He as (V1,V2); case V2.
intros V; now rewrite V.
intros (G1,(g,(G2,(G3,G4)))).
rewrite G2; intros K.
contradict G4.
rewrite F2R_eq_0_reg with beta (Fnum g) (Fexp g).
now simpl.
rewrite <- K; reflexivity.
(* . *)
assert (R:(2 <= C)%Z).
unfold C; apply Zplus_le_reg_l with (ln_beta beta e).
ring_simplify.
rewrite <- ln_beta_mult_bpow; try assumption.
apply ln_beta_le_abs.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rgt_not_eq, bpow_gt_0.
pattern e at 2; replace e with (--e)%R by ring.
apply Rle_trans with (2:=Rabs_triang_inv _ _).
rewrite Rabs_Ropp.
apply Rplus_le_reg_l with (Rabs e); ring_simplify.
apply Rle_trans with (2:=Hex).
rewrite Rabs_mult.
rewrite (Rabs_right (bpow beta 2)).
simpl; right; unfold Z.pow_pos; simpl.
rewrite Z2R_mult, Zmult_1_r; ring.
apply Rle_ge, bpow_ge_0.
(* . *)
assert (T:(canonic_exp beta fexp e <= canonic_exp beta fexp x)%Z).
(* apply monotone_exp...
apply ln_beta_le_abs.
assumption.
apply abs_round_le_generic...
now apply generic_format_abs.
apply Rle_trans with (2:=H).*)
admit. (* grmbl <= ou < ou +2 <= ?? *)
(*betw_eq_DN
pred_plus_ulp*)
(*apply Rplus_le_reg_l with (-Rabs y)%R; ring_simplify.
apply Rmult_le_pos; try apply Rabs_pos.
apply Rmult_le_pos; auto with real.
replace 0%R with (Z2R 0) by reflexivity; left.
apply Z2R_lt; apply radix_gt_0.
replace 0%R with (Z2R 0) by reflexivity; left.
rewrite Rmult_1_r; apply Z2R_lt; apply radix_gt_0.*)
(* . *)
assert (K:(generic_format beta fexpe (x+e))).
eapply generic_format_F2R'.
rewrite Fx, (proj1 He), <- F2R_plus.
easy.
intros M.
apply Zle_trans with (canonic_exp beta fexp e).
unfold canonic_exp, fexpe.
unfold FLT_exp.
replace (ln_beta beta (x + e) - (prec + C))%Z with (ln_beta beta e - prec)%Z.
apply Z.max_le_compat_l.
omega.
unfold C; ring.
rewrite Fexp_Fplus; simpl.
rewrite Z.min_r; try assumption; omega.
(* . *)
assert (Valid_exp fexpe).
apply FLT_exp_valid.
unfold Prec_gt_0; omega.
assert (Exists_NE beta fexpe).
apply exists_NE_FLT.
right; omega.
assert (Monotone_exp fexpe).
apply FLT_exp_monotone.
(* *)
fold fexpe.
split; trivial.
split; try exact K.
case (Req_dec e y); intros P.
left; now rewrite P.
right.
elim He; intros _ L; destruct L as [M|(M1,M2)].
now contradict M.
split.
(* *)
destruct M1 as [M1|M1].
(* . *)
left.
rewrite betw_eq_DN with beta fexpe (x+y)%R (x+e)%R...
apply round_DN_pt.
exact H.
admit. (* 0 < x+e *)
split.
apply Rplus_le_compat_l.
apply M1.
rewrite Rplus_assoc; apply Rplus_lt_compat_l.
apply Rplus_lt_reg_l with (-e)%R.
apply Rle_lt_trans with (1:=RRle_abs _).
replace e with (round beta fexp Zfloor y).
rewrite <- Rabs_Ropp.
replace (-(-round beta fexp Zfloor y + y))%R with
(round beta fexp Zfloor y - y)%R by ring.
apply Rlt_le_trans with (ulp beta fexp (round beta fexp Zfloor y)).
apply ulp_error_f...
admit. (* ok *)
ring_simplify.
apply bpow_le.
(*
replace (round beta fexp Zfloor y) with e.
unfold fexpe, canonic_exp, FLT_exp.
replace (ln_beta beta (x + e) - (prec + C))%Z with (ln_beta beta e - prec)%Z.
apply Z.max_le_compat_l.
omega.
toto.*)
admit.
admit.
(*
split; trivial.
split.
apply Rplus_le_compat_l.
apply M1.
intros g Fg Hg.
apply Rplus_le_reg_l with (-x)%R; ring_simplify.
apply M1.
admit. (* ?????????????*)
admit. (* ok Hg *)
*)
(* . *)
admit.
(* *)
destruct M2 as (g, (L1,(L2,L3))).
exists (Float beta (Ztrunc (scaled_mantissa beta fexp x)*beta^(cexp x -cexp e)+Fnum g) (Fexp g)).
assert (B: (x+e =
F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x)*beta^(cexp x -cexp e)
+Fnum g) (Fexp g)))%R).
(* . *)
unfold F2R; simpl.
rewrite Z2R_plus, Z2R_mult.
rewrite Rmult_plus_distr_r.
fold (F2R g); rewrite <- L1.
apply f_equal2; trivial.
rewrite Z2R_Zpower.
2: omega.
rewrite Rmult_assoc, <- bpow_plus.
rewrite Fx at 1; simpl.
unfold F2R; apply f_equal.
simpl; apply f_equal.
rewrite L2, <- L1; ring.
split; trivial.
split.
(* . *)
unfold canonic; simpl.
rewrite <- B, L2, <- L1.
unfold canonic_exp, fexpe, FLT_exp.
replace (ln_beta beta (x + e) - (prec + C))%Z with
(ln_beta beta e -prec)%Z.
2: unfold C; ring.
admit. (* euh... *)
simpl.
rewrite Zeven_plus, L3.
rewrite Zeven_mult.
rewrite Zeven_Zpower.
rewrite Even_beta.
rewrite Bool.orb_true_intro.
reflexivity.
now right.
admit.
Qed.
Theorem round_add_odd: forall x y:R,
generic_format beta fexp x ->
(exists m:Z, y = F2R (Float beta m emin)) \/ (bpow beta (emin+prec-1)%Z <= Rabs y)%R ->
((Z2R beta*Z2R beta+1)*Rabs (round beta fexp Zrnd_odd y) <= Rabs x)%R ->
round beta fexp (Znearest choice) (x+(round beta fexp Zrnd_odd y))
= round beta fexp (Znearest choice) (x+y).
Proof with auto with typeclass_instances.
intros x y Fx M Hex.
destruct (fexpe_add_odd x y (round beta fexp Zrnd_odd y)) as (C,(K1,K2)); try assumption.
apply round_odd_pt...
assert (Valid_exp (FLT_exp (emin - C) (prec + C))).
apply FLT_exp_valid; unfold Prec_gt_0; omega.
assert (Exists_NE beta (FLT_exp (emin - C) (prec + C))).
apply exists_NE_FLT; right; omega.
rewrite <- round_odd_prop with (fexpe :=(FLT_exp (emin-C) (prec+C))) (x:=(x+y)%R)...
apply f_equal.
apply Rnd_odd_pt_unicity with beta (FLT_exp (emin-C) (prec+C)) (x+y)%R...
apply round_odd_pt...
unfold FLT_exp; intros e.
rewrite <- Z.sub_max_distr_r.
apply Z.max_le_compat; omega.
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