How could I implement a program that takes in the two sides of a trig equation (could be generalized to anything but for now I'll leave it at just trig identities) and the program will output the steps to transform one side into another (or transform them both) to show that they are in fact equal. The program will assume that they are equal in the first place. I am quite stumped as to how I might implement an algorithm to do this. My first thought was something to do with graphs, but I couldn't think of anything beyond this. From there, I thought that I should first parse both sides of the equation into trees. For example (cot x * sin) / (sin x + cos x) would look like this:
division
/ \
* +
/ \ / \
cot sin sin cos
After this, I had two similar ideas, both of which have problems. The first idea was to pick the side with the least number of leaves and try to manipulate it into the other side by using equivalencies that would be represented by "tree regexs." Examples of these "tree regexs" would be csc = 1 / sin or cot = cos / sin (in tree form of course), etc. My second idea would be to pick the side with more leaves and try to find some expression that when multiplied by that expression would equal the other side. Using reciprocals this wouldn't be too bad, however, I would then have to prove that the thing I multiplied by equals 1. Again I am back to this "tree regex" thing.
The major flaw with both of these is in what order/how could I apply these substitutions. Will it just have to be a big mess of if statements or is there a more elegant solution? Is there actually a graph-based solution that I'm not seeing. What (if any) might be a good algorithm to prove trig identities.
To be clear I am not talking about the "solve for x" type problem such as tan(x)sin(x) = 5, find all values of x but rather prove that sqrt((1 + sin x) / (1 - sin x)) = sec x + tan x
Look out for texts on computer algebra (which I haven't), I'm sure you'll find clever ideas there.
My approach would be a graph-based search, as I doubt that a linear application of transformations will reliably lead to a solution.
Express the whole equation as an expression-tree the way you already started, but including an "equals" node above.
For the search-graph view, take one expression-tree as one search-state. The search-target is a decidable expression-tree like 1=1 or 1=0. When searching (expanding a search-state), create the child states by applying equivalence transformations on your expression (regex-like sounds quite plausible to me). Define an evaluation function that counts the overall complexity of an expression (e.g. number of nodes in the expression-tree). Do a directed search minimizing the evaluation function (expanding the lowest-complexity expression first), thus simplifying the expression until you reach a decidable form.
Depending on the expressions, it's quite possible that an unrestricted search never terminates. I don't know how you'd handle that, maybe by limiting the allowed complexity of expressions to some multiple of the original one. That would reduce the risk of running indefinitely, but leave you with undecided cases.