Trigonometry B

Average Error: 0.3 → 0.4

Time: 11.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]

↓

\[\frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\log \left(e^{\tan x + \sqrt{1}}\right)}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

C

double f(double x) {
        double r13501 = 1.0;
        double r13502 = x;
        double r13503 = tan(r13502);
        double r13504 = r13503 * r13503;
        double r13505 = r13501 - r13504;
        double r13506 = r13501 + r13504;
        double r13507 = r13505 / r13506;
        return r13507;
}

↓

double f(double x) {
        double r13508 = 1.0;
        double r13509 = sqrt(r13508);
        double r13510 = x;
        double r13511 = tan(r13510);
        double r13512 = r13509 + r13511;
        double r13513 = r13511 * r13511;
        double r13514 = r13508 - r13513;
        double r13515 = r13511 + r13509;
        double r13516 = exp(r13515);
        double r13517 = log(r13516);
        double r13518 = r13514 / r13517;
        double r13519 = r13512 * r13518;
        double r13520 = fma(r13511, r13511, r13508);
        double r13521 = r13519 / r13520;
        return r13521;
}

Error

Bits error versus x

Derivation

1. Initial program 0.3

   \[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]

2. Simplified 0.3

   \[\leadsto \color{blue}{\frac{1 - \tan x \cdot \tan x}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}}\]
3. Using strategy rm

4. Applied *-un-lft-identity 0.3

   \[\leadsto \frac{1 - \tan x \cdot \tan x}{\color{blue}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}}\]
5. Using strategy rm

6. Applied add-sqr-sqrt 0.3

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

7. Applied difference-of-squares 0.3

   \[\leadsto \frac{\color{blue}{\left(\sqrt{1} + \tan x\right) \cdot \left(\sqrt{1} - \tan x\right)}}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}\]
8. Using strategy rm

9. Applied flip-- 0.3

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

10. Simplified 0.3

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

11. Simplified 0.3

    \[\leadsto \frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\color{blue}{\tan x + \sqrt{1}}}}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}\]
12. Using strategy rm

13. Applied add-log-exp 0.3

    \[\leadsto \frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\tan x + \color{blue}{\log \left(e^{\sqrt{1}}\right)}}}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

14. Applied add-log-exp 0.4

    \[\leadsto \frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\color{blue}{\log \left(e^{\tan x}\right)} + \log \left(e^{\sqrt{1}}\right)}}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

15. Applied sum-log 0.5

    \[\leadsto \frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\color{blue}{\log \left(e^{\tan x} \cdot e^{\sqrt{1}}\right)}}}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

16. Simplified 0.4

    \[\leadsto \frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\log \color{blue}{\left(e^{\tan x + \sqrt{1}}\right)}}}{1 \cdot \mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

17. Final simplification 0.4

    \[\leadsto \frac{\left(\sqrt{1} + \tan x\right) \cdot \frac{1 - \tan x \cdot \tan x}{\log \left(e^{\tan x + \sqrt{1}}\right)}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

Reproduce

herbie shell --seed 2019350 +o rules:numerics
(FPCore (x)
  :name "Trigonometry B"
  :precision binary64
  (/ (- 1 (* (tan x) (tan x))) (+ 1 (* (tan x) (tan x)))))