5.4. Picking a pattern
So how do you pick a pattern for your theorem?
Firstly, if you just tag it with @[grind] without any modifiers, there will be a helpful message suggesting different modifiers and the patterns they would generate.
If in our example from above we write
@[grind]
theorem gf'' (x : Nat) : g (f x) = x := x:ℕ⊢ g (f x) = x
All goals completed! 🐙
We get the following suggestions:
where we could then directly consider whether we might prefer the second option.
5.4.1. Identifying bad tagging
If your grind call is slow you might want to check whether it might be due to e-matching by checking what theorems it instantiates. You can do this by setting the option trace.grind.ematch.instance to true.
Sometimes a combination of tagged theorems can produce loops. These loops can be identified with #grind_lint.
Here is an example from the Language Reference. If we tag List.reverse_flatMap and List.flatMap_reverse like this:
attribute [grind =] List.reverse_flatMap
List.flatMap_reverse
Then #grind_lint inspect will show us that these theorems now produce a loop:
#grind_lint inspect List.reverse_flatMap
If we do what the the suggestion tells us to do we get:
set_option trace.grind.ematch.instance true in
#grind_lint inspect List.reverse_flatMap
with the following (shortened) output:
[grind.ematch.instance] reverse_flatMap: (flatMap f l).reverse = flatMap (reverse ∘ f) l.reverse
[grind.ematch.instance] flatMap_reverse: flatMap (reverse ∘ f) l.reverse = (flatMap (reverse ∘ reverse ∘ f) l).reverse
[grind.ematch.instance] flatMap_def: flatMap (reverse ∘ f) l.reverse = (List.map (reverse ∘ f) l.reverse).flatten
[grind.ematch.instance] flatMap_def: flatMap f l = (List.map f l).flatten
[grind.ematch.instance] reverse_flatMap: (flatMap (reverse ∘ reverse ∘ f) l).reverse = flatMap (reverse ∘ reverse ∘ reverse ∘ f) l.reverse
[grind.ematch.instance] flatMap_def: flatMap (reverse ∘ reverse ∘ f) l = (List.map (reverse ∘ reverse ∘ f) l).flatten
[grind.ematch.instance] flatMap_reverse: flatMap (reverse ∘ reverse ∘ reverse ∘ f) l.reverse =
(flatMap (reverse ∘ reverse ∘ reverse ∘ reverse ∘ f) l).reverse
[grind.ematch.instance] flatMap_def: flatMap (reverse ∘ reverse ∘ reverse ∘ f) l.reverse =
(List.map (reverse ∘ reverse ∘ reverse ∘ f) l.reverse).flatten
where we can actually observe the loop.
If we want to see all theorems that are problematic in this way, we can do this with #grind_lint check. We can be more specific and only search in a specific module and require a specific number of additionally instantiated theorems.
(I am not including the following code as Lean code, to not make the build slow.)
#grind_lint check (min := 20) in module Mathlib
for my current imports this gives
instantiating `Set.Icc.convexComb_symm` triggers 24 additional `grind` theorem instantiations
instantiating `Path.symm_apply` triggers 24 additional `grind` theorem instantiations
Mathlib performs this exact test above, the two lemmas we found above are currently the only exceptions.
As you can see the lemmas reverse_flatMap and flatMap_reverse don't appear here, meaning they don't produce the loop we discovered above in Mathlib. They are still tagged but have additional conditions imposed to prevent the looping:
grind_pattern reverse_flatMap => (l.flatMap f).reverse where
f =/= List.reverse ∘ _
grind_pattern flatMap_reverse => l.reverse.flatMap f where
f =/= List.reverse ∘ _
5.4.2. Recommended patterns
Per the language reference, any lemma that is tagged with simp should usually also be tagged with grind =.
The only exception to this is, if this lemma introduced a case distinction on the right side. Then you should instead write and tag lemmas for the specific cases.