Deciding Equality for Trigonometric Expressions

One key to any discussion of trigonometric stuff is the Weirstrass substitution.¹ [¹ Which Wikipedia informs me was actually invented by Euler and doesn't have much to do with Weirstrass! If we didn't want to name it after Euler (reasonable) we should name it after Legendre.]

This substitution just observes the following fact. Both sin(x) and cos(x) can be rewritten as rational functions of tan(x/2). If \(t = \tan(x/2)\) then:

\[ \sin(x) = \frac{2t}{1 + t^2} \text{ and } \cos(x) = \frac{1 - t^2}{1 + t^2} \]

Moreover, tan(x/2) can take on any real value, so this is a complete parameterization.

This already suggests a decision procedure over expressions of sin(x) and cos(x): rewrite using the Weirstrass substitution and check equality by cross-multiplying, distributing, and canceling.

Now let's suppose you have multiple variables, like x, y, and so on. And let's suppose we constrain the arguments to trig functions to be rational linear combinations of those variables.

Then for each variable, we can compute the common denominator for its terms. Next, we can expand sin(a x + b y) into sin(a x) and sin(b y) and similar cosine terms, using the normal angle addition rules. Next, we can put all the coefficients into that common denominator and expand sin(a x / n) to sin(x / n), and likewise for cosine, using again the standard angle addition rules. Finally, we can apply the Weirstrass (Legendre) substitution, which finally transforms us into a rational function with a single \(t_x\) variable for each initial variable.

We can now decide equality for these rational functions, again using normal polynomial steps.

I don't have a use case for this yet, but I was delighted to be reminded of the Legendre (Weirstrass) substitution and how useful it is for all sorts of polynomial reasoning.