proposition: Lemma neq_midpoint_beta_odd_aux1 : 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 - / 2 * ulp beta fexp2 x <= x < midp beta fexp1 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 (Prx1 : 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. } destruct (midpoint_beta_odd_remains rx1 Prx1 ex1 ex2 Hf2f1 Hrx1) as (rx2,(Nnrx2, (Hrx2, Hrx12))). assert (Hx' : rx2 <= x < rx2 + / 2 * bpow ex2). { split. - replace rx2 with (rx2 + / 2 * bpow ex2 - / 2 * bpow ex2) by ring. rewrite <- Hrx12; apply Hx. - rewrite <- Hrx12; apply Hx. } assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2). { unfold round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_eq_reg_r (bpow (- fexp2 (mag x)))); [|now apply Rgt_not_eq, Rlt_gt, bpow_gt_0]. bpow_simplify. rewrite (Znearest_imp _ _ (Zfloor (rx2 * bpow (- ex2)))). - now rewrite Hrx2 at 2; unfold ex2; bpow_simplify. - apply Rabs_lt; split. + apply Rlt_le_trans with 0; [lra|]. apply Rle_0_minus. apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|]. fold ex2; bpow_simplify. now rewrite <- Hrx2. + apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r; fold ex2; bpow_simplify. rewrite <- Hrx2. now apply (Rplus_lt_reg_l rx2); ring_simplify. } rewrite Hr2. assert (Hrx2' : rx1 <= rx2 < rx1 + / 2 * bpow ex1). { split. - apply (Rplus_le_reg_r (/ 2 * bpow ex1)). rewrite Hrx12. apply Rplus_le_compat_l. apply Rmult_le_compat_l; [lra|]. now apply bpow_le. - apply (Rle_lt_trans _ _ _ (proj1 Hx') (proj2 Hx)). } assert (Hrx2r : rx2 = round beta fexp2 Zfloor x). { unfold round, F2R, scaled_mantissa, cexp; simpl. fold ex2; rewrite Hrx2. apply Rmult_eq_compat_r, f_equal. apply eq_sym, Zfloor_imp; split. - apply (Rle_trans _ _ _ (Zfloor_lb _)). now apply Rmult_le_compat_r; [apply bpow_ge_0|]. - apply (Rmult_lt_reg_r (bpow ex2)); [now apply bpow_gt_0|]; bpow_simplify. rewrite plus_IZR, Rmult_plus_distr_r, <- Hrx2. apply (Rlt_le_trans _ _ _ (proj2 Hx')). apply Rplus_le_compat_l, Rmult_le_compat_r; [apply bpow_ge_0|simpl; lra]. } destruct (Rle_or_lt rx2 0) as [Nprx2|Prx2]. { assert (Zrx2 : rx2 = 0); [now apply Rle_antisym|]. rewrite Zrx2, round_0; [|now apply valid_rnd_N]. unfold round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x)))); [|now apply Rgt_not_eq, bpow_gt_0]; rewrite Rmult_0_l; bpow_simplify. apply IZR_eq, eq_sym, Znearest_imp. apply Rabs_lt; simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r. split. - apply Rlt_trans with 0; [lra|]. now apply Rmult_lt_0_compat; [|apply bpow_gt_0]. - apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. rewrite Zrx2, Rplus_0_l in Hx'. apply (Rlt_le_trans _ _ _ (proj2 Hx')), Rmult_le_compat_l; [lra|]. now apply bpow_le. } assert (Hl2 : mag rx2 = mag x :> Z). { now rewrite Hrx2r; apply mag_DN; [|rewrite <- Hrx2r]. } assert (Hr12 : round beta fexp1 (Znearest choice1) rx2 = rx1). { 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. unfold rx1, round, F2R, scaled_mantissa, cexp; simpl. fold ex1; bpow_simplify. apply f_equal, Znearest_imp. apply Rabs_lt; split. - apply Rlt_le_trans with 0; [lra|apply Rle_0_minus]. now apply (Rmult_le_reg_r (bpow ex1)); bpow_simplify; [apply bpow_gt_0|]. - 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_r rx1); ring_simplify. apply (Rlt_le_trans _ _ _ (proj2 Hrx2')), Rplus_le_compat_l. now apply Rmult_le_compat_l; [lra|right]. } rewrite Hr12. unfold rx1, round, F2R, scaled_mantissa, cexp; simpl; fold ex1. apply Rmult_eq_compat_r, f_equal, eq_sym, Znearest_imp, Rabs_lt; split. - apply Rlt_le_trans with 0; [lra|]; apply Rle_0_minus, Zfloor_lb. - apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r; bpow_simplify. change (IZR _ * _) with rx1. now apply (Rplus_lt_reg_l rx1); ring_simplify. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)