4.3. Case Splits🔗

We already saw that grind can perform case splits. It does so mainly on if-expressions and match-statements.

Excessive case splits can make grind very slow. You can use the option trace.grind.split to inspect the splits grind performs and determine whether this might be the reason your grind call is slow. If this is the case, you can use grind -splitIfs and grind -splitMatch to disable certain types of splits or specify the maximal depth of the search tree given by the splits with grind (splits := n). The default value here is 9. You can also use this to increase the depth which you should only do if your proof does really require more splits.

You can also label your own inductive definitions with the grind cases attribute to enable case splitting on them. Lean itself does this for example for Or and Sum. Mathlib basically doesn't use this feature, yet. I think this is mainly because people tag lemmas instead to achieve similar effects when needed.