I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. Also, the tool must be able to save a session and later prove that the given set of saved operations is valid.
Note: I am Not looking for a system to generate proofs, only that check that the steps I manually specify are valid.
I have used ACL2 for similar operations and it does well for some cases but it is very hard to use for everything else.
This little project is my motivation. It is a D template type that allows for equation solving. Given this equation:
(A * B) = C + D / F;
Any one of the symbols can be set as unknown and evaluating that expression will result an an assignment to that variable. It works by building expression trees into the type and then using rewrite rules to convert it to something that can be eventuated for the unknown type.
What I need is some way to validate the rewrite rule. They can be validated by testing the assertion that given some relation is true, another one is also.