SymPy had implemented the binary relation as Relational class in core/relation module. In this document, I propose a new system which implements general binary relation as Predicate which is defined in assumptions module.

Since predicates are registered on Q such as Q.positive, I will call the relational predicate as Q.eq, Q.gt, etc in this document. Please note that registering the predicate on Q is not mandatory, and these predicates can have different name when SymPy 1.8 is released. After a few releases, relation predicates will completely replace relational classes so that Eq, Gt, etc return Q.eq, Q.gt, etc.

Why do we need relation predicates?

There are two design shifts that need to be done across the SymPy codebase. First, we need to avoid automatic evaluation, which means Add(x, x) should return Add instance rather than 2*x. This is because evaluating the non-evaluated expression can always be easily done, but doing it vice versa is very difficult. Matrices module adopts this idea. With matrix A, A + A is evaluated to 2*A but Add(A, A) is not evaluated - and we need to make every object behave like this. Second, functions should be object. This allows the function itself to be dealt as a separate entity.

Predicate in assumption module is a good example for these designs. Predicate like Q.positive is an object, and Q.positive(x) returns AppliedPredicate instance. Unlike Eq(x, x) which automatically evaluates to true, Q.eq(x, x) is not evaluated unless passed to ask() or refine() functions. Q.positive itself can be an argument of other SymPy class to form a tree structure. Most importantly, Predicate supports fact management system and sat solver. With relation predicate, we can make ask(Q.extended_real(x), Q.gt(x, y)) return True by adding this rule to known facts. Relational classes cannot support this properly. In fact, relational classes cannot even be proposed nor assumed without being wrapped by Q.is_true predicate like Q.is_true(Eq(x, y)). Using relation predicate instead of relational class gets rid of this nuisance.

Evaluation of relation predicates

Like any other applied predicate, Q.eq(x, y) is never evaluated by construction or simplification. In other words, Q.eq(x, x), Q.eq(x, x).doit() or Q.eq(x, x).simplify() does not return true. Instead, ask(Q.eq(x, x)) returns True and refine(Q.eq(x, x)) returns S.true.

After relation predicates replace relational classes (so that x > 1 returns Q.gt(x, 1)), using infix relational operator will return evaluated result. This is to follow the evaluation logic of matrix module where A + A returns 2*A.

Symbolic manipulation of relation predicates

Since Q.eq(x, y) is never automatically evaluated, we can safely introduce symbolic manipulation of the relation.

Q.eq(x, y) is strictly boolean and does not have direct symbolic manipulation methods. For example Eq(x, y).expand() returns Eq(x.expand(), y.expand()), but Q.eq(x, y).expand() is not allowed.

Instead, Q.eq(x, y) will have proxy object as @oscarbenjamin suggested for 'Equation' in this comment, which can be called by .apply property. Q.eq(x, y).apply.expand() will return Q.eq(x.expand(), y.expand()).

Also, Q.eq(x, y) will be able to support algebra between the relational as @sylee957 shared in this comment. Q.eq(x, 1) + Q.eq(y, 1) will return AddSides(Q.eq(x, 1), Q.eq(y, 1), evaluate=True), which in turn will be evaluated to Q.eq(x + y, 2). Q.gt(x, 2) * -1 will return Q.lt(-x, -2), and Q.gt(x, 2) * y will return MultiplySides(Q.gt(x, 2), y) if the sign of y cannot be determined.

This way, Q.eq can make Equation no longer be required to be implemented. However this idea can be discarded if it does not get approved.

Compatibility with Eq around codebase

Every codebase will be modified so that Q.eq can be used instead of Eq everywhere. For example Piecewise((1, Q.eq(x, 0)), (0, True)) will be supported, and solveset(Q.eq(x**2, 1)) will return {-1, 1}.

Migration from Eq to Q.eq

Eq and other relational will be retained only for backwards compatibility. Documentation for Q.eq will be thoroughly made and users will be informed to use Q.eq instead of Eq. After a few release, Q.eq will be renamed to Eq.