Sympy Equation Mathematical Equality?

Question

I'm trying to compare two equations to determine if they're mathematically equivalent using SymPy. For example, I have the string 2y = x^2 + x and I want to see if it is mathematically equivalent to y = x^2 + 2x - x - y (with some basic algebra you can see that they are). This doesn't have to be mathematically rigorous, just something that handles a vast majority of relatively simple cases.

Another constraint I have is that I don't necessarily know the variable names present in the string. It could have x, it could have y, it could have t, etc. etc. since I am creating a front-serving service, and I don't want users to have to worry about these definitions.

I know when comparing expressions, the best-practice way is to use .equals() or sympify(Ex2 - Ex1)==0. However, I don't think it is so simple when dealing with equations, since you have to deal with proportionality and other cases (e.g, x=2y is the same as 2x=4y). Another way I saw online to handle comparing expressions is to brute-force a bunch of numbers and see if it works out. How would I go about implementing this for equations? Especially since I don't know what the names of my variables will be? Is there a way to programmatically determine what the variables are?

EDIT FOR REVIEW: My question is unique, because the one that was linked is about evaluating equivalent expressions. This is subtly but significantly different than evaluating equivalent equations in my opinion, and it is not clear from those answers how to solve my problem.

Answer 1

The answer to the question patterned after this one gives a good solution that will probably solve most of your needs. It suggests comparing the monic forms of the expressions that you parse.

The monic form makes the coefficient on the leading term term equal to 1 after expanding. So if you have two polynomial expressions, a and b and they are the same except for a multiplicative number, then monic(a) == monic(b) will be True if they are the same.

Since you are working with equations (which allows you to ignore multiplicative constant appearing on both side of the equation), you will need to do monic(a.rewrite(Add)) == monic(b.rewrite(Add)) to get the Eq instances expressed as sums -- and because of the action of monic it will not matter on which side of the equal sign a given term appears since for Eq(L, R), monic(L - R) == monic(R - L).

I'm not sure in what context you are making these comparisons, but since you are parsing strings it seems like you might be checking input from users (expecially since you said that you wouldn't know what the free symbols were). If so, you might want to align the symbols in both expressions before making the comparison. Assuming the number of symbols is small, we are looking for a permutation of symbols that will allow the two expressions to compare as equal. Something like the following might be useful for checking the parsed expressions:

def are_same(a, b):
    """return True if a and b represent the same polynomial
    except for a change of variables and elimination of a
    multiplicative constant. The dictionary included will
    indicate any variables that were changed. If the expressions
    are not the same, then False is returned.

    The input expressions can be instances of Eq or Expr.

    Examples
    ========

    >>> are_same(x**3 + 2*y, 2*x + y**3)
    True, {x: y, y: x}
    """
    from sympy.utilities.iterables import permutations
    from sympy.polys.polytools import monic
    from sympy.core.add import Add
    a, b = a.rewrite(Add), b.rewrite(Add)
    afree = a.free_symbols
    bfree = b.free_symbols
    if len(afree) != len(bfree):
        return False
    ma = monic(a)
    for bi in permutations(bfree):
        reps = dict(zip(afree, bi))
        if ma == monic(b.subs(reps, simultaneous=True)):
            return True, {i:j for i,j in reps.items() if i!=j}
    return False

Answer 2

I think (not sure) this is a simple problem of Gröbner reduction. You can do it with Xcas, R, probably Sage, and maybe Python. I'm using R.

One has to apply the Gröbner reduction two times. First write your expressions as P1(x,y)=0 and P2(x,y)=0. The first result below shows that P1 is in the ideal generated by P2. The second result shows the converse.

library(giacR)

giac <- Giac$new()

command <- "greduce(2*y - x^2 - x, [y - x^2 - 2x + x + y], [x, y])"
giac$execute(command)
# this gives 0

command <- "greduce(y - x^2 - 2x + x + y, [2*y - x^2 - x], [x, y])"
giac$execute(command)
# this gives 0

giac$close()

It also works for your example x=2y and 2x=4y.

One constraint though is that you have to deal with polynomial expressions only.