feat: add cdot combinator in grind tactic mode (#10975)
This PR adds the combinator ` · t_1 ... t_n` to the `grind` interactive
mode. The `finish?` tactic now generates scripts using this combinator
to conform to Mathlib coding standards. The new format is also more
compact. Example:
```lean
/--
info: Try this:
[apply] ⏎
instantiate only [= mem_indices_of_mem, insert, = getElem_def]
instantiate only [= getElem?_neg, = getElem?_pos]
cases #f590
· cases #ffdf
· instantiate only
instantiate only [= Array.getElem_set]
· instantiate only
instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
· instantiate only [= mem_indices_of_mem, = getElem_def]
instantiate only [usr getElem_indices_lt]
instantiate only [size]
cases #ffdf
· instantiate only [=_ WF]
instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
instantiate only [WF']
· instantiate only
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-/
#guard_msgs in
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
(m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
grind => finish?
```
This commit is contained in:
Leonardo de Moura
GitHub
parent
77ddfd49e6
commit
50e2fdaa74
7 changed files with 280 additions and 288 deletions
216
src/Init/Grind/Config.lean
Normal file
216
src/Init/Grind/Config.lean
Normal file
|
|
@ -0,0 +1,216 @@
|
|||
/-
|
||||
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
module
|
||||
prelude
|
||||
public import Init.Core
|
||||
public section
|
||||
namespace Lean.Grind
|
||||
/--
|
||||
The configuration for `grind`.
|
||||
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
|
||||
-/
|
||||
structure Config where
|
||||
/-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
|
||||
trace : Bool := false
|
||||
/-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
|
||||
or for which no patterns can be generated. -/
|
||||
lax : Bool := false
|
||||
/-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
|
||||
and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
|
||||
premises : Bool := false
|
||||
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
|
||||
splits : Nat := 9
|
||||
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
|
||||
ematch : Nat := 5
|
||||
/--
|
||||
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. -/
|
||||
gen : Nat := 8
|
||||
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
|
||||
instances : Nat := 1000
|
||||
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
|
||||
matchEqs : Bool := true
|
||||
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
|
||||
splitMatch : Bool := true
|
||||
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
|
||||
splitIte : Bool := true
|
||||
/--
|
||||
If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
|
||||
Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
|
||||
splitIndPred : Bool := false
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
splitImp : Bool := false
|
||||
/-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
|
||||
canonHeartbeats : Nat := 1000
|
||||
/-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
|
||||
ext : Bool := true
|
||||
/-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
|
||||
extAll : Bool := false
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
etaStruct : Bool := true
|
||||
/--
|
||||
If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
|
||||
on equalities between lambda expressions.
|
||||
-/
|
||||
funext : Bool := true
|
||||
/-- TODO -/
|
||||
lookahead : Bool := true
|
||||
/-- If `verbose` is `false`, additional diagnostics information is not collected. -/
|
||||
verbose : Bool := true
|
||||
/-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
|
||||
clean : Bool := true
|
||||
/--
|
||||
If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
|
||||
using rational numbers, and ignoring divisibility constraints.
|
||||
This approach is cheaper but incomplete. -/
|
||||
qlia : Bool := false
|
||||
/--
|
||||
If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
|
||||
See paper "Model-based Theory Combination" for details.
|
||||
-/
|
||||
mbtc : Bool := true
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
zetaDelta := true
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
zeta := true
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
ring := true
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
ringSteps := 10000
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
|
||||
`CommRing`.
|
||||
-/
|
||||
linarith := true
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
|
||||
-/
|
||||
cutsat := true
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
|
||||
-/
|
||||
ac := true
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
acSteps := 1000
|
||||
/--
|
||||
Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
|
||||
the characteristic of a ring.
|
||||
-/
|
||||
exp : Nat := 2^20
|
||||
/--
|
||||
When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
|
||||
-/
|
||||
abstractProof := true
|
||||
/--
|
||||
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
|
||||
```
|
||||
-/
|
||||
inj := true
|
||||
/--
|
||||
When `true` (default: `true`), enables the procedure for handling orders that implement
|
||||
at least `Std.IsPreorder`
|
||||
-/
|
||||
order := true
|
||||
/--
|
||||
When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
|
||||
the future.
|
||||
-/
|
||||
offset := true
|
||||
deriving Inhabited, BEq
|
||||
|
||||
/--
|
||||
Configuration for interactive mode.
|
||||
We disable `clean := false`.
|
||||
-/
|
||||
structure ConfigInteractive extends Config where
|
||||
clean := false
|
||||
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
|
||||
structure NoopConfig extends Config where
|
||||
-- Disable splitting
|
||||
splits := 0
|
||||
-- We don't override the various `splitMatch` / `splitIte` settings separately.
|
||||
|
||||
-- Disable e-matching
|
||||
ematch := 0
|
||||
-- We don't override `matchEqs` separately.
|
||||
|
||||
-- Disable extensionality
|
||||
ext := false
|
||||
extAll := false
|
||||
etaStruct := false
|
||||
funext := false
|
||||
|
||||
-- Disable all solver modules
|
||||
ring := false
|
||||
linarith := false
|
||||
cutsat := false
|
||||
ac := false
|
||||
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
|
||||
structure CutsatConfig extends NoopConfig where
|
||||
cutsat := true
|
||||
-- Allow the default number of splits.
|
||||
splits := ({} : Config).splits
|
||||
|
||||
/--
|
||||
A `grind` configuration that only uses `ring`.
|
||||
-/
|
||||
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
|
||||
structure GrobnerConfig extends NoopConfig where
|
||||
ring := true
|
||||
|
||||
end Lean.Grind
|
||||
|
|
@ -16,6 +16,16 @@ when selecting patterns.
|
|||
-/
|
||||
syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
|
||||
|
||||
/-!
|
||||
`grind` tactic and related tactics.
|
||||
-/
|
||||
syntax grindErase := "-" ident
|
||||
/--
|
||||
The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
|
||||
when selecting patterns.
|
||||
-/
|
||||
syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin
|
||||
|
||||
namespace Grind
|
||||
declare_syntax_cat grind_filter (behavior := both)
|
||||
|
||||
|
|
@ -152,6 +162,12 @@ inaccessible names to the given names.
|
|||
-/
|
||||
syntax (name := next) "next " binderIdent* " => " grindSeq : grind
|
||||
|
||||
/--
|
||||
`· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
|
||||
sequence of `grind` tactics.
|
||||
-/
|
||||
macro dot:patternIgnore("· " <|> ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
|
||||
|
||||
/--
|
||||
`any_goals tac` applies the tactic `tac` to every goal,
|
||||
concatenating the resulting goals for successful tactic applications.
|
||||
|
|
|
|||
|
|
@ -7,227 +7,9 @@ module
|
|||
prelude
|
||||
public import Init.Core
|
||||
public import Init.Grind.Interactive
|
||||
public import Init.Grind.Config
|
||||
public section
|
||||
namespace Lean.Grind
|
||||
/--
|
||||
The configuration for `grind`.
|
||||
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
|
||||
-/
|
||||
structure Config where
|
||||
/-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
|
||||
trace : Bool := false
|
||||
/-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
|
||||
or for which no patterns can be generated. -/
|
||||
lax : Bool := false
|
||||
/-- If `premises` is `true`, `grind` will invoke the currently configured premise selecor on the current goal,
|
||||
and add attempt to use the resulting suggestions as premises to the `grind` tactic. -/
|
||||
premises : Bool := false
|
||||
/-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
|
||||
splits : Nat := 9
|
||||
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
|
||||
ematch : Nat := 5
|
||||
/--
|
||||
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. -/
|
||||
gen : Nat := 8
|
||||
/-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
|
||||
instances : Nat := 1000
|
||||
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/
|
||||
matchEqs : Bool := true
|
||||
/-- If `splitMatch` is `true`, `grind` performs case-splitting on `match`-expressions during the search. -/
|
||||
splitMatch : Bool := true
|
||||
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search. -/
|
||||
splitIte : Bool := true
|
||||
/--
|
||||
If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
|
||||
Otherwise, it performs case-splitting only on types marked with `[grind cases]` attribute. -/
|
||||
splitIndPred : Bool := false
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
splitImp : Bool := false
|
||||
/-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
|
||||
canonHeartbeats : Nat := 1000
|
||||
/-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/
|
||||
ext : Bool := true
|
||||
/-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
|
||||
extAll : Bool := false
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
etaStruct : Bool := true
|
||||
/--
|
||||
If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
|
||||
on equalities between lambda expressions.
|
||||
-/
|
||||
funext : Bool := true
|
||||
/-- TODO -/
|
||||
lookahead : Bool := true
|
||||
/-- If `verbose` is `false`, additional diagnostics information is not collected. -/
|
||||
verbose : Bool := true
|
||||
/-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
|
||||
clean : Bool := true
|
||||
/--
|
||||
If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
|
||||
using rational numbers, and ignoring divisibility constraints.
|
||||
This approach is cheaper but incomplete. -/
|
||||
qlia : Bool := false
|
||||
/--
|
||||
If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
|
||||
See paper "Model-based Theory Combination" for details.
|
||||
-/
|
||||
mbtc : Bool := true
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
zetaDelta := true
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
zeta := true
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
ring := true
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
ringSteps := 10000
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
|
||||
`CommRing`.
|
||||
-/
|
||||
linarith := true
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
|
||||
-/
|
||||
cutsat := true
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
|
||||
-/
|
||||
ac := true
|
||||
/--
|
||||
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`.
|
||||
-/
|
||||
acSteps := 1000
|
||||
/--
|
||||
Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
|
||||
the characteristic of a ring.
|
||||
-/
|
||||
exp : Nat := 2^20
|
||||
/--
|
||||
When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
|
||||
-/
|
||||
abstractProof := true
|
||||
/--
|
||||
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
|
||||
```
|
||||
-/
|
||||
inj := true
|
||||
/--
|
||||
When `true` (default: `true`), enables the procedure for handling orders that implement
|
||||
at least `Std.IsPreorder`
|
||||
-/
|
||||
order := true
|
||||
/--
|
||||
When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
|
||||
the future.
|
||||
-/
|
||||
offset := true
|
||||
deriving Inhabited, BEq
|
||||
|
||||
/--
|
||||
Configuration for interactive mode.
|
||||
We disable `clean := false`.
|
||||
-/
|
||||
structure ConfigInteractive extends Config where
|
||||
clean := false
|
||||
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
|
||||
structure NoopConfig extends Config where
|
||||
-- Disable splitting
|
||||
splits := 0
|
||||
-- We don't override the various `splitMatch` / `splitIte` settings separately.
|
||||
|
||||
-- Disable e-matching
|
||||
ematch := 0
|
||||
-- We don't override `matchEqs` separately.
|
||||
|
||||
-- Disable extensionality
|
||||
ext := false
|
||||
extAll := false
|
||||
etaStruct := false
|
||||
funext := false
|
||||
|
||||
-- Disable all solver modules
|
||||
ring := false
|
||||
linarith := false
|
||||
cutsat := false
|
||||
ac := false
|
||||
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
|
||||
structure CutsatConfig extends NoopConfig where
|
||||
cutsat := true
|
||||
-- Allow the default number of splits.
|
||||
splits := ({} : Config).splits
|
||||
|
||||
/--
|
||||
A `grind` configuration that only uses `ring`.
|
||||
-/
|
||||
-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
|
||||
structure GrobnerConfig extends NoopConfig where
|
||||
ring := true
|
||||
|
||||
end Lean.Grind
|
||||
|
||||
namespace Lean.Parser.Tactic
|
||||
|
||||
/-!
|
||||
`grind` tactic and related tactics.
|
||||
-/
|
||||
syntax grindErase := "-" ident
|
||||
/--
|
||||
The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
|
||||
when selecting patterns.
|
||||
-/
|
||||
syntax grindParam := grindErase <|> grindLemma <|> grindLemmaMin
|
||||
|
||||
open Parser.Tactic.Grind
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -159,17 +159,16 @@ def mkGrindSeq (s : List TGrind) : TSyntax ``Parser.Tactic.Grind.grindSeq :=
|
|||
/--
|
||||
Given `[t₁, ..., tₙ]`, returns
|
||||
```
|
||||
next =>
|
||||
t₁
|
||||
· t₁
|
||||
...
|
||||
tₙ
|
||||
```
|
||||
If the list is empty, it returns `next => done`.
|
||||
If the list is empty, it returns `· done`.
|
||||
-/
|
||||
def mkGrindNext (s : List TGrind) : CoreM TGrind := do
|
||||
let s ← if s == [] then pure [← `(grind| done)] else pure s
|
||||
let s := mkGrindSeq s
|
||||
`(grind| next => $s:grindSeq)
|
||||
`(grind| · $s:grindSeq)
|
||||
|
||||
/--
|
||||
Given `[t₁, ..., tₙ]`, returns
|
||||
|
|
@ -189,8 +188,7 @@ private def mkGrindParen (s : List TGrind) : CoreM TGrind := do
|
|||
If tracing is enabled and continuation produced `.closed [t₁, ..., tₙ]`,
|
||||
returns the singleton sequence `[t]` where `t` is
|
||||
```
|
||||
next =>
|
||||
t₁
|
||||
· t₁
|
||||
...
|
||||
tₙ
|
||||
```
|
||||
|
|
@ -205,7 +203,7 @@ def group : Action := fun goal _ kp => do
|
|||
return r
|
||||
|
||||
/--
|
||||
If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]`,
|
||||
If tracing is enabled and continuation produced `.closed [(next => t₁; ...; tₙ)]` or its variant using `·`
|
||||
returns `.close [t₁, ... tₙ]`
|
||||
-/
|
||||
def ungroup : Action := fun goal _ kp => do
|
||||
|
|
@ -214,7 +212,9 @@ def ungroup : Action := fun goal _ kp => do
|
|||
match r with
|
||||
| .closed [tac] =>
|
||||
match tac with
|
||||
| `(grind| next => $seq;*) => return .closed <| seq.getElems.toList.map TGrindStep.getTactic
|
||||
| `(grind| next => $seq;*)
|
||||
| `(grind| · $seq;*) =>
|
||||
return .closed <| seq.getElems.toList.map TGrindStep.getTactic
|
||||
| _ => return r
|
||||
| _ => return r
|
||||
else
|
||||
|
|
|
|||
|
|
@ -322,6 +322,7 @@ where
|
|||
private def isCompressibleSeq (seq : List (TSyntax `grind)) : Bool :=
|
||||
seq.all fun tac => match tac with
|
||||
| `(grind| next $_* => $_:grindSeq) => false
|
||||
| `(grind| · $_:grindSeq) => false
|
||||
| _ => true
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -17,8 +17,8 @@ example {α : Type} [CommRing α] (a b c d e : α) :
|
|||
info: Try this:
|
||||
[apply] ⏎
|
||||
cases #b0f4
|
||||
next => cases #50fc
|
||||
next => cases #50fc <;> lia
|
||||
· cases #50fc
|
||||
· cases #50fc <;> lia
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (p : Nat → Prop) (x y z w : Int) :
|
||||
|
|
@ -65,14 +65,12 @@ set_option warn.sorry false
|
|||
info: Try this:
|
||||
[apply] ⏎
|
||||
cases #c4b6
|
||||
next =>
|
||||
cases #8c9f
|
||||
next => ring
|
||||
next => sorry
|
||||
next =>
|
||||
cases #8c9f
|
||||
next => ring
|
||||
next => sorry
|
||||
· cases #8c9f
|
||||
· ring
|
||||
· sorry
|
||||
· cases #8c9f
|
||||
· ring
|
||||
· sorry
|
||||
-/
|
||||
#guard_msgs in
|
||||
example {α : Type} [CommRing α] (a b c d e : α) :
|
||||
|
|
@ -86,8 +84,8 @@ info: Try this:
|
|||
[apply] ⏎
|
||||
instantiate only [= Nat.min_def]
|
||||
cases #7640
|
||||
next => sorry
|
||||
next => lia
|
||||
· sorry
|
||||
· lia
|
||||
-/
|
||||
#guard_msgs in
|
||||
example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
|
||||
|
|
|
|||
|
|
@ -149,25 +149,18 @@ info: Try this:
|
|||
instantiate only [= mem_indices_of_mem, insert]
|
||||
instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
|
||||
cases #4ed2
|
||||
next =>
|
||||
cases #ffdf
|
||||
next => instantiate only
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #ffdf
|
||||
· instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.contains_insert]
|
||||
next =>
|
||||
cases #95a0
|
||||
next =>
|
||||
cases #2688
|
||||
next => instantiate only
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #95a0
|
||||
· cases #2688
|
||||
· instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.contains_insert]
|
||||
next =>
|
||||
cases #ffdf
|
||||
next => instantiate only
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #ffdf
|
||||
· instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.contains_insert]
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
@ -181,25 +174,18 @@ info: Try this:
|
|||
instantiate only [= mem_indices_of_mem, insert]
|
||||
instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
|
||||
cases #4ed2
|
||||
next =>
|
||||
cases #ffdf
|
||||
next => instantiate only
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #ffdf
|
||||
· instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.contains_insert]
|
||||
next =>
|
||||
cases #95a0
|
||||
next =>
|
||||
cases #2688
|
||||
next => instantiate only
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #95a0
|
||||
· cases #2688
|
||||
· instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.contains_insert]
|
||||
next =>
|
||||
cases #ffdf
|
||||
next => instantiate only
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #ffdf
|
||||
· instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.contains_insert]
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
@ -240,25 +226,19 @@ info: Try this:
|
|||
instantiate only [= mem_indices_of_mem, insert, = getElem_def]
|
||||
instantiate only [= getElem?_neg, = getElem?_pos]
|
||||
cases #f590
|
||||
next =>
|
||||
cases #ffdf
|
||||
next =>
|
||||
instantiate only
|
||||
· cases #ffdf
|
||||
· instantiate only
|
||||
instantiate only [= Array.getElem_set]
|
||||
next =>
|
||||
instantiate only
|
||||
· instantiate only
|
||||
instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
|
||||
next =>
|
||||
instantiate only [= mem_indices_of_mem, = getElem_def]
|
||||
· instantiate only [= mem_indices_of_mem, = getElem_def]
|
||||
instantiate only [usr getElem_indices_lt]
|
||||
instantiate only [size]
|
||||
cases #ffdf
|
||||
next =>
|
||||
instantiate only [=_ WF]
|
||||
· instantiate only [=_ WF]
|
||||
instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
|
||||
instantiate only [WF']
|
||||
next =>
|
||||
instantiate only
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
@ -300,9 +280,8 @@ info: Try this:
|
|||
instantiate only [findIdx, insert, = mem_indices_of_mem]
|
||||
instantiate only [= getElem?_neg, = getElem?_pos]
|
||||
cases #1bba
|
||||
next => instantiate only [findIdx]
|
||||
next =>
|
||||
instantiate only
|
||||
· instantiate only [findIdx]
|
||||
· instantiate only
|
||||
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue