proposition: Theorem round_flx_sqr_sqrt_le: (beta <= 4)%Z -> z <= x.
proof: Proof. Proof with auto with typeclass_instances. intros Hb. case (Req_dec x (sqrt (IZR beta) * bpow (mag beta x - 1))). intros L; right; now apply round_flx_sqr_sqrt_middle. intros Hx'. assert (0 < x*x) by now apply Rmult_lt_0_compat. assert (0 <= 1 + ulp_flx (x * x) / 2 / (x * x)). rewrite <- (Rplus_0_l 0). apply Rplus_le_compat; auto with real. unfold Rdiv; apply Rmult_le_pos. apply Rmult_le_pos; auto with real; apply ulp_ge_0. left; auto with real. assert (0 <= 1 + ulp_flx x / 2 / x). rewrite <- (Rplus_0_l 0). apply Rplus_le_compat; auto with real. unfold Rdiv; apply Rmult_le_pos. apply Rmult_le_pos; auto with real; apply ulp_ge_0. left; auto with real. apply round_N_le_midp; try assumption... apply Rlt_le_trans with (x*(1+ulp_flx x / 2 / x)). 2: right; rewrite succ_eq_pos; try now left. 2: field; auto with real. apply Rle_lt_trans with (sqrt ((x*x)*(1+ulp_flx (x*x)/2/(x*x)))). apply sqrt_le_1_alt. apply Rplus_le_reg_l with (-x*x). apply Rle_trans with (y-x*x);[right; ring|idtac]. apply Rle_trans with (/2*ulp_flx (x*x));[idtac|right; field; auto with real]. apply Rle_trans with (1:=RRle_abs _). apply error_le_half_ulp... rewrite sqrt_mult; auto with real. rewrite sqrt_square; auto with real. apply Rmult_lt_compat_l. assumption. rewrite <- (sqrt_square (1 + ulp_flx x / 2 / x)); try assumption. apply sqrt_lt_1_alt. split; try assumption. apply Rmult_lt_reg_l with (2*x*x). rewrite Rmult_assoc; apply Rmult_lt_0_compat; auto with real. apply Rplus_lt_reg_r with (-2*x*x - ulp_flx x*ulp_flx x/2). apply Rle_lt_trans with (ulp_flx (x*x) - ulp_flx x*ulp_flx x/2). right; field. auto with real. apply Rlt_le_trans with (2*x*ulp_flx x). 2: right; field; auto with real. apply Rle_lt_trans with (ulp_flx (x * x) + ulp_flx x * ulp_flx x / 2). apply Rplus_le_compat_l. apply Rplus_le_reg_r with (ulp_flx x * ulp_flx x / 2). apply Rle_trans with 0;[right; ring|idtac]. apply Rle_trans with (ulp_flx x * ulp_flx x). apply Rmult_le_pos; apply ulp_ge_0. right; field. rewrite 2!ulp_neq_0. 2: now apply Rgt_not_eq. 2: now apply Rgt_not_eq. unfold cexp, FLX_exp. destruct (mag beta x) as (e,He). simpl. assert (bpow (e - 1) <= x < bpow e). rewrite <- (Rabs_right x). apply He; auto with real. apply Rle_ge; auto with real. rewrite <- bpow_plus. case (Rle_or_lt x (sqrt (IZR (radix_val beta))*bpow (e-1))); intros Hx. destruct Hx. replace (mag beta (x * x)-prec)%Z with (2*e-1-prec)%Z. apply Rlt_le_trans with (bpow (2 * e - 1 - prec) + bpow (2*e - 1 - prec) / 2). apply Rplus_lt_compat_l. unfold Rdiv; apply Rmult_lt_compat_r. auto with real. apply bpow_lt. lia. apply Rle_trans with (2*bpow (2 * e - 1 - prec)). apply Rle_trans with (3/2*bpow (2 * e - 1 - prec)). right; field. apply Rmult_le_compat_r. apply bpow_ge_0. interval. rewrite Rmult_assoc; apply Rmult_le_compat_l. auto with real. apply Rle_trans with (bpow (e-1)*bpow (e - prec)). rewrite <- bpow_plus. apply bpow_le. lia. apply Rmult_le_compat_r. apply bpow_ge_0. apply H2. apply f_equal with (f:= fun z => (z-prec)%Z). apply sym_eq, mag_unique. rewrite Rabs_right. split. apply Rle_trans with (bpow (e-1)*bpow (e-1)). rewrite <- bpow_plus. right; apply f_equal; ring. apply Rmult_le_compat; try apply H2; try apply bpow_ge_0. apply Rlt_le_trans with ((sqrt (IZR beta)*bpow (e-1))*(sqrt (IZR beta)*bpow (e-1))). apply Rmult_le_0_lt_compat; try apply H3; now left. apply Rle_trans with ((sqrt (IZR beta)*sqrt (IZR beta)) * (bpow (e-1)*bpow (e-1))). right; ring. rewrite <- bpow_plus, sqrt_def, <- bpow_1, <- bpow_plus. right; apply f_equal; ring. left; apply radix_pos. apply Rle_ge; auto with real. simpl in Hx'; contradict H3; assumption. replace (mag beta (x * x)-prec)%Z with (2*e-prec)%Z. case (Zle_lt_or_eq _ _ Hb); clear Hb; intros Hb. apply Rle_lt_trans with (2*(sqrt (IZR beta) * bpow (e - 1))* bpow (e - prec)). 2: apply Rmult_lt_compat_r. 2: apply bpow_gt_0. 2: apply Rmult_lt_compat_l; try assumption. 2: auto with real. apply Rle_trans with ((2 * sqrt (IZR beta)) * bpow (2*e - 1- prec)). 2: replace (2*e)%Z with (e+e)%Z by ring; unfold Zminus. 2: repeat rewrite bpow_plus; right; ring. apply Rle_trans with ((IZR beta + /4)*bpow (2 * e - 1 - prec)). rewrite Rmult_plus_distr_r. apply Rplus_le_compat. rewrite <- bpow_1, <- bpow_plus. right; apply f_equal; ring. apply Rmult_le_reg_l with 4%R. apply Rmult_lt_0_compat; auto with real. apply Rle_trans with (2*bpow (e - prec + (e - prec))). right; field. apply Rle_trans with (bpow (2 * e - 1 - prec)). 2: right; field. apply Rle_trans with (bpow (1+(e - prec + (e - prec)))). rewrite (bpow_plus _ 1%Z). apply Rmult_le_compat_r. apply bpow_ge_0. rewrite bpow_1. apply IZR_le. generalize (radix_gt_1 beta). lia. apply bpow_le. lia. apply Rmult_le_compat_r. apply bpow_ge_0. assert ((radix_val beta = 2%Z)%Z \/ radix_val beta = 3)%Z. assert (1 < radix_val beta)%Z by apply radix_gt_1. lia. destruct H3; rewrite H3; simpl; interval. apply Rlt_le_trans with (2 * (2*bpow (e - 1)+bpow (e-prec)) * bpow (e - prec)). apply Rlt_le_trans with (4* bpow (e - 1)* bpow (e - prec) + bpow (e - prec) * bpow (e - prec)*2). 2: right; ring. replace (4 * bpow (e - 1) * bpow (e - prec)) with (bpow (2 * e - prec)). apply Rplus_lt_compat_l. rewrite <- bpow_plus. unfold Rdiv; apply Rmult_lt_compat_l. apply bpow_gt_0. interval. replace 4 with (bpow 1). repeat rewrite <- bpow_plus. apply f_equal; ring. rewrite bpow_1, Hb; reflexivity. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rmult_le_compat_l. auto with real. apply Rle_trans with (2 * bpow (e - 1) + ulp_flx (2 * bpow (e - 1))). apply Rplus_le_compat_l. rewrite ulp_neq_0. 2: apply Rmult_integral_contrapositive_currified; apply Rgt_not_eq. 2: apply Rlt_0_2. 2: apply bpow_gt_0. unfold cexp, FLX_exp. right; apply f_equal. apply f_equal2; try reflexivity. apply sym_eq, mag_unique. rewrite Rabs_right. split. rewrite <- (Rmult_1_l (bpow (e-1))) at 1. apply Rmult_le_compat_r. apply bpow_ge_0. auto with real. apply Rlt_le_trans with (IZR beta*bpow (e - 1)). apply Rmult_lt_compat_r. apply bpow_gt_0. rewrite Hb; simpl; interval. rewrite <- bpow_1, <- bpow_plus. right; apply f_equal; ring. apply Rle_ge, Rmult_le_pos. auto with real. apply bpow_ge_0. rewrite <- succ_eq_pos. apply succ_le_lt... apply generic_format_FLX. exists (Float beta 2 (e-1)). unfold F2R; now simpl. apply Z.lt_le_trans with (4^1)%Z. simpl; unfold Z.pow_pos; simpl; lia. rewrite Hb. apply (Zpower_le (Build_radix 4 eq_refl)). now apply Zlt_le_weak. apply Rle_lt_trans with (2:=Hx). replace (sqrt (IZR beta)) with 2%R. now right. rewrite Hb; simpl. apply sym_eq, sqrt_square; auto with real. apply Rmult_le_pos. now auto with real. apply bpow_ge_0. apply f_equal with (f:= fun z => (z-prec)%Z). apply sym_eq, mag_unique. rewrite Rabs_right. split. apply Rle_trans with ((sqrt (IZR beta)*bpow (e-1))*(sqrt (IZR beta)*bpow (e-1))). apply Rle_trans with ((sqrt (IZR beta)*sqrt (IZR beta)) * (bpow (e-1)*bpow (e-1))). 2: right; ring. rewrite <- bpow_plus, sqrt_def, <- bpow_1, <- bpow_plus. right; apply f_equal; ring. left; apply radix_pos. apply Rmult_le_compat. apply Rmult_le_pos; try apply sqrt_pos; apply bpow_ge_0. apply Rmult_le_pos; try apply sqrt_pos; apply bpow_ge_0. now left. now left. apply Rlt_le_trans with (bpow (e)*bpow (e)). 2: rewrite <- bpow_plus. 2: right; apply f_equal; ring. apply Rmult_le_0_lt_compat; try apply H2. now left. now left. apply Rle_ge; auto with real. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)