Standard trig identity isn't simplifying

Question

Mathematica isn't recognizing that both

FullSimplify[2 ArcTan[x + Sqrt[1 + x^2]] == Pi - ArcCot[x], x > 0]

and

FullSimplify[2 ArcTan[x + Sqrt[1 + x^2]] == -ArcCot[x], x < 0]

can simplify to True. Is there any way for me to tell it to perform this simplification, e.g. when expressions similar to 2 ArcTan[x + Sqrt[1 + x^2]] appear in more complicated expressions? (Obviously I could set up a transformation rule, but that would miss, say, expressions that don't have the prefactor of 2.)

Answer 1

Simplification of expressions is not trivial. Even stronger, in general it seems to be impossible.

My understanding is based on what I learned a very long time ago from Andrzej Kozlowski in the oldest discussion group on Mathematica, MathGroup. At the moment I would formulate it as follows.

Consider the set of all expressions that are equal to zero. For every algorithm that can reduce expressions to zero, there is an expression for which the algorithm will fail.

Every function for simplification can only contain a finite set of algorithms. In Mathematica we even have two functions for simplification: Simplify and FullSimplify. The first one contains less algorithms and has a smaller TimeConstrained than the second one. But due to the above observation, for each of these functions examples exist for which the function will fail. That is not a bug in Mathematica!

Unfortunately, I cannot find back Andrzej's message in MathGroup. I remember having seen that he has given a link to the above theoretical result, found about 50 years ago. Hopefully I am not mislead by my memory. But even if I am wrong, I think that simplification is so complicated that for every algorithm there will exist examples for which the algorithm does not work in practice.

It seems to me that your example is one of those exceptions for Simplify and FullSimplify. It is extra complicated because of the conditions x>0 and x<0.

You can find many examples in MathGroup and SE Mathematica where (Full)Simplify fails. Here is another one:

expr= With[{z=1/(x^7+1)}, D[Integrate[z, x], x]-z]

(* fairly long expression *)

Obviously, this expression equals zero. But FullSimplify cannot show that directly:

FullSimplify[expr] // Timing

(* {1499.48, long expression} *)

On the other hand, we can reduce the expression to zero:

FullSimplify[TrigToExp[expr]] // Timing

(* {0.4375,0} *)

By first applying TrigToExp, the expression becomes more complex. After that, FullSimplify can do the job. Have a look at this link.

For your example, I could not find a similar trick. Pretty close:

FullSimplify[Exp[I(2 ArcTan[x+Sqrt[1+x^2]]+ ArcCot[x])], x<0]

(* 1 *)

Given that your expression is between -π/2 and 3π/2, it follows that your expression equals 0.