proposition: Theorem exp_correct : forall prec, extension Xexp (exp prec).
proof: Proof. intros prec [|xl xu]. easy. intros [|x]. now simpl; case (_ && _)%bool. unfold convert at 1. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; lra]. intros Vxu Vxl [Hxl Hxu]. simpl. set (l := if F.real xl then _ else _). set (u := if F.real xu then _ else _). assert (Vl : F.valid_lb l = true). { unfold l. rewrite F.real_correct. generalize (T.exp_fast_correct prec xl). case F.toX. { now simpl; rewrite F'.valid_lb_zero. } intro rxl. unfold T.I.convert. simpl. case T.exp_fast. { now simpl; rewrite F'.valid_lb_nan. } intros rl ru. simpl. now case F.valid_lb; [|intros [H0 H1]; lra]. } assert (Vu : F.valid_ub u = true). { unfold u. rewrite F.real_correct. generalize (T.exp_fast_correct prec xu). case F.toX. { now rewrite F'.valid_ub_nan. } intro rxu. unfold T.I.convert. simpl. case T.exp_fast. { now simpl; rewrite F'.valid_ub_nan. } intros rl ru. simpl; rewrite Bool.andb_comm. now case F.valid_ub; [|intros [H0 H1]; lra]. } rewrite Vl, Vu; unfold l, u. split. clear Hxu. rewrite F.real_correct. xreal_tac xl. rewrite F.zero_correct. simpl. apply Rlt_le. apply exp_pos. generalize (T.exp_fast_correct prec xl). destruct (T.exp_fast prec xl) as [|yl yu]. unfold lower. now rewrite F'.nan_correct. rewrite X. unfold T.I.convert. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros (H, _). simpl. xreal_tac2. apply Rle_trans with (1 := H). now apply Raux.exp_le. clear Hxl. rewrite F.real_correct. xreal_tac xu. now rewrite F'.nan_correct. generalize (T.exp_fast_correct prec xu). destruct (T.exp_fast prec xu) as [|yl yu]. unfold upper. now rewrite F'.nan_correct. rewrite X. unfold T.I.convert. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros (_, H). simpl. xreal_tac2. apply Rle_trans with (2 := H). now apply Raux.exp_le. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend