16.5.1. 选择启发式方法🔗

grind 综合以下三类信号来决定要拆分哪个子项：

结构标志

以下配置标志决定 grind 是否进行特定的情形拆分：

splitIte（默认 true）

拆分每个 Lean.Parser.Term.iteif 项，就像使用 split 策略一样。

splitMatch（默认 true）

拆分每个 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 项，就像使用 split 策略一样。

splitImp（默认 false）

对于形如 A → B 且前件 A 是命题的假设，通过考虑 A 的所有可能情况进行拆分。 算术前件会受到特殊处理：如果 A 是算术文字（即由 ≤、=、¬、Dvd 等运算符构成的命题），那么即使 splitImp := false，grind 也会拆分它，以便整数求解器传播事实。

全局限制

grind 的 splits := n 选项限制搜索树的深度。 一旦某个分支进行了 n 次拆分，grind 就不再继续拆分该分支；如果无法关闭该分支，它会报告已达到拆分阈值。

手动标注

可以用 grind cases 属性标记归纳谓词或结构。 grind 会将该谓词的每个实例视为拆分候选。

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

16.5.2. 性能🔗

情形分析功能强大，但计算代价高昂：每增加一层情形拆分，搜索空间都会成倍增长。 因此务必谨慎，避免不必要的拆分。 具体而言：

• 仅当目标确实需要更深的分支时才增大 splits；每多一层都会成倍扩大搜索空间。

• 当大型模式匹配定义使搜索树急剧膨胀时，禁用 splitMatch；可设置 trace.grind.split 来观察这种情况。

• 标志可以组合使用，例如 by grind -splitMatch (splits := 10) +splitImp。

• grind cases 属性是有作用域的。 修饰符 Lean.Parser.Term.attrKind`attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。local 和 Lean.Parser.Term.attrKind`attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。scoped 可将额外拆分限制在某个节或命名空间内。

trace.grind.split