proposition: Lemma neq_midpoint_beta_odd_aux2 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (fexp2 (mag x) < fexp1 (mag x))%Z -> midp beta fexp1 x < x <= midp beta fexp1 x + / 2 * ulp beta fexp2 x -> round_round_eq beta fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx. unfold midp in Hx. rewrite 2!ulp_neq_0 in Hx; try now apply Rgt_not_eq. unfold round_round_eq. set (ex1 := fexp1 (mag x)). set (ex2 := fexp2 (mag x)). set (rx1 := round beta fexp1 Zfloor x). assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x]. { now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. } assert (Nnrx1 : 0 <= rx1). { rewrite <- (round_0 beta fexp1 Zfloor). now apply round_le; [exact Vfexp1|apply valid_rnd_DN|apply Rlt_le]. } assert (Hrx1 : rx1 = IZR (Zfloor (rx1 * bpow (- ex1))) * bpow ex1). { unfold rx1 at 2; unfold round, F2R, scaled_mantissa, cexp; simpl. unfold ex1; bpow_simplify. now rewrite Zfloor_IZR. } set (rx1c := round beta fexp1 Zceil x). assert (Hf2f1' : (fexp2 (mag x) <= fexp1 (mag x))%Z) by lia. assert (NF1x : ~ generic_format beta fexp1 x). { now intro H; apply NF2x, (generic_inclusion_mag _ fexp1). } assert (Hrx1c : rx1c = rx1 + ulp beta fexp1 x). { now apply round_UP_DN_ulp. } rewrite ulp_neq_0 in Hrx1c; try now apply Rgt_not_eq. destruct (midpoint_beta_odd_remains rx1 Nnrx1 ex1 ex2 Hf2f1' Hrx1) as (rx2,(Nnrx2, (Hrx2, Hrx12))). set (rx2c := rx2 + bpow (fexp2 (mag x))). assert (Hx' : rx2c - / 2 * bpow ex2 < x <= rx2c). { unfold rx2c, cexp; fold ex1; fold ex2; split. - replace (_ - _) with (rx2 + / 2 * bpow ex2) by field. rewrite <- Hrx12; apply Hx. - replace (_ + _) with (rx2 + / 2 * bpow ex2 + / 2 * bpow ex2) by field. rewrite <- Hrx12; apply Hx. } assert (Hrx2c : rx2c = IZR (Zfloor (rx2c * bpow (- ex2))) * bpow ex2). { unfold rx2c, ulp, cexp; fold ex2; rewrite Rmult_plus_distr_r. bpow_simplify. rewrite Hrx2 at 2; bpow_simplify. rewrite <- plus_IZR, Zfloor_IZR, plus_IZR; simpl. now rewrite Rmult_plus_distr_r; apply f_equal2; [|now rewrite Rmult_1_l]. } assert (Prx2c : 0 < rx2c). { now apply Rplus_le_lt_0_compat; [|apply bpow_gt_0]. } assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2c). { unfold round, F2R, scaled_mantissa, cexp; simpl; fold ex2. apply (Rmult_eq_reg_r (bpow (- ex2))); [|now apply Rgt_not_eq, bpow_gt_0]. bpow_simplify. rewrite (Znearest_imp _ _ (Zfloor (rx2c * bpow (- ex2)))). - now apply (Rmult_eq_reg_r (bpow ex2)); bpow_simplify; [apply eq_sym|apply Rgt_not_eq, bpow_gt_0]. - apply Rabs_lt; split. + apply (Rmult_lt_reg_r (bpow ex2)); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r; bpow_simplify. rewrite <- Hrx2c. now apply (Rplus_lt_reg_l rx2c); ring_simplify. + apply Rle_lt_trans with 0; [|lra]. apply Rle_minus. apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|]; bpow_simplify. now rewrite <- Hrx2c. } rewrite Hr2. assert (Hrx2' : rx1c - / 2 * bpow ex1 < rx2c <= rx1c). { split. - rewrite Hrx1c; unfold ulp, cexp; fold ex1. replace (_ - _) with (rx1 + / 2 * bpow ex1) by field. apply (Rlt_le_trans _ _ _ (proj1 Hx) (proj2 Hx')). - apply (Rplus_le_reg_r (- / 2 * bpow ex2)). unfold rx2c, ulp, cexp; fold ex2. replace (_ + _) with (rx2 + / 2 * bpow ex2) by field. rewrite <- Hrx12. rewrite Hrx1c, Rplus_assoc; apply Rplus_le_compat_l. unfold ulp, cexp; fold ex1. apply (Rplus_le_reg_r (- / 2 * bpow ex1)); field_simplify. unfold Rdiv; apply Rmult_le_compat_r; [lra|]. now apply Rle_0_minus, bpow_le. } assert (Hr1 : round beta fexp1 (Znearest choice1) x = rx1c). { unfold rx1c, round, F2R, scaled_mantissa, cexp; simpl; fold ex1. apply Rmult_eq_compat_r, f_equal, Znearest_imp, Rabs_lt; split. - apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r; bpow_simplify. change (IZR _ * _) with rx1c. apply (Rplus_lt_reg_l rx1c); ring_simplify. rewrite Hrx1c; unfold ulp, cexp; fold ex1. now replace (_ - _) with (rx1 + / 2 * bpow ex1) by field. - apply Rlt_le_trans with 0; [|lra]; apply Rlt_minus. apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]; bpow_simplify. assert (H : x <= rx1c); [now apply round_UP_pt|]. destruct H as [H|H]; [exact H|]. exfalso; apply NF1x. unfold generic_format, F2R, scaled_mantissa, cexp; simpl; fold ex1. rewrite Ztrunc_floor; [|now apply Rmult_le_pos;[apply Rlt_le|apply bpow_ge_0]]. rewrite H at 2. unfold rx1c, round, F2R, scaled_mantissa, cexp; simpl; fold ex1. now bpow_simplify; rewrite Zfloor_IZR; rewrite H at 1. } rewrite Hr1. destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1]. { assert (Zrx1 : rx1 = 0); [now apply Rle_antisym|]. rewrite Hrx1c, Zrx1, Rplus_0_l. unfold rx2c, ulp, cexp; fold ex1; fold ex2. replace (_ + _) with (rx2 + / 2 * bpow ex2 + / 2 * bpow ex2) by field. rewrite <- Hrx12, Zrx1, Rplus_0_l. assert (Ph12 : 0 < / 2 * bpow ex1 + / 2 * bpow ex2). { now apply Rplus_lt_0_compat; (apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]). } assert (Hf1 : (fexp1 (mag x) <= mag x)%Z). { apply mag_ge_bpow. rewrite Rabs_right; [|now apply Rle_ge, Rlt_le]. apply Rle_trans with (/ 2 * bpow ex1). - unfold Zminus; rewrite bpow_plus, Rmult_comm. fold ex1; apply Rmult_le_compat_r; [now apply bpow_ge_0|]. rewrite bpow_opp; apply Rinv_le; [lra|]. simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r. now apply IZR_le. - apply Rlt_le. now rewrite <- (Rplus_0_l (_ * _)), <- Zrx1. } assert (Hl1 : mag (/ 2 * bpow ex1 + / 2 * bpow ex2) = mag x :> Z). { apply mag_unique; split. - rewrite Rabs_right; [|now apply Rle_ge, Rlt_le]. apply Rle_trans with x. + destruct (mag x) as (ex, Hex); simpl. now rewrite <- (Rabs_right x); [apply Hex, Rgt_not_eq|apply Rle_ge, Rlt_le]. + rewrite <- (Rplus_0_l (_ * _)), <- Zrx1. apply Hx. - rewrite Rabs_right; [|now apply Rle_ge, Rlt_le]. apply Rlt_le_trans with (bpow ex1); [|now apply bpow_le]. rewrite <- (Rmult_1_l (bpow ex1)) at 2. replace (1 * bpow ex1) with (/ 2 * bpow ex1 + / 2 * bpow ex1) by field. now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt]. } unfold round, F2R, scaled_mantissa, cexp; simpl; rewrite Hl1. fold ex1; apply (Rmult_eq_reg_r (bpow (- ex1))); [|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify. apply IZR_eq, Znearest_imp; simpl. apply Rabs_lt; simpl; split. - apply (Rplus_lt_reg_r 1); replace (- _ + _) with (/ 2) by field. ring_simplify; apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r; bpow_simplify. rewrite <- (Rplus_0_r (_ * _)) at 1; apply Rplus_lt_compat_l. apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. - apply (Rplus_lt_reg_r 1); ring_simplify. apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]. do 2 rewrite Rmult_plus_distr_r; bpow_simplify. now apply Rplus_lt_compat_l, Rmult_lt_compat; [lra|apply bpow_ge_0|lra|apply bpow_lt]. } assert (Hl1 : mag rx1 = mag x :> Z). { now apply mag_DN. } assert (Hl2 : mag rx2c = mag x :> Z). { apply mag_unique; rewrite Rabs_right; [|now apply Rle_ge, Rlt_le]. replace rx2c with (rx1 + (/ 2 * bpow ex1 + / 2 * bpow ex2)); [|now rewrite <- Rplus_assoc, Hrx12; replace (_ + _) with (rx2 + bpow ex2) by field]. split. - rewrite <- Rplus_assoc. apply Rle_trans with x; [|now apply Hx]. apply Rge_le; rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge, Rlt_le]; apply Rle_ge; destruct (mag x) as (ex,Hex); simpl; apply Hex. now apply Rgt_not_eq. - apply Rlt_le_trans with (rx1 + bpow ex1). + apply Rplus_lt_compat_l. rewrite <- (Rmult_1_l (bpow ex1)) at 2. replace (1 * bpow ex1) with (/ 2 * bpow ex1 + / 2 * bpow ex1) by field. now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt]. + unfold ex1; rewrite <- Hl1. fold (cexp beta fexp1 rx1); rewrite <- ulp_neq_0; try now apply Rgt_not_eq. apply id_p_ulp_le_bpow; [exact Prx1| |]. * now apply generic_format_round; [|apply valid_rnd_DN]. * destruct (mag rx1) as (erx1, Herx1); simpl. rewrite <- (Rabs_right rx1) at 1; [|now apply Rle_ge, Rlt_le]. now apply Herx1, Rgt_not_eq. } unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Hl2; fold ex1. apply (Rmult_eq_reg_r (bpow (- ex1))); [|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify. rewrite Hrx1c, Rmult_plus_distr_r. unfold rx1, round, F2R, scaled_mantissa, ulp, cexp; simpl; fold ex1. bpow_simplify. rewrite <- plus_IZR; apply f_equal, Znearest_imp. apply Rabs_lt; split. - rewrite plus_IZR; simpl; apply (Rplus_lt_reg_r 1); ring_simplify. replace (- _ + _) with (/ 2) by field. apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r; bpow_simplify. change (IZR _ * _) with rx1. apply (Rplus_lt_reg_l rx1); ring_simplify. apply Rlt_le_trans with x; [apply Hx|apply Hx']. - apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r; bpow_simplify. rewrite plus_IZR, Rmult_plus_distr_r; simpl; rewrite Rmult_1_l. change (IZR _ * _ + _) with (rx1 + bpow (cexp beta fexp1 x)). rewrite <- Hrx1c; lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)