proposition: Theorem ln_correct : forall prec, extension Xln (ln prec).
proof: Proof. intros prec [|xl xu]. easy. unfold Xln'. intros [|x]; [now unfold convert; case (_ && _)%bool|]. simpl. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; lra]. intros Vxu Vxl [Hl Hu]. case_eq (F'.lt' F.zero xl) ; intros Hlt ; [|easy]. apply F'.lt'_correct in Hlt. rewrite F.zero_correct in Hlt. simpl. set (l := lower _). set (u := if F.real xu then _ else _). assert (Vl : F.valid_lb l = true). { generalize (T.ln_fast_correct prec xl). unfold l, T.I.convert. case T.ln_fast; [now simpl; rewrite F'.valid_lb_nan|]. intros rl ru. simpl. now case F.valid_lb; [|case Xln; [|intros r [H0 H1]; lra]]. } assert (Vu : F.valid_ub u = true). { generalize (T.ln_fast_correct prec xu). unfold u, T.I.convert; simpl. rewrite F.real_correct. case F.toX; [now rewrite F'.valid_ub_nan|]. intro r. case T.ln_fast; [now simpl; rewrite F'.valid_ub_nan|]. intros rl ru. rewrite Bool.andb_comm; simpl. now case F.valid_ub; [|case Xln'; [|intros r' [H0 H1]; lra]]. } rewrite Vl, Vu; unfold l, u; clear Vl l Vu u; simpl. case is_positive_spec. intros Hx. simpl. split. generalize (T.ln_fast_correct prec xl). case T.ln_fast. intros _. simpl. now rewrite F'.nan_correct. intros l u. simpl. case_eq (Xln (F.toX xl)); [now intros _; case (_ && _)%bool|]. intros lnx Hlnx. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [H _]. destruct (F.toX l) as [|lr]. easy. apply Rle_trans with (1 := H). destruct (F.toX xl) as [|xlr]. easy. revert Hlnx. unfold Xln'. simpl. case is_positive_spec. intros _ H'. injection H'. intros <-. destruct Hl as [Hl|Hl]. now apply Rlt_le, ln_increasing. rewrite Hl. apply Rle_refl. easy. rewrite F.real_correct. case_eq (F.toX xu). now rewrite F'.nan_correct. intros xur Hxu. rewrite Hxu in Hu. generalize (T.ln_fast_correct prec xu). case T.ln_fast. intros _. simpl. now rewrite F'.nan_correct. intros l u. simpl. rewrite Hxu. unfold Xln'. simpl. case (_ && _)%bool; [|now case is_positive; [intros [H0 H1]; lra|]]. case is_positive_spec. intros _. intros [_ H]. destruct (F.toX u) as [|ur]. easy. apply Rle_trans with (2 := H). destruct Hu as [Hu|Hu]. now apply Rlt_le, ln_increasing. rewrite Hu. apply Rle_refl. easy. intros Hx. destruct (F.toX xl) as [|xlr]. easy. elim Rle_not_lt with (1 := Hx). now apply Rlt_le_trans with xlr. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend