proposition: Theorem round_flx_sqr_sqrt_exact_case1: (x < sqrt (IZR (radix_val beta)) * bpow (mag beta x-1)) -> z = x.
proof: Proof. Proof with auto with typeclass_instances. intros Cu. case (Req_dec x (bpow (mag beta x - 1))); intros Hx. unfold z, y. rewrite Hx, <- bpow_plus. rewrite (round_generic _ _ _ (bpow (mag beta x - 1 + (mag beta x - 1))))... replace (sqrt (bpow (mag beta x - 1 + (mag beta x - 1)))) with (bpow (mag beta x - 1 )). apply round_generic... apply generic_format_bpow. unfold FLX_exp; auto with zarith. apply sym_eq, sqrt_lem_1; try apply bpow_ge_0. apply sym_eq, bpow_plus. apply generic_format_bpow. unfold FLX_exp; auto with zarith. assert (0 < x*x) by now apply Rmult_lt_0_compat. assert (0 <= 1 - ulp_flx x / 2 / x). apply Rplus_le_reg_l with (ulp_flx x / 2 / x); ring_simplify. apply Rmult_le_reg_l with 2; auto with real. apply Rmult_le_reg_l with x; auto with real. apply Rle_trans with (ulp_flx x). right; field; auto with real. apply Rle_trans with x. apply ulp_le_id; auto. lra. assert (0 <= 1 - ulp_flx (x * x) / 2 / (x * x)). apply Rplus_le_reg_l with (ulp_flx (x*x) / 2 / (x*x)); ring_simplify. apply Rmult_le_reg_l with 2; auto with real. apply Rmult_le_reg_l with (x*x); auto with real. apply Rle_trans with (ulp_flx (x*x)). right; field; auto with real. apply Rle_trans with (x*x). rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp, FLX_exp. destruct (mag beta (x*x)) as (e,He); simpl. apply Rle_trans with (bpow (e-1)). apply bpow_le; auto with zarith. rewrite <- (Rabs_right (x*x)). apply He; auto with real. apply Rle_ge; auto with real. lra. 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. 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. apply sym_eq, Rle_antisym. apply round_N_ge_midp; try assumption... apply Rle_lt_trans with (x*(1-ulp_flx x / 2 / x)). rewrite pred_eq_pos;[idtac|now left]. unfold pred_pos; rewrite Req_bool_false; trivial. right; field; auto with real. apply Rlt_le_trans with (sqrt ((x*x)*(1-ulp_flx (x*x)/2/(x*x)))). 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. apply Rmult_le_pos; 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+2*x*ulp_flx x+ ulp_flx(x*x)). 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 ulp_sqr_ulp_lt; auto. apply sqrt_le_1_alt. apply Rplus_le_reg_l with (-y+ulp_flx (x * x)/2). apply Rle_trans with (-(y-x*x));[right; field; auto with real|idtac]. apply Rle_trans with (/2*ulp_flx (x*x));[idtac|right; field; auto with real]. apply Rle_trans with (1:=RRle_abs _). rewrite Rabs_Ropp. apply error_le_half_ulp... apply round_N_le_midp; try assumption... apply Rlt_le_trans with (x*(1+ulp_flx x / 2 / x)). 2: rewrite succ_eq_pos; try now left. 2: right; 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). 2: apply ulp_sqr_ulp_lt; auto. 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. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)