8.2. Defining custom `grind` sets🔗

Similarly, you might want to use a certain lemma for grind only in a certain situation, for example only when proving things about a specific object. This is possible by defining your own grind attribute using register_grind_attr.

For example, Mathlib has the following. (Not included as Lean code because to work the attribute has to be defined in a different file to the ones using it.)

/-- The `compactness` attribute is a custom grind-set
specialized to prove that sets are compact.
It is called by the `compactness` tactic. -/
register_grind_attr compactness

/-- The `closedness` attribute is a custom grind-set specialized to prove that sets are closed.
It is called by the `closedness` tactic. -/
register_grind_attr closedness

But there are currently no usage examples since this a relatively new addition. A subsequent PR by Floris van Doorn does however show what using this could look like:

attribute [compactness .] isCompact_Icc

@[to_dual self, simp, closedness =]
theorem closure_Icc' {α : Type*} [TopologicalSpace α]
    [Preorder α]  [OrderClosedTopology α] (a b : α) :
    closure (Set.Icc a b) = Set.Icc a b :=
  isClosed_Icc.closure_eq

and then it can be used like this:

example : IsCompact <|
    closure (Set.Icc (1 : ℝ) (3 : ℝ)) := by⊢ IsCompact (closure (Set.Icc 1 3))
  grind only [compactness, closedness]All goals completed! 🐙

In this case there is also some code on top to be able to use these grind sets as there own tactic. So you can do:

example : IsCompact <| Set.Icc (1 : ℝ) (3 : ℝ) := by⊢ IsCompact (Set.Icc 1 3)
  compactnessAll goals completed! 🐙

This is however not provided by grind and needs to be added manually.

8.2. Defining custom grind sets🔗

8.2. Defining custom `grind` sets🔗