proposition: Theorem round_flx_sqr_sqrt_aux: (4 < radix_val beta)%Z -> ((radix_val beta=5)%Z -> (3 < prec)%Z) -> (sqrt (IZR (radix_val beta)) * bpow (mag beta x-1) < x) -> round_flx3(x/z) <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros Hbeta Hprec5 H1. apply Rle_trans with (round_flx3 (x/(x-IZR k*ulp_flx x))). apply round_le... unfold Rdiv; apply Rmult_le_compat_l. now left. apply Rinv_le. apply xkpos; try assumption. apply kLe. right; lia. apply round_flx_sqr_sqrt_aux1... apply kpos. apply kLe. right; lia. apply Rplus_lt_reg_l with ((IZR k + / 2) * (IZR k + / 2) * bpow (mag beta x - prec)). apply Rlt_le_trans with ((2 * IZR k + 1) * x). 2: right; ring. apply Rle_lt_trans with (/4*bpow (2+(mag beta x - prec)) + / 2 * bpow (mag beta x)). apply Rplus_le_compat_r. rewrite bpow_plus, <- Rmult_assoc. apply Rmult_le_compat_r. apply bpow_ge_0. assert (0 <= IZR k + / 2). replace 0 with (0+0) by (simpl;ring); apply Rplus_le_compat. apply IZR_le, kpos. apply Rlt_le, Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. assert (IZR k + / 2 <= IZR beta / 2). apply Rle_trans with ((IZR (Zceil (IZR beta / 2) - 1)) + /2). apply Rplus_le_compat_r. apply IZR_le, kLe2. rewrite minus_IZR; simpl. generalize (beta); intros n. destruct (Zeven_ex n) as [m Hm]. destruct (Z.even n). rewrite Zplus_0_r in Hm. rewrite Hm, mult_IZR. replace (2*IZR m / 2) with (IZR m). rewrite Zceil_IZR. apply Rplus_le_reg_l with (-IZR m + /2). field_simplify. unfold Rdiv; apply Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat. apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rlt_le, Rlt_0_1. simpl; field. rewrite Hm, plus_IZR, mult_IZR. replace ((2*IZR m + 1)/2) with (IZR m+/2). replace (Zceil (IZR m + / 2)) with (m+1)%Z. rewrite plus_IZR; simpl; right; field. apply sym_eq, Zceil_imp. split. ring_simplify (m+1-1)%Z. apply Rplus_lt_reg_r with (-IZR m). ring_simplify. apply Rinv_0_lt_compat. apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. rewrite plus_IZR; apply Rplus_le_compat_l. apply Rplus_le_reg_l with (-/2). simpl; field_simplify. unfold Rdiv; apply Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat. apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rlt_le, Rlt_0_1. simpl; field. apply Rle_trans with ((IZR beta / 2)*(IZR beta / 2)). now apply Rmult_le_compat. simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, mult_IZR. right; field. generalize kpos; unfold k; intros Y. assert (round_flx_sqr_sqrt_snd_deg := round_flx_sqr_sqrt_snd_deg). destruct (mag beta x) as (e,He). simpl (mag_val beta x (Build_mag_prop beta x e He)) in *. apply Rle_lt_trans with (bpow (e-1)*(/4*bpow (3-prec) + (IZR beta) / 2)). rewrite (Rmult_plus_distr_l (bpow (e-1))). apply Rplus_le_compat. rewrite (Rmult_comm (bpow (e-1))). rewrite Rmult_assoc; apply Rmult_le_compat_l. apply Rlt_le, Rinv_0_lt_compat. apply Rmult_lt_0_compat; apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. rewrite <- bpow_plus. right; apply f_equal; ring. unfold Zminus; rewrite bpow_plus, bpow_opp, bpow_1. right; field. apply Rgt_not_eq, radix_pos. apply Rle_lt_trans with ((2 * (x * bpow (1 - e) / (2+bpow (1-prec)) - 1) + 1) * (sqrt (IZR beta) * bpow (e - 1))). apply Rle_trans with (bpow (e - 1)*((2 * (x * bpow (1 - e) / (2+bpow (1-prec)) - 1) + 1) * sqrt (IZR beta))). 2: right; ring. apply Rmult_le_compat_l. apply bpow_ge_0. apply Rplus_le_reg_l with (-(IZR beta/2)+sqrt (IZR beta)). ring_simplify. apply Rle_trans with (IZR beta *(2-bpow(1-prec))/ (2*(2+bpow (1-prec)))). apply round_flx_sqr_sqrt_snd_deg. case (Zle_lt_or_eq 5 (radix_val beta)). lia. intros G; now right. intros G; left; split. now rewrite G. apply Hprec5; now rewrite G. apply Rle_trans with (- (IZR beta / 2) + IZR (beta)*2/(2+bpow (1-prec))). right; field. apply Rgt_not_eq. generalize (bpow_gt_0 beta (1 - prec)) ; lra. apply Rplus_le_compat_l. apply Rle_trans with (2*sqrt (IZR beta) * ((sqrt (IZR beta) * bpow (e - 1))*bpow (1 - e) /(2+bpow (1-prec)))). apply Rle_trans with ((sqrt (IZR beta) * sqrt (IZR beta)) * ((bpow (e - 1) * bpow (1 - e))) *(2/(2+bpow (1-prec)))). 2: right; field. rewrite <- bpow_plus. rewrite sqrt_sqrt. ring_simplify (e-1+(1-e))%Z. simpl; unfold Rdiv; right; simpl; ring. left; apply radix_pos. generalize (bpow_gt_0 beta (1 - prec)) ; lra. apply Rmult_le_compat_l. apply Rmult_le_pos. apply Rlt_le, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply sqrt_pos. apply Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat. generalize (bpow_gt_0 beta (1 - prec)) ; lra. apply Rmult_le_compat_r. apply bpow_ge_0. now left. apply Rle_lt_trans with ((2 * IZR (Zceil (x * bpow (1 - e) / (2+bpow (1-prec))) - 1) + 1)* (sqrt (IZR beta) * bpow (e - 1))). apply Rmult_le_compat_r. apply Rmult_le_pos. apply sqrt_pos. apply bpow_ge_0. apply Rplus_le_compat_r. apply Rmult_le_compat_l. apply Rlt_le, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. rewrite minus_IZR. apply Rplus_le_compat_r. apply Zceil_ub. apply Rmult_lt_compat_l. apply Rle_lt_0_plus_1. apply Rmult_le_pos. apply Rlt_le, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply IZR_le, Y. assumption. apply round_flx_sqr_sqrt_aux2... apply kpos. rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold k, cexp, FLX_exp. destruct (mag beta x) as (e,He). simpl (mag_val beta x (Build_mag_prop beta x e He)) in *. apply Rle_lt_trans with (2 * IZR (Zceil (x * bpow (1 - e) / (2+bpow (1-prec))) - 1) * (bpow (prec - 1) * bpow (e - prec)) * (1 + bpow (1 - prec) / 2)). right; ring. rewrite <- bpow_plus. apply Rlt_le_trans with (2 * (x * bpow (1 - e) / (2+bpow (1-prec))) * bpow (prec - 1 + (e - prec)) * (1 + bpow (1 - prec) / 2)). apply Rmult_lt_compat_r. rewrite Rplus_comm; apply Rle_lt_0_plus_1. unfold Rdiv; apply Rmult_le_pos. apply bpow_ge_0. apply Rlt_le, Rinv_0_lt_compat, Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. apply Rmult_lt_compat_r. apply bpow_gt_0. apply Rmult_lt_compat_l. apply Rle_lt_0_plus_1, Rlt_le, Rlt_0_1. generalize ((x * bpow (1 - e) / (2+bpow (1-prec)))). intros r; case (Req_dec (IZR (Zfloor r)) r). intros V; rewrite <- V; rewrite Zceil_IZR. apply IZR_lt; lia. intros V; rewrite (Zceil_floor_neq _ V). ring_simplify (Zfloor r+1-1)%Z. case (Zfloor_lb r); try trivial. intros W; now contradict W. apply Rle_trans with (x*(bpow (1 - e)*bpow (prec - 1 + (e - prec)))* (2*(1 + bpow (1 - prec) / 2)/(2+bpow (1-prec)))). right; unfold Rdiv; ring. rewrite <- bpow_plus. ring_simplify (1 - e + (prec - 1 + (e - prec)))%Z. simpl (bpow 0); rewrite Rmult_1_r. right; field. apply Rgt_not_eq. generalize (bpow_gt_0 beta (1 - prec)) ; lra. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)