Can aesop take a simp-list

Stream: lean4

[Bhavik Mehta]

I find myself using aesop fairly often, and noticing that when it gets stuck I can add or remove one or two simp lemmas to make it succeed - is it possible to give aesop a list of lemmas to add/remove from the simp call (ie if I give it [a,-b,←c] then instead of calling simp it'd call simp [a,-b,←c]), like we can with norm_num? I'm aware of aesop (add simp a), but I can't get it to work to remove lemmas or reverse them.
(Tangentially, might it be sensible for ext to be one of the things aesop should try?)

[Jannis Limperg]

You can erase Aesop rules:

import Aesop

@[irreducible]
def foo := 42

@[aesop simp]
theorem foo_def : foo = 42 := by unfold foo; rfl

example : foo = 42 := by
  aesop (erase foo_def) -- fails
  aesop

The ←c syntax for reversing a lemma is currently not supported. Could be added with some effort.

ext sounds like a sensible candidate for the global rule set.

[Bhavik Mehta]

Ah, I was misunderstanding the syntax for erase - I tried (erase simp foo_def) - thanks for the clarification

[Jannis Limperg]

If you got it wrong, that probably means the docs are not great. I'll take a look. :)

[Jireh Loreaux]

This is a slightly different question, but is it possible to avoid using a lemma tagged @[simp] in an aesop call?

[Alex Keizer]

A particular lemma tagged @[simp], or do you want it to not use any simp-lemmas at all?

[Jireh Loreaux]

A particular lemma. But either option would be interesting.

[James Gallicchio]

how's that different from erasing a lemma? :thinking:

[Jireh Loreaux]

I thought aesop can only erase @[aesop simp] lemmas, not @[simp] lemmas. Am I wrong?

[James Gallicchio]

Ohhhhh maybe

[Jannis Limperg]

Digging up this thread after the holidays, sorry. Apparently I did implement this:

import Aesop

@[simp]
def A := True

example : A := by
  fail_if_success aesop (erase A) (options := { terminal := true })
  aesop

[Jireh Loreaux]

@Jannis Limperg I don't think so: that fail_if_success succeeds, but for the wrong reason.

import Aesop

@[simp]
def A := True

example : A := by
  aesop (erase A) (options := { terminal := true }) -- aesop: 'A' is not registered (with the given features) in any rule set.

[Jireh Loreaux]

Do you want me to create an issue on the aesop repo for this?

[Jannis Limperg]

Ah! Sorry, I'll look into it. No issue necessary (but do remind me if I forget).

[Jannis Limperg]

This is now fixed on Aesop master.

[Jireh Loreaux]

Thanks!

[Jireh Loreaux]

#7461 is the mathlib bump

[Jannis Limperg]

Aesop master currently has some other commits that'll (very mildly) break mathlib. #7462 avoids this breakage.

[Patrick Massot]

I borsed that but it would be nice to have a better fix where aesop still works there.

[Jannis Limperg]

Thanks! The issue with these goals is that they contain an equational hypothesis w that, when rewritten left to right, makes the goal unprovable. Aesop runs simp_all and so potentially rewrites with w. New Aesop still proves the goals when w is cleared. Old Aesop proved the goal in the presence of w because the simp lemmas were applied in a different order, so the correct simp lemma would fire before w. I consider such proofs inherently brittle (there's no guarantee anywhere about the order in which simp lemmas are tried), so I think it's good to replace them.

[Patrick Massot]

I understand but I thought that aesop was meant to be strictly stronger than simp. Of course, deep down, I know that there is never any such ordering between automation tactic...

[Jannis Limperg]

That's fair. I can't guarantee this property, but I'll see if I can avoid this specific discrepancy.

[Jannis Limperg]

Fixed on Aesop master.