News for hackers. Stuff that matters.
Re:Matrix Calculus by rav on Saturday November 18, 2017 @08:48AM (#15728914)
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"
Re:Matrix Calculus by yorwba on Saturday November 18, 2017 @09:40AM (#15729094)
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), 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?