proposition: Theorem mag_round_odd: forall (x:R), (emin < mag beta x)%Z -> (mag_val beta _ (mag beta (round beta (FLT_exp emin prec) Zrnd_odd x)) = mag_val beta x (mag beta x))%Z.
proof: Proof. Proof with auto with typeclass_instances. intros x. assert (T:Prec_gt_0 prec). unfold Prec_gt_0; auto with zarith. case (Req_dec x 0); intros Zx. intros _; rewrite Zx, round_0... destruct (mag beta x) as (e,He); simpl; intros H. apply mag_unique; split. apply abs_round_ge_generic... apply generic_format_FLT_bpow... now apply Z.lt_le_pred. now apply He. assert (V: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta e)%R). apply abs_round_le_generic... apply generic_format_FLT_bpow... now apply Zlt_le_weak. left; now apply He. case V; try easy; intros K. assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x (round beta (FLT_exp emin prec) Zrnd_odd x)). apply round_odd_pt... destruct H0 as (_,HH); destruct HH as [H0|(H0,(g,(Hg1,(Hg2,Hg3))))]. absurd (Rabs x < bpow beta e)%R. apply Rle_not_lt; right. now rewrite <- H0,K. now apply He. pose (gg:=Float beta (Zpower beta (e-FLT_exp emin prec (e+1))) (FLT_exp emin prec (e+1))). assert (Y1: F2R gg = bpow beta e). unfold F2R; simpl. rewrite IZR_Zpower. rewrite <- bpow_plus. f_equal; ring. assert (FLT_exp emin prec (e+1) <= e)%Z; [idtac|auto with zarith]. unfold FLT_exp. apply Z.max_case_strong; auto with zarith. assert (Y2: canonical beta (FLT_exp emin prec) gg). unfold canonical; rewrite Y1; unfold gg; simpl. unfold cexp; now rewrite mag_bpow. assert (Y3: Fnum gg = Z.abs (Fnum g)). apply trans_eq with (Fnum (Fabs g)). 2: destruct g; unfold Fabs; now simpl. f_equal. apply canonical_unique with (FLT_exp emin prec); try assumption. destruct g; unfold Fabs; apply canonical_abs; easy. now rewrite Y1, F2R_abs, <- Hg1,K. assert (Y4: Z.even (Fnum gg) = true). unfold gg; simpl. rewrite Z.even_pow; try assumption. assert (FLT_exp emin prec (e+1) < e)%Z; [idtac|auto with zarith]. unfold FLT_exp. apply Z.max_case_strong; auto with zarith. absurd (true = false). discriminate. rewrite <- Hg3. rewrite <- Zeven_abs. now rewrite <- Y3. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations