doc: improve grind doc string

src/Init/Grind/Ring/Envelope.lean

@@ -504,8 +504,8 @@ def ofCommSemiring : CommRing (OfSemiring.Q α) :=
 attribute [instance] ofCommSemiring
 
 /-
-Remark: `↑a` is notation for `OfSemring.toQ a`.
-We want to hide `OfSemring.toQ` applications in the diagnostic information produced by
+Remark: `↑a` is notation for `OfSemiring.toQ a`.
+We want to hide `OfSemiring.toQ` applications in the diagnostic information produced by
 the `ring` procedure in `grind`.
 -/
 @[app_unexpander OfSemiring.toQ]

src/Init/Grind/Tactics.lean

@@ -210,13 +210,13 @@ syntax grindLemma := (Attr.grindMod ppSpace)? ident
 syntax grindParam := grindErase <|> grindLemma
 
 /--
-`grind` is a tactic inspired by modern SMT solvers.
-**Picture a virtual white‑board:** every time `grind` discovers a new equality, inequality,
-or Boolean literal it writes that fact on the board, merges equivalent terms into buckets,
-and invites each engine to read from, and add back to, the same workspace.
-The cooperating engines are: congruence closure, constraint propagation, E‑matching,
-guided case analysis, and a suite of satellite theory solvers (linear integer arithmetic,
-commutative rings, ...).
+`grind` is a tactic inspired by modern SMT solvers. **Picture a virtual whiteboard**:
+every time grind discovers a new equality, inequality, or logical fact,
+it writes it on the board, groups together terms known to be equal,
+and lets each reasoning engine read from and contribute to the shared workspace.
+These engines work together to handle equality reasoning, apply known theorems,
+propagate new facts, perform case analysis, and run specialized solvers
+for domains like linear arithmetic and commutative rings.
 
 `grind` is *not* designed for goals whose search space explodes combinatorially,
 think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards,
@@ -227,15 +227,28 @@ For **bit‑level or combinatorial problems**, consider using **`bv_decide`**.
 `bv_decide` calls a state‑of‑the‑art SAT solver (CaDiCaL) and then returns a
 *compact, machine‑checkable certificate*.
 
-E-matching is a mechanism used by `grind` to instantiate theorems efficiently.
-It is especially effective when combined with congruence closure, enabling
-`grind` to discover non-obvious consequences of equalities and annotated theorems
-automatically. The theorem instantiation process is interrupted using the `generation` threshold.
-Terms occurring in the input goal have `generation` zero. When `grind` instantiates
-a theorem using terms with generation `≤ n`, the new generated terms have generation `n+1`.
+### Equality reasoning
+
+`grind` uses **congruence closure** to track equalities between terms.
+When two terms are known to be equal, congruence closure automatically deduces
+equalities between more complex expressions built from them.
+For example, if `a = b`, then congruence closure will also conclude that `f a` = `f b`
+for any function `f`. This forms the foundation for efficient equality reasoning in `grind`.
+Here is an example:
+```
+example (f : Nat → Nat) (h : a = b) : f (f b) = f (f a) := by
+  grind
+```
+
+### Applying theorems using E-matching
+
+To apply existing theorems, `grind` uses a technique called **E-matching**,
+which finds matches for known theorem patterns while taking equalities into account.
+Combined with congruence closure, E-matching helps `grind` discover
+non-obvious consequences of theorems and equalities automatically.
 
 Consider the following functions and theorems:
-```lean
+```
 def f (a : Nat) : Nat :=
   a + 1
 
@@ -248,9 +261,9 @@ theorem gf (x : Nat) : g (f x) = x := by
 ```
 The theorem `gf` asserts that `g (f x) = x` for all natural numbers `x`.
 The attribute `[grind =]` instructs `grind` to use the left-hand side of the equation,
-`g (f x)`, as a pattern for heuristic instantiation via E-matching.
+`g (f x)`, as a pattern for E-matching.
 Suppose we now have a goal involving:
-```lean
+```
 example {a b} (h : f b = a) : g a = b := by
   grind
 ```
@@ -268,7 +281,7 @@ For example, the pattern `g (f x)` is too restrictive in the following case:
 the theorem `gf` will not be instantiated because the goal does not even
 contain the function symbol `g`.
 
-```lean (error := true)
+```
 example (h₁ : f b = a) (h₂ : f c = a) : b = c := by
   grind
 ```
@@ -276,7 +289,7 @@ example (h₁ : f b = a) (h₂ : f c = a) : b = c := by
 You can use the command `grind_pattern` to manually select a pattern for a given theorem.
 In the following example, we instruct `grind` to use `f x` as the pattern,
 allowing it to solve the goal automatically:
-```lean
+```
 grind_pattern gf => f x
 
 example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by
@@ -285,6 +298,25 @@ example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by
 You can enable the option `trace.grind.ematch.instance` to make `grind` print a
 trace message for each theorem instance it generates.
 
+You can also specify a **multi-pattern** to control when `grind` should apply a theorem.
+A multi-pattern requires that all specified patterns are matched in the current context
+before the theorem is applied. This is useful for theorems such as transitivity rules,
+where multiple premises must be simultaneously present for the rule to apply.
+The following example demonstrates this feature using a transitivity axiom for a binary relation `R`:
+```
+opaque R : Int → Int → Prop
+axiom Rtrans {x y z : Int} : R x y → R y z → R x z
+
+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
+```
+By specifying the multi-pattern `R x y, R y z`, we instruct `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`.
+
 Instead of using `grind_pattern` to explicitly specify a pattern,
 you can use the `@[grind]` attribute or one of its variants, which will use a heuristic to
 generate a (multi-)pattern. The complete list is available in the reference manual. The main ones are:
@@ -300,45 +332,61 @@ generate a (multi-)pattern. The complete list is available in the reference manu
 - `@[grind =]` checks 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.
 
-Main configuration options:
+Here is the previous example again but using the attribute `[grind →]`
+```
+opaque R : Int → Int → Prop
+@[grind →] axiom Rtrans {x y z : Int} : R x y → R y z → R x z
 
-- `grind (splits := <num>)` caps the *depth* of the search tree.  Once a branch performs `num` splits
-  `grind` stops splitting further in that branch.
-- `grind -splitIte` disables case splitting on if-then-else expressions.
-- `grind -splitMatch` disables case splitting on `match` expressions.
-- `grind +splitImp` instructs `grind` to split on any hypothesis `A → B` whose antecedent `A` is **propositional**.
+example {a b c d} : R a b → R b c → R c d → R a d := by
+  grind
+```
+
+To control theorem instantiation and avoid generating an unbounded number of instances,
+`grind` uses a generation counter. Terms in the original goal are assigned generation zero.
+When `grind` applies a theorem using terms of generation `≤ n`, any new terms it creates
+are assigned generation `n + 1`. This limits how far the tactic explores when applying
+theorems and helps prevent an excessive number of instantiations.
+
+#### Key options:
 - `grind (ematch := <num>)` controls the number of E-matching rounds.
 - `grind [<name>, ...]` instructs `grind` to use the declaration `name` during E-matching.
 - `grind only [<name>, ...]` is like `grind [<name>, ...]` but does not use theorems tagged with `@[grind]`.
 - `grind (gen := <num>)` sets the maximum generation.
-- `grind -ring` disables the ring solver based on Gröbner basis.
-- `grind (ringSteps := <num>)` limits the number of steps performed by ring solver.
-- `grind -cutsat` disables the linear integer arithmetic solver based on the cutsat procedure.
-- `grind -linarith` disables the linear arithmetic solver for (ordered) modules and rings.
 
-Examples:
+### Linear integer arithmetic (`cutsat`)
+
+`grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an
+integrated decision procedure called **`cutsat`**.  It understands
+
+* equalities   `p = 0`
+* inequalities  `p ≤ 0`
+* disequalities `p ≠ 0`
+* divisibility  `d ∣ p`
+
+The solver incrementally assigns integer values to variables; when a partial
+assignment violates a constraint it adds a new, implied constraint and retries.
+This *model-based* search is **complete for LIA**.
+
+#### Key options:
+
+* `grind -cutsat` disable the solver (useful for debugging)
+* `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ)
+
+#### Examples:
+
 ```
-example {a b} {as bs : List α} : (as ++ bs ++ [b]).getLastD a = b := by
+-- Even + even is never odd.
+example {x y : Int} : 2 * x + 4 * y ≠ 5 := by
   grind
 
-example (x : BitVec (w+1)) : (BitVec.cons x.msb (x.setWidth w)) = x := by
+-- Mixing equalities and inequalities.
+example {x y : Int} :
+    2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by
   grind
 
-example (a b c : UInt64) : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by
-  grind
-
-example [Field α] (a : α) : (2 : α) ≠ 0 → 1 / a + 1 / (2 * a) = 3 / (2 * a) := by
-  grind
-
-example (as : Array α) (lo hi i j : Nat) :
-    lo ≤ i → i < j → j ≤ hi → j < as.size → min lo (as.size - 1) ≤ i := by
-  grind
-
-example [CommRing α] [NoNatZeroDivisors α] (a b c : α)
-    : a + b + c = 3 →
-      a^2 + b^2 + c^2 = 5 →
-      a^3 + b^3 + c^3 = 7 →
-      a^4 + b^4 = 9 - c^4 := by
+-- Reasoning with divisibility.
+example (a b : Int) :
+    2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by
   grind
 
 example (x y : Int) :
@@ -347,6 +395,85 @@ example (x y : Int) :
     -10 ≤ 7*x - 9*y →
     7*x - 9*y ≤ 4 → False := by
   grind
+
+-- Types that implement the `ToInt` type-class.
+example (a b c : UInt64)
+    : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by
+  grind
+```
+
+### Algebraic solver (`ring`)
+
+`grind` ships with an algebraic solver nick-named **`ring`** for goals that can
+be phrased as polynomial equations (or disequations) over commutative rings,
+semirings, or fields.
+
+*Works out of the box*
+All core numeric types and relevant Mathlib types already provide the required
+type-class instances, so the solver is ready to use in most developments.
+
+What it can decide:
+
+* equalities of the form `p = q`
+* disequalities `p ≠ q`
+* basic reasoning under field inverses (`a / b := a * b⁻¹`)
+* goals that mix ring facts with other `grind` engines
+
+#### Key options:
+
+* `grind -ring` turn the solver off (useful when debugging)
+* `grind (ringSteps := n)` cap the number of steps performed by this procedure.
+
+#### Examples
+
+```
+open Lean Grind
+
+example [CommRing α] (x : α) : (x + 1) * (x - 1) = x^2 - 1 := by
+  grind
+
+-- Characteristic 256 means 16 * 16 = 0.
+example [CommRing α] [IsCharP α 256] (x : α) :
+    (x + 16) * (x - 16) = x^2 := by
+  grind
+
+-- Works on built-in rings such as `UInt8`.
+example (x : UInt8) : (x + 16) * (x - 16) = x^2 := by
+  grind
+
+example [CommRing α] (a b c : α) :
+    a + b + c = 3 →
+    a^2 + b^2 + c^2 = 5 →
+    a^3 + b^3 + c^3 = 7 →
+    a^4 + b^4 = 9 - c^4 := by
+  grind
+
+example [Field α] [NoNatZeroDivisors α] (a : α) :
+    1 / a + 1 / (2 * a) = 3 / (2 * a) := by
+  grind
+```
+
+### Other options
+
+- `grind (splits := <num>)` caps the *depth* of the search tree.  Once a branch performs `num` splits
+  `grind` stops splitting further in that branch.
+- `grind -splitIte` disables case splitting on if-then-else expressions.
+- `grind -splitMatch` disables case splitting on `match` expressions.
+- `grind +splitImp` instructs `grind` to split on any hypothesis `A → B` whose antecedent `A` is **propositional**.
+- `grind -linarith` disables the linear arithmetic solver for (ordered) modules and rings.
+
+### Additional Examples
+
+```
+example {a b} {as bs : List α} : (as ++ bs ++ [b]).getLastD a = b := by
+  grind
+
+example (x : BitVec (w+1)) : (BitVec.cons x.msb (x.setWidth w)) = x := by
+  grind
+
+example (as : Array α) (lo hi i j : Nat) :
+    lo ≤ i → i < j → j ≤ hi → j < as.size → min lo (as.size - 1) ≤ i := by
+  grind
 ```
 -/
 syntax (name := grind)

src/Lean/Meta/Basic.lean

@@ -1052,7 +1052,7 @@ Lift a `MkBindingM` monadic action `x` to `MetaM`.
     throwError "failed to create binder due to failure when reverting variable dependencies"
 
 /--
-Similar to `abstracM` but consider only the first `min n xs.size` entries in `xs`
+Similar to `abstractM` but consider only the first `min n xs.size` entries in `xs`
 
 It is also similar to `Expr.abstractRange`, but handles metavariables correctly.
 It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -69,7 +69,7 @@ structure Context where
   /--
   Stores the "parent" term for the term being simplified.
   If a simplification procedure result depends on this value,
-  then it is its reponsability to set `Result.cache := false`.
+  then it is its responsibility to set `Result.cache := false`.
 
   Motivation for this field:
   Suppose we have a simplification procedure for normalizing arithmetic terms.
@@ -107,7 +107,7 @@ structure Context where
   lctxInitIndices   : Nat := 0
   /--
   If `inDSimp := true`, then `simp` is in `dsimp` mode, and only applying
-  transformations that presereve definitional equality.
+  transformations that preserve definitional equality.
   -/
   inDSimp : Bool := false
   deriving Inhabited

tests/lean/run/grind_semiring.lean

@@ -39,3 +39,6 @@ trace: [grind.ring.assert.basis] ↑x + ↑y + -2 = 0
 set_option trace.grind.ring.assert.basis true in
 example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α) : x^2*y = 1 → x*y^2 = y → x + y = 2 → False := by
   grind
+
+example [CommSemiring α] [AddRightCancel α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
+  grind