17.5.1. Selection Heuristics

grind decides which sub‑term to split on by combining three sources of signal:

Structural flags

These configuration flags determine whether grind performs certain case splits:

splitIte (default true)

Every Lean.Parser.Term.iteif-term should be split, as if by the split tactic.

splitMatch (default true)

Every Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match-term should be split, as if by the split tactic.

splitImp (default false)

Hypotheses of the form A → B whose antecedent A is propositional are split by considering all possibilities for A. Arithmetic antecedents are special‑cased: if A is an arithmetic literal (that is, a proposition formed by operators such as ≤, =, ¬, Dvd, …) then grind will split even when splitImp := false so the integer solver can propagate facts.

Global limits

The grind option splits := n caps the depth of the search tree. Once a branch performs n splits grind stops splitting further in that branch; if the branch cannot be closed it reports that the split threshold has been reached.

Manual annotations

Inductive predicates or structures may be tagged with the grind cases attribute. grind treats every instance of that predicate as a candidate for splitting.

attr ::= ...
    | Marks a theorem or definition for use by the `grind` tactic.

An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.

See the individual modifier docstrings for details.
grind The `cases` modifier marks inductively-defined predicates as suitable for case splitting.
cases

attr ::= ...
    | Marks a theorem or definition for use by the `grind` tactic.

An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.

See the individual modifier docstrings for details.
grind The `cases eager` modifier marks inductively-defined predicates as suitable for case splitting,
and instructs `grind` to perform it eagerly while preprocessing hypotheses.
cases eager

`grind` failed
grindc:Boolx y:Nath:(if c = true then x else y) = 0left:¬x = 0right:¬y = 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] (if c = true then x else y) = 0
[prop] ¬x = 0
[prop] ¬y = 0
[eqc] False propositions
[prop] x = 0
[prop] y = 0
[eqc] Equivalence classes
[eqc] others
[eqc] {0, if c = true then x else y}
[cutsat] Assignment satisfying linear constraints
[assign] x := 1
[assign] y := 2

`grind` failed
grindc:Boolx y:Nath:(if c = true then x else y) = 0left:¬x = 0right:¬y = 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] (if c = true then x else y) = 0
[prop] ¬x = 0
[prop] ¬y = 0
[eqc] False propositions
[prop] x = 0
[prop] y = 0
[eqc] Equivalence classes
[eqc] others
[eqc] {0, if c = true then x else y}
[cutsat] Assignment satisfying linear constraints
[assign] x := 1
[assign] y := 2
[limits] Thresholds reached
[limit] maximum number of case-splits has been reached, threshold: `(splits := 0)`

`grind` failed
grindy x:Nath:y =
  match x with
  | 0 => 1
  | x => 2h_1:y = 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] y =
      match x with
      | 0 => 1
      | x => 2
[prop] y = 0
[prop] (x = 0 → False) →
      (match x with
        | 0 => 1
        | x => 2) =
        2
[eqc] True propositions
[prop] (x = 0 → False) →
      (match x with
        | 0 => 1
        | x => 2) =
        2
[eqc] Equivalence classes
[eqc] {y, 0}
[eqc] {match x with
    | 0 => 1
    | x => 2}
[eqc] {x = 0 → False, (fun x_0 => x_0 = 0 → False) x, x = 0 → False}
[ematch] E-matching patterns
[thm] _example.match_1.congr_eq_1: [_example.match_1 #4 (@Lean.Grind.genPattern `[Nat] #0 #3 `[0]) #2 #1]
[thm] _example.match_1.congr_eq_2: [_example.match_1 #6 (@Lean.Grind.genPattern `[Nat] #1 #5 #2) #4 #3]
[cutsat] Assignment satisfying linear constraints
[assign] y := 0
[assign] x := 1
[assign] match x with
    | 0 => 1
    | x => 2 := 0

[grind] Diagnostics
[thm] E-Matching instances
[thm] _example.match_1.congr_eq_2 ↦ 1

`grind` failed
grindn:Nath:Not30 nh_1:n = 30⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] Not30 n
[prop] n = 30
[eqc] True propositions
[prop] Not30 n
[eqc] Equivalence classes
[eqc] {n, 30}
[cutsat] Assignment satisfying linear constraints
[assign] n := 30

17.5.2. Performance

Case analysis is powerful, but computationally expensive: each level of case splitting multiplies the search space. It's important to be judicious and not perform unnecessary splits. In particular:

• Increase splits only when the goal genuinely needs deeper branching; each extra level multiplies the search space.

• Disable splitMatch when large pattern‑matching definitions explode the tree; this can be observed by setting the trace.grind.split.

• Flags can be combined, e.g. by grind -splitMatch (splits := 10) +splitImp.

• The grind cases attribute is scoped. The modifiers Lean.Parser.Term.attrKind`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. local and Lean.Parser.Term.attrKind`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. scoped restrict extra splitting to a section or namespace.

trace.grind.split