4 ms·

SymPy does not take Latex as input, but it has symbolic equivalence checkers. Methods are highly heuristic, and some languages (all expressions with,say, \pi

SymPy does not take Latex as input, but it has symbolic equivalence checkers. Methods are highly heuristic, and some languages (all expressions with,say, \pi, and exp function, or something similar) are in general undecidable.

rav 9y ago
To elaborate: Symbolic equivalence checking for two expressions f1 and f2 can be done by seeing if sympy.simplify(sympy.Eq(f1, f2)) is sympy.true. import sympy from sympy.abc import x, y, alpha, s quad = s ** 2 - alpha * s - 2 # Let s1 and s2 be the two solutions to the quadratic equation 'quad == 0' s1, s2 = sympy.solve(quad, s) u = (x - s2) / (x - s1) * (y - s1) / (y - s2) f1 = (s2 - s1 * u) / (1 - u) f2 = (x * y - alpha * x - 2) / (y - x) # Claim: f1 is equal to f2 print(sympy.simplify(sympy.Eq(f1, f2))) # Prints "True"
- yorwba 9y ago
  Is there something for implication or equivalence of equations? I was trying the example from Smaug123's sibling comment (https://news.ycombinator.com/item?id=15728598 https://news.ycombinator.com/item?id=15728598), but >>> import sympy as sp >>> x = sp.Symbol('x') >>> sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1))) Eq(x, -1) | Ne(x**2 + 2*x + 1, 0) >>> sp.solve(sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1)))) Traceback (most recent call last): File "<stdin>", line 1, in <module> File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1065, in solve solution = _solve(f[0], *symbols, **flags) File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1401, in _solve f_num, sol = solve_linear(f, symbols=symbols) File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1971, in solve_linear eq = lhs - rhs TypeError: unsupported operand type(s) for -: 'Or' and 'int' >>> sp.solveset(sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1)))) Traceback (most recent call last): File "<stdin>", line 1, in <module> File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solveset.py", line 880, in solveset raise ValueError("%s is not a valid SymPy expression" % (f)) ValueError: Eq(x, -1) | Ne(x**2 + 2*x + 1, 0) is not a valid SymPy expression none of the obvious ways appear to work. Does Sympy not support this kind of equational reasoning?

rav 9y ago

To elaborate: Symbolic equivalence checking for two expressions f1 and f2 can be done by seeing if sympy.simplify(sympy.Eq(f1, f2)) is sympy.true. import sympy from sympy.abc import x, y, alpha, s quad = s ** 2 - alpha * s - 2 # Let s1 and s2 be the two solutions to the quadratic equation 'quad == 0' s1, s2 = sympy.solve(quad, s) u = (x - s2) / (x - s1) * (y - s1) / (y - s2) f1 = (s2 - s1 * u) / (1 - u) f2 = (x * y - alpha * x - 2) / (y - x) # Claim: f1 is equal to f2 print(sympy.simplify(sympy.Eq(f1, f2))) # Prints "True"

yorwba 9y ago
Is there something for implication or equivalence of equations? I was trying the example from Smaug123's sibling comment (https://news.ycombinator.com/item?id=15728598 https://news.ycombinator.com/item?id=15728598), but >>> import sympy as sp >>> x = sp.Symbol('x') >>> sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1))) Eq(x, -1) | Ne(x**2 + 2*x + 1, 0) >>> sp.solve(sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1)))) Traceback (most recent call last): File "<stdin>", line 1, in <module> File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1065, in solve solution = _solve(f[0], *symbols, **flags) File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1401, in _solve f_num, sol = solve_linear(f, symbols=symbols) File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1971, in solve_linear eq = lhs - rhs TypeError: unsupported operand type(s) for -: 'Or' and 'int' >>> sp.solveset(sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1)))) Traceback (most recent call last): File "<stdin>", line 1, in <module> File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solveset.py", line 880, in solveset raise ValueError("%s is not a valid SymPy expression" % (f)) ValueError: Eq(x, -1) | Ne(x**2 + 2*x + 1, 0) is not a valid SymPy expression none of the obvious ways appear to work. Does Sympy not support this kind of equational reasoning?