interplay of simp and grind

Stream: general

[Chris Henson]

As an example of joint simp and grind golfing, see this proof #mathlib4 > filter coprod lemma @ 💬 that @Bhavik Mehta wrote. This is something I find myself doing often, especially when seeing how grind can fit into an existing proof.

Is there any reasonable way this could be automated, something like a simp_grind? tactic? Somewhat related is if grind? +suggestions and simp? +suggestions could work together. Has anyone been thinking along these lines already?

[Chris Henson]

At a minimum, I think a grind premise selector that adds the theorems that simp? sees would be helpful. I often do exactly this when trying to finish a proof with grind.

[Jakub Nowak]

Maybe related discussion? #new members > Should `grind` use `simp` lemmas?

[Kim Morrison]

Yes, we're definitely thinking about this. With the new grind => tactic language that is arriving soon, we want to support e.g. running simp at steps inside a grind proof, and we may well add some syntax for just running simp at every term.