16.11.1. Entry Points🔗

There are two versions of grind's interactive mode. The first, introduced with Lean.Parser.Tactic.grind : tactic`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. See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information. `grind` is *not* designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm `grind`’s branching search. 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*. ### 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: ``` def f (a : Nat) : Nat := a + 1 def g (a : Nat) : Nat := a - 1 @[grind =] theorem gf (x : Nat) : g (f x) = x := by simp [f, g] ``` 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 E-matching. Suppose we now have a goal involving: ``` example {a b} (h : f b = a) : g a = b := by grind ``` Although `g a` is not an instance of the pattern `g (f x)`, it becomes one modulo the equation `f b = a`. By substituting `a` with `f b` in `g a`, we obtain the term `g (f b)`, which matches the pattern `g (f x)` with the assignment `x := b`. Thus, the theorem `gf` is instantiated with `x := b`, and the new equality `g (f b) = b` is asserted. `grind` then uses congruence closure to derive the implied equality `g a = g (f b)` and completes the proof. The pattern used to instantiate theorems affects the effectiveness of `grind`. 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`. ``` example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: ``` grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: - `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. - `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion. - `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered. - `@[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. 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 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. ### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an integrated decision procedure called **`lia`**. 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 -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: ``` -- Even + even is never odd. example {x y : Int} : 2 * x + 4 * y ≠ 5 := by grind -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by grind -- Reasoning with divisibility. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by grind example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -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 ``` grind =>, is designed for controlling grind and automatically takes certain steps that are needed for most proofs. The other, introduced with sym, allows a higher degree of manual control and is intended for use in symbolic simulation workflows.

When used with a script, grind initializes the proof by introducing all hypotheses and then invoking proof by contradiction so the initial goal is always False. It then runs the script.

tactic ::= ...
    | `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.

See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information.

`grind` is *not* designed for goals whose search space explodes combinatorially,
think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards,
or a 200‑variable Sudoku encoded as Boolean constraints.  Such encodings require
 thousands (or millions) of case‑splits that overwhelm `grind`’s branching search.

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*.

### 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:
```
def f (a : Nat) : Nat :=
  a + 1

def g (a : Nat) : Nat :=
  a - 1

@[grind =]
theorem gf (x : Nat) : g (f x) = x := by
  simp [f, g]
```
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 E-matching.
Suppose we now have a goal involving:
```
example {a b} (h : f b = a) : g a = b := by
  grind
```
Although `g a` is not an instance of the pattern `g (f x)`,
it becomes one modulo the equation `f b = a`. By substituting `a`
with `f b` in `g a`, we obtain the term `g (f b)`,
which matches the pattern `g (f x)` with the assignment `x := b`.
Thus, the theorem `gf` is instantiated with `x := b`,
and the new equality `g (f b) = b` is asserted.
`grind` then uses congruence closure to derive the implied equality
`g a = g (f b)` and completes the proof.

The pattern used to instantiate theorems affects the effectiveness of `grind`.
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`.

```
example (h₁ : f b = a) (h₂ : f c = a) : b = c := by
  grind
```

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:
```
grind_pattern gf => f x

example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by
  grind
```
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:

- `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning).
  In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable
  (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not
  previously covered, it will add that subexpression as a pattern, until all arguments have been covered.
- `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning).
  This may fail if not all the arguments to the theorem appear in the conclusion.
- `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage,
  stopping when all arguments are covered.
- `@[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.

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

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.

### Linear integer arithmetic (`lia`)

`grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an
integrated decision procedure called **`lia`**.  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 -lia` disable the solver (useful for debugging)
* `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ)

#### Examples:

```
-- Even + even is never odd.
example {x y : Int} : 2 * x + 4 * y ≠ 5 := by
  grind

-- Mixing equalities and inequalities.
example {x y : Int} :
    2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by
  grind

-- Reasoning with divisibility.
example (a b : Int) :
    2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by
  grind

example (x y : Int) :
    27 ≤ 11*x + 13*y →
    11*x + 13*y ≤ 45 →
    -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
```
grind Configuration options for tactics. optConfig only? ([ The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
when selecting patterns.
grindParam,* ] )? => grindSeq

Unlike grind, the sym tactic does not begin by introducing hypotheses or invoking proof by contradiction. The author of the script has full control over the context and goal.

tactic ::= ...
    | `sym` enters an interactive symbolic simulation mode built on `grind`.
Unlike `grind =>`, it does not eagerly introduce hypotheses or apply by-contradiction,
giving the user explicit control over `intro`, `apply`, and `internalize` steps.

Example:
```
example (x : Nat) : myP x → myQ x := by
  sym [myP_myQ] =>
    intro h
    finish
```
sym Configuration options for tactics. optConfig only? ([ The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
when selecting patterns.
grindParam,* ] )? => grindSeq

Both tactics accept the same configuration options, the Lean.Parser.Tactic.grind : tactic`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. See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information. `grind` is *not* designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm `grind`’s branching search. 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*. ### 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: ``` def f (a : Nat) : Nat := a + 1 def g (a : Nat) : Nat := a - 1 @[grind =] theorem gf (x : Nat) : g (f x) = x := by simp [f, g] ``` 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 E-matching. Suppose we now have a goal involving: ``` example {a b} (h : f b = a) : g a = b := by grind ``` Although `g a` is not an instance of the pattern `g (f x)`, it becomes one modulo the equation `f b = a`. By substituting `a` with `f b` in `g a`, we obtain the term `g (f b)`, which matches the pattern `g (f x)` with the assignment `x := b`. Thus, the theorem `gf` is instantiated with `x := b`, and the new equality `g (f b) = b` is asserted. `grind` then uses congruence closure to derive the implied equality `g a = g (f b)` and completes the proof. The pattern used to instantiate theorems affects the effectiveness of `grind`. 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`. ``` example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: ``` grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: - `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. - `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion. - `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered. - `@[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. 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 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. ### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an integrated decision procedure called **`lia`**. 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 -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: ``` -- Even + even is never odd. example {x y : Int} : 2 * x + 4 * y ≠ 5 := by grind -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by grind -- Reasoning with divisibility. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by grind example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -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 ``` only modifier, and the bracketed list of theorems and parameters that ordinary grind accepts. Certain features that are invoked automatically by grind and manually in sym have dedicated tactics that are described in the symbolic simulation mode section.

The grind? tactic takes the same arguments as grind but does not support entering interactive mode. It suggests an equivalent Lean.Parser.Tactic.grind : tactic`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. See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information. `grind` is *not* designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm `grind`’s branching search. 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*. ### 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: ``` def f (a : Nat) : Nat := a + 1 def g (a : Nat) : Nat := a - 1 @[grind =] theorem gf (x : Nat) : g (f x) = x := by simp [f, g] ``` 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 E-matching. Suppose we now have a goal involving: ``` example {a b} (h : f b = a) : g a = b := by grind ``` Although `g a` is not an instance of the pattern `g (f x)`, it becomes one modulo the equation `f b = a`. By substituting `a` with `f b` in `g a`, we obtain the term `g (f b)`, which matches the pattern `g (f x)` with the assignment `x := b`. Thus, the theorem `gf` is instantiated with `x := b`, and the new equality `g (f b) = b` is asserted. `grind` then uses congruence closure to derive the implied equality `g a = g (f b)` and completes the proof. The pattern used to instantiate theorems affects the effectiveness of `grind`. 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`. ``` example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: ``` grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: - `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. - `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion. - `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered. - `@[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. 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 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. ### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an integrated decision procedure called **`lia`**. 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 -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: ``` -- Even + even is never odd. example {x y : Int} : 2 * x + 4 * y ≠ 5 := by grind -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by grind -- Reasoning with divisibility. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by grind example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -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 ``` grind only call, as well as an equivalent script. Within an interactive grind script, the finish? and cases? tactics similarly suggest scripts.

16.11.2. The grind Tactic Language🔗

The sequence of steps that follow Lean.Parser.Tactic.grind : tactic`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. See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information. `grind` is *not* designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm `grind`’s branching search. 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*. ### 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: ``` def f (a : Nat) : Nat := a + 1 def g (a : Nat) : Nat := a - 1 @[grind =] theorem gf (x : Nat) : g (f x) = x := by simp [f, g] ``` 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 E-matching. Suppose we now have a goal involving: ``` example {a b} (h : f b = a) : g a = b := by grind ``` Although `g a` is not an instance of the pattern `g (f x)`, it becomes one modulo the equation `f b = a`. By substituting `a` with `f b` in `g a`, we obtain the term `g (f b)`, which matches the pattern `g (f x)` with the assignment `x := b`. Thus, the theorem `gf` is instantiated with `x := b`, and the new equality `g (f b) = b` is asserted. `grind` then uses congruence closure to derive the implied equality `g a = g (f b)` and completes the proof. The pattern used to instantiate theorems affects the effectiveness of `grind`. 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`. ``` example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: ``` grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: - `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. - `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion. - `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered. - `@[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. 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 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. ### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an integrated decision procedure called **`lia`**. 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 -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: ``` -- Even + even is never odd. example {x y : Int} : 2 * x + 4 * y ≠ 5 := by grind -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by grind -- Reasoning with divisibility. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by grind example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -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 ``` grind => is written in an indented block, with one step on each line; multiple steps may also be separated by ;. As an alternative to indentation, they may be enclosed in braces. Such a sequence is represented by the syntax category grindSeq.

Just as in an ordinary Lean tactic script, grind tactics manipulate a proof state that consists of a sequence of goals, each of which consists of a sequence of assumptions and a conclusion. When there are no further goals, the proof is complete. Most tactics operate on the main goal, and goal-management tactics redistribute goals across steps exactly as their ordinary tactic counterparts do. Additionally, grind tactics have access to the “whiteboard”.

grind_filter ::= ...
    | gen < num

grind_filter ::= ...
    | gen ≤ num

grind_filter ::= ...
    | gen <= num

grind_filter ::= ...
    | gen = num

grind_filter ::= ...
    | gen != num

grind_filter ::= ...
    | gen ≥ num

grind_filter ::= ...
    | gen >= num

grind_filter ::= ...
    | gen > num

grind_filter ::= ...
    | ident

grind_filter ::= ...
    | (grind_filter)

grind_filter ::= ...
    | grind_filter && grind_filter

grind_filter ::= ...
    | grind_filter || grind_filter

grind_filter ::= ...
    | !grind_filter

[grind] Grind state
  [facts] Asserted facts
  [props] True propositions
    [_] ∀ (f : Fruit), pulp f = Color.red
  [eqc] Equivalence classes
    [eqc] {peel Fruit.cherry, pulp Fruit.cherry}

16.11.3. Goal Management and Sequencing🔗

These tactics don't invoke a solver or modify the grind state. They mirror the corresponding control structures and tactics in the primary tactic language.

skip

done

A sequence may be grouped with parentheses, written ( steps ), which runs the enclosed steps on the current goals with no added effect. This grouping is used to delimit the scope of a control structure such as first or repeat.

focus

next =>

·

The bullet is shorthand for next. It focuses on the main goal, suppressing all others. It is an error if the enclosed tactic script does not result in a successful proof of the focused goal.

all_goals

any_goals

first

try

repeat

fail_if_success

fail

<;>

16.11.4. Completing Proofs🔗

These tactics close goals, either by handing control back to grind's automatic search or by escaping into Lean's ordinary tactic language. Goals may also be closed by one of the theory solvers.

finish

finish?

When finish? closes a goal, it offers a code action that replaces the call with the script it discovered, just as grind? suggests a Lean.Parser.Tactic.grind : tactic`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. See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information. `grind` is *not* designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm `grind`’s branching search. 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*. ### 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: ``` def f (a : Nat) : Nat := a + 1 def g (a : Nat) : Nat := a - 1 @[grind =] theorem gf (x : Nat) : g (f x) = x := by simp [f, g] ``` 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 E-matching. Suppose we now have a goal involving: ``` example {a b} (h : f b = a) : g a = b := by grind ``` Although `g a` is not an instance of the pattern `g (f x)`, it becomes one modulo the equation `f b = a`. By substituting `a` with `f b` in `g a`, we obtain the term `g (f b)`, which matches the pattern `g (f x)` with the assignment `x := b`. Thus, the theorem `gf` is instantiated with `x := b`, and the new equality `g (f b) = b` is asserted. `grind` then uses congruence closure to derive the implied equality `g a = g (f b)` and completes the proof. The pattern used to instantiate theorems affects the effectiveness of `grind`. 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`. ``` example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: ``` grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: - `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. - `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion. - `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered. - `@[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. 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 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. ### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an integrated decision procedure called **`lia`**. 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 -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: ``` -- Even + even is never odd. example {x y : Int} : 2 * x + 4 * y ≠ 5 := by grind -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by grind -- Reasoning with divisibility. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by grind example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -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 ``` grind only call. This enables an interactive workflow where parts of the proof can be discovered by grind and then manually modified if needed.

sorry

admit

tactic =>

exact

16.11.5. Theory Solvers🔗

Each of these tactics runs one of grind's decision procedures on the current state.

lia

linarith

ring

ac

16.11.6. Theorem Instantiation🔗

These tactics add new facts to the grind state (that is, the “whiteboard”) by instantiating theorems.

instantiate

instantiate runs a single round of E-matching. By default, this round uses all of grind's currently active theorems; the bracketed list supplies further theorems to instantiate alongside them, and an anchor adds a specific local theorem from the state. Running show_local_thms displays the local theorems' anchors. The Lean.Parser.Tactic.Grind.instantiate : grindInstantiates theorems using E-matching. The `approx` modifier is just a marker for users to easily identify automatically generated `instantiate` tactics that may have redundant arguments. only modifier restricts the round to the listed theorems.

The Lean.Parser.Tactic.Grind.instantiate : grindInstantiates theorems using E-matching. The `approx` modifier is just a marker for users to easily identify automatically generated `instantiate` tactics that may have redundant arguments. approx modifier has no effect on how the step runs. It is a marker that appears in automatically generated scripts, such as those suggested by grind? and finish?, when grind cannot determine a precise list of theorems for the step. It signals that the listed theorems are an approximation that may need to be adjusted by hand.

[thms] Local theorems
[thm] #7468 := ∀ (n : Nat), f n ≤ n * n

use

mbtc

16.11.7. Case Analysis🔗

These tactics invoke grind's case splitting.

cases

cases?

cases_next

16.11.8. State Inspection🔗

Many of the tactics in this section take an optional filter as a parameter. This filter should be provided without the | character, because that invokes the general state display mechanism instead of customizing the tactic's display.

[grind] Grind state
[facts] Asserted facts
[_] peel Fruit.cherry = pulp Fruit.cherry
[_] ∀ (f : Fruit), pulp f = Color.red
[_] ¬peel Fruit.cherry = Color.red
[props] True propositions
[_] ∀ (f : Fruit), pulp f = Color.red
[props] False propositions
[_] peel Fruit.cherry = Color.red
[eqc] Equivalence classes
[eqc] {peel Fruit.cherry, pulp Fruit.cherry}

show_state

show_asserted

show_true

show_false

show_eqcs

show_cases

show_local_thms

show_goals

show_term

16.11.9. Local Context and Naming🔗

These tactics add hypotheses to the local context and make inaccessible names available to later steps.

have

A second form of Lean.Parser.Tactic.Grind.haveSilent : grindProves `<term>` using the current `grind` state and default search strategy. have, written have h : t with no value, proves t from the current grind state using the default search strategy and adds it as a hypothesis.

have

rename_i

expose_names

16.11.10. Configuration🔗

These tactics run a sequence of grind tactics with modified options or configuration.

set_option

set_config

16.11.11. Symbolic Simulation Mode🔗

The sym tactic is a lower-level version of Lean.Parser.Tactic.grind : tactic`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. See [the reference manual's chapter on `grind`](https://lean-lang.org/doc/reference/4.31.0/find/?domain=Verso.Genre.Manual.section&name=grind-tactic) for more information. `grind` is *not* designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm `grind`’s branching search. 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*. ### 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: ``` def f (a : Nat) : Nat := a + 1 def g (a : Nat) : Nat := a - 1 @[grind =] theorem gf (x : Nat) : g (f x) = x := by simp [f, g] ``` 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 E-matching. Suppose we now have a goal involving: ``` example {a b} (h : f b = a) : g a = b := by grind ``` Although `g a` is not an instance of the pattern `g (f x)`, it becomes one modulo the equation `f b = a`. By substituting `a` with `f b` in `g a`, we obtain the term `g (f b)`, which matches the pattern `g (f x)` with the assignment `x := b`. Thus, the theorem `gf` is instantiated with `x := b`, and the new equality `g (f b) = b` is asserted. `grind` then uses congruence closure to derive the implied equality `g a = g (f b)` and completes the proof. The pattern used to instantiate theorems affects the effectiveness of `grind`. 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`. ``` example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: ``` grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind ``` 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: - `@[grind →]` will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. - `@[grind ←]` will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion. - `@[grind]` will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered. - `@[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. 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 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. ### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an integrated decision procedure called **`lia`**. 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 -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: ``` -- Even + even is never odd. example {x y : Int} : 2 * x + 4 * y ≠ 5 := by grind -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by grind -- Reasoning with divisibility. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by grind example (x y : Int) : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 → -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 ``` grind => that provides a higher degree of manual control over the state. When run, sym enters interactive mode without the eager introduction of hypotheses and use of proof by contradiction that grind performs.

When using sym, assumptions must be manually introduced, just as in the standard proof tactic language. Introducing an assumption moves it from the goal's conclusion into a new hypothesis. It is often also useful to add the assumption to the “whiteboard”, so that it participates in congruence closure and grind's other processes. Adding a hypothesis or term to the whiteboard is called internalization. Once internalized, a hypothesis participates in congruence reasoning, constraint propagation, and the theory solvers; until then, grind does not reason about it.

The following tactics are available only after sym; they are not available in plain interactive grind because it carries out their operations automatically when needed.

intro

intro a b

[grind] Grind state

[grind] Grind state
[facts] Asserted facts
[_] a = b
[eqc] Equivalence classes
[eqc] {a, b}

intro a b

[grind] Grind state

[grind] Grind state

The shorthand intro~ introduces binders without internalizing them, equivalent to intro (internalize := false).

intros

The shorthand intros~ introduces all remaining binders without internalizing them.

apply

internalize

internalize_all

by_contra

The simp and dsimp tactics in sym scripts run grind's own simplifier, a separate implementation built for its internal representation of terms, with its own performance characteristics and feature set. This simplifier operates directly on that representation and avoids testing definitional equality. Instead of simp sets, it uses named variants: named bundles of simprocs (to be run before and after simplification) along with configuration overrides. Named variants are described in more detail in the next section.

simp

dsimp

command ::= ...
    | Register a named `Sym.simp` variant.

```
register_sym_simp myVariant where
  pre  := telescope
  post := ground >> rewrite [thm1, thm2] with self
  maxSteps := 50000
```
register_sym_simp ident where
        sym_simp_field*

register_sym_simp myVariant where
  pre  := telescope
  post := ground >> rewrite [thm1, thm2] with self
  maxSteps := 50000

command ::= ...
    | Register a named `Sym.dsimp` variant.

```
register_sym_dsimp myVariant where
  pre  := match
  post := ground >> zeta_delta
  maxSteps := 50000
```
register_sym_dsimp ident where
        sym_dsimp_field*

register_sym_dsimp myVariant where
  pre  := match
  post := ground >> zeta_delta
  maxSteps := 50000