def Lean.Grind.genPattern {α : Sort u} (_h : Prop) (x _val : α) : α

Gadget for representing generalization steps h : x = val in patterns This gadget is used to represent patterns in theorems that have been generalized to reduce the number of casts introduced during E-matching based instantiation.

For example, consider the theorem

Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
    {f : (a_1 : α1) → some a = some a_1 → Option α2}
    : (some a).pbind f = f a rfl

Now, suppose we have a goal containing the term c.pbind g and the equivalence class {c, some b}. The E-matching module generates the instance

(some b).pbind (cast ⋯ g)

The cast is necessary because g's type contains c instead of some b. This cast` problematic because we don't have a systematic way of pushing casts over functions to its arguments. Moreover, heterogeneous equality is not effective because the following theorem is not provable in DTT:

theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...

The standard solution is to generalize the theorem above and write it as

theorem Option.pbind_some'
        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
        {x : Option α1}
        {f : (a_1 : α1) → x = some a_1 → Option α2}
        (h : x = some a)
        : x.pbind f = f a h := by
  subst h
  apply Option.pbind_some

Internally, we use this gadget to mark the E-matching pattern as

(genPattern h x (some a)).pbind f

This pattern is matched in the same way we match (some a).pbind f, but it saves the proof for the actual term to the some-application in f, and the actual term in x.

In the example above, c.pbind g also matches the pattern (genPattern h x (some a)).pbind f, and stores c in x, b in a, and the proof that c = some b in h.

Equations

• Lean.Grind.genPattern _h x _val = x

def Lean.Grind.genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α

Similar to genPattern but for the heterogeneous case

Equations

• Lean.Grind.genHEqPattern _h x _val = x

def Lean.Parser.resetGrindAttrs : ParserDescr

Reset all grind attributes. This command is intended for testing purposes only and should not be used in applications.

Equations

• Lean.Parser.resetGrindAttrs = Lean.ParserDescr.node `Lean.Parser.resetGrindAttrs 1024 (Lean.ParserDescr.symbol "reset_grind_attrs%")

def Lean.Parser.Attr.grindGen : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEq : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEqBoth : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEqRhs : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEqBwd : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindBwd : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindFwd : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindRL : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindLR : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindUsr : ParserDescr

Equations

• Lean.Parser.Attr.grindUsr = Lean.ParserDescr.nodeWithAntiquot "grindUsr" `Lean.Parser.Attr.grindUsr (Lean.ParserDescr.nonReservedSymbol "usr" false)

def Lean.Parser.Attr.grindCases : ParserDescr

Equations

• Lean.Parser.Attr.grindCases = Lean.ParserDescr.nodeWithAntiquot "grindCases" `Lean.Parser.Attr.grindCases (Lean.ParserDescr.nonReservedSymbol "cases" false)

def Lean.Parser.Attr.grindCasesEager : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindIntro : ParserDescr

Equations

• Lean.Parser.Attr.grindIntro = Lean.ParserDescr.nodeWithAntiquot "grindIntro" `Lean.Parser.Attr.grindIntro (Lean.ParserDescr.nonReservedSymbol "intro" false)

def Lean.Parser.Attr.grindExt : ParserDescr

Equations

• Lean.Parser.Attr.grindExt = Lean.ParserDescr.nodeWithAntiquot "grindExt" `Lean.Parser.Attr.grindExt (Lean.ParserDescr.nonReservedSymbol "ext" false)

def Lean.Parser.Attr.grindMod : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grind : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grind? : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Grind.Config : Type

The configuration for grind. Passed to grind using, for example, the grind (config := { matchEqs := true }) syntax.

• trace : Bool

  If trace is true, grind records used E-matching theorems and case-splits.

• splits : Nat

  Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization.

• ematch : Nat

  Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split.

• gen : Nat

  Maximum term generation. The input goal terms have generation 0. When we instantiate a theorem using a term from generation n, the new terms have generation n+1. Thus, this parameter limits the length of an instantiation chain.

• instances : Nat

  Maximum number of theorem instances generated using E-matching in a proof search tree branch.

• matchEqs : Bool

  If matchEqs is true, grind uses match-equations as E-matching theorems.

• splitMatch : Bool

  If splitMatch is true, grind performs case-splitting on match-expressions during the search.

• splitIte : Bool

  If splitIte is true, grind performs case-splitting on if-then-else expressions during the search.

• splitIndPred : Bool

  If splitIndPred is true, grind performs case-splitting on inductive predicates. Otherwise, it performs case-splitting only on types marked with [grind cases] attribute.

• splitImp : Bool

  If splitImp is true, then given an implication p → q or (h : p) → q h, grind splits on p if the implication is true. Otherwise, it will split only if p is an arithmetic predicate.

• canonHeartbeats : Nat

  Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test.

• ext : Bool

  If ext is true, grind uses extensionality theorems that have been marked with [grind ext].

• extAll : Bool

  If extAll is true, grind uses any extensionality theorems available in the environment.

• etaStruct : Bool

  If etaStruct is true, then for each term t : S such that S is a structure, and is tagged with [grind ext], grind adds the equation t = ⟨t.1, ..., t.n⟩ which holds by reflexivity. Moreover, the extensionality theorem for S is not used.

• funext : Bool

  If funext is true, grind creates new opportunities for applying function extensionality by case-splitting on equalities between lambda expressions.

• lookahead : Bool

  TODO

• verbose : Bool

  If verbose is false, additional diagnostics information is not collected.

• clean : Bool

  If clean is true, grind uses expose_names and only generates accessible names.

• qlia : Bool

  If qlia is true, grind may generate counterexamples for integer constraints using rational numbers, and ignoring divisibility constraints. This approach is cheaper but incomplete.

• mbtc : Bool

  If mbtc is true, grind will use model-based theory combination for creating new case splits. See paper "Model-based Theory Combination" for details.

• zetaDelta : Bool

  When set to true (default: true), local definitions are unfolded during normalization and internalization. In other words, given a local context with an entry x : t := e, the free variable x is reduced to e. Note that this behavior is also available in simp, but there its default is false because simp is not always used as a terminal tactic, and it important to preserve the abstractions introduced by users. Additionally, in grind we observed that zetaDelta is particularly important when combined with function induction. In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the corresponding definition. We want to avoid a situation in which zetaDelta is not applied to let-declarations introduced by function induction while zeta unfolds the definition, causing a mismatch. Finally, note that congruence closure is less effective on terms containing many binders such as lambda and let expressions.

• zeta : Bool

  When true (default: true), performs zeta reduction of let expressions during normalization. That is, let x := v; e[x] reduces to e[v]. See also zetaDelta.

• ring : Bool

  When true (default: true), uses procedure for handling equalities over commutative rings.

• ringSteps : Nat
• ringNull : Bool

  When true (default: false), the commutative ring procedure in grind constructs stepwise proof terms, instead of a single-step Nullstellensatz certificate

• linarith : Bool

  When true (default: true), uses procedure for handling linear arithmetic for IntModule, and CommRing.

• cutsat : Bool

  When true (default: true), uses procedure for handling linear integer arithmetic for Int and Nat.

instance Lean.Grind.instInhabitedConfig : Inhabited Config

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Grind.instBEqConfig : BEq Config

Equations

• Lean.Grind.instBEqConfig = { beq := Lean.Grind.beqConfig✝ }

grind tactic and related tactics.

def Lean.Parser.Tactic.grindErase : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.grindLemma : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.grindParam : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.grind : ParserDescr

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

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.

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 heuristic instantiation via 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.

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.

Main configuration 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 (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:

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 (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
  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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.grindTrace : ParserDescr

grind? takes the same arguments as grind, but reports an equivalent call to grind only that would be sufficient to close the goal. This is useful for reducing the size of the grind theorems in a local invocation.

Equations

• One or more equations did not get rendered due to their size.