proposition: Lemma Delta_correct_ : /4 * bpow (Zceil ((IZR (emin+prec-1))/2)) < Delta -> (Rabs (Delta - E_Delta) <= (23/4*eps+38*eps*eps) * E_Delta).
proof: Proof. Proof with auto with typeclass_instances. intros Y. assert (bpow (Zceil (IZR (emin + prec - 1) / 2)) < round_flt (sqrt M)). case (Rle_or_lt (round_flt (sqrt M)) (bpow (Zceil (IZR (emin + prec - 1) / 2)))); intros Y1. 2: easy. contradict Y; apply Rle_not_lt. apply round_le_generic... apply fourth_format_gen. apply le_IZR. apply Rle_trans with (2:=Zceil_ub _). apply Rmult_le_reg_r with 2%R. intuition. unfold Rdiv; rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r. rewrite <- mult_IZR. apply IZR_le. lia. apply Rgt_not_eq; intuition. replace (round_flt (/ 4)) with (/4). apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; intuition. exact Y1. apply sym_eq, round_generic... apply fourth_format. pattern E_Delta at 2; replace E_Delta with (Rabs E_Delta). eapply err_aux. apply err_mult_. apply generic_format_round... apply generic_format_round... replace (round_flt (/ 4)) with (/4). apply err_0. apply sym_eq, round_generic... apply fourth_format. apply err_sqrt_. repeat apply Rmult_le_pos. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); apply Rle_trans with (1:=cLeb); assumption. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); assumption. assumption. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); apply Rle_trans with (1:=cLeb); assumption. now apply Rle_0_minus. apply Rplus_le_le_0_compat. assumption. now apply Rle_0_minus. apply Rplus_le_reg_l with a; ring_simplify. rewrite Rplus_comm; assumption. instantiate (1:=(15/2*eps+26*eps*eps)). generalize prec_suff (epsPos beta prec). generalize eps; clear. intros r H1 H2; interval_intro (/100) upper. assert (J := conj H2 (Rle_trans _ _ _ H1 H)). interval. apply M_correct_. apply err_sqrt_aux. exact H. apply Rle_lt_trans with (2:=H). apply bpow_le. rewrite <- (Zceil_IZR (emin+prec-1)) at 1. apply Zceil_le. apply Rmult_le_reg_l with 2%R. intuition. apply Rplus_le_reg_l with (-IZR (emin+prec-1)). apply Rle_trans with (IZR (emin + prec - 1));[right; ring|idtac]. apply Rle_trans with 0%R;[idtac|right;simpl;field]. apply IZR_le. lia. rewrite Rabs_right. apply Rle_lt_trans with (2:=Y). apply Rmult_le_reg_l with 4. apply Rmult_lt_0_compat; intuition. rewrite <- Rmult_assoc, Rinv_r. rewrite Rmult_1_l. apply Rle_trans with (bpow (2+(emin + prec - 1))). rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rle_trans with (IZR (radix_val beta)*IZR (radix_val beta)). apply (Rmult_le_compat 2 _ 2); try apply IZR_le; try easy; clear. apply Zle_bool_imp_le; now destruct beta. apply Zle_bool_imp_le; now destruct beta. right; simpl. unfold Zpower_pos; simpl. now rewrite mult_IZR, Zmult_1_r. apply bpow_le. apply le_IZR. apply Rle_trans with (2:=Zceil_ub _). apply Rmult_le_reg_r with 2%R. intuition. unfold Rdiv; rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r. rewrite <- mult_IZR. apply IZR_le. lia. apply Rgt_not_eq. intuition. apply Rgt_not_eq. apply Rmult_lt_0_compat; intuition. apply Rle_ge; apply FLT_pos_is_pos. apply Rmult_le_pos. apply FLT_pos_is_pos. left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1. apply FLT_pos_is_pos. apply sqrt_pos. generalize prec_suff (epsPos beta prec). cut (0 < eps). generalize eps; clear. intros r H0 H1 H2. field_simplify. apply Rmult_le_reg_r with 16. repeat apply Rmult_lt_0_compat; auto with real. unfold Rdiv; rewrite Rmult_assoc. replace (/64*16) with (/4) by field. field_simplify. unfold Rdiv; apply Rmult_le_compat_r. interval. apply Rplus_le_reg_l with (-368*r - 2431*r*r); ring_simplify. apply Rmult_le_reg_l with (/(r*r)). apply Rinv_0_lt_compat. now apply Rmult_lt_0_compat. apply Rle_trans with (10816 * r ^ 4 + 27872 * r ^ 3 + 25028 * r ^ 2 + 9944 * r -155). right; field. now apply Rgt_not_eq. apply Rle_trans with 1. 2: right; field. unfold pow; rewrite Rmult_1_r. interval_intro (/100) upper. assert (J := conj H2 (Rle_trans _ _ _ H1 H)). clear -J. interval. now apply Rgt_not_eq. apply Rmult_lt_0_compat. apply Rinv_0_lt_compat. apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1. apply bpow_gt_0. apply Rabs_right. apply Rle_ge; apply Rmult_le_pos. left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1. apply sqrt_pos. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)