feat: modify withNewMCtxDepth
#1
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
thorimur
force-pushed
the
withNewMCtxDepth-mod
branch
2 times, most recently
from
b98818b to
e091f66
Compare
thorimur
force-pushed
the
withNewMCtxDepth-mod
branch
from
e091f66 to
5ef6e1f
Compare
thorimur
pushed a commit
that referenced
this pull request
May 8, 2025
This PR improves the E-matching pattern inference procedure in `grind`.
Consider the following theorem:
```lean
@[grind →]
theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] :=
append_eq_empty_iff.mp h
```
Before this PR, `grind` inferred the following pattern:
```lean
@HAppend.hAppend _ _ _ _ leanprover#2 #1
```
Note that this pattern would match any `++` application, even if it had
nothing to do with arrays. With this PR, the inferred pattern becomes:
```lean
@HAppend.hAppend (Array leanprover#3) (Array _) (Array _) _ leanprover#2 #1
```
With the new pattern, the theorem will not be considered by `grind` for
goals that do not involve `Array`s.
thorimur
pushed a commit
that referenced
this pull request
Aug 15, 2025
…rns in `grind` (leanprover#9857) This PR ensures `grind` can E-match patterns containing universe polymorphic ground sub-patterns. For example, given ``` set_option pp.universes true in attribute [grind?] Id.run_pure ``` the pattern ``` Id.run_pure.{u_1}: [@Id.run.{u_1} #1 (@pure.{u_1, u_1} `[Id.{u_1}] `[Applicative.toPure.{u_1, u_1}] _ #0)] ``` contains two nested universe polymorphic ground patterns - `Id.{u_1}` - `Applicative.toPure.{u_1, u_1}` This kind of pattern is not common, but it occurs in core.
thorimur
pushed a commit
that referenced
this pull request
Sep 23, 2025
This PR implements a new E-matching pattern inference procedure that is faithful to the behavior documented in the reference manual regarding minimal indexable subexpressions. The old inference procedure was failing to enforce this condition. For example, the manual documents `[grind ->]` as follows `[@GRIND →]` selects a multi-pattern from the hypotheses of the theorem. In other words, `grind` will use the theorem for forwards reasoning. To generate a pattern, it traverses the hypotheses of the theorem from left to right. Each time it encounters a **minimal indexable subexpression** which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered. That said, the new procedure is currently disabled, and the following option must be used to enable it. ``` set_option backward.grind.inferPattern false ``` Users can inspect differences between the old a new procedures using the option ``` set_option backward.grind.checkInferPatternDiscrepancy true ``` Example: ```lean /-- warning: found discrepancy between old and new `grind` pattern inference procedures, old: [@List.length leanprover#2 (@tolist _ #1 #0)] new: [@tolist leanprover#2 #1 #0] use `set_option backward.grind.inferPattern true` to force old procedure -/ #guard_msgs in set_option backward.grind.checkInferPatternDiscrepancy true in @[grind] theorem Vector.length_toList' (xs : Vector α n) : xs.toList.length = n := by sorry ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.