17.7. Case Analysis

17.7.1. Selection heuristics

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

Structural flags — quick booleans that enable whole syntactic classes:
- splitIte (default true) → split every if … then … else … term.
- splitMatch (default true)→ split on all match expressions (the grind analogue of Lean’s split tactic, just like splitIte).
- splitImp (default false) → when true splits on any hypothesis A → B whose antecedent A is propositional. Arithmetic antecedents are special‑cased: if A is an arithmetic literal (≤, =, ¬, Dvd, …) grind will split even when splitImp := false so the integer solver can propagate facts.

👉 Shorthand toggles: by grind -splitIte +splitImp expands to by grind (splitIte := false) (splitImp := true).

Global limit — 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 — you may mark any inductive predicate or structure with

attribute [grind cases] Even Sorted

and grind will treat every instance of that predicate as a split candidate.

17.7.2. Examples

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! 🐙

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
  -- The following fails because we need one case split
  fail_if_success grind (splits := 0)c:Boolx:Naty:Nath:(if c = true then x else y) = 0⊢ x = 0 ∨ y = 0
  grind (splits := 1)All goals completed! 🐙

-- User‑defined predicate with [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
  -- With the attribute,
  -- grind immediately splits on the Even hypothesis
  grindAll goals completed! 🐙

example (h : Even (n + 2)) : Even n := byn:Nath:Even (n + 2)⊢ Even n
  grindAll goals completed! 🐙

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` fails if we disable `splitMatch`
  fail_if_success grind -splitMatchy:Natx:Nath:y =
  match x with
  | 0 => 1
  | x => 2⊢ y > 0
  grindAll goals completed! 🐙

17.7.3. Tips

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.
You can combine flags: by grind -splitMatch (splits := 10) +splitImp.
The [grind cases] attribute is scoped; you can use the modifiers local/scoped if you only want extra splits inside a section or namespace.