Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: try more specific matches first in simp #7195

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

feat: try more specific matches first in simp #7195

wants to merge 4 commits into from
+4 −2

Conversation

JovanGerb
Copy link
Contributor

@JovanGerb JovanGerb commented Feb 23, 2025 •
edited
Loading

This PR modifies the order in which simp lemmas are tried, so that among lemmas with the same priority, the closer matches are tried first.

This makes it easier to make a good and performant simp set:

  • When choosing between two lemmas, the closer matching one is almost always more useful.
  • Often the more general lemma fails more slowly, so it's better to not try it first.

This matches the behaviour of type class synthesis.

The implementation uses Array.reverse, before iterating through the array, which isn't great, but as far as I know there is no way to loop through an Array backwards in a for-loop.

TODO: fix test and Mathlib (lots of breakage)

Zulip

@JovanGerb
Copy link
Contributor Author

changelog-language

@github-actions github-actions bot added changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Feb 23, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7195
1f4c562
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7195
47bab9b
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 23, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 23, 2025 •
edited
Loading

Mathlib CI status (docs):

@JovanGerb JovanGerb marked this pull request as draft February 23, 2025 20:02
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7195
295cabc
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7195
3de8ddb
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Feb 24, 2025
@JovanGerb
Copy link
Contributor Author

release-ci

@github-actions github-actions bot added the release-ci Enable all CI checks for a PR, like is done for releases label Feb 24, 2025
@hargoniX hargoniX removed the release-ci Enable all CI checks for a PR, like is done for releases label Feb 24, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7195
ef00ad4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7195
611f833
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@JovanGerb @leanprover-community-bot @hargoniX