tactic for partial orders

Stream: mathlib4

[Vasilii Nesterov]

Would it be useful to have a tactic in Mathlib that can solve goals in partial order theory? It is easy to implement, and I'd like to create one to practice metaprogramming.

[Kim Morrison]

What goals would this tactic solve?

[Vasilii Nesterov]

Those that can be closed by applying reflexivity, transitivity, or antisymmetry to local hypotheses and the goal. It would also use the linearity of the order when applicable.

In both cases (partial order and linear order), the quantifier-free theory is decidable in linear time.

[Kevin Buzzard]

Is it this ?

[Vasilii Nesterov]

Hmm, I'm not sure if an aesop-based approach is the best here because it searches for the proof using tree search by guessing proof steps, whereas in this case, it can be done without guessing.

By the way, it's easy to add support for lattices in the tactic I have in mind.

[Bhavik Mehta]

Heather and I have discussed this a bit - I agree this would be nice to have. For the tactic you have in mind, would it be able to prove that a <= b <= c <= d <= e and b != d implies a != e in a partial order?

[Peter Nelson]

It would be nice to have something work for lattices, as well, even if it is just as simple as adding all the trivial inequalities that come from le_sup_iff, sup_le_iff, le_sup_left, le_sup_right and similar for inf.

[Bhavik Mehta]

(The thread that Kevin links to does this, but I think Vasily's idea would perform better than the aesop approach. It might work to just preprocess like nlinarith does to add all those inequalities, then running the partial/linear order version)

[Vasilii Nesterov]

Bhavik Mehta said:

Heather and I have discussed this a bit - I agree this would be nice to have. For the tactic you have in mind, would it be able to prove that a <= b <= c <= d <= e and b != d implies a != e in a partial order?

Thank you for this example! Everything turned out to be more complicated than I initially thought. Anyway, it seems that the problem can be solved in quadratic time (not linear as I promised).

Let me describe my algorithm for partial orders.

1. First, we negate the goal, so our new goal is to prove False.
2. We collect all facts in the form of x = y, x ≤ y, x < y, x ≠ y, ¬(x ≤ y), and ¬(x < y) from the context. Here, we split conjunctions. Splitting disjunctions would result in exponential blow-up, and I guess we can't do anything smart about it here. However, there should be an option to enable this splitting if needed.
3. We replace each fact of the form x < y with two equivalent facts: x ≤ y and x ≠ y.
4. We replace each fact of the form ¬(x ≤ y) with two equivalent facts: ¬(x < y) and x ≠ y.

5. We define the ≤-graph as a directed graph whose vertices are variables and whose edges correspond to facts of the form x ≤ y. Similarly, we define (undirected) =-graph.
   We then find all connected components in =-graph. Variables within the same component are be provably equal. Thus, we can "compress" them into a single vertex. During this process, we check that no fact of the form x ≠ y leads to a contradiction — otherwise, we have found a contradiction, and the goal is accomplished. After this step, we may assume that the remaining facts are in one of three forms: x ≤ y, x ≠ y, and ¬(x < y).

6. We identify all (directed) cycles in the ≤-graph. All variables within such a cycle must be equal, so we perform compression as before. After this step, we can assume that the ≤-graph is acyclic.

7. For each fact of the form ¬(x < y), we check whether y is reachable from x in the ≤-graph. If it is, then x ≤ y, which implies x = y, allowing us to compress the graph further.

At each step, we replace our set of facts with an equisatisfiable one. If no contradiction is found by the end, then there exists a model satisfying the final set of facts: one can use the set of variables with x R y holds iff y is reachable from x in the ≤-graph. In this case, it is impossible to derive a contradiction from the theory of partial orders.

[Vasilii Nesterov]

In your example, after negation, we would have a ≤ b ≤ c ≤ d ≤ e, b ≠ d, and a = e. After step 5, a and e would be compressed into a single variable, say s. Then, in step 6, we would detect the cycle s ≤ b ≤ c ≤ d ≤ s, and compressing it would lead to a contradiction with b ≠ d.

[Bhavik Mehta]

Nice, I can see this working! Indeed the reason I shared that example is that we'd also come up with the "do search in the directed graph on ≤" approach, but I didn't get time to think about how to make this example work (ie I just had a preorder tactic), I'm glad to hear it helped you figure out your algorithm!

[Vasilii Nesterov]

Here is the PR: #21877.

[Vasilii Nesterov]

While coding I simplified the algorithm and also added a Preorder version.

[Jireh Loreaux]

feature request:

order [h1, h2, h3]

Allow the user to supply inequalities.

[Bhavik Mehta]

Second feature request (which can and maybe should be a secondary PR to make this one easier to review): a preprocessing step which runs the lemmas that Peter mentions first, and then does order. I don't think this will be complete for lattices, but it could be convenient nonetheless (similar to how linarith is complete for linear arithmetic and nlinarith is not complete for nonlinear arithmetic, but it's still sometimes pretty useful!)

[Vasilii Nesterov]

Yes, I plan to do this in the next PR.

[Vasilii Nesterov]

I extended the tactic to Lattice (#21966), and it seems to be complete for them as well. I wonder if it would be useful to make it complete for DistribLattice. In any case, it seems to be an interesting and nontrivial task (maybe I should use the M3-N5 theorem somehow).

Btw, the cases of HeytingAlgebra and BooleanAlgebra can be handled by reducing them to intuitionistic or classical logic and then calling itauto or tauto :upside_down: .

[Yaël Dillies]

Vasily Nesterov said:

Btw, the cases of HeytingAlgebra and BooleanAlgebra can be handled by reducing them to intuitionistic or classical logic and then calling itauto or tauto :upside_down: .

This was one of the motivations for getting the theory of Heyting algebras off the ground: to get to write a cool tactic :grinning_face_with_smiling_eyes: