5.2. Specifying default patterns
There is a list of modifiers to the grind attribute that can be used to specify patterns using different algorithms.
Here is an overview of the options with examples from Mathlib.
You can use grind? to see which pattern is picked.
Arguments of the lemma are indexed with numbers starting with 0 for the first argument.
Some of these strategies require that a pattern can only be used when it covers all the arguments of the theorem, i.e. if all the arguments are fixed by the pattern. A multi-pattern can then only be used if every argument is covered by at least one of the included patterns. This is so that a theorem isn't applied too eagerly.
5.2.1. =: left side of equality
This instructs grind to use the left side of the goal (if it is an equality) as a pattern. It fails if not all arguments are covered in this way.
Here is an example from Mathlib:
@[grind? =]
lemma even_iff {n : ℤ} : Even n ↔ n % 2 = 0 where
mp := fun ⟨m, hm⟩ ↦ n:ℤx✝:Even nm:ℤhm:n = m + m⊢ n % 2 = 0 All goals completed! 🐙
mpr h := ⟨n / 2, n:ℤh:n % 2 = 0⊢ n = n / 2 + n / 2 All goals completed! 🐙⟩
where grind? outputs
#0 refers to the first argument, so n.
An equivalence is treated as an equality of propositions, so we can also use this modifier here. The pattern means that this theorem is used whenever there is a statement Even n on the whiteboard.
5.2.2. =_: right side of equality
This instructs grind to use the right side of the goal (if it is an equality) as a pattern. It fails if not all arguments are covered in this way.
I could not find an example in Mathlib so here is an example from Lean:
@[grind? =_]
theorem toList_toArray {α : Type*} {n : ℕ}
{xs : Vector α n} : xs.toArray.toList = xs.toList :=
rfl
with the grind? output
5.2.3. _=_: both sides of equality as two patterns
This modifier adds two patterns corresponding to = and =_. Thus the theorem can be used if the left or the right side matches something on the whiteboard.
Here is an example from Mathlib:
@[simp, grind? _=_]
theorem trans_symm {C : Type*} [Category C] {X Y Z : C}
(α : X ≅ Y) (β : Y ≅ Z) :
(α ≪≫ β).symm = β.symm ≪≫ α.symm :=
rfl
with the grind? output
Here we can see that the modifier produced two patterns. So if either sides of the equality are present somewhere on the whiteboard, grind will use this theorem to add the other one to the same equivalence class.
5.2.4. →: starting with hypotheses
With this pattern, grind will start with the hypotheses starting with the first.
It will add these hypotheses to a multi-pattern if they cover a previously not covered argument.
Here is an example from Mathlib:
@[aesop safe forward, grind? →]
lemma EqOn.eq_of_mem {α β : Type*} {s : Set α}
{f₁ f₂ : α → β} {a : α} (h : s.EqOn f₁ f₂)
(ha : a ∈ s) : f₁ a = f₂ a :=
h ha
with the grind? output
This time, the modifier produced a multi-pattern. You can see that this differs from the example above: multi-patterns are presented as lists with more than one entry, while multiple patterns are presented as different lists. So this theorem will only be used if grind finds both an expression s.EqOn f₁ f₂ and a ∈ s on the whiteboard.
5.2.5. .: starting with conclusion
This is the default strategy. Here grind picks expressions for a multi-pattern by first considering the conclusion and then the hypotheses starting with the first one.
(We introduce this last because I could find no easy examples in Mathlib.)
Here is an example from Mathlib:
@[grind? .]
theorem isClosed_dsupport {α β F V : Type*} [FunLike F α β]
[TopologicalSpace α] [Zero β] [Zero V] {f : F → V} :
IsClosed (dsupport f) := α:Type u_1β:Type u_2F:Type u_3V:Type u_4inst✝³:FunLike F α βinst✝²:TopologicalSpace αinst✝¹:Zero βinst✝:Zero Vf:F → V⊢ IsClosed (dsupport f)
All goals completed! 🐙
with the grind? output
5.2.6. Further modifiers
There a more modifiers that tell grind the order in which it should pick patterns such as ←, ⇒ and ⇐. Additionally, there are some modifiers to be used for specific types of theorems such as ext for extensionality theorems and inj for theorems showing injectivity.
Learn more about these modifiers in the Lean Language Reference.
5.2.7. grind!
Sometimes you want to pick a subterm or subexpression as a pattern. If you want to be as "aggressive" as possible with this, you can pick minimal indexable subexpression.
An expression is minimally indexable if it has no indexable subexpressions (respecting additionally some priorities).
You can use the grind! attribute in the same way as grind with the modifiers described above.
Here is an example from the Language Reference that shows why you might prefer grind! in some situations. Consider the following setup:
def f (a : Nat) : Nat :=
a + 1
def g (a : Nat) : Nat :=
a - 1
@[grind? .]
theorem gf (x : Nat) : g (f x) = x := x:ℕ⊢ g (f x) = x
All goals completed! 🐙
where the selected pattern is
Then the following cannot be proven by grind because the chosen pattern does not appear:
example {a b c : ℕ} (h₁ : f b = a) (h₂ : f c = a) :
b = c := a:ℕb:ℕc:ℕh₁:f b = ah₂:f c = a⊢ b = c
All goals completed! 🐙
Clearly, we need to trigger the use of fg already when f x appears.
If we use grind! in the tagging above, this works:
@[grind!? .]
theorem gf' (x : Nat) : g (f x) = x := x:ℕ⊢ g (f x) = x
All goals completed! 🐙
example {a b c : ℕ} (h₁ : f b = a) (h₂ : f c = a) :
b = c := a:ℕb:ℕc:ℕh₁:f b = ah₂:f c = a⊢ b = c
All goals completed! 🐙
This works because g (f x) isn't minimally indexable and thus the following pattern is chosen
Notice that this pattern doesn't cover the argument g. Above we discussed that some modifiers such as = don't allow this. So if you were to use the modifier = instead of . in this example, grind! wouldn't change anything.