aesop and inequalities

Stream: mathlib4

[Violeta Hernández]

I find it pretty unfortunate that aesop can't solve goals like these:

import Mathlib

example {x y : ℕ} (h₁ : x < y) (h₂ : y ≤ x) : False := by
  aesop -- fails

example {x y : ℕ} (h₁ : x < y) (h₂ : y < x) : False := by
  aesop -- fails

It's possible to sidestep this, though my solution is quite a bit of a hack.

import Mathlib

example {x y : ℕ} (h₁ : x < y) (h₂ : y ≤ x) : False := by
  aesop (add simp [le_iff_lt_or_eq, lt_asymm])

example {x y : ℕ} (h₁ : x < y) (h₂ : y < x) : False := by
  aesop (add simp [lt_asymm])

Is there some other (better) way to get aesop to solve goals like these? I know of the order tactic of course, but what I'm describing is often the final state in a much larger goal, which aesop falls short of solving.

[Bhavik Mehta]

attribute [aesop safe forward] le_of_lt
attribute [aesop safe forward] lt_of_le_of_ne
attribute [aesop safe forward] not_lt_of_ge

are tags which would solve this, perhaps they might want to be added?

[Violeta Hernández]

On that note, what do safe and unsafe mean for applied lemmas?

[Jannis Limperg]

safe = Aesop will never look at the parent goal of the rule again, so you should make sure that a provable goal remains provable after the rule is applied. E.g. apply x <= y /\ x /= y -> x < y is safe because no information is lost. unsafe = Aesop will try other rules that may apply to the parent goal. E.g. apply x < y -> x <= y is unsafe because you could prove le via eq as well.

Forward rules are generally safe because they only add stuff to the context and don't destroy information, though it practice it can occasionally make sense to make a forward rule unsafe as well, to deprioritise it.

[Artie Khovanov]

I've thought about this before, and I'm not sure aesop's branching search is well-suited to closing these sorts of trivial order goals efficiently. I worry adding those forward rules will just slow every Aesop call with an inequality in the context down.

Perhaps we could gate the proposed forward order rules behind a ruleset that you can then activate? Or maybe is there a way to get Aesop to call finishing tactics like order to close goals?

[Violeta Hernández]

Either a ruleset or a discharger seem like really nice solutions.

[Jannis Limperg]

Adding order and similar tactics is definitely worth a try imo.

I think Mathlib should also experiment with more aggressive rule sets, e.g. more forward rules. We've tried fairly hard to make forward rules efficient to apply, so I suspect even if Aesop ends up using a lot of them, it shouldn't degrade performance too much. (Currently, simp absolutely dominates Aesop processing time, anything else doesn't really make a difference. ^^) If this approach does run into performance issues, I'd be happy to hear about them.

[TongKe Xue]

I believe linarith solves both. Is there a reason to not use linarith instead ?

[Violeta Hernández]

I know of the order tactic of course, but what I'm describing is often the final state in a much larger goal, which aesop falls short of solving.

[Violeta Hernández]

Similar remark applies for linarith, I'm trying to prove much larger goals and I'm getting left with these subgoals which aesop can't finish off

[TongKe Xue]

If you're willing to hack on aesop, I think the following is possible.
With slight loss of generality, assume we only have \leq and not \le.

All the linear ineqs can be written up as

0 \leq C + M v

where v is the list of vars, M is matrix, and C is a vec of constants.

Then we compute the nullspace of M (ensuring cancelling of vars), take a basis of that null space, and see of any of the dot product with C to a value < 0.

If so, we have a contradiction.

I've never studied aesop, so no idea how hard to hack this in.

[Henrik Böving]

Violeta Hernández said:

I know of the order tactic of course, but what I'm describing is often the final state in a much larger goal, which aesop falls short of solving.

Could you add linarith as a low priority tactical to aesop? Re-implementing a LIA procedure using aesop seems like a good recipe for unpredictability and inefficient proofs.

[Henrik Böving]

For example aesop (add safe tactic (by linarith)) or if that turns out to be too eager give it a penalty? aesop (add safe 10 tactic (by linarith)) or something like that

[Artie Khovanov]

I think adding order this way is too a good idea
order closes lots of goals that linarith cannot because linarith needs a ring structure, order isn't a downgrade

[Artie Khovanov]

Here is a problem I am running into with adding forward rules aggressively to aesop: simp_all erases hypotheses that it can prove from the other hypotheses. This invariant is very unhelpful because typeclass search can't see through implications . Here is a minimal example of the issue:

variable {P Q : Nat → Prop}

class my_class (n : Nat) : Prop

@[aesop safe apply]
theorem library_lemma (n) [my_class n] : P n := by sorry

theorem test_aesop (h1 : ∀ n, Q n → my_class n) (h0 : Q 0) : P 0 := by
  have := h1 _ h0
  aesop -- fails
  sorry

theorem test_manual (h1 : ∀ n, Q n → my_class n) (h0 : Q 0) : P 0 := by
  have := h1 _ h0
  apply library_lemma -- succeeds

[Artie Khovanov]

Changing the normalisation step to simp at [*] works:

theorem test_aesop (h1 : ∀ n, Q n → my_class n) (h0 : Q 0) : P 0 := by
  aesop (config := {useSimpAll := false}) (add safe forward h1)

but then you don't get the automatic rewriting that simp_all provides. Maybe simp [*] at * is a good compromise?

[Artie Khovanov]

And by the way the following, which is closer to my real use case, doesn't work at all :cry:

variable {P : Nat → Prop} {α : Type*} [SetLike α Nat] {Q : α}

class my_class (n : Nat) : Prop

@[aesop safe apply]

theorem library_lemma (n) [my_class n] : P n := by sorry

theorem test_aesop (h1 : ∀ n ∈ Q, my_class n) (h0 : 0 ∈ Q) : P 0 := by

  aesop (config := {useSimpAll := false}) (add safe forward h1) -- fails, made no progress

[Jannis Limperg]

The latter issue is the one you reported, right? So this should be fixed.

simp_all rewriting hyps to True is indeed a problem. Conceptually, I think it would make sense to downgrade Aesop's simp to simp at * and to reimplement a version of the propositional reasoning that simp_all provides in Aesop. This would also be good for performance; simp at * may even be cacheable. But it would also be a fairly major operation.

[Artie Khovanov]

Jannis Limperg said:

The latter issue is the one you reported, right? So this should be fixed.

So it is!

[Artie Khovanov]

Jannis Limperg said:

Conceptually, I think it would make sense to downgrade Aesop's simp to simp at * and to reimplement a version of the propositional reasoning that simp_all provides in Aesop.

Is this not as simple as adding (dependent) arrow elimination as a safe forward rule? Probably there is something I am missing.

[Jannis Limperg]

simp_all supports much more fancy simplifications, e.g. P /\ (Q \/ R) becomes P /\ R if h : Not Q is in the context. It might be possible to isolate this functionality, though. So we would have a first simp pass that does simp only [<all h : P or h : Not P>], then a second one that does non-contextual simp at * (cacheable?). This almost certainly gives worse performance because in CategoryTheory specifically, terms are huge and so each simp pass is very expensive. But I generally think sensible behaviour is more important than speed (up to a point).

[Artie Khovanov]

I wonder if the simp_all only behaviour can be implemented without using simp

[Jannis Limperg]

Yeah, but not sure how much we can optimise beyond what simp already does. Actually, maybe you could do a raw traversal without locally nameless opening/abstraction; that would be very fast.