proposition: Theorem sqrt_error_FLX_N : forall x, format x -> format (x - Rsqr (round beta (FLX_exp prec) (Znearest choice) (sqrt x)))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. destruct (total_order_T x 0) as [[Hxz|Hxz]|Hxz]. unfold sqrt. destruct (Rcase_abs x). rewrite round_0... unfold Rsqr. now rewrite Rmult_0_l, Rminus_0_r. elim (Rlt_irrefl 0). now apply Rgt_ge_trans with x. rewrite Hxz, sqrt_0, round_0... unfold Rsqr. rewrite Rmult_0_l, Rminus_0_r. apply generic_format_0. case (Req_dec (round beta (FLX_exp prec) (Znearest choice) (sqrt x)) 0); intros Hr. rewrite Hr; unfold Rsqr; ring_simplify (x-0*0)%R; assumption. destruct (canonical_generic_format _ _ x Hx) as (fx,(Hx1,Hx2)). destruct (canonical_generic_format beta (FLX_exp prec) (round beta (FLX_exp prec) (Znearest choice) (sqrt x))) as (fr,(Hr1,Hr2)). apply generic_format_round... unfold Rminus; apply generic_format_plus_prec with fx (Fopp (Fmult fr fr)); trivial. intros e; apply Z.le_refl. unfold Rsqr; now rewrite F2R_opp,F2R_mult, <- Hr1. apply Rle_lt_trans with x. apply Rabs_minus_le. apply Rle_0_sqr. destruct (relative_error_N_FLX_ex beta prec (prec_gt_0 prec) choice (sqrt x)) as (eps,(Heps1,Heps2)). rewrite Heps2. rewrite Rsqr_mult, Rsqr_sqrt, Rmult_comm. 2: now apply Rlt_le. apply Rmult_le_compat_r. now apply Rlt_le. apply Rle_trans with (5²/4²)%R. rewrite <- Rsqr_div. apply Rsqr_le_abs_1. apply Rle_trans with (1 := Rabs_triang _ _). rewrite Rabs_R1. apply Rplus_le_reg_l with (-1)%R. replace (-1 + (1 + Rabs eps))%R with (Rabs eps) by ring. apply Rle_trans with (1 := Heps1). rewrite Rabs_pos_eq. apply Rmult_le_reg_l with 2%R. now apply IZR_lt. rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l. apply Rle_trans with (bpow (-1)). apply bpow_le. lia. replace (2 * (-1 + 5 / 4))%R with (/2)%R by field. apply Rinv_le. now apply IZR_lt. apply IZR_le. unfold Zpower_pos. simpl. rewrite Zmult_1_r. apply Zle_bool_imp_le. apply beta. now apply IZR_neq. unfold Rdiv. apply Rmult_le_pos. now apply IZR_le. apply Rlt_le. apply Rinv_0_lt_compat. now apply IZR_lt. now apply IZR_neq. unfold Rsqr. replace (5 * 5 / (4 * 4))%R with (25 * /16)%R by field. apply Rmult_le_reg_r with 16%R. now apply IZR_lt. rewrite Rmult_assoc, Rinv_l, Rmult_1_r. now apply (IZR_le _ 32). now apply IZR_neq. rewrite Hx2, <- Hx1; unfold cexp, FLX_exp. ring_simplify (prec + (mag beta x - prec))%Z. destruct (mag beta x); simpl. rewrite <- (Rabs_right x). apply a. now apply Rgt_not_eq. now apply Rgt_ge. replace (Fexp (Fopp (Fmult fr fr))) with (Fexp fr + Fexp fr)%Z. 2: unfold Fopp, Fmult; destruct fr; now simpl. rewrite Hr1. replace (x + - Rsqr (F2R fr))%R with (-((F2R fr - sqrt x)*(F2R fr + sqrt x)))%R. 2: rewrite <- (sqrt_sqrt x) at 3; auto. 2: unfold Rsqr; ring. rewrite Rabs_Ropp, Rabs_mult. apply Rle_lt_trans with ((/2*bpow (Fexp fr))* Rabs (F2R fr + sqrt x))%R. apply Rmult_le_compat_r. apply Rabs_pos. apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R. rewrite <- Hr1. apply error_le_half_ulp_round... right; rewrite ulp_neq_0. 2: now rewrite <- Hr1. apply f_equal. rewrite Hr2, <- Hr1; trivial. rewrite Rmult_assoc, Rmult_comm. replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring. rewrite bpow_plus, Rmult_assoc. apply Rmult_lt_compat_l. apply bpow_gt_0. apply Rmult_lt_reg_l with (1 := Rlt_0_2). apply Rle_lt_trans with (Rabs (F2R fr + sqrt x)). right; field. apply Rle_lt_trans with (1:=Rabs_triang _ _). assert (Rabs (F2R fr) < bpow (prec + Fexp fr))%R. rewrite Hr2. unfold cexp, FLX_exp. ring_simplify (prec + (mag beta (F2R fr) - prec))%Z. destruct (mag beta (F2R fr)); simpl. apply a. rewrite <- Hr1; auto. apply Rlt_le_trans with (bpow (prec + Fexp fr)+ Rabs (sqrt x))%R. now apply Rplus_lt_compat_r. replace (2 * bpow (prec + Fexp fr))%R with (bpow (prec + Fexp fr) + bpow (prec + Fexp fr))%R by ring. apply Rplus_le_compat_l. assert (sqrt x <> 0)%R. apply Rgt_not_eq. now apply sqrt_lt_R0. destruct (mag beta (sqrt x)) as (es,Es). specialize (Es H0). apply Rle_trans with (bpow es). now apply Rlt_le. apply bpow_le. case (Zle_or_lt es (prec + Fexp fr)) ; trivial. intros H1. absurd (Rabs (F2R fr) < bpow (es - 1))%R. apply Rle_not_lt. rewrite <- Hr1. apply abs_round_ge_generic... apply generic_format_bpow. unfold FLX_exp; lia. apply Es. apply Rlt_le_trans with (1:=H). apply bpow_le. lia. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error