grind vs aesop

Stream: mathlib4

[Jakub Nowak]

I might be mistaken, but I believe grind should be able to replace aesop in most cases. Should I prefer grind over aesop in proofs in mathlib, or should I prefer aesop?

[Kim Morrison]

No, that's incorrect, they have very different scope and behaviour. In particular, grind does not use the simp set (aesop heavily does), and grind will not make any attempt to fill in existential quantifiers.

If both work, use either. But it's less often that you'd expect (and in cases where both work, quite possible simp does too).

[Jakub Nowak]

Kim Morrison said:

grind does not use the simp set

I know, I meant to use grind, after adding @[grind] attribute to relevant lemmas.

Kim Morrison said:

grind will not make any attempt to fill in existential quantifiers.

Good to know! Thanks!

Kim Morrison said:

and in cases where both work, quite possible simp does too

That's a bit of overstatement. Both grind and aesop can do case splitting, which simp can't.

[Kim Morrison]

Good. I would personally encourage you to use grind, because we think it is more scalable, and it's going to get much more powerful still. :-)