command ::= ... |The `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 ident => term,*`attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。
将一个定理与一个或多个模式关联起来。
如果在同一个 Lean.Parser.Command.grind_patterngrind_pattern 命令中给出了多个模式，那么必须全部匹配到项，grind 才会尝试实例化该定理。
command ::= ... |The `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 ident => term,* where (isValue | isStrictValue | notValue | notStrictValue | isGround | sizeLt | depthLt | genLt | maxInsts | guard | check | notDefEq | defEq)`attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。
可选的 Lean.Parser.Command.grind_patternwhere 子句给出了一组约束；只有满足这些约束时，grind 才会尝试实例化该定理。
每个约束都形如 variable =/= value，用于阻止在模式变量会被赋成指定值时发生实例化。
这对于避免某些问题项导致的无界或过度实例化很有用。