aesop with a "bad simp hypothesis" in the context

Stream: lean4

[Frédéric Dupuis]

It seems like aesop adds all the hypotheses in the current context to the simp-set it uses in the normalization phase. Is this correct? The issue with this is that it makes aesop unexpectedly fail when the user puts a hypothesis that would be a bad simp lemma in the context using have -- in fact I just got bitten by this. Here's a MWE:

import Aesop

example (h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp
  aesop
  sorry

On this, I get the error aesop: error in norm simp: tactic 'simp' failed, nested error: maximum recursion depth has been reached, presumably because it keeps rewriting 1 into 1+1-1.

Is this a known issue? @Jannis Limperg

[Artie Khovanov]

There's

example (h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp
  aesop (config := { useSimpAll := false })

The docs for this option say:
Use simp_all, rather than simp at *, for the builtin simp normalisation rule.

[Jannis Limperg]

Yes, this is by design. Aesop's default simp is simp_all, which rewrites with equations in the context. This can lead to issues like this one, but they're surprisingly rare (from what I can tell, i.e. I rarely get complaints about this feature. :sweat_smile:)

You can use the option mentioned by @Artie Khovanov (thanks!) to switch to the less aggressive simp at *.

The reason for this design choice is that simp_all is much more powerful than simp at * since it rewrites with propositions as well. E.g. simp_all closes the goal h : A |- A \/ B.

However, now that I think about this, it would be possible to use a hybrid between simp_all and simp at * that only does propositional rewriting but doesn't use equations. Maybe this would be the best default for Aesop.

[Artie Khovanov]

@Jannis Limperg I think you would need to compensate for that, for instance by having Aesop rewrite using hypotheses as an unsafe 90% rule application.

[Jannis Limperg]

It would certainly weaken Aesop, but the more powerful behaviour would of course remain available. Unsafe rewriting is also an interesting idea.

[Jannis Limperg]

aesop#190

[Artie Khovanov]

I think this weaker variant could break a lot of common use cases, but I'm not 100% sure of that. It would certainly make using Aesop easier in some cases where I've had to eg remove hypotheses or avoid simp in Aesop altogether.

[Jannis Limperg]

Yeah. I'll evaluate on Mathlib as usual before making any changes. (Would be nice if I could easily evaluate on non-Mathlib projects as well, but I don't know how many non-Mathlib code bases with substantial Aesop use are actually out there.)

[Artie Khovanov]

I understand if not, but could you evaluate on https://github.com/artie2000/real_closed_field?

[Jannis Limperg]

Sure, I've made a note in the issue.

[Artie Khovanov]

thanks!

[Frédéric Dupuis]

I see, thanks!