Partial order with equalities
I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which is a contradiction.
Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, I add an edge a→b to the graph. Then, I check "digraph.all_simple_cycles()". If it is not empty, i.e. the graph has a directed cycle such as a→b→c→a, this is a contradiction.
Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and "e<a", this is a contradiction.
What is a good way to implement this?