# Why do Resolve and ForAll fail with trigonometric expressions?

Why Resolve is not able to solve this problem? Similarly Solve and Reduce are not able to do it.

The first code returns back the input, the second one keeps running forever.

Resolve[ForAll[t, 2 Sin[t + 3/10] + 5 Cos[t + π/4] + Cos[t - 31/10] ==
a Sin[t] + b Cos[t]]]

Resolve[ForAll[t, 2 Sin[t + 3/10] + 5 Cos[t + π/4] + Cos[t - 31/10] ==
a Cos[b + t]], Reals]

Up to the documentation to Resolve (see the "Details" section)

Resolve[expr] can in principle always eliminate quantifiers if expr contains only polynomial equations and inequalities over the reals or complexes. Resolve[expr] can in principle always eliminate quantifiers for any Boolean expression expr.

, the commands are mainly oriented towards polynomials and Boolean expressions. In view of it we should to switch from trigonometry to polynomials by

Resolve[ForAll[{c, s}, TrigExpand[2 Sin[t + 3/10] + 5 Cos[t + \[Pi]/4] +
Cos[t - 31/10]] == a Sin[t] + b Cos[t] /. {Sin[t] -> s, Cos[t] -> c}],Reals]

5/Sqrt[2] + a - 2 Cos[1/10]^3 - 31 Cos[1/10]^30 Sin[1/10] + 6 Cos[1/10] Sin[1/10]^2 + 4495 Cos[1/10]^28 Sin[1/10]^3 - 169911 Cos[1/10]^26 Sin[1/10]^5 + 2629575 Cos[1/10]^24 Sin[1/10]^7 - 20160075 Cos[1/10]^22 Sin[1/10]^9 + 84672315 Cos[1/10]^20 Sin[1/10]^11 - 206253075 Cos[1/10]^18 Sin[1/10]^13 + 300540195 Cos[1/10]^16 Sin[1/10]^15 - 265182525 Cos[1/10]^14 Sin[1/10]^17 + 141120525 Cos[1/10]^12 Sin[1/10]^19 - 44352165 Cos[1/10]^10 Sin[1/10]^21 + 7888725 Cos[1/10]^8 Sin[1/10]^23 - 736281 Cos[1/10]^6 Sin[1/10]^25 + 31465 Cos[1/10]^4 Sin[1/10]^27 - 465 Cos[1/10]^2 Sin[1/10]^29 + Sin[1/10]^31 == 0 && -(5/Sqrt[2]) + b - Cos[1/10]^31 - 6 Cos[1/10]^2 Sin[1/10] + 465 Cos[1/10]^29 Sin[1/10]^2 + 2 Sin[1/10]^3 - 31465 Cos[1/10]^27 Sin[1/10]^4 + 736281 Cos[1/10]^25 Sin[1/10]^6 - 7888725 Cos[1/10]^23 Sin[1/10]^8 + 44352165 Cos[1/10]^21 Sin[1/10]^10 - 141120525 Cos[1/10]^19 Sin[1/10]^12 + 265182525 Cos[1/10]^17 Sin[1/10]^14 - 300540195 Cos[1/10]^15 Sin[1/10]^16 + 206253075 Cos[1/10]^13 Sin[1/10]^18 - 84672315 Cos[1/10]^11 Sin[1/10]^20 + 20160075 Cos[1/10]^9 Sin[1/10]^22 - 2629575 Cos[1/10]^7 Sin[1/10]^24 + 169911 Cos[1/10]^5 Sin[1/10]^26 - 4495 Cos[1/10]^3 Sin[1/10]^28 + 31 Cos[1/10] Sin[1/10]^30 == 0

and then

Solve[%, {a, b}, Reals]

{{a -> -(5/Sqrt[2]) + 2 Cos[1/10]^3 + 31 Cos[1/10]^30 Sin[1/10] - 6 Cos[1/10] Sin[1/10]^2 - 4495 Cos[1/10]^28 Sin[1/10]^3 + 169911 Cos[1/10]^26 Sin[1/10]^5 - 2629575 Cos[1/10]^24 Sin[1/10]^7 + 20160075 Cos[1/10]^22 Sin[1/10]^9 - 84672315 Cos[1/10]^20 Sin[1/10]^11 + 206253075 Cos[1/10]^18 Sin[1/10]^13 - 300540195 Cos[1/10]^16 Sin[1/10]^15 + 265182525 Cos[1/10]^14 Sin[1/10]^17 - 141120525 Cos[1/10]^12 Sin[1/10]^19 + 44352165 Cos[1/10]^10 Sin[1/10]^21 - 7888725 Cos[1/10]^8 Sin[1/10]^23 + 736281 Cos[1/10]^6 Sin[1/10]^25 - 31465 Cos[1/10]^4 Sin[1/10]^27 + 465 Cos[1/10]^2 Sin[1/10]^29 - Sin[1/10]^31, b -> 5/Sqrt[2] + Cos[1/10]^31 + 6 Cos[1/10]^2 Sin[1/10] - 465 Cos[1/10]^29 Sin[1/10]^2 - 2 Sin[1/10]^3 + 31465 Cos[1/10]^27 Sin[1/10]^4 - 736281 Cos[1/10]^25 Sin[1/10]^6 + 7888725 Cos[1/10]^23 Sin[1/10]^8 - 44352165 Cos[1/10]^21 Sin[1/10]^10 + 141120525 Cos[1/10]^19 Sin[1/10]^12 - 265182525 Cos[1/10]^17 Sin[1/10]^14 + 300540195 Cos[1/10]^15 Sin[1/10]^16 - 206253075 Cos[1/10]^13 Sin[1/10]^18 + 84672315 Cos[1/10]^11 Sin[1/10]^20 - 20160075 Cos[1/10]^9 Sin[1/10]^22 + 2629575 Cos[1/10]^7 Sin[1/10]^24 - 169911 Cos[1/10]^5 Sin[1/10]^26 + 4495 Cos[1/10]^3 Sin[1/10]^28 - 31 Cos[1/10] Sin[1/10]^30}}

• Finally, FullSimplify[%] results in {{a -> -(5/Sqrt[2]) + 2 Cos[3/10] + Sin[31/10], b -> 5/Sqrt[2] + Cos[31/10] + 2 Sin[3/10]}}. Commented Dec 8, 2023 at 12:57