proposition: Lemma ln_fast1P_correct : forall prec xi x, (1 <= x)%R -> contains (I.convert xi) (Xreal x) -> contains (I.convert (ln_fast1P prec xi)) (Xreal (ln x)).
proof: Proof. set (thre := c1_p_c1_8). assert (H: forall prec xi x, (1 <= x)%R -> (F'.le' (I.upper xi) thre = true) -> contains (I.convert xi) (Xreal x) -> contains (I.convert (ln1p_fast0 prec (I.sub prec xi i1))) (Xreal (ln x))). intros prec xi x Hx Hxu Ix. replace x with (1 + (x - 1))%R by ring. apply ln1p_fast0_correct. split. lra. apply F'.le'_correct in Hxu. rewrite I.upper_correct in Hxu; [|now exists x]. destruct (I.convert xi) as [|l [|u]] ; try easy. revert Hxu. simpl. unfold thre, c1_p_c1_8, c1. elim (F.add_DN_correct (F.PtoP 52) (F.fromZ 1) c1_8). 2: apply F'.valid_lb_real ; now rewrite F.real_correct, F.fromZ_correct. 2: apply F'.valid_lb_real ; now rewrite F.real_correct, c1_8_correct. intros Va. case (F.toX _) ; [easy|intro r]. rewrite c1_8_correct, F.fromZ_correct by easy. simpl. intro Hr. apply Ropp_le_cancel in Hr. intro H. assert (H' : (u <= 1 + / 256)%R). { now apply (Rle_trans _ _ _ H). } generalize (proj2 Ix). lra. apply J.sub_correct with (1 := Ix). now apply I.fromZ_small_correct. intros prec xi x Hx Ix. unfold ln_fast1P. fold thre. case_eq (F'.le' (I.upper xi) thre) ; intros Hxu. now apply H. clear Hxu. set (m := Zdigits2 (F.StoZ (F.mag (I.upper xi)))). clearbody m. generalize (F.incr_prec prec 10). clear prec; intro prec. generalize (8 + Z2nat m). intro nb. revert xi x Hx Ix. induction nb as [|nb] ; intros xi x Hx Ix. simpl. case_eq (F'.le' (I.upper xi) thre) ; intros Hxu. now apply H. simpl. rewrite F.zero_correct, F'.nan_correct. rewrite F'.valid_lb_zero, F'.valid_ub_nan. refine (conj _ I). destruct (Rlt_dec 1 x) as [Hx'|Hx']. rewrite <- ln_1. apply Rlt_le, ln_increasing. exact Rlt_0_1. exact Hx'. replace x with 1%R by lra. rewrite ln_1. apply Rle_refl. case_eq (F'.le' (I.upper xi) thre) ; intros Hxu. now apply H. clear H Hxu. replace (ln x) with (ln (sqrt x) * 2)%R. change (Xreal (ln (sqrt x) * 2)) with (Xmul (Xreal (ln (sqrt x))) (Xreal (bpow radix2 1))). apply I.mul2_correct. apply IHnb. clear IHnb. rewrite <- sqrt_1. now apply sqrt_le_1_alt. now apply J.sqrt_correct. rewrite <- (sqrt_sqrt x) at 2 by lra. assert (0 < sqrt x)%R. apply sqrt_lt_R0. lra. rewrite ln_mult by easy. ring. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float