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
```
`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. grind_pattern ident => term,*

Associates a theorem with one or more patterns. When multiple patterns are provided in a single Lean.Parser.Command.grind_patterngrind_pattern command, all of them must match a term before grind will attempt to instantiate the theorem.

When the grind attribute is added to a definition, it causes grind to unfold that definition to its body whenever it is encountered. When using the module system, if the body of the definition is not visible (e.g. via @[expose]), then the grind attribute is ignored.

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 grindMod?

The grind attribute automatically generates an E-matching pattern for a theorem, using a strategy determined by the provided modifier. If no modifier is provided, then grind suggests suitable modifiers, displaying the resulting patterns.

attr ::= ...
    | Like `@[grind]`, but enforces the **minimal indexable subexpression condition**:
when several subterms cover the same free variables, `grind!` chooses the smallest one.

This influences E-matching pattern selection.

### Example
```lean
theorem fg_eq (h : x > 0) : f (g x) = x

@[grind <-] theorem fg_eq (h : x > 0) : f (g x) = x
-- Pattern selected: `f (g x)`

-- With minimal subexpression:
@[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
-- Pattern selected: `g x`
grind! grindMod?

The grind! attribute automatically generates an E-matching pattern for a theorem, using a strategy determined by the provided modifier. It additionally enforces the condition that the selected pattern(s) should be minimal indexable subexpressions.

attr ::= ...
    | Like `@[grind]`, but also prints the pattern(s) selected by `grind`
as info messages. Useful for debugging annotations and modifiers.
grind? grindMod?

The grind? displays the pattern that was generated.

attr ::= ...
    | Like `@[grind!]`, but also prints the pattern(s) selected by `grind`
as info messages. Combines minimal subexpression selection with debugging output.
grind!? grindMod?

The grind!? attribute is equivalent to grind!, except it displays the resulting pattern for inspection.

Without any modifier, @[grind] traverses the conclusion and then the hypotheses from left to right, adding patterns as they increase the coverage, stopping when all arguments are covered. This default strategy can be explicitly requested using the Lean.Parser.Attr.grindDefThe `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the theorem, and then the hypotheses from left to right. We say this is the default modifier. Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. If `grind!` is used, then only minimal indexable subexpressions are considered. . modifier. In addition to using the default strategy, the attribute checks which other strategies could be applied, and displays all of the resulting patterns.

grindMod ::= ...
    | The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from left to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
.

grindMod ::= ...
    | The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from left to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
·

The . modifier instructs grind to select a multi-pattern by traversing the conclusion of the theorem, and then the hypotheses from left to right. We say this is the default modifier. Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. If grind! is used, then only minimal indexable subexpressions are considered.

grindMod ::= ...
    | The `=` modifier instructs `grind` to check that the conclusion of the theorem is an equality,
and then uses the left-hand side of the equality as a pattern. This may fail if not all of the arguments appear
in the left-hand side.
=

The = modifier instructs grind to check that the conclusion of the theorem is an equality, and then uses the left-hand side of the equality as a pattern. This may fail if not all of the arguments appear in the left-hand side.

grindMod ::= ...
    | The `=_` modifier instructs `grind` to check that the conclusion of the theorem is an equality,
and then uses the right-hand side of the equality as a pattern. This may fail if not all of the arguments appear
in the right-hand side.
=_

The =_ modifier instructs grind to check that the conclusion of the theorem is an equality, and then uses the right-hand side of the equality as a pattern. This may fail if not all of the arguments appear in the right-hand side.

grindMod ::= ...
    | The `_=_` modifier acts like a macro which expands to `=` and `=_`.  It adds two patterns,
allowing the equality theorem to trigger in either direction.
_=_

The _=_ modifier acts like a macro which expands to = and =_. It adds two patterns, allowing the equality theorem to trigger in either direction.

grindMod ::= ...
    | The `→` modifier instructs `grind` to select a multi-pattern from the hypotheses of the theorem.
In other words, `grind` will use the theorem for forwards reasoning.
To generate a pattern, it traverses the hypotheses of the theorem from left to right.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
→

The → modifier instructs grind to select a multi-pattern from the hypotheses of the theorem. In other words, grind will use the theorem for forwards reasoning. To generate a pattern, it traverses the hypotheses of the theorem from left to right. Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. If grind! is used, then only minimal indexable subexpressions are considered.

grindMod ::= ...
    | The `←` modifier instructs `grind` to select a multi-pattern from the conclusion of theorem.
In other words, `grind` will use the theorem for backwards reasoning.
This may fail if not all of the arguments to the theorem appear in the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
←

The ← modifier instructs grind to select a multi-pattern from the conclusion of theorem. In other words, grind will use the theorem for backwards reasoning. This may fail if not all of the arguments to the theorem appear in the conclusion. Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. If grind! is used, then only minimal indexable subexpressions are considered.

grindMod ::= ...
    | The `⇒` modifier instructs `grind` to select a multi-pattern by traversing all the hypotheses from
left to right, followed by the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
=>

grindMod ::= ...
    | The `⇒` modifier instructs `grind` to select a multi-pattern by traversing all the hypotheses from
left to right, followed by the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
⇒

The ⇒ modifier instructs grind to select a multi-pattern by traversing all the hypotheses from left to right, followed by the conclusion. Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. If grind! is used, then only minimal indexable subexpressions are considered.

grindMod ::= ...
    | The `⇐` modifier instructs `grind` to select a multi-pattern by traversing the conclusion, and then
all the hypotheses from right to left.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
<=

grindMod ::= ...
    | The `⇐` modifier instructs `grind` to select a multi-pattern by traversing the conclusion, and then
all the hypotheses from right to left.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
⇐

The ⇐ modifier instructs grind to select a multi-pattern by traversing the conclusion, and then all the hypotheses from right to left. Each time it encounters a subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. If grind! is used, then only minimal indexable subexpressions are considered.

grindMod ::= ...
    | The `←=` modifier is unlike the other `grind` modifiers, and it used specifically for
backwards reasoning on equality. When a theorem's conclusion is an equality proposition and it
is annotated with `@[grind ←=]`, grind `will` instantiate it whenever the corresponding disequality
is assumed—this is a consequence of the fact that grind performs all proofs by contradiction.
Ordinarily, the grind attribute does not consider the `=` symbol when generating patterns.
←=

The ←= modifier is unlike the other grind modifiers, and it used specifically for backwards reasoning on equality. When a theorem's conclusion is an equality proposition and it is annotated with @[grind ←=], grind will instantiate it whenever the corresponding disequality is assumed—this is a consequence of the fact that grind performs all proofs by contradiction. Ordinarily, the grind attribute does not consider the = symbol when generating patterns.

grindMod ::= ...
    | The `funCC` modifier marks global functions that support **function-valued congruence closure**.
Given an application `f a₁ a₂ … aₙ`, when `funCC := true`,
`grind` generates and tracks equalities for all partial applications:
- `f a₁`
- `f a₁ a₂`
- `…`
- `f a₁ a₂ … aₙ`
funCC

The funCC modifier marks global functions that support function-valued congruence closure. Given an application f a₁ a₂ … aₙ, when funCC := true, grind generates and tracks equalities for all partial applications:

• f a₁

• f a₁ a₂

• …

• f a₁ a₂ … aₙ

grindMod ::= ...
    | The `ext` modifier marks extensionality theorems for use by `grind`.
For example, the standard library marks `funext` with this attribute.

Whenever `grind` encounters a disequality `a ≠ b`, it attempts to apply any
available extensionality theorems whose matches the type of `a` and `b`.
ext

The ext modifier marks extensionality theorems for use by grind. For example, the standard library marks funext with this attribute.

Whenever grind encounters a disequality a ≠ b, it attempts to apply any available extensionality theorems whose matches the type of a and b.

In addition, adding @[grind ext] to a structure registers a its extensionality theorem.

grindMod ::= ...
    | The `inj` modifier marks injectivity theorems for use by `grind`.
The conclusion of the theorem must be of the form `Function.Injective f`
where the term `f` contains at least one constant symbol.
inj

The inj modifier marks injectivity theorems for use by grind. The conclusion of the theorem must be of the form Function.Injective f where the term f contains at least one constant symbol.

grindMod ::= ...
    | The `intro` modifier instructs `grind` to use the constructors (introduction rules)
of an inductive predicate as E-matching theorems.Example:
```
inductive Even : Nat → Prop where
| zero : Even 0
| add2 : Even x → Even (x + 2)

attribute [grind intro] Even
example (h : Even x) : Even (x + 6) := by grind
example : Even 0 := by grind
```
Here `attribute [grind intro] Even` acts like a macro that expands to
`attribute [grind] Even.zero` and `attribute [grind] Even.add2`.
This is especially convenient for inductive predicates with many constructors.
intro

The intro modifier instructs grind to use the constructors (introduction rules) of an inductive predicate as E-matching theorems.Example:

Here attribute [grind intro] Even acts like a macro that expands to attribute [grind] Even.zero and attribute [grind] Even.add2. This is especially convenient for inductive predicates with many constructors.