proposition: Theorem sqrt_sqr_pos: forall x y:R, format x -> 0 <= x -> 0 <= round_flx3 (x / round_flx2(sqrt (round_flx4(round_flx1(x*x)+round_flx5(y*y))))) <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Hx. case Hx; intros Hx'. assert (round_flx2 (sqrt (round_flx1 (x * x))) <= round_flx2 (sqrt (round_flx4 (round_flx1 (x * x) + round_flx5 (y * y))))). apply round_le... apply sqrt_le_1_alt. apply round_ge_generic... apply generic_format_round... apply Rplus_le_reg_l with (-(round_flx1 (x*x))); ring_simplify. rewrite <- round_0 with beta (FLX_exp prec) (Znearest choice5)... apply round_le... apply Rle_trans with (Rsqr y);[auto with real|right ; unfold Rsqr; ring]. assert (0 < round_flx2 (sqrt (round_flx1 (x * x)))). destruct (mag beta x) as (e,He). apply Rlt_le_trans with (bpow (e-1)). apply bpow_gt_0. apply round_ge_generic... apply generic_format_bpow. unfold FLX_exp; auto with zarith. rewrite <- (sqrt_sqrt (bpow (e-1))). 2: apply bpow_ge_0. rewrite <- sqrt_mult; try apply bpow_ge_0. apply sqrt_le_1_alt. rewrite <- bpow_plus. apply round_ge_generic... apply generic_format_bpow. unfold FLX_exp; auto with zarith. rewrite bpow_plus. rewrite Rabs_right in He by now apply Rle_ge. apply Rmult_le_compat; try apply bpow_ge_0; apply He; auto with real. split. replace 0 with (round_flx3 0). apply round_le... unfold Rdiv; apply Rmult_le_pos; try assumption. left; apply Rinv_0_lt_compat. apply Rlt_le_trans with (1:=H0); exact H. apply round_0... apply Rle_trans with (round_flx3 (x / round_flx2 (sqrt (round_flx1 (x * x))))). apply round_le... unfold Rdiv; apply Rmult_le_compat_l; try exact Hx. apply Rinv_le; assumption. case (Zle_or_lt (radix_val beta) 4); intros Hradix. rewrite round_flx_sqr_sqrt_exact; try assumption. rewrite Rabs_right. 2: now apply Rle_ge. replace (x/x) with 1;[idtac|field; auto with real]. right; apply round_generic... replace 1 with (bpow 0) by reflexivity. apply generic_format_bpow. unfold FLX_exp; auto with zarith. now apply round_flx_sqr_sqrt_pos. unfold Rdiv; rewrite <- Hx', Rmult_0_l. rewrite round_0... auto with real. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)