proposition: Lemma float_neq_midpoint_beta_odd : forall (mx ex : Z), forall (fexp : Z -> Z), 0 < IZR mx -> IZR mx * bpow ex <> midp beta fexp (IZR mx * bpow ex).
proof: Proof. intros mx ex fexp Hmx. unfold midp; rewrite ulp_neq_0. unfold round, F2R, scaled_mantissa, cexp; simpl. set (exf := fexp (mag (IZR mx * bpow ex))). set (mxf := Zfloor (IZR mx * bpow ex * bpow (- exf))). destruct (Zle_or_lt exf ex) as [Hm|Hm]. - replace ex with (ex - exf + exf)%Z by ring. rewrite bpow_plus. intro H. apply (Rplus_eq_compat_l (- IZR mxf * bpow exf)) in H. revert H. rewrite <- Rmult_assoc, <- Rmult_plus_distr_r. rewrite <- (IZR_Zpower _ (_ - _)); [|now apply Zle_minus_le_0]. intro H. ring_simplify in H. rewrite <- Rmult_plus_distr_r in H. rewrite <- opp_IZR, <- mult_IZR, <- plus_IZR, Rmult_comm in H. apply Rmult_eq_reg_l in H; [|now apply Rgt_not_eq, bpow_gt_0]. apply (Rmult_eq_compat_l 2) in H. revert H. rewrite <- mult_IZR, Rinv_r; [|lra]. apply IZR_neq. intro H. apply (Zodd_not_Zeven 1); [now simpl|]. rewrite <- H. now apply Zeven_mult_Zeven_l. - assert (Hm' : (ex <= exf)%Z) by lia. assert (Nnmxy : 0 <= IZR mxf * bpow exf). { apply Rmult_le_pos; [|now apply bpow_ge_0]. apply IZR_le; unfold mxf. apply Zfloor_lub; simpl. apply Rmult_le_pos; [|now apply bpow_ge_0]. now apply Rmult_le_pos; [now left|apply bpow_ge_0]. } destruct (midpoint_beta_odd_remains _ Nnmxy _ _ Hm') as (x',(_,(Hx',Hxx'))). { now bpow_simplify; rewrite Zfloor_IZR. } rewrite Hxx', Hx'. set (mx' := Zfloor (x' * bpow (- ex))). intro H. apply (Rplus_eq_compat_l (- IZR mx' * bpow ex)) in H. revert H. rewrite <- Rmult_plus_distr_r. intro H. ring_simplify in H. rewrite <- Rmult_plus_distr_r in H. rewrite <- opp_IZR, <- plus_IZR, Rmult_comm in H. apply Rmult_eq_reg_l in H; [|now apply Rgt_not_eq, bpow_gt_0]. apply (Rmult_eq_compat_l 2) in H. revert H. rewrite <- mult_IZR, Rinv_r; [|lra]. apply IZR_neq. intro H. apply (Zodd_not_Zeven 1); [now simpl|]. rewrite <- H. now apply Zeven_mult_Zeven_l. - apply Rmult_integral_contrapositive_currified. now apply Rgt_not_eq, Rlt_gt. apply Rgt_not_eq, bpow_gt_0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)