doc: add docstring for grind_pattern command

This PR documents the `grind_pattern` command for manually selecting
theorem instantiation patterns, including multi-patterns and the
constraint system (`=/=`, `=?=`, `size`, `depth`, `is_ground`,
`is_value`, `is_strict_value`, `gen`, `max_insts`, `guard`, `check`).

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -35,6 +35,102 @@ def grindPatternCnstrs : Parser := leading_parser "where " >> many1Indent (ppLin
 /-!
 Builtin parsers for `grind` related commands
 -/
+
+/--
+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.
+
+- `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
+```
+-/
 @[builtin_command_parser] def grindPattern := leading_parser
   Term.attrKind >> "grind_pattern " >>  ident >> darrow >> sepBy1 termParser "," >> optional grindPatternCnstrs