proposition: Theorem ln_fast_correct : forall prec x, contains (I.convert (ln_fast prec x)) (Xln (F.toX x)).
proof: Proof. intros prec x. unfold ln_fast. rewrite F.cmp_correct, F.zero_correct, F'.classify_zero. generalize (F.classify_correct x); rewrite F.real_correct. case_eq (F.classify x); intro Cx; [|easy..|]; [case_eq (F.toX x); [easy|]; intros rx Hrx _ |case_eq (F.toX x); [|easy]; intros Hx _]. { unfold Xcmp, c1. case Rcompare_spec; intro Hrx0; [easy..|]. rewrite F.cmp_correct, Cx, Hrx. generalize (F.classify_correct (F.fromZ 1)). rewrite F.real_correct, F.fromZ_correct by easy. case F.classify; [|easy..]; intros _. unfold Xcmp. case Rcompare_spec. { intros Hx'. generalize (F.incr_prec prec (Z2P (Z.opp (F.StoZ (F.mag (F.sub_UP prec (F.fromZ 1) x)))))). intros prec'. rewrite <- (Rinv_involutive rx); [|lra]. unfold Xln, Xln'. rewrite ln_Rinv; [|now apply Rinv_0_lt_compat]. rewrite is_positive_true; [|now do 2 apply Rinv_0_lt_compat]. apply J.neg_correct. apply ln_fast1P_correct. { rewrite <- Rinv_1. apply Rinv_le. { exact Hrx0. } now apply Rlt_le. } apply J.inv_correct. rewrite I.bnd_correct, Hrx. { split ; apply Rle_refl. } { now apply I.valid_lb_real; rewrite Hrx. } now apply I.valid_ub_real; rewrite Hrx. } { intros ->. unfold Xln, Xln'. rewrite is_positive_true; [|lra]. rewrite I.zero_correct, ln_1. split ; apply Rle_refl. } intros Hx'. unfold Xln, Xln'. rewrite is_positive_true; [|lra]. apply ln_fast1P_correct. { now apply Rlt_le. } rewrite I.bnd_correct, Hrx. { split ; apply Rle_refl. } { now apply I.valid_lb_real; rewrite Hrx. } now apply I.valid_ub_real; rewrite Hrx. } rewrite F.cmp_correct, Cx. unfold c1. generalize (F.classify_correct (F.fromZ 1)). rewrite F.real_correct, F.fromZ_correct by easy. now case F.classify. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float