Good practices for grind annotation

Stream: lean4

[HenrikT]

Hello,
i am currently working on a project and want to make good use of the grind tactic.
Similarly to @[simp], theorems can be annotated with @[grind] (or some variant of that, like @[grind =] etc.). While it is clear to me when to annotate with @[simp] i struggle with a good intuition on when to annotate with the@[grind] variants.

So now i am wondering,

• Are there any downsides to just annotate each of my theorems with just @[grind] except performance ?
• Are there some best practices on what to annotate and if so, how to annotate each theorem with some variation of @[grind]
• Is there some official guideline for annotation with @[grind] like there is for @[simp] like in the doc. of Mathlib ?

Thanks in advance :)

[Julia Scheaffer]

I have been wondering about these things too. I am sometimes confused by why a theorem doesn't work with grind but does work with something like @[simp]. I mainly want to know if there some advice for writing theorems in a way that works better for grind.

[Lawrence Wu (llllvvuu)]

https://lean-lang.org/doc/reference/latest/The--grind--tactic/E___matching/

[HenrikT]

So what i get from reading this article is, that:

• you can increase resource limits for cases when grind runs out (decreasing them for performance reasons is also an option i guess)
• define (multi-)patterns for each theorem that when present, grind will attempt to instantiate the corresponding theorem
• the grind attribute generates a (multi-)patterns using a heuristic

However while the article states that: (*) "Although it is tempting to just use @[grind] by default, we recommend using one of the other forms when it achieves the desired effect.", it does not explicitly state why it is not recommended.

I assume that while performance is one factor, another factor could be that the automatically generated patters can be too restrictive, thus theorems that are applicable are not instantiated by grind, thus grind fails more often. Am i correct in that assumption ?

If so, does this entail that one should use grind in combination with a custom pattern for each theorem, if performance allows it ?

As a side-node to this, if i define a very narrow pattern for each theorem instead of just using @[grind], wouldn't i often have to constantly update the pattern each time i write a new theorem using a slightly different pattern, thus making the workflow of just using @[grind] (or using overly broad patterns) more feasible (if performance allows it) ?

The article does not mention any clear guidelines for how/when to annotate with @[grind] (or some variant of it), except the quote (*) seen above.

Maybe someone with some experience in grind can chime in ?
Thanks in advance :)

[Lawrence Wu (llllvvuu)]

Your worry about grind patterns being too narrow is probably the opposite of what you should worry about. What you should avoid is a grind pattern that triggers a lot when the lemma is not relevant.

In any case, it is usually intuitively clear whether you want @[grind =], @[grind \l] or @[grind \r] so I don’t think this (along with inspecting the grind?) is onerous or undue effort

[Lawrence Wu (llllvvuu)]

wouldn't i often have to constantly update the pattern each time i write a new theorem using a slightly different pattern

I don't understand what this means. But grind annotations in core and mathlib, as far as I can tell, have not required maintenance once set.

[HenrikT]

What i was trying to say is,
Say i have all my theorems marked with very narrow patterns.
Now when i add new code / theorems which i want to prove using grind, can grind` fails because the patterns i have chosen worked only for the existing theorems but not for the new use case in the new theorem ?
Thus wouldn't i have to update the patterns each time there is a new use case ?
Maybe i am looking at it wrongly ?

[HenrikT]

"What you should avoid is a grind pattern that triggers a lot when the lemma is not relevant."

So i can write set_option diagnostics true in above the theorem in question and unfold the E-matching instances tab to see how often each theorem is instantiated.

However, how do i know from this diagnostic if a patterns is triggered too often or is not relevant at all. Is there some way to tell ?

[Lawrence Wu (llllvvuu)]

Thus wouldn't i have to update the patterns each time there is a new use case ?

Then you shouldn't use grind IMO, or you should explicitly pass in like grind [mylemma]. The point of a grind annotation is that it should be knowable without looking at the specific downstream uses. Adding a global grind pattern for a specific use would be a mis-use.