Average Error: 15.4 → 0.4
Time: 5.3s
Precision: binary64
Cost: 6912
\[\tan^{-1} \left(N + 1\right) - \tan^{-1} N \]
↓
\[\tan^{-1}_* \frac{1}{1 + N \cdot \left(1 + N\right)} \]
(FPCore (N) :precision binary64 (- (atan (+ N 1.0)) (atan N)))
↓
(FPCore (N) :precision binary64 (atan2 1.0 (+ 1.0 (* N (+ 1.0 N)))))
double code(double N) {
	return atan((N + 1.0)) - atan(N);
}
↓
double code(double N) {
	return atan2(1.0, (1.0 + (N * (1.0 + N))));
}

real(8) function code(n)
    real(8), intent (in) :: n
    code = atan((n + 1.0d0)) - atan(n)
end function
↓
real(8) function code(n)
    real(8), intent (in) :: n
    code = atan2(1.0d0, (1.0d0 + (n * (1.0d0 + n))))
end function

public static double code(double N) {
	return Math.atan((N + 1.0)) - Math.atan(N);
}
↓
public static double code(double N) {
	return Math.atan2(1.0, (1.0 + (N * (1.0 + N))));
}

def code(N):
	return math.atan((N + 1.0)) - math.atan(N)
↓
def code(N):
	return math.atan2(1.0, (1.0 + (N * (1.0 + N))))

function code(N)
	return Float64(atan(Float64(N + 1.0)) - atan(N))
end
↓
function code(N)
	return atan(1.0, Float64(1.0 + Float64(N * Float64(1.0 + N))))
end

function tmp = code(N)
	tmp = atan((N + 1.0)) - atan(N);
end
↓
function tmp = code(N)
	tmp = atan2(1.0, (1.0 + (N * (1.0 + N))));
end

code[N_] := N[(N[ArcTan[N[(N + 1.0), $MachinePrecision]], $MachinePrecision] - N[ArcTan[N], $MachinePrecision]), $MachinePrecision]
↓
code[N_] := N[ArcTan[1.0 / N[(1.0 + N[(N * N[(1.0 + N), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]

\tan^{-1} \left(N + 1\right) - \tan^{-1} N
↓
\tan^{-1}_* \frac{1}{1 + N \cdot \left(1 + N\right)}

Error

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original15.4
Target0.4
Herbie0.4
\[\tan^{-1} \left(\frac{1}{1 + N \cdot \left(N + 1\right)}\right) \]

Derivation

  1. Initial program 15.4

    \[\tan^{-1} \left(N + 1\right) - \tan^{-1} N \]

  2. Applied egg-rr14.1

    \[\leadsto \color{blue}{\tan^{-1}_* \frac{N + \left(1 - N\right)}{1 + N \cdot \left(N + 1\right)}} \]

  3. Simplified14.1

    \[\leadsto \color{blue}{\tan^{-1}_* \frac{\left(N + 1\right) - N}{1 + N \cdot \left(N + 1\right)}} \]
    Proof
    (atan2.f64 (-.f64 (+.f64 N 1) N) (+.f64 1 (*.f64 N (+.f64 N 1)))): 0 points increase in error, 0 points decrease in error
    (atan2.f64 (Rewrite<= associate-+r-_binary64 (+.f64 N (-.f64 1 N))) (+.f64 1 (*.f64 N (+.f64 N 1)))): 1 points increase in error, 0 points decrease in error

  4. Applied egg-rr14.1

    \[\leadsto \tan^{-1}_* \frac{\color{blue}{N + \left(1 - N\right)}}{1 + N \cdot \left(N + 1\right)} \]

  5. Simplified0.4

    \[\leadsto \tan^{-1}_* \frac{\color{blue}{1}}{1 + N \cdot \left(N + 1\right)} \]
    Proof
    1: 0 points increase in error, 0 points decrease in error
    (Rewrite<= metadata-eval (-.f64 1 0)): 0 points increase in error, 0 points decrease in error
    (-.f64 1 (Rewrite<= +-inverses_binary64 (-.f64 N N))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 1 N) N)): 27 points increase in error, 89 points decrease in error
    (Rewrite<= +-commutative_binary64 (+.f64 N (-.f64 1 N))): 0 points increase in error, 0 points decrease in error

  6. Final simplification0.4

    \[\leadsto \tan^{-1}_* \frac{1}{1 + N \cdot \left(1 + N\right)} \]

Reproduce

herbie shell --seed 2022334 
(FPCore (N)
  :name "2atan (example 3.5)"
  :precision binary64

  :herbie-target
  (atan (/ 1.0 (+ 1.0 (* N (+ N 1.0)))))

  (- (atan (+ N 1.0)) (atan N)))