proposition: Theorem fexp_round_odd: forall (x:R), (cexp_flt (round beta (FLT_exp emin prec) Zrnd_odd x) = cexp_flt x)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros x. assert (G0:Valid_exp (FLT_exp emin prec)). apply FLT_exp_valid; unfold Prec_gt_0; auto with zarith. case (Req_dec x 0); intros Zx. rewrite Zx, round_0... case (Zle_or_lt (mag beta x) emin). unfold cexp; destruct (mag beta x) as (e,He); simpl. intros H; unfold FLT_exp at 4. rewrite Z.max_r. 2: auto with zarith. apply Z.max_r. assert (G: Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) = bpow beta emin). assert (G1: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta emin)%R). apply abs_round_le_generic... apply generic_format_bpow'... unfold FLT_exp; rewrite Z.max_r; auto with zarith. left; apply Rlt_le_trans with (bpow beta e). now apply He. now apply bpow_le. assert (G2: (0 <= Rabs (round beta (FLT_exp emin prec) Zrnd_odd x))%R). apply Rabs_pos. assert (G3: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <> 0)%R). 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 (_,H0); destruct H0 as [H0|(_,(g,(Hg1,(Hg2,Hg3))))]. apply Rgt_not_eq; rewrite H0. apply Rlt_le_trans with (bpow beta (e-1)). apply bpow_gt_0. now apply He. rewrite Hg1; intros K. contradict Hg3. replace (Fnum g) with 0%Z. easy. case (Z.eq_dec (Fnum g) Z0); intros W; try easy. contradict K. apply Rabs_no_R0. now apply F2R_neq_0. apply Rle_antisym; try assumption. apply Rle_trans with (succ beta (FLT_exp emin prec) 0). right; rewrite succ_0. rewrite ulp_FLT_small; try easy. unfold Prec_gt_0; auto with zarith. rewrite Rabs_R0; apply bpow_gt_0. apply succ_le_lt... apply generic_format_0. apply generic_format_abs; apply generic_format_round... case G2; [easy|intros; now contradict G3]. rewrite <- mag_abs. rewrite G, mag_bpow; auto with zarith. intros H; unfold cexp. now rewrite mag_round_odd. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations