proposition: Lemma expn_reduce_correct : forall prec x, F.toX x = Xreal (toR x) -> (0 < toR x)%R -> contains (I.convert (expn_reduce prec x)) (Xreal (exp (- toR x))).
proof: Proof. assert (forall prec x, F.toX x = Xreal (toR x) -> (0 < toR x)%R -> F'.le' x c1_8 = true -> contains (I.convert (expn_fast0 prec x)) (Xreal (exp (- toR x)))). { intros prec x Hx1 Hx2 Hx3. apply expn_fast0_correct. { exact Hx1. } split. { now apply Rlt_le. } apply F'.le'_correct in Hx3. revert Hx3. rewrite Hx1. rewrite c1_8_correct. lra. } intros prec x Hx H0. unfold expn_reduce. case_eq (F'.le' x c1_8) ; intros Hx'. { now apply H. } clear Hx'. generalize (F.incr_prec prec (Z2P (9 + F.StoZ (F.mag x)))). clear prec. intro prec. generalize (8 + Z2nat (F.StoZ (F.mag x))). intro nb. revert x Hx H0. induction nb ; intros ; simpl. { case_eq (F'.le' x c1_8) ; intros Hx'. { now apply H. } simpl. unfold c1. rewrite F'.valid_lb_zero. rewrite F'.valid_ub_real by now rewrite F.real_correct, F.fromZ_correct. rewrite F.zero_correct, F.fromZ_correct by easy. split. { apply Rlt_le. apply exp_pos. } simpl. rewrite <- exp_0. apply Rlt_le. apply exp_increasing. rewrite <- Ropp_0. now apply Ropp_lt_contravar. } case_eq (F'.le' x c1_8) ; intros Hx'. { now apply H. } assert (1 / 256 <= Rabs (F.toR x))%R. { rewrite (Rabs_pos_eq _ (Rlt_le _ _ H0)). revert Hx'. unfold F'.le'. rewrite F'.cmp_correct. rewrite Hx. rewrite c1_8_correct. unfold Rdiv; rewrite Rmult_1_l. simpl. now case Rcompare_spec; [easy..|]; intros H' _; apply Rlt_le. } assert (toR (F.div2 x) = toR x * /2)%R. { unfold toR; rewrite F.div2_correct; [|easy..]. rewrite Xdiv_split; simpl; unfold Xinv'; rewrite is_zero_false; [|easy]. rewrite Hx; simpl; lra. } replace (toR x) with (toR (F.div2 x) + toR (F.div2 x))%R. { rewrite Ropp_plus_distr. rewrite exp_plus. change (Xreal (exp (- toR (F.div2 x)) * exp (- toR (F.div2 x)))) with (Xsqr (Xreal (exp (- toR (F.div2 x))))). apply I.sqr_correct. apply IHnb. { unfold F.toR; rewrite F.div2_correct; [|easy..]. rewrite Xdiv_split; simpl; unfold Xinv'; rewrite is_zero_false; [|easy]. now rewrite Hx. } rewrite H2; lra. } rewrite H2. apply sym_eq, double_var. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float