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 等运算符形成的命题），则 grind 将在以下情况下拆分 even： splitImp := false 因此整数求解器可以传播事实。

全球限制

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 属性是 scoped。 修饰符 Lean.Parser.Term.attrKind`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. local 和 Lean.Parser.Term.attrKind`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. scoped 限制对节或命名空间的额外拆分。

trace.grind.split