16.10. 为库添加 grind 标注
要在库中有效使用 grind，必须为库添加标注：给合适的引理应用 grind 属性，或声明 Lean.Parser.Command.grindPattern : commandThe `grind_pattern` command can be used to manually select a pattern for theorem instantiation.
Enabling the option `trace.grind.ematch.instance` causes `grind` to print a trace message for each
theorem instance it generates, which can be helpful when determining patterns.
When multiple patterns are specified together, all of them must match in the current context before
`grind` attempts to instantiate the theorem. This is referred to as a *multi-pattern*.
This is useful for theorems such as transitivity rules, where multiple premises must be simultaneously
present for the rule to apply.
In the following example, `R` is a transitive binary relation over `Int`.
```
opaque R : Int → Int → Prop
axiom Rtrans {x y z : Int} : R x y → R y z → R x z
```
To use the fact that `R` is transitive, `grind` must already be able to satisfy both premises.
This is represented using a multi-pattern:
```
grind_pattern Rtrans => R x y, R y z
example {a b c d} : R a b → R b c → R c d → R a d := by
grind
```
The multi-pattern `R x y`, `R y z` instructs `grind` to instantiate `Rtrans` only when both `R x y`
and `R y z` are available in the context. In the example, `grind` applies `Rtrans` to derive `R a c`
from `R a b` and `R b c`, and can then repeat the same reasoning to deduce `R a d` from `R a c` and
`R c d`.
You can add constraints to restrict theorem instantiation. For example:
```
grind_pattern extract_extract => (as.extract i j).extract k l where
as =/= #[]
```
The constraint instructs `grind` to instantiate the theorem only if `as` is **not** definitionally equal
to `#[]`.
## Constraints
- `x =/= term`: The term bound to `x` (one of the theorem parameters) is **not** definitionally equal to `term`.
The term may contain holes (i.e., `_`).
- `x =?= term`: The term bound to `x` is definitionally equal to `term`.
The term may contain holes (i.e., `_`).
- `size x < n`: The term bound to `x` has size less than `n`. Implicit arguments
and binder types are ignored when computing the size.
- `depth x < n`: The term bound to `x` has depth less than `n`.
- `is_ground x`: The term bound to `x` does not contain local variables or meta-variables.
- `is_value x`: The term bound to `x` is a value. That is, it is a constructor fully applied to value arguments,
a literal (`Nat`, `Int`, `String`, etc.), or a lambda `fun x => t`.
- `is_strict_value x`: Similar to `is_value`, but without lambdas.
- `not_value x`: The term bound to `x` is a **not** value (see `is_value`).
- `not_strict_value x`: Similar to `not_value`, but without lambdas.
- `gen < n`: The theorem instance has generation less than `n`. Recall that each term is assigned a
generation, and terms produced by theorem instantiation have a generation that is one greater than
the maximal generation of all the terms used to instantiate the theorem. This constraint complements
the `gen` option available in `grind`.
- `max_insts < n`: A new instance is generated only if less than `n` instances have been generated so far.
- `guard e`: The instantiation is delayed until `grind` learns that `e` is `true` in this state.
- `check e`: Similar to `guard e`, but `grind` checks whether `e` is implied by its current state by
assuming `¬ e` and trying to deduce an inconsistency.
## Example
Consider the following example where `f` is a monotonic function
```
opaque f : Nat → Nat
axiom fMono : x ≤ y → f x ≤ f y
```
and you want to instruct `grind` to instantiate `fMono` for every pair of terms `f x` and `f y` when
`x ≤ y` and `x` is **not** definitionally equal to `y`. You can use
```
grind_pattern fMono => f x, f y where
guard x ≤ y
x =/= y
```
Then, in the following example, only three instances are generated.
```
/--
trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
-/
#guard_msgs in
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
set_option trace.grind.ematch.instance true in
grind
```
grind_pattern。
这些标注引导 grind 选择定理，进而在比喻中的白板上产生更多事实。
标注太少时，grind 将无法使用这些引理；标注太多时，它可能变慢，或因耗尽资源限制而失败。
添加标注通常应当保守：只有当你认为模式一旦匹配，grind 就应当总是实例化该定理时，才添加标注。
16.10.1. simp 引理
通常，许多带有 @[simp] 标注的定理也应带有 @[grind =] 标注。
一个重要的例外是：我们通常避免让 @[simp] 定理在右侧引入 Lean.Parser.Term.ifif，而倾向于使用一对分别以肯定条件和否定条件为假设的定理。
由于 grind 的设计目标之一就是进行情形拆分，通常更适合改为给那个引入 Lean.Parser.Term.ifif 的单一定理添加 @[grind =] 标注。
除了使用 @[grind =] 促使 grind 从左向右重写外，还可以使用 @[grind _=_] 进行“饱和”：遇到任意一侧时都允许双向重写。
16.10.2. 逆向与正向推理
对逆向推理定理使用 @[grind ←]（它从定理结论生成模式）；也就是说，当定理结论与目标匹配时，就应尝试该定理。
标准库中带有 grind ← 标注的定理包括：
-
Array.not_mem_empty (a : α) : ¬ a ∈ #[] -
Array.getElem_filter {xs : Array α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).size) : p (xs.filter p)[i] -
List.Pairwise.tail {l : List α} (h : Pairwise R l) : Pairwise R l.tail
在每个例子中，当引理的结论与证明目标匹配时，它便与当前证明相关。
对正向推理定理使用 @[grind →]（它从假设生成模式），
也就是从白板上的已有事实传播出新事实的定理。
标准库中带有 grind → 标注的定理包括：
-
List.getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.length, l[i] = a -
Array.mem_of_mem_erase [BEq α] {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a ∈ xs -
List.forall_none_of_filterMap_eq_nil (h : filterMap f xs = []) : ∀ x ∈ xs, f x = none
在这些例子中，定理的假设决定它们何时与当前证明相关。
使用 Lean.Parser.Command.grindPattern : commandThe `grind_pattern` command can be used to manually select a pattern for theorem instantiation.
Enabling the option `trace.grind.ematch.instance` causes `grind` to print a trace message for each
theorem instance it generates, which can be helpful when determining patterns.
When multiple patterns are specified together, all of them must match in the current context before
`grind` attempts to instantiate the theorem. This is referred to as a *multi-pattern*.
This is useful for theorems such as transitivity rules, where multiple premises must be simultaneously
present for the rule to apply.
In the following example, `R` is a transitive binary relation over `Int`.
```
opaque R : Int → Int → Prop
axiom Rtrans {x y z : Int} : R x y → R y z → R x z
```
To use the fact that `R` is transitive, `grind` must already be able to satisfy both premises.
This is represented using a multi-pattern:
```
grind_pattern Rtrans => R x y, R y z
example {a b c d} : R a b → R b c → R c d → R a d := by
grind
```
The multi-pattern `R x y`, `R y z` instructs `grind` to instantiate `Rtrans` only when both `R x y`
and `R y z` are available in the context. In the example, `grind` applies `Rtrans` to derive `R a c`
from `R a b` and `R b c`, and can then repeat the same reasoning to deduce `R a d` from `R a c` and
`R c d`.
You can add constraints to restrict theorem instantiation. For example:
```
grind_pattern extract_extract => (as.extract i j).extract k l where
as =/= #[]
```
The constraint instructs `grind` to instantiate the theorem only if `as` is **not** definitionally equal
to `#[]`.
## Constraints
- `x =/= term`: The term bound to `x` (one of the theorem parameters) is **not** definitionally equal to `term`.
The term may contain holes (i.e., `_`).
- `x =?= term`: The term bound to `x` is definitionally equal to `term`.
The term may contain holes (i.e., `_`).
- `size x < n`: The term bound to `x` has size less than `n`. Implicit arguments
and binder types are ignored when computing the size.
- `depth x < n`: The term bound to `x` has depth less than `n`.
- `is_ground x`: The term bound to `x` does not contain local variables or meta-variables.
- `is_value x`: The term bound to `x` is a value. That is, it is a constructor fully applied to value arguments,
a literal (`Nat`, `Int`, `String`, etc.), or a lambda `fun x => t`.
- `is_strict_value x`: Similar to `is_value`, but without lambdas.
- `not_value x`: The term bound to `x` is a **not** value (see `is_value`).
- `not_strict_value x`: Similar to `not_value`, but without lambdas.
- `gen < n`: The theorem instance has generation less than `n`. Recall that each term is assigned a
generation, and terms produced by theorem instantiation have a generation that is one greater than
the maximal generation of all the terms used to instantiate the theorem. This constraint complements
the `gen` option available in `grind`.
- `max_insts < n`: A new instance is generated only if less than `n` instances have been generated so far.
- `guard e`: The instantiation is delayed until `grind` learns that `e` is `true` in this state.
- `check e`: Similar to `guard e`, but `grind` checks whether `e` is implied by its current state by
assuming `¬ e` and trying to deduce an inconsistency.
## Example
Consider the following example where `f` is a monotonic function
```
opaque f : Nat → Nat
axiom fMono : x ≤ y → f x ≤ f y
```
and you want to instruct `grind` to instantiate `fMono` for every pair of terms `f x` and `f y` when
`x ≤ y` and `x` is **not** definitionally equal to `y`. You can use
```
grind_pattern fMono => f x, f y where
guard x ≤ y
x =/= y
```
Then, in the following example, only three instances are generated.
```
/--
trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
-/
#guard_msgs in
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
set_option trace.grind.ematch.instance true in
grind
```
grind_pattern 命令创建的自定义模式有许多用途。
一种常见用途是引入关于项的不等式或成员关系命题。
例如，可以有：
variable [BEq α]
theorem count_le_size {a : α} {xs : Array α} : count a xs ≤ xs.size :=
...
grind_pattern count_le_size => count a xs
这样，一旦遇到 count a xs 项，就会登记该不等式（即使此前的问题中尚未涉及不等式）。
还可以使用多模式施加更严格的限制，例如只有当白板上已经有关于大小的事实时，才引入关于大小的不等式：
theorem size_pos_of_mem {xs : Array α} (h : a ∈ xs) : 0 < xs.size :=
sorry
grind_pattern size_pos_of_mem => a ∈ xs, xs.size
若使用 @[grind →] 属性，每当遇到 a ∈ xs 时都会实例化该定理；与之不同，这个模式只会在白板上已有 xs.size 时使用。
（注意，也可以使用 @[grind <=] 属性产生这个 grind 模式；该属性先查看结论，再逆向查看假设以选择模式。
另一方面，@[grind →] 只会选择 a ∈ xs。）
在 Mathlib 中，我们可能希望启用关于正弦和余弦函数的多项式推理， 因此添加如下自定义 grind 模式：
theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 := ...
grind_pattern sin_sq_add_cos_sq => sin x, cos x
这样，一旦同时遇到具有同一个 x 的 sin x 和 cos x，就会实例化该定理。
随后，该定理会自动进入 Gröbner 基模块，用于推理同时包含 sin x 和 cos x 的多项式表达式。
另一种更激进的做法是分别编写两个 grind 模式，使该定理在遇到 sin x 或 cos x 中任意一个时就被实例化。