proposition: Theorem DN_UP_parity_generic_pos : DN_UP_parity_pos_prop.
proof: Proof. Proof with auto with typeclass_instances. intros x xd xu H0x Hfx Hd Hu Hxd Hxu. destruct (mag beta x) as (ex, Hexa). specialize (Hexa (Rgt_not_eq _ _ H0x)). generalize Hexa. intros Hex. rewrite (Rabs_pos_eq _ (Rlt_le _ _ H0x)) in Hex. destruct (Zle_or_lt ex (fexp ex)) as [Hxe|Hxe]. assert (Hd3 : Fnum xd = Z0). apply eq_0_F2R with beta (Fexp xd). change (F2R xd = R0). rewrite Hxd. apply round_DN_small_pos with (1 := Hex) (2 := Hxe). assert (Hu3 : xu = Float beta (1 * Zpower beta (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))). apply canonical_unique with (1 := Hu). apply (f_equal fexp). rewrite <- F2R_change_exp. now rewrite F2R_bpow, mag_bpow. now apply valid_exp. rewrite <- F2R_change_exp. rewrite F2R_bpow. apply sym_eq. rewrite Hxu. apply sym_eq. apply round_UP_small_pos with (1 := Hex) (2 := Hxe). now apply valid_exp. rewrite Hd3, Hu3. rewrite Zmult_1_l. simpl. destruct exists_NE_ as [H|H]. apply Zeven_Zpower_odd with (2 := H). apply Zle_minus_le_0. now apply valid_exp. rewrite (proj2 (H ex)). now rewrite Zminus_diag. exact Hxe. assert (Hd4: (bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R). rewrite Rabs_pos_eq. rewrite Hxd. split. apply (round_DN_pt beta fexp x). apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. lia. apply Hex. apply Rle_lt_trans with (2 := proj2 Hex). apply (round_DN_pt beta fexp x). rewrite Hxd. apply (round_DN_pt beta fexp x). apply generic_format_0. now apply Rlt_le. assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp. assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R). rewrite Hxu, Hxd. now apply round_UP_DN_ulp. destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2]. elim (Rlt_not_le _ _ Hu2). rewrite Hxu. apply round_bounded_large_pos... assert (Hu3: xu = Float beta (1 * Zpower beta (ex - fexp (ex + 1))) (fexp (ex + 1))). apply canonical_unique with (1 := Hu). apply (f_equal fexp). rewrite <- F2R_change_exp. now rewrite F2R_bpow, mag_bpow. now apply valid_exp. rewrite <- Hu2. apply sym_eq. rewrite <- F2R_change_exp. apply F2R_bpow. exact Hxe2. assert (Hd3: xd = Float beta (Zpower beta (ex - fexp ex) - 1) (fexp ex)). assert (H: F2R xd = F2R (Float beta (Zpower beta (ex - fexp ex) - 1) (fexp ex))). unfold F2R. simpl. rewrite minus_IZR. unfold Rminus. rewrite Rmult_plus_distr_r. rewrite IZR_Zpower, <- bpow_plus. ring_simplify (ex - fexp ex + fexp ex)%Z. rewrite Hu2, Hud. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. unfold cexp. rewrite mag_unique with beta x ex. unfold F2R. simpl. ring. rewrite Rabs_pos_eq. exact Hex. now apply Rlt_le. apply Zle_minus_le_0. now apply Zlt_le_weak. apply canonical_unique with (1 := Hd) (3 := H). apply (f_equal fexp). rewrite <- H. apply sym_eq. now apply mag_unique. rewrite Hd3, Hu3. unfold Fnum. rewrite Z.even_mul. simpl. unfold Zminus at 2. rewrite Z.even_add. rewrite eqb_sym. simpl. fold (negb (Z.even (beta ^ (ex - fexp ex)))). rewrite Bool.negb_involutive. rewrite (Z.even_pow beta (ex - fexp ex)) by lia. destruct exists_NE_. rewrite H. apply Zeven_Zpower_odd with (2 := H). now apply Zle_minus_le_0. apply Z.even_pow. specialize (H ex). lia. revert Hud. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. unfold F2R. rewrite Hd, Hu. unfold cexp. rewrite mag_unique with beta (F2R xu) ex. rewrite mag_unique with (1 := Hd4). rewrite mag_unique with (1 := Hexa). intros H. replace (Fnum xu) with (Fnum xd + 1)%Z. rewrite Z.even_add. now apply eqb_sym. apply sym_eq. apply eq_IZR. rewrite plus_IZR. apply Rmult_eq_reg_r with (bpow (fexp ex)). rewrite H. simpl. ring. apply Rgt_not_eq. apply bpow_gt_0. rewrite Rabs_pos_eq. split. apply Rle_trans with (1 := proj1 Hex). rewrite Hxu. apply (round_UP_pt beta fexp x). exact Hu2. apply Rlt_le. apply Rlt_le_trans with (1 := H0x). rewrite Hxu. apply (round_UP_pt beta fexp x). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp