feat: exact? uses star-indexed lemmas as fallback #11494
Merged
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
kim-em
changed the title
exact? falls back to trying un-indexable theorems
github-actions
bot
added
the
toolchain-available
Collaborator
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Collaborator
Author
|
I would like to rebase this onto |
This PR adds support for star-indexed lemmas (like `Empty.elim`, `And.left`, `not_not.mp`) to `exact?` and `apply?` as a fallback search when no concrete-keyed lemmas are found. Star-indexed lemmas are those whose discrimination tree keys are `[*]` or patterns like `[Eq,*,*,*]` - these match too broadly to include in the primary search, but can be helpful when the goal type is headed by a free variable (e.g., `⊢ h` where `h : P`). The fallback is only triggered when: 1. No results are found from the primary (concrete-keyed) search 2. The goal type is headed by a free variable 3. The `-star` flag is not set Use `exact? -star` or `apply? -star` to disable the fallback. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
This PR makes two main improvements to library search:
1. **Replace duplicate tree with array for star-indexed lemmas**
- Instead of maintaining `fullExt` (a complete duplicate discrimination tree),
use `starLemmasExt` (a simple array for lemmas with `[*]` or `[Eq,*,*,*]` keys)
- Star-indexed lemmas are captured during tree initialization via `extractKeys`
- Two-pass search: first excludes star lemmas, fallback includes them
- Controlled by `-star`/`+star` flags
2. **Support eliminator-style theorems like `iteInduction`**
- Add `getFirstArgEntry` to create secondary index entries for fvar-headed theorems
- For `motive (ite c t e)`, creates entry keyed by `.const ite 4`
- Modify `getMatchCore` to check first argument's const key for fvar-headed goals
- This enables finding eliminators even with `-star`
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude <[email protected]>
kim-em
force-pushed
the
librarySearch-star2
branch
from
48be6a0 to
36b63ce
Compare
kim-em
added
awaiting-mathlib
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Dec 4, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Dec 4, 2025
leanprover-community-bot
removed
the
awaiting-mathlib
Collaborator
|
leanprover-community-bot
added
the
builds-mathlib
Collaborator
Author
|
Performance in Mathlib seems acceptable. |
algebraic-dev
pushed a commit
that referenced
this pull request
Dec 8, 2025
This PR re-enables star-indexed lemmas as a fallback for `exact?` and
`apply?`.
Star-indexed lemmas (those with overly-general discrimination tree keys
like `[*]`)
were previously dropped entirely for performance reasons. This caused
useful lemmas
like `Empty.elim`, `And.left`, `not_not.mp`, `Sum.elim`, and
`Function.mtr` to be
unfindable by library search.
The implementation adds a two-pass search strategy:
1. First, search using concrete discrimination keys (the current
behavior)
2. If no results are found, fall back to trying star-indexed lemmas
The star-indexed lemmas are extracted during tree initialization and
cached in an
environment extension, avoiding repeated computation.
Users can disable the fallback with `-star`:
```lean
example {α : Sort u} (h : Empty) : α := by apply? -star -- error: no lemmas found
example {α : Sort u} (h : Empty) : α := by apply? -- finds Empty.elim
```
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <[email protected]>
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.
This PR re-enables star-indexed lemmas as a fallback for
exact?andapply?.Star-indexed lemmas (those with overly-general discrimination tree keys like
[*])were previously dropped entirely for performance reasons. This caused useful lemmas
like
Empty.elim,And.left,not_not.mp,Sum.elim, andFunction.mtrto beunfindable by library search.
The implementation adds a two-pass search strategy:
The star-indexed lemmas are extracted during tree initialization and cached in an
environment extension, avoiding repeated computation.
Users can disable the fallback with
-star:🤖 Prepared with Claude Code