proposition: Theorem round_odd_pt : forall x, Rnd_odd_pt x (round beta fexp Zrnd_odd x).
proof: Proof. Proof with auto with typeclass_instances. cut (forall x : R, (0 < x)%R -> Rnd_odd_pt x (round beta fexp Zrnd_odd x)). intros H x; case (Rle_or_lt 0 x). intros H1; destruct H1. now apply H. rewrite <- H0. rewrite round_0... split. apply generic_format_0. now left. intros Hx; apply Rnd_odd_pt_opp_inv. rewrite <- round_odd_opp. apply H. auto with real. intros x Hxp. generalize (generic_format_round beta fexp Zrnd_odd x). set (o:=round beta fexp Zrnd_odd x). intros Ho. split. assumption. case (Req_dec o x); intros Hx. now left. right. assert (o=round beta fexp Zfloor x \/ o=round beta fexp Zceil x). unfold o, round, F2R;simpl. case (Zrnd_DN_or_UP Zrnd_odd (scaled_mantissa beta fexp x))... intros H; rewrite H; now left. intros H; rewrite H; now right. split. destruct H; rewrite H. left; apply round_DN_pt... right; apply round_UP_pt... unfold o, Zrnd_odd, round. case (Req_EM_T (scaled_mantissa beta fexp x) (IZR (Zfloor (scaled_mantissa beta fexp x)))). intros T. absurd (o=x); trivial. apply round_generic... unfold generic_format, F2R; simpl. rewrite <- (scaled_mantissa_mult_bpow beta fexp) at 1. apply f_equal2; trivial; rewrite T at 1. apply f_equal, sym_eq, Ztrunc_floor. apply Rmult_le_pos. now left. apply bpow_ge_0. intros L. case_eq (Z.even (Zfloor (scaled_mantissa beta fexp x))). generalize (generic_format_round beta fexp Zceil x). unfold generic_format. set (f:=round beta fexp Zceil x). set (ef := cexp f). set (mf := Ztrunc (scaled_mantissa beta fexp f)). exists (Float beta mf ef). unfold canonical. rewrite <- H0. repeat split; try assumption. apply trans_eq with (negb (Z.even (Zfloor (scaled_mantissa beta fexp x)))). 2: rewrite H1; reflexivity. apply trans_eq with (negb (Z.even (Fnum (Float beta (Zfloor (scaled_mantissa beta fexp x)) (cexp x))))). 2: reflexivity. case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)). rewrite <- round_0 with beta fexp Zfloor... apply round_le... now left. intros Y. generalize (DN_UP_parity_generic beta fexp)... unfold DN_UP_parity_prop. intros T; apply T with x; clear T. unfold generic_format. rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1. unfold F2R; simpl. apply Rmult_neq_compat_r. apply Rgt_not_eq, bpow_gt_0. rewrite Ztrunc_floor. assumption. apply Rmult_le_pos. now left. apply bpow_ge_0. unfold canonical. simpl. apply sym_eq, cexp_DN... unfold canonical. rewrite <- H0; reflexivity. reflexivity. apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)). reflexivity. apply round_generic... intros Y. replace (Fnum {| Fnum := Zfloor (scaled_mantissa beta fexp x); Fexp := cexp x |}) with (Fnum (Float beta 0 (fexp (mag beta 0)))). generalize (DN_UP_parity_generic beta fexp)... unfold DN_UP_parity_prop. intros T; apply T with x; clear T. unfold generic_format. rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1. unfold F2R; simpl. apply Rmult_neq_compat_r. apply Rgt_not_eq, bpow_gt_0. rewrite Ztrunc_floor. assumption. apply Rmult_le_pos. now left. apply bpow_ge_0. apply canonical_0. unfold canonical. rewrite <- H0; reflexivity. rewrite <- Y; unfold F2R; simpl; ring. apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)). reflexivity. apply round_generic... simpl. apply eq_IZR, Rmult_eq_reg_r with (bpow (cexp x)). unfold round, F2R in Y; simpl in Y; rewrite <- Y. simpl; ring. apply Rgt_not_eq, bpow_gt_0. intros Y. case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)). rewrite <- round_0 with beta fexp Zfloor... apply round_le... now left. intros Hrx. set (ef := cexp x). set (mf := Zfloor (scaled_mantissa beta fexp x)). exists (Float beta mf ef). unfold canonical. repeat split; try assumption. simpl. apply trans_eq with (cexp (round beta fexp Zfloor x )). apply sym_eq, cexp_DN... reflexivity. intros Hrx; contradict Y. replace (Zfloor (scaled_mantissa beta fexp x)) with 0%Z. simpl; discriminate. apply eq_IZR, Rmult_eq_reg_r with (bpow (cexp x)). unfold round, F2R in Hrx; simpl in Hrx; rewrite <- Hrx. simpl; ring. apply Rgt_not_eq, bpow_gt_0. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations