proposition: Theorem round_flx_sqr_sqrt_exact_aux: (radix_val beta <= 4)%Z -> z=x.
proof: Proof. Proof with auto with typeclass_instances. intros Hb. apply Rle_antisym. apply round_flx_sqr_sqrt_le... assert (((radix_val beta = 2)%Z \/ (radix_val beta=3)%Z) \/ (radix_val beta=4)%Z). generalize (radix_gt_1 beta); lia. destruct H. apply Rle_trans with (x - 0 * ulp_flx x). right; simpl; ring. apply round_flx_sqr_sqrt_aux1... lia. apply radix_gt_0. apply Rlt_le_trans with (x-/4*bpow (mag beta x - prec)). 2: right; simpl; field. apply Rle_lt_trans with (sqrt (IZR beta) * bpow (mag beta x - 1) - / 4 * bpow (mag beta x - prec)). 2: apply Rplus_lt_compat_r; assumption. apply Rle_trans with ((IZR beta / 2)*bpow (mag beta x-1)). replace (bpow (mag beta x)) with (bpow (1+(mag beta x-1))). rewrite bpow_plus, bpow_1. right; unfold Rdiv; ring. apply f_equal; ring. apply Rle_trans with ((sqrt (IZR beta) - /4* / IZR beta) * bpow (mag beta x-1)). apply Rmult_le_compat_r. apply bpow_ge_0. destruct H; rewrite H; simpl; interval. rewrite Rmult_minus_distr_r. apply Rplus_le_compat_l. apply Ropp_le_contravar. rewrite Rmult_assoc; apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; auto with real. apply Rle_trans with (bpow (-1+(mag beta x - 1))). apply bpow_le; lia. rewrite bpow_plus. right; apply f_equal2; try reflexivity. rewrite <- bpow_1, <- bpow_opp. apply f_equal; reflexivity. assert (2 * bpow (mag beta x - 1) < x). apply Rle_lt_trans with (2:=Hx). right; apply f_equal2; try reflexivity. rewrite H; simpl. apply sym_eq, sqrt_square; auto with real. assert ((2 * bpow (mag beta x - 1)+1*bpow (mag beta x - prec)) <= x). assert (0 < 2 * bpow (mag beta x - 1)). apply Rmult_lt_0_compat. auto with real. apply bpow_gt_0. assert (bpow (mag beta x - prec)=ulp_flx (2 * bpow (mag beta x - 1))). rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp, FLX_exp. apply f_equal. apply f_equal2; try reflexivity. apply sym_eq, mag_unique. rewrite Rabs_right. 2: apply Rle_ge; left; assumption. split. apply Rle_trans with (1*bpow (mag beta x - 1)). right; ring. apply Rmult_le_compat_r. apply bpow_ge_0. auto with real. apply Rlt_le_trans with (4*bpow (mag beta x - 1)). apply Rmult_lt_compat_r. apply bpow_gt_0. interval. rewrite <- H, <- bpow_1, <- bpow_plus. right; apply f_equal; ring. rewrite H2, Rmult_1_l. rewrite <- succ_eq_pos;[idtac|now left]. apply succ_le_lt... apply generic_format_FLX. exists (Float beta 2 (mag beta x -1)). easy. rewrite H; apply Z.lt_le_trans with (4^1)%Z. simpl; unfold Z.pow_pos; simpl; lia. apply (Zpower_le (Build_radix 4 eq_refl)). now apply Zlt_le_weak. apply Rle_trans with (x - 0 * ulp_flx x). right; simpl; ring. apply round_flx_sqr_sqrt_aux1... lia. apply radix_gt_0. apply Rlt_le_trans with (x-/4*bpow (mag beta x - prec)). 2: right; simpl; field. apply Rlt_le_trans with ( (2* bpow (mag beta x - 1) + 1 * bpow (mag beta x - prec)) - / 4 * bpow (mag beta x - prec)). 2: apply Rplus_le_compat_r; assumption. apply Rlt_le_trans with ((/2 + (1-/4)*bpow (-prec)) * bpow (mag beta x)). apply Rmult_lt_compat_r. apply bpow_gt_0. apply Rle_lt_trans with (/2+0);[right; ring|idtac]. apply Rplus_lt_compat_l. apply Rmult_lt_0_compat. interval. apply bpow_gt_0. unfold Zminus; repeat rewrite bpow_plus. replace (bpow (- (1))) with (/4). right; field. rewrite bpow_opp, bpow_1, H; reflexivity. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)