Still WIP renaming

src/Appli/Fappli_rnd_odd.v

@@ -935,7 +935,7 @@ case K2; clear K2; intros K2.
 case (Rle_or_lt  x m); intros Y;[destruct Y|idtac].
 (* . *)
 apply trans_eq with (F2R d).
-apply betw_eq_N_DN' with (F2R u)...
+apply round_N_eq_DN_pt with (F2R u)...
 apply DN_odd_d_aux; split; try left; assumption.
 apply UP_odd_d_aux; split; try left; assumption.
 assert (o <= (F2R d + F2R u) / 2)%R.
@@ -946,7 +946,7 @@ destruct H1; trivial.
 apply P.
 now apply Rlt_not_eq.
 trivial.
-apply sym_eq, betw_eq_N_DN' with (F2R u)...
+apply sym_eq, round_N_eq_DN_pt with (F2R u)...
 (* . *)
 replace o with x.
 reflexivity.
@@ -954,7 +954,7 @@ apply sym_eq, round_generic...
 rewrite H0; apply Fm.
 (* . *)
 apply trans_eq with (F2R u).
-apply betw_eq_N_UP' with (F2R d)...
+apply round_N_eq_UP_pt with (F2R d)...
 apply DN_odd_d_aux; split; try left; assumption.
 apply UP_odd_d_aux; split; try left; assumption.
 assert ((F2R d + F2R u) / 2 <= o)%R.
@@ -965,7 +965,7 @@ destruct H0; trivial.
 apply P.
 now apply Rgt_not_eq.
 rewrite <- H0; trivial.
-apply sym_eq, betw_eq_N_UP' with (F2R d)...
+apply sym_eq, round_N_eq_UP_pt with (F2R d)...
 Qed.
 
 
@@ -1037,3 +1037,266 @@ 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.
+
+
+*)
+
+
+