17.4. Case Analysis🔗

In addition to congruence closure and constraint propagation, grind performs case analysis. During case analysis, grind considers each possible way that a term could have been built, or each possbile value of a particular term, in a manner similar to the cases and split tactics. This case analysis is not exhaustive: grind only recursively splits cases up to a configured depth limit, and configuration options and annotations control which terms are candidates for splitting.

17.4.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.

attributeCase analysis

attr ::= ...
    | grind cases

The grind cases attribute marks inductively-defined predicates as suitable for case splitting.

Splitting Conditional Expressions

In this example, grind proves the theorem by considering both cases for the conditional:

example (c : Bool) (x y : Nat)
    (h : (if c then x else y) = 0) :
    x = 0 ∨ y = 0 := byc:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0
  grindAll goals completed! 🐙

Disabling splitIte causes the proof to fail:

example (c : Bool) (x y : Nat)
    (h : (if c then x else y) = 0) :
    x = 0 ∨ y = 0 := byc:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0
  `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] {0, if c = true then x else y}
[cutsat] Assignment satisfying linear constraints
[assign] x := 1
[assign] y := 2
grind -splitItec:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0

In particular, it cannot make progress after discovering that the conditional expression is equal to 0:

`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] {0, if c = true then x else y}
[cutsat] Assignment satisfying linear constraints
[assign] x := 1
[assign] y := 2

Forbidding all case splitting causes the proof to fail for the same reason:

example (c : Bool) (x y : Nat)
    (h : (if c then x else y) = 0) :
    x = 0 ∨ y = 0 := byc:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0
  `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] {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 (splits := 0)c:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0

`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] {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)`

Allowing just one split is sufficient:

example (c : Bool) (x y : Nat)
    (h : (if c then x else y) = 0) :
    x = 0 ∨ y = 0 := byc:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0
  grind (splits := 1)All goals completed! 🐙

Splitting Pattern Matching

Disabling case splitting on pattern matches causes grind to fail in this example:

example (h : y = match x with | 0 => 1 | _ => 2) :
    y > 0 := byy:Natx:Nath:y =
  match x with
  | 0 => 1
  | x => 2⊢ y > 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,
    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 -splitMatchy:Natx:Nath:y =
  match x with
  | 0 => 1
  | x => 2⊢ y > 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,
    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

Enabling the option causes the proof to succeed:

example (h : y = match x with | 0 => 1 | _ => 2) :
    y > 0 := byy:Natx:Nath:y =
  match x with
  | 0 => 1
  | x => 2⊢ y > 0
  grindAll goals completed! 🐙

Splitting Predicates

Not30 is a somewhat verbose way to state that a number is not 30:

inductive Not30 : Nat → Prop where
  | gt : x > 30 → Not30 x
  | lt : x < 30 → Not30 x

By default, grind cannot show that Not30 implies that a number is, in fact, not 30:

example : Not30 n → n ≠ 30 := byn:Nat⊢ Not30 n → n ≠ 30 `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
grindn:Nat⊢ Not30 n → n ≠ 30

This is because grind does not consider both cases for Not30

`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

Adding the grind cases attribute to Not30 allows the proof to succeed:

attribute [grind cases] Not30

example : Not30 n → n ≠ 30 := byn:Nat⊢ Not30 n → n ≠ 30 grindAll goals completed! 🐙

Similarly, the grind cases attribute on Even allows grind to perform case splits:

@[grind cases]
inductive Even : Nat → Prop
  | zero : Even 0
  | step : Even n → Even (n + 2)

attribute [grind cases] Even

example (h : Even 5) : False := byh:Even 5⊢ False
  grindAll goals completed! 🐙

set_option trace.grind.split true in
example (h : Even (n + 2)) : Even n := byn:Nath:Even (n + 2)⊢ Even n
  [grind.split] Even (n + 2), generation: 0grindAll goals completed! 🐙

17.4.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.

option

trace.grind.split

Default value: false

enable/disable tracing for the given module and submodules