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] 注释的定理也应该用 @[grind =] 注释。
一个重要的例外是，通常我们避免使用在右侧引入 Lean.Parser.Term.ifif 的 @[simp] 定理，而是更喜欢以正条件和负条件作为假设的一对定理。
由于 grind 设计用于执行案例分割，因此通常最好用 @[grind =] 来注释引入 Lean.Parser.Term.ifif 的单个定理。
除了使用 @[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
In each case, the lemma is relevant when its conclusion matches a proof goal.
Use @[grind →] (which generates patterns from the hypotheses) for forwards reasoning theorems,
i.e. where facts should be propagated from existing facts on the whiteboard.
Some examples of theorems in the standard library that are annotated with grind → are:
-
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 →] 将仅选择 a ∈ xs。）
在 Mathlib 中，我们可能希望启用关于正弦和余弦函数的多项式推理， 添加自定义研磨图案
theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 := ...
grind_pattern sin_sq_add_cos_sq => sin x, cos x
一旦遇到两个 sin x 和 cos x（具有相同的 x），它将实例化该定理。
然后，该定理将自动进入 Gröbner 基础模块，并用于推理涉及 sin x 和 cos x 的多项式表达式。
或者，更积极地编写两个单独的研磨模式，以便在遇到 sin x 或 cos x 时实例化该定理。