proposition: Lemma sqrt_neq_midpoint : forall fexp : Z -> Z, Valid_exp fexp -> forall x, 0 < x -> generic_format beta fexp x -> sqrt x <> midp beta fexp (sqrt x).
proof: Proof. intros fexp Vfexp x Px Fx. unfold midp. set (r := round beta fexp Zfloor (sqrt x)). revert Fx. rewrite ulp_neq_0. 2: now apply Rgt_not_eq, sqrt_lt_R0. unfold generic_format, round, F2R, scaled_mantissa, cexp; simpl. set (m := Ztrunc (x * bpow (- fexp (mag x)))). intro Fx. assert (Nnr : 0 <= r). { unfold r; rewrite <- (round_0 beta fexp Zfloor); apply round_le. - exact Vfexp. - apply valid_rnd_DN. - apply sqrt_ge_0. } set (exsx := fexp (mag (sqrt x))). set (exx := (fexp (mag x))). destruct (Req_dec r 0) as [Zr|Nzr]. { rewrite Zr. destruct (Zle_or_lt exx (2 * exsx)) as [H1|H1]. - set (ex2 := Zfloor (IZR exx / 2)). assert (H1' : (ex2 <= exsx)%Z). { apply le_IZR. apply (Rle_trans _ _ _ (Zfloor_lb _)). apply (Rmult_le_reg_l 2); [lra|]. replace (_ * (_ / _)) with (IZR exx) by field. now rewrite <- mult_IZR; apply IZR_le. } assert (H1'' : (2 * ex2 <= exx)%Z). { apply le_IZR, (Rmult_le_reg_r (/ 2)); [lra|]. rewrite Zmult_comm, mult_IZR, Rmult_assoc; simpl. rewrite Rinv_r; [|lra]; rewrite Rmult_1_r. apply Zfloor_lb. } destruct (midpoint_beta_odd_remains _ (Rle_refl 0) _ _ H1') as (x',(Nnx',(Fx',Hx'))). { rewrite Rmult_0_l. now rewrite Zfloor_IZR; simpl; rewrite Rmult_0_l. } rewrite Hx'. intro H. assert (H' := H). apply (Rmult_eq_compat_l (sqrt x)) in H. rewrite H' in H at 3. clear H'. revert H. rewrite sqrt_def; [|now apply Rlt_le]. replace (_ * _) with (x' * x' + x' * bpow ex2 + / 4 * bpow ex2 * bpow ex2) by field. rewrite Fx; fold exx. revert Fx'; set (m' := Zfloor ((x' * bpow (- ex2)))); intro Fx'. rewrite Fx'. replace (_ + IZR m' * _ * _) with ((IZR m' * IZR m' + IZR m') * (bpow ex2 * bpow ex2)) by ring. rewrite (Rmult_assoc (/ 4)), <- Rmult_plus_distr_r. bpow_simplify. intro H; apply (Rmult_eq_compat_r (bpow (- 2 * ex2))) in H; revert H. bpow_simplify. rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0]. do 2 rewrite <- mult_IZR; rewrite <- plus_IZR. intro H. apply (Rplus_eq_compat_l (- IZR (m' * m' + m'))) in H. ring_simplify in H. rewrite <- opp_IZR, <- plus_IZR in H. apply (Rmult_eq_compat_l 4) 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. - rewrite Rplus_0_l. intro H. assert (H' := H). apply (Rmult_eq_compat_l (sqrt x)) in H. rewrite H' in H at 3. clear H'. revert H. rewrite sqrt_def; [|now apply Rlt_le]. replace (_ * _) with (/ 4 * bpow exsx * bpow exsx) by field. rewrite Fx; fold exx. bpow_simplify. intro H; apply (Rmult_eq_compat_r (bpow (- 2 * exsx))) in H; revert H. bpow_simplify. rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0; lia]. rewrite <- mult_IZR. intro H. apply (Rmult_eq_compat_l 4) 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 (Pr : 0 < r) by lra. destruct (Zle_or_lt exx (2 * exsx)) as [H1|H1]. - set (ex2 := Zfloor (IZR exx / 2)). assert (H1' : (ex2 <= exsx)%Z). { apply le_IZR. apply (Rle_trans _ _ _ (Zfloor_lb _)). apply (Rmult_le_reg_l 2); [lra|]. replace (_ * (_ / _)) with (IZR exx) by field. now rewrite <- mult_IZR; apply IZR_le. } assert (H1'' : (2 * ex2 <= exx)%Z). { apply le_IZR, (Rmult_le_reg_r (/ 2)); [lra|]. rewrite Zmult_comm, mult_IZR, Rmult_assoc; simpl. rewrite Rinv_r; [|lra]; rewrite Rmult_1_r. apply Zfloor_lb. } destruct (midpoint_beta_odd_remains_pos _ Pr _ _ H1') as (x',(Px',(Lx',(Fx',Hx')))). { unfold r at 2, round, F2R, scaled_mantissa, cexp; simpl. fold exsx; bpow_simplify. now rewrite Zfloor_IZR. } rewrite Hx'. intro H. assert (H' := H). apply (Rmult_eq_compat_l (sqrt x)) in H. rewrite H' in H at 3. clear H'. revert H. rewrite sqrt_def; [|now apply Rlt_le]. replace (_ * _) with (x' * x' + x' * bpow ex2 + / 4 * bpow ex2 * bpow ex2) by field. rewrite Fx; fold exx. revert Fx'; set (m' := Zfloor ((x' * bpow (- ex2)))); intro Fx'. rewrite Fx'. replace (_ + IZR m' * _ * _) with ((IZR m' * IZR m' + IZR m') * (bpow ex2 * bpow ex2)) by ring. rewrite (Rmult_assoc (/ 4)), <- Rmult_plus_distr_r. bpow_simplify. intro H; apply (Rmult_eq_compat_r (bpow (- 2 * ex2))) in H; revert H. bpow_simplify. rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0]. do 2 rewrite <- mult_IZR; rewrite <- plus_IZR. intro H. apply (Rplus_eq_compat_l (- IZR (m' * m' + m'))) in H. ring_simplify in H. rewrite <- opp_IZR, <- plus_IZR in H. apply (Rmult_eq_compat_l 4) 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. - intro H. assert (H' := H). apply (Rmult_eq_compat_l (sqrt x)) in H. rewrite H' in H at 3. clear H'. revert H. rewrite sqrt_def; [|now apply Rlt_le]. replace (_ * _) with (r * r + r * bpow exsx + / 4 * bpow exsx * bpow exsx) by field. rewrite Fx; fold exx. set (mr := Zfloor (sqrt x * bpow (- exsx))). assert (Hr : r = IZR mr * bpow exsx); [now simpl|]. rewrite Hr. replace (_ + _) with ((IZR mr * IZR mr + IZR mr + / 4) * bpow exsx * bpow exsx) by ring. bpow_simplify. intro H; apply (Rmult_eq_compat_r (bpow (- 2 * exsx))) in H; revert H. bpow_simplify. rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0; lia]. do 2 rewrite <- mult_IZR; rewrite <- plus_IZR. intro H. apply (Rplus_eq_compat_l (- IZR (mr * mr + mr))) in H. ring_simplify in H. rewrite <- opp_IZR, <- plus_IZR in H. apply (Rmult_eq_compat_l 4) 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. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)