proposition: Lemma midpoint_beta_odd_remains : forall x, 0 <= x -> forall (ex1 ex2 : Z), (ex2 <= ex1)%Z -> x = IZR (Zfloor (x * bpow (- ex1))) * bpow ex1 -> exists x', 0 <= x' /\ x' = IZR (Zfloor (x' * bpow (- ex2))) * bpow ex2 /\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
proof: Proof. intros x Px ex1 ex2 Hf2 Hx. set (x1 := x + bpow ex1). assert (Px1 : 0 < x1). { apply (Rle_lt_trans _ _ _ Px). rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l, bpow_gt_0. } destruct (midpoint_beta_odd_remains_pos x1 Px1 ex1 ex2 Hf2) as (x',(Hx'1,(Hx'2,(Hx'3,Hx'4)))). { unfold x1 at 2. rewrite Rmult_plus_distr_r, Hx; bpow_simplify. rewrite <- plus_IZR. now rewrite Zfloor_IZR, plus_IZR, Rmult_plus_distr_r, Rmult_1_l, <- Hx. } assert (Hx' : x' = x1 + / 2 * bpow ex1 - / 2 * bpow ex2). { rewrite Hx'4; ring. } exists (x' - bpow ex1); split; [|split]. - rewrite Hx'; unfold x1; ring_simplify. replace (_ - _) with (x + (/ 2 * (bpow ex1 - bpow ex2))) by ring. apply Rplus_le_le_0_compat; [exact Px|]; apply Rmult_le_pos; [lra|]. now apply Rle_0_minus, bpow_le. - rewrite Rmult_minus_distr_r; rewrite Hx'3 at 2; bpow_simplify. rewrite <- (IZR_Zpower beta (ex1 - ex2)); [|now apply Zle_minus_le_0]. rewrite <- minus_IZR, Zfloor_IZR, minus_IZR. rewrite (IZR_Zpower beta (ex1 - ex2)); [|now apply Zle_minus_le_0]. rewrite Rmult_minus_distr_r; bpow_simplify. now rewrite Hx'3 at 1. - rewrite Hx'; unfold x1; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)