Trigonometry B

Average Error: 0.3 → 0.4

Time: 10.8s

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}\]

↓

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

C

double f(double x) {
        double r14029 = 1.0;
        double r14030 = x;
        double r14031 = tan(r14030);
        double r14032 = r14031 * r14031;
        double r14033 = r14029 - r14032;
        double r14034 = r14029 + r14032;
        double r14035 = r14033 / r14034;
        return r14035;
}

↓

double f(double x) {
        double r14036 = x;
        double r14037 = tan(r14036);
        double r14038 = 1.0;
        double r14039 = sqrt(r14038);
        double r14040 = r14037 + r14039;
        double r14041 = r14037 * r14037;
        double r14042 = r14038 - r14041;
        double r14043 = fma(r14037, r14037, r14038);
        double r14044 = r14042 / r14043;
        double r14045 = r14039 + r14037;
        double r14046 = r14044 / r14045;
        double r14047 = r14040 * r14046;
        return r14047;
}

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. Using strategy rm

3. Applied clear-num 0.4

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

4. Simplified 0.4

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

6. Applied add-sqr-sqrt 0.4

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

7. Applied difference-of-squares 0.4

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

8. Applied *-un-lft-identity 0.4

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

9. Applied times-frac 0.4

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

10. Applied add-cube-cbrt 0.4

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

11. Applied times-frac 0.4

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

12. Simplified 0.4

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

13. Simplified 0.4

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

15. Applied flip-- 0.4

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

16. Applied associate-/r/ 0.4

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

17. Applied associate-/r* 0.4

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

18. Simplified 0.4

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

19. Final simplification 0.4

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

Reproduce

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