proposition: Lemma Delta_correct_2_ : radix_val beta=2%Z -> bpow (Zceil ((IZR (emin+prec-1))/2) -2) < Delta -> (Rabs (Delta - E_Delta) <= (19/4*eps+33*eps*eps) * E_Delta).
proof: Proof. Proof with auto with typeclass_instances. intros Hradix 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 generic_format_bpow. unfold FLT_exp. rewrite Z.max_l. lia. cut (emin+prec+1 <= Zceil (IZR (emin + prec - 1) / 2))%Z. lia. 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). unfold Zminus; rewrite Rmult_comm, bpow_plus. replace (bpow (-(2))) with (/4). apply Rmult_le_compat_r. left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; intuition. exact Y1. simpl; apply f_equal; unfold Zpower_pos; simpl. rewrite Hradix; simpl; ring. apply sym_eq, round_generic... apply fourth_format. replace Delta with (/ 4 * round_flt (sqrt M)). pattern E_Delta at 2; replace E_Delta with (Rabs E_Delta). apply err_mult_exact. apply Rmult_lt_0_compat; auto with real. eapply err_aux. 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. 2: apply M_correct_. 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 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. 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 (-304*r - 2111*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 ^ 3 + 17056 * r ^ 2 + 7972 * r -139). 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. apply trans_eq with (round_flt (/ 4 * round_flt (sqrt M))). apply sym_eq, round_generic... apply generic_format_FLT. assert (format (round_flt (sqrt M))). apply generic_format_round... apply FLT_format_generic in H0... destruct H0 as [f Hf1 Hf2 Hf3]. exists (Float beta (Fnum f) (Fexp f -2)). rewrite Hf1; unfold F2R; simpl. unfold Zminus;rewrite bpow_plus. replace (bpow (-(2))) with (/4). ring. simpl; unfold Zpower_pos;simpl. rewrite Hradix; apply f_equal. simpl; ring. now simpl. simpl. assert (emin+1+prec < prec+Fexp f)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (bpow (Zceil (IZR (emin + prec - 1) / 2))). 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 Rlt_le_trans with (1:=H). rewrite Hf1. apply Rle_trans with (1:=RRle_abs _). rewrite <- F2R_abs. unfold F2R; rewrite bpow_plus. replace (Fexp (Fabs f)) with (Fexp f). apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- IZR_Zpower. left; apply IZR_lt. replace (Fnum (Fabs f)) with (Z.abs (Fnum f)). assumption. destruct f; unfold Fabs; reflexivity. lia. destruct f; unfold Fabs; reflexivity. apply f_equal. apply f_equal2. apply sym_eq, round_generic... apply fourth_format. reflexivity. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)