proposition: Theorem sqrt_sqr: forall x y:R, format x -> -1 <= round_flx1 (x / round_flx2(R_sqrt.sqrt (round_flx3(round_flx4(x*x)+round_flx5(y*y))))) <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx. assert (Y:Valid_exp (FLX_exp prec)). apply FLX_exp_valid; unfold Prec_gt_0; lia. assert (H: ((radix_val beta=5)%Z -> (3 < prec)%Z) \/ ((radix_val beta=5)%Z /\ (prec=3)%Z)). case (Zle_lt_or_eq 3 prec); lia. case H; intros H'; clear H. now apply sqrt_sqr_except. destruct H' as (H1,H2). apply Rabs_le_inv. apply abs_round_le_generic... apply generic_format_FLX. exists (Float beta 1 0). unfold F2R; simpl; ring. simpl. apply Zpower_gt_1; lia. case (Req_dec x 0); intros Hx. rewrite Hx; unfold Rdiv; rewrite Rmult_0_l, Rabs_R0. left; apply Rlt_0_1. unfold Rdiv; rewrite Rabs_mult. apply Rle_trans with (Rabs x * / (Rabs x)). 2: right; field. 2: apply Rgt_not_eq, Rabs_pos_lt; easy. apply Rmult_le_compat_l. apply Rabs_pos. rewrite Rabs_right. apply Rinv_le. apply Rabs_pos_lt; easy. apply Rle_trans with (round_flx2 (R_sqrt.sqrt (round_flx4 (x * x)))). right; apply sym_eq. now apply sqrt_sqr_special_case_all. apply round_le... apply sqrt_le_1_alt. apply round_ge_generic... apply generic_format_round... apply Rplus_le_reg_r with (-round_flx4 (x * x)); ring_simplify. replace 0 with (round_flx5 0). apply round_le... apply Rle_trans with (1:=Rle_0_sqr y). right; unfold Rsqr; ring. apply round_0... apply Rle_ge; left. apply Rinv_0_lt_compat. apply round_FLX_gt_0... unfold Prec_gt_0; lia. apply sqrt_lt_R0. apply round_FLX_gt_0... unfold Prec_gt_0; lia. apply Rle_lt_trans with (0+ round_flx5 (y * y)). rewrite Rplus_0_l. replace 0 with (round_flx5 0). apply round_le... apply Rle_trans with (1:=Rle_0_sqr y). right; unfold Rsqr; ring. apply round_0... apply Rplus_lt_compat_r. apply round_FLX_gt_0... unfold Prec_gt_0; lia. apply Rlt_le_trans with (Rsqr x). now apply Rlt_0_sqr. right; unfold Rsqr; ring. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic) ComputeMore Flocq(Bracket Round Operations Div)