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

fix: set iota := true in simpGlobalConfig #6909

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

fix: set iota := true in simpGlobalConfig #6909

wants to merge 11 commits into from
+37 −56

Conversation

JovanGerb
Copy link
Contributor

@JovanGerb JovanGerb commented Feb 3, 2025 •
edited
Loading

This PR sets iota := true in simpGlobalConfig. This means that iota reduction happens when creating the discrimination tree keys, matching the behaviour of the default iota := true during simp. This means that some simp lemmas that previously didn't work now do work.

It also updates acLt to use withSimpIndexConfig, restoring the intended behaviour of using the same reductions as the indexing does.

This issue was recently reported again on Zulip

Closes #6331

@JovanGerb JovanGerb requested a review from leodemoura as a code owner February 3, 2025 02:17
@JovanGerb JovanGerb marked this pull request as draft February 3, 2025 02:17
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 3, 2025
@leanprover-community-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-03 02:49:52)
  • 💥 Mathlib branch lean-pr-testing-6909 build failed against this PR. (2025-02-03 21:10:35) View Log
  • 💥 Mathlib branch lean-pr-testing-6909 build failed against this PR. (2025-02-04 00:03:03) View Log
  • ✅ Mathlib branch lean-pr-testing-6909 has successfully built against this PR. (2025-02-04 06:48:09) View Log
  • ✅ Mathlib branch lean-pr-testing-6909 has successfully built against this PR. (2025-02-04 08:46:37) View Log
  • ✅ Mathlib branch lean-pr-testing-6909 has successfully built against this PR. (2025-02-06 14:13:39) View Log

@JovanGerb JovanGerb changed the title fix: set iota := true in simpGlobalConfig fix: set iota := false in Simp.mkIndexConfig Feb 3, 2025
@JovanGerb JovanGerb changed the title fix: set iota := false in Simp.mkIndexConfig fix: set iota := true in simpGlobalConfig Feb 3, 2025
@JovanGerb JovanGerb changed the title fix: set iota := true in simpGlobalConfig fix: set iota := true in simpGlobalConfig Feb 3, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6909
81f2435
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6909
cf1697c
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Feb 3, 2025
@JovanGerb JovanGerb force-pushed the simpGlobalConfig-iota branch from c3e5304 to e13dde2 Compare February 4, 2025 07:27
@JovanGerb
Copy link
Contributor Author

A few small changes in Mathlib were required, but these are positive changes that could also be backported to the main mathlib.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6909
15c9318
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 4, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6909
28e834e
@JovanGerb JovanGerb marked this pull request as ready for review February 4, 2025 22:54
@JovanGerb JovanGerb force-pushed the simpGlobalConfig-iota branch from 44ed139 to 18c9e61 Compare February 6, 2025 13:02
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6909
a1e3acd
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6909
1872bfe
@JovanGerb JovanGerb marked this pull request as draft February 8, 2025 16:46
@JovanGerb JovanGerb marked this pull request as ready for review February 8, 2025 16:46
@kim-em kim-em added the changelog-language Language features, tactics, and metaprograms label Feb 10, 2025
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

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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.

simp lemma discrimination tree keys are computed with iota := false, while simp uses iota := true
3 participants
@JovanGerb @leanprover-community-bot @kim-em