8.3. Style and Conventions🔗

Since grind is a very new tactic, there is no real consensus on style yet. In particular, the style guide doesn't provide any guidelines for grind. So take everything presented in this section with a grain of salt. However, ideas are beginning to emerge which we want to discuss some here. The ideas presented here mainly come from Chris Henson here.

8.3.1. Readability🔗

One big issue with grind is readability. Since it can be used to prove so many different things, it can be hard to decipher what it is used to prove in a specific instance. Here are a few rules that follow from this:

Tactics with names that better describe their purpose are to be preferred over grind. For example, if there is an equally short and fast proof using ring, simp or linarith, that proof should be used instead. Similarly, if the goal just follows from a single lemma.
When providing additional lemmas to grind it should ideally be very clear where those are used. For example, if the forward and backward direction of an iff-statement uses different lemmas, it is clearer to have two different grind proofs rather than one.
For the same reason as the above point, proofs of the form apply foo; grind [bar] should usually not be golfed into grind [foo, bar].

8.3.2. Performance🔗

If a proof repeatedly uses grind to prove different have statements, this means that grind will do the same basic setup multiple times. It is usually better to use interactive mode to circumvent this. Our example from before:

theorem exists_subset_or_subset_of_two_mul_lt_card5
    {α : Type*} [DecidableEq α] {X Y : Finset α} {n : ℕ}
    (hXY : 2 * n < #(X ∪ Y)) :
    ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) := byα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)
  grind =>
    have : #(X ∪ Y) = #X + #(Y \ X)grindα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h✝:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Ythis:#(X ∪ Y) = #X + #(Y \ X)⊢ False
    finishAll goals completed! 🐙

could also have been written like this:

theorem exists_subset_or_subset_of_two_mul_lt_card6
    {α : Type*} [DecidableEq α] {X Y : Finset α} {n : ℕ}
    (hXY : 2 * n < #(X ∪ Y)) :
    ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) := byα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)
  have : #(X ∪ Y) = #X + #(Y \ X) := by grindα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)this:#(X ∪ Y) = #X + #(Y \ X)⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)
  grindAll goals completed! 🐙

8.3.3. Maintainability🔗

Since grind is always a finishing tactic it should in general not be squeezed for the same reason that we don't squeeze terminal simps.

There are bugs in grind that makes it so that grind? sometimes doesn't return a working proof. This is an issue when trying to fix grind calls that break during Mathlib updates. Mathlib tracks these cases in the Weekly linting log but currently doesn't refactor these grind calls. Instead Mathlib is waiting for a bug fix. (See this PR for the discussion on this decision.)