proposition: Lemma midpoint_beta_odd_remains_pos : forall x, 0 < x -> forall (ex1 ex2 : Z), (ex2 <= ex1)%Z -> x = IZR (Zfloor (x * bpow (- ex1))) * bpow ex1 -> exists x', 0 < x' /\ (mag x' = mag x :> Z) /\ x' = IZR (Zfloor (x' * bpow (- ex2))) * bpow ex2 /\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
proof: Proof. intros x Px ex1 ex2 Hf2. set (z := (ex1 - ex2)%Z). assert (Hz : Z_of_nat (Z.abs_nat z) = z). { rewrite Zabs2Nat.id_abs. rewrite <- cond_Zopp_Zlt_bool; unfold cond_Zopp. assert (H : (z <? 0)%Z = false); [|now rewrite H]. apply Zlt_bool_false; unfold z; lia. } revert Hz. generalize (Z.abs_nat z); intro n. unfold z; clear z; revert ex1 ex2 Hf2. induction n. - simpl. intros ex1 ex2 _ Hf1 Fx. exists x. assert (H : ex2 = ex1) by lia. split; [|split; [|split]]. + exact Px. + reflexivity. + revert Fx; unfold generic_format, F2R, scaled_mantissa, cexp; simpl. now rewrite H. + now unfold ulp, cexp; rewrite H. - intros ex1 ex2 Hf2 HSn Fx. destruct Obeta as (nb,Hb). assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } assert (Nnnb : (1 <= nb)%Z) by lia. assert (Hf1 : (ex1 = ex2 + Z.of_nat n + 1 :> Z)%Z); [|clear HSn]. { rewrite <- Zplus_assoc. replace (_ + 1)%Z with (Z.of_nat (S n)); [lia|]. simpl. now rewrite Zpos_P_of_succ_nat. } assert (Hf2' : (ex2 + 1 <= ex1)%Z). { rewrite Hf1. rewrite <- Zplus_assoc. apply Zplus_le_compat_l. rewrite <- (Zplus_0_l 1) at 1; apply Zplus_le_compat_r. apply Zle_0_nat. } assert (Hd1 : Z.of_nat n = (ex1 - (ex2 + 1))%Z); [now rewrite Hf1; ring|]. set (ex2' := (ex2 + 1)%Z). destruct (IHn ex1 ex2' Hf2' Hd1 Fx) as (x',(Px',(Hlx',(Fx',Hx')))); clear Hd1 IHn. set (u := bpow ex2). exists (x' + IZR nb * u). split; [|split; [|split]]. + apply (Rlt_le_trans _ _ _ Px'). rewrite <- (Rplus_0_r x') at 1; apply Rplus_le_compat_l. apply Rmult_le_pos. * apply IZR_le; lia. * now apply bpow_ge_0. + rewrite <- Hlx'. apply (mag_plus_eps beta (fun e => (e - (mag x' - ex2'))%Z)); [| |split]. * exact Px'. * unfold generic_format, F2R, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite Ztrunc_floor; [exact Fx'|]. now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]. * apply Rmult_le_pos; [|now apply bpow_ge_0]. apply IZR_le; lia. * rewrite ulp_neq_0;[idtac| now apply Rgt_not_eq]. unfold u, ex2', cexp; bpow_simplify. rewrite Zplus_comm; rewrite bpow_plus. apply Rmult_lt_compat_r; [now apply bpow_gt_0|]. rewrite bpow_1. apply IZR_lt; lia. + rewrite Fx' at 1. unfold ex2' at 2. rewrite Zplus_comm; rewrite bpow_plus; fold u. rewrite <- Rmult_assoc; rewrite <- Rmult_plus_distr_r. apply Rmult_eq_compat_r. replace (IZR _) with (x' * bpow (- ex2')); [|now apply (Rmult_eq_reg_r (bpow ex2')); [|now apply Rgt_not_eq; apply bpow_gt_0]; bpow_simplify]. rewrite Rmult_plus_distr_r. unfold u, ex2'; bpow_simplify. rewrite Fx' at 2; unfold ex2'; bpow_simplify. rewrite bpow_1; rewrite <- mult_IZR; rewrite <- plus_IZR. rewrite Zfloor_IZR. rewrite plus_IZR. apply f_equal2; [|reflexivity]. replace (- ex2 - 1)%Z with (- ex2')%Z; [|now unfold ex2'; ring]. rewrite Fx' at 1; unfold ex2'; bpow_simplify. now rewrite mult_IZR; rewrite <- bpow_1. + rewrite Hx'. rewrite Rplus_assoc; apply Rplus_eq_compat_l. rewrite <- Rmult_plus_distr_r. unfold ex2'; rewrite Zplus_comm; rewrite bpow_plus. rewrite <- Rmult_assoc; apply Rmult_eq_compat_r. rewrite (Rmult_eq_reg_l 2 _ (IZR nb + / 2)); [reflexivity| |lra]. rewrite bpow_1, Hb, plus_IZR, mult_IZR. field. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)