Recent change in assumption module made it possible to define polyadic predicate, which is a function that takes multiple arguments and return boolean value. Binary relations such as =, !=, <, etc, fit right into this definition - they are binary predicates. I suggest that we redesign these objects as predicates, such as Q.eq, Q.gt, etc.
Current binary relations in core module has many flaws, which can be easily overcome by refactoring them to predicates.
1. They prone to be evaluated to boolean value (True/False), making symbolic manipulation of equations difficult.
-> Predicate is never evaluated to boolean unless applied to ask or refine.
2. They are specified for comparing numerical expressions, and it is hard to extend for new expressions.
-> Predicate use multipledispatch handler for evaluation, which has good extensibility.
3. They have poor API with assumption module. Currently every relation needs to be wrapped by `Q.is_true` to be assumed as predicate. This makes them difficult to be melt into fact management system.
-> Refactoring them to predicate removes this redundancy, and allows us to add facts such as `Implies(Q.gt, ~Q.lt)`,
I already made basic implementation of binary relation in PR
#20723. Eventually, I plan to completely replace `core/relational` module with this design.
Please take a look at the PR and leave your thoughts here. Thanks!