Average Error: 39.5 → 15.7
Time: 6.7s
Precision: 64
\[\cos \left(x + \varepsilon\right) - \cos x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.49577892975883131 \cdot 10^{-15}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x\right) + \cos x \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 3.29102456452854126 \cdot 10^{-8}:\\ \;\;\;\;1 \cdot \left(\varepsilon \cdot \left({\varepsilon}^{3} \cdot \frac{1}{24} - \mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{log1p}\left(\log \left(e^{\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)}\right)\right)\right)\\ \end{array}\]
\cos \left(x + \varepsilon\right) - \cos x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.49577892975883131 \cdot 10^{-15}:\\
\;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x\right) + \cos x \cdot \cos x}\\

\mathbf{elif}\;\varepsilon \le 3.29102456452854126 \cdot 10^{-8}:\\
\;\;\;\;1 \cdot \left(\varepsilon \cdot \left({\varepsilon}^{3} \cdot \frac{1}{24} - \mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;1 \cdot \mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{log1p}\left(\log \left(e^{\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)}\right)\right)\right)\\

\end{array}
double f(double x, double eps) {
        double r40714 = x;
        double r40715 = eps;
        double r40716 = r40714 + r40715;
        double r40717 = cos(r40716);
        double r40718 = cos(r40714);
        double r40719 = r40717 - r40718;
        return r40719;
}
↓
double f(double x, double eps) {
        double r40720 = eps;
        double r40721 = -2.4957789297588313e-15;
        bool r40722 = r40720 <= r40721;
        double r40723 = x;
        double r40724 = cos(r40723);
        double r40725 = cos(r40720);
        double r40726 = r40724 * r40725;
        double r40727 = sin(r40723);
        double r40728 = sin(r40720);
        double r40729 = r40727 * r40728;
        double r40730 = r40726 - r40729;
        double r40731 = 3.0;
        double r40732 = pow(r40730, r40731);
        double r40733 = pow(r40724, r40731);
        double r40734 = r40732 - r40733;
        double r40735 = r40725 * r40724;
        double r40736 = r40735 - r40729;
        double r40737 = r40730 + r40724;
        double r40738 = r40736 * r40737;
        double r40739 = r40724 * r40724;
        double r40740 = r40738 + r40739;
        double r40741 = r40734 / r40740;
        double r40742 = 3.291024564528541e-08;
        bool r40743 = r40720 <= r40742;
        double r40744 = 1.0;
        double r40745 = pow(r40720, r40731);
        double r40746 = 0.041666666666666664;
        double r40747 = r40745 * r40746;
        double r40748 = 0.5;
        double r40749 = fma(r40748, r40720, r40723);
        double r40750 = r40747 - r40749;
        double r40751 = r40720 * r40750;
        double r40752 = r40744 * r40751;
        double r40753 = fma(r40727, r40728, r40724);
        double r40754 = expm1(r40753);
        double r40755 = exp(r40754);
        double r40756 = log(r40755);
        double r40757 = log1p(r40756);
        double r40758 = -r40757;
        double r40759 = fma(r40725, r40724, r40758);
        double r40760 = r40744 * r40759;
        double r40761 = r40743 ? r40752 : r40760;
        double r40762 = r40722 ? r40741 : r40761;
        return r40762;
}

Error

Bits error versus x

Bits error versus eps

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.4957789297588313e-15

    1. Initial program 31.5

      \[\cos \left(x + \varepsilon\right) - \cos x\]
    2. Using strategy rm

    3. Applied cos-sum2.1

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
    4. Using strategy rm

    5. Applied flip3--2.3

      \[\leadsto \color{blue}{\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \left(\cos x \cdot \cos x + \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) \cdot \cos x\right)}}\]

    6. Simplified2.3

      \[\leadsto \frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x\right) + \cos x \cdot \cos x}}\]

    if -2.4957789297588313e-15 < eps < 3.291024564528541e-08

    1. Initial program 48.8

      \[\cos \left(x + \varepsilon\right) - \cos x\]
    2. Using strategy rm

    3. Applied cos-sum48.6

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
    4. Using strategy rm

    5. Applied *-un-lft-identity48.6

      \[\leadsto \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \color{blue}{1 \cdot \cos x}\]

    6. Applied *-un-lft-identity48.6

      \[\leadsto \color{blue}{1 \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - 1 \cdot \cos x\]

    7. Applied distribute-lft-out--48.6

      \[\leadsto \color{blue}{1 \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x\right)}\]

    8. Simplified48.6

      \[\leadsto 1 \cdot \color{blue}{\mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)}\]

    9. Taylor expanded around 0 30.7

      \[\leadsto 1 \cdot \color{blue}{\left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(x \cdot \varepsilon + \frac{1}{2} \cdot {\varepsilon}^{2}\right)\right)}\]

    10. Simplified30.7

      \[\leadsto 1 \cdot \color{blue}{\left(\varepsilon \cdot \left({\varepsilon}^{3} \cdot \frac{1}{24} - \mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)\right)}\]

    if 3.291024564528541e-08 < eps

    1. Initial program 30.1

      \[\cos \left(x + \varepsilon\right) - \cos x\]
    2. Using strategy rm

    3. Applied cos-sum1.1

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - \cos x\]
    4. Using strategy rm

    5. Applied *-un-lft-identity1.1

      \[\leadsto \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \color{blue}{1 \cdot \cos x}\]

    6. Applied *-un-lft-identity1.1

      \[\leadsto \color{blue}{1 \cdot \left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)} - 1 \cdot \cos x\]

    7. Applied distribute-lft-out--1.1

      \[\leadsto \color{blue}{1 \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) - \cos x\right)}\]

    8. Simplified1.0

      \[\leadsto 1 \cdot \color{blue}{\mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)}\]
    9. Using strategy rm

    10. Applied log1p-expm1-u1.1

      \[\leadsto 1 \cdot \mathsf{fma}\left(\cos \varepsilon, \cos x, -\color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)\right)}\right)\]
    11. Using strategy rm

    12. Applied add-log-exp1.2

      \[\leadsto 1 \cdot \mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{log1p}\left(\color{blue}{\log \left(e^{\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)}\right)}\right)\right)\]
  3. Recombined 3 regimes into one program.

  4. Final simplification15.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.49577892975883131 \cdot 10^{-15}:\\ \;\;\;\;\frac{{\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right)}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos \varepsilon \cdot \cos x - \sin x \cdot \sin \varepsilon\right) \cdot \left(\left(\cos x \cdot \cos \varepsilon - \sin x \cdot \sin \varepsilon\right) + \cos x\right) + \cos x \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 3.29102456452854126 \cdot 10^{-8}:\\ \;\;\;\;1 \cdot \left(\varepsilon \cdot \left({\varepsilon}^{3} \cdot \frac{1}{24} - \mathsf{fma}\left(\frac{1}{2}, \varepsilon, x\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \mathsf{fma}\left(\cos \varepsilon, \cos x, -\mathsf{log1p}\left(\log \left(e^{\mathsf{expm1}\left(\mathsf{fma}\left(\sin x, \sin \varepsilon, \cos x\right)\right)}\right)\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020083 +o rules:numerics
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))