Skip to content

Commit fc10fc3

Browse files
leodemouraleodemoura
committed
feat: add Init/Grind/Config.lean 
1 parent 77ddfd4 commit fc10fc3

File tree

3 files changed

+227
-219
lines changed

3 files changed

+227
-219
lines changed

‎src/Init/Grind/Config.lean‎

Lines changed: 216 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,216 @@
1+
/-
2+
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Leonardo de Moura
5+
-/
6+
module
7+
prelude
8+
public import Init.Core
9+
public section
10+
namespace Lean.Grind
11+
/--
12+
The configuration for `grind`.
13+
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
14+
-/
15+
structure Config where
16+
/-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
17+
trace : Bool := false
18+
/-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
19+
or for which no patterns can be generated. -/
20+
lax : Bool := false
21+
/-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
22+
and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
23+
premises : Bool := false
24+
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
25+
splits : Nat := 9
26+
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
27+
ematch : Nat := 5
28+
/--
29+
Maximum term generation.
30+
The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
31+
the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
32+
gen : Nat := 8
33+
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
34+
instances : Nat := 1000
35+
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
36+
matchEqs : Bool := true
37+
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
38+
splitMatch : Bool := true
39+
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
40+
splitIte : Bool := true
41+
/--
42+
If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
43+
Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
44+
splitIndPred : Bool := false
45+
/--
46+
If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
47+
if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
48+
-/
49+
splitImp : Bool := false
50+
/-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
51+
canonHeartbeats : Nat := 1000
52+
/-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
53+
ext : Bool := true
54+
/-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
55+
extAll : Bool := false
56+
/--
57+
If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
58+
and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
59+
which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
60+
-/
61+
etaStruct : Bool := true
62+
/--
63+
If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
64+
on equalities between lambda expressions.
65+
-/
66+
funext : Bool := true
67+
/-- TODO -/
68+
lookahead : Bool := true
69+
/-- If `verbose` is `false`, additional diagnostics information is not collected. -/
70+
verbose : Bool := true
71+
/-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
72+
clean : Bool := true
73+
/--
74+
If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
75+
using rational numbers, and ignoring divisibility constraints.
76+
This approach is cheaper but incomplete. -/
77+
qlia : Bool := false
78+
/--
79+
If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
80+
See paper "Model-based Theory Combination" for details.
81+
-/
82+
mbtc : Bool := true
83+
/--
84+
When set to `true` (default: `true`), local definitions are unfolded during normalization and internalization.
85+
In other words, given a local context with an entry `x : t := e`, the free variable `x` is reduced to `e`.
86+
Note that this behavior is also available in `simp`, but there its default is `false` because `simp` is not
87+
always used as a terminal tactic, and it important to preserve the abstractions introduced by users.
88+
Additionally, in `grind` we observed that `zetaDelta` is particularly important when combined with function induction.
89+
In such scenarios, the same let-expressions can be introduced by function induction and also by unfolding the
90+
corresponding definition. We want to avoid a situation in which `zetaDelta` is not applied to let-declarations
91+
introduced by function induction while `zeta` unfolds the definition, causing a mismatch.
92+
Finally, note that congruence closure is less effective on terms containing many binders such as
93+
`lambda` and `let` expressions.
94+
-/
95+
zetaDelta := true
96+
/--
97+
When `true` (default: `true`), performs zeta reduction of let expressions during normalization.
98+
That is, `let x := v; e[x]` reduces to `e[v]`. See also `zetaDelta`.
99+
-/
100+
zeta := true
101+
/--
102+
When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
103+
This solver also support commutative semirings, fields, and normalizer non-commutative rings and
104+
semirings.
105+
-/
106+
ring := true
107+
/--
108+
Maximum number of steps performed by the `ring` solver.
109+
A step is counted whenever one polynomial is used to simplify another.
110+
For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
111+
used to simplify the second to `-1 * y^3 + x * y`.
112+
-/
113+
ringSteps := 10000
114+
/--
115+
When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
116+
`CommRing`.
117+
-/
118+
linarith := true
119+
/--
120+
When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
121+
-/
122+
cutsat := true
123+
/--
124+
When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
125+
-/
126+
ac := true
127+
/--
128+
Maximum number of steps performed by the `ac` solver.
129+
A step is counted whenever one AC equation is used to simplify another.
130+
For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
131+
used to simplify the second to `max w y = x`.
132+
-/
133+
acSteps := 1000
134+
/--
135+
Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
136+
the characteristic of a ring.
137+
-/
138+
exp : Nat := 2^20
139+
/--
140+
When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
141+
-/
142+
abstractProof := true
143+
/--
144+
When `true` (default: `true`), enables the procedure for handling injective functions.
145+
In this mode, `grind` takes into account theorems such as:
146+
```
147+
@[grind inj] theorem double_inj : Function.Injective double
148+
```
149+
-/
150+
inj := true
151+
/--
152+
When `true` (default: `true`), enables the procedure for handling orders that implement
153+
at least `Std.IsPreorder`
154+
-/
155+
order := true
156+
/--
157+
When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
158+
the future.
159+
-/
160+
offset := true
161+
deriving Inhabited, BEq
162+
163+
/--
164+
Configuration for interactive mode.
165+
We disable `clean := false`.
166+
-/
167+
structure ConfigInteractive extends Config where
168+
clean := false
169+
170+
/--
171+
A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
172+
`grind` will not do anything in this configuration,
173+
which can be used a starting point for minimal configurations.
174+
-/
175+
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
176+
structure NoopConfig extends Config where
177+
-- Disable splitting
178+
splits := 0
179+
-- We don't override the various `splitMatch` / `splitIte` settings separately.
180+
181+
-- Disable e-matching
182+
ematch := 0
183+
-- We don't override `matchEqs` separately.
184+
185+
-- Disable extensionality
186+
ext := false
187+
extAll := false
188+
etaStruct := false
189+
funext := false
190+
191+
-- Disable all solver modules
192+
ring := false
193+
linarith := false
194+
cutsat := false
195+
ac := false
196+
197+
/--
198+
A `grind` configuration that only uses `cutsat` and splitting.
199+
200+
Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
201+
We don't currently have a mechanism to enable only a small set of lemmas.
202+
-/
203+
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
204+
structure CutsatConfig extends NoopConfig where
205+
cutsat := true
206+
-- Allow the default number of splits.
207+
splits := ({} : Config).splits
208+
209+
/--
210+
A `grind` configuration that only uses `ring`.
211+
-/
212+
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
213+
structure GrobnerConfig extends NoopConfig where
214+
ring := true
215+
216+
end Lean.Grind

‎src/Init/Grind/Interactive.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,16 @@ when selecting patterns.
1616
-/
1717
syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
1818

19+
/-!
20+
`grind` tactic and related tactics.
21+
-/
22+
syntax grindErase := "-" ident
23+
/--
24+
The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
25+
when selecting patterns.
26+
-/
27+
syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin
28+
1929
namespace Grind
2030
declare_syntax_cat grind_filter (behavior := both)
2131

0 commit comments

Comments
 (0)