proposition: Theorem exp_correct : forall x : R, generic_format radix2 (FLT_exp (-1074) 53) x -> -746 <= x <= 710 -> Rabs ((cw_exp x - exp x) / exp x) <= 1 * pow2 (-51).
proof: Proof. intros x Fx Bx. generalize (argument_reduction x Fx Bx). unfold cw_exp. set (k := nearbyint (mul x InvLog2)). set (t := sub (sub x (mul k Log2h)) (mul k Log2l)). set (t2 := mul t t). intros [Bt Et]. clearbody t. generalize (method_error t Bt). intros Ef. rewrite bpow_plus, Rmult_assoc. assert (exp x = pow2 (Zfloor k) * exp (x - k * ln 2)) as ->. assert (exists k', k = IZR k') as [k' ->] by (eexists ; apply Rmult_1_r). rewrite Zfloor_IZR, bpow_exp, <- exp_plus. apply f_equal. simpl ; ring. rewrite <- Rmult_minus_distr_l. rewrite Rdiv_compat_r. 2: apply Rgt_not_eq, bpow_gt_0. 2: apply Rgt_not_eq, exp_pos. clearbody k. revert Et. generalize (x - k * ln 2). clear x Fx Bx. intros x Ex. assert (Rabs ((exp t - exp x) / exp x) <= 33 * pow2 (-60)). unfold Rdiv. rewrite Rmult_minus_distr_r. rewrite Rinv_r by apply Rgt_not_eq, exp_pos. rewrite <- exp_Ropp, <- exp_plus. revert Ex. unfold Rminus ; generalize (t + - x) ; clear. intros r Hr ; interval with (i_prec 60). apply rel_helper. apply Rgt_not_eq, exp_pos. apply rel_helper in H. 2: apply Rgt_not_eq, exp_pos. apply rel_helper in Ef. 2: apply Rgt_not_eq, exp_pos. unfold t2, add, mul, sub, div, p0, p1, p2, q0, q1, q2 in * ; gappa. Qed.
imports: Coq(Reals) Flocq(Core) Gappa(Gappa_tactic) Interval(Tactic)