Average Error: 36.9 → 13.0
Time: 32.8s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - {\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)}^{3}}, 1 + \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x} + \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)\right), \frac{-\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \sin x}{\cos x}}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - {\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)}^{3}}, 1 + \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x} + \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)\right), \frac{-\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \sin x}{\cos x}}
double f(double x, double eps) {
        double r121736 = x;
        double r121737 = eps;
        double r121738 = r121736 + r121737;
        double r121739 = tan(r121738);
        double r121740 = tan(r121736);
        double r121741 = r121739 - r121740;
        return r121741;
}
↓
double f(double x, double eps) {
        double r121742 = x;
        double r121743 = sin(r121742);
        double r121744 = cos(r121742);
        double r121745 = r121743 / r121744;
        double r121746 = 1.0;
        double r121747 = eps;
        double r121748 = sin(r121747);
        double r121749 = cos(r121747);
        double r121750 = r121748 / r121749;
        double r121751 = r121750 * r121745;
        double r121752 = 3.0;
        double r121753 = pow(r121751, r121752);
        double r121754 = r121746 - r121753;
        double r121755 = r121745 / r121754;
        double r121756 = r121751 * r121751;
        double r121757 = r121751 + r121756;
        double r121758 = r121746 + r121757;
        double r121759 = -r121743;
        double r121760 = r121759 / r121744;
        double r121761 = fma(r121755, r121758, r121760);
        double r121762 = r121750 * r121743;
        double r121763 = r121762 / r121744;
        double r121764 = r121746 - r121763;
        double r121765 = r121750 / r121764;
        double r121766 = r121761 + r121765;
        return r121766;
}

Error

Bits error versus x

Bits error versus eps

Target

Original36.9
Target15.3
Herbie13.0
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Initial program 36.9

    \[\tan \left(x + \varepsilon\right) - \tan x\]

  2. Simplified36.9

    \[\leadsto \color{blue}{\tan \left(\varepsilon + x\right) - \tan x}\]
  3. Using strategy rm

  4. Applied tan-sum21.5

    \[\leadsto \color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x}} - \tan x\]

  5. Simplified21.5

    \[\leadsto \frac{\tan \varepsilon + \tan x}{\color{blue}{\mathsf{fma}\left(-\tan \varepsilon, \tan x, 1\right)}} - \tan x\]

  6. Taylor expanded around inf 21.6

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

  7. Simplified13.0

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

  8. Taylor expanded around inf 13.0

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

  9. Simplified13.0

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

  11. Applied flip3--13.0

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

  12. Applied associate-/r/13.0

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

  13. Applied fma-neg13.0

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

  14. Simplified13.0

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

  15. Final simplification13.0

    \[\leadsto \mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - {\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)}^{3}}, 1 + \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x} + \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right)\right), \frac{-\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \sin x}{\cos x}}\]

Reproduce

herbie shell --seed 2019174 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))