Init.Grind.Config

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.
lax : Bool
If lax is true, grind will silently ignore any parameters referring to non-existent theorems or for which no patterns can be generated.
suggestions : Bool
If suggestions is true, grind will invoke the currently configured library suggestion engine on the current goal, and add attempt to use the resulting suggestions as additional parameters to the grind tactic.
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. This solver also support commutative semirings, fields, and normalizer non-commutative rings and semirings.
ringSteps : Nat
Maximum number of steps performed by the ring solver. A step is counted whenever one polynomial is used to simplify another. For example, given x^2 + 1 and x^2 * y^3 + x * y, the first can be used to simplify the second to -1 * y^3 + x * y.
linarith : Bool
When true (default: true), uses procedure for handling linear arithmetic for IntModule, and CommRing.
lia : Bool
When true (default: true), uses procedure for handling linear integer arithmetic for Int and Nat.
ac : Bool
When true (default: true), uses procedure for handling associative (and commutative) operators.
acSteps : Nat
Maximum number of steps performed by the ac solver. A step is counted whenever one AC equation is used to simplify another. For example, given ma x z = w and max x (max y z) = x, the first can be used to simplify the second to max w y = x.
exp : Nat
Maximum exponent eagerly evaluated while computing bounds for ToInt and the characteristic of a ring.
abstractProof : Bool
When true (default: true), automatically creates an auxiliary theorem to store the proof.
inj : Bool
When true (default: true), enables the procedure for handling injective functions. In this mode, grind takes into account theorems such as:
```
@[grind inj] theorem double_inj : Function.Injective double
```
order : Bool
When true (default: true), enables the procedure for handling orders that implement at least Std.IsPreorder
min : Nat
Minimum number of instantiations to trigger summary report in #grind_lint. Remark: this option is only relevant for the #grind_lint command.
detailed : Nat
Minimum number of instantiations to trigger detailed report in #grind_lint. Remark: this option is only relevant for the #grind_lint command.
useSorry : Bool
When trace := true, uses sorry to close unsolved branches.

Instances For

source

def Lean.Grind.instInhabitedConfig.default :

Config

Equations

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

Instances For

source

instance Lean.Grind.instInhabitedConfig :

Inhabited Config

Equations

Lean.Grind.instInhabitedConfig = { default := Lean.Grind.instInhabitedConfig.default }

source

def Lean.Grind.instBEqConfig.beq :

Config → Config → Bool

Equations

One or more equations did not get rendered due to their size.
Lean.Grind.instBEqConfig.beq x✝¹ x✝ = false

Instances For

source

instance Lean.Grind.instBEqConfig :

BEq Config

Equations

Lean.Grind.instBEqConfig = { beq := Lean.Grind.instBEqConfig.beq }

source

structure Lean.Grind.ConfigInteractiveextends Lean.Grind.Config :

Type

Configuration for interactive mode. We disable clean := false.

Instances For

source

structure Lean.Grind.NoopConfigextends Lean.Grind.Config :

Type

A minimal configuration, with ematching and splitting disabled, and all solver modules turned off. grind will not do anything in this configuration, which can be used a starting point for minimal configurations.

Instances For

source

structure Lean.Grind.CutsatConfigextends Lean.Grind.NoopConfig :

Type

A grind configuration that only uses cutsat and splitting.

Note: cutsat benefits from some amount of instantiation, e.g. Nat.max_def. We don't currently have a mechanism to enable only a small set of lemmas.

Instances For

source

structure Lean.Grind.GrobnerConfigextends Lean.Grind.NoopConfig :

Type

A grind configuration that only uses ring.

Instances For