Skip to content

chore: more simp lemmas for LawfulGetElem #8470

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
Merged
kim-em merged 12 commits into from
May 27, 2025
Merged

chore: more simp lemmas for LawfulGetElem #8470

kim-em merged 12 commits into from
May 27, 2025

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented May 25, 2025 •
edited
Loading

This PR adds @[simp] to getElem_pos/neg (similarly for getElem!). These are often already simp lemmas for concrete types.

@kim-em kim-em added awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-library Library labels May 25, 2025
@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 May 25, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 25, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8470
4c790c9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 25, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8470
ebdb211
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build labels May 25, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 25, 2025 •
edited
Loading

  • ✅ Mathlib branch lean-pr-testing-8470 has successfully built against this PR. (2025-05-25 06:56:35) View Log
  • ✅ Mathlib branch lean-pr-testing-8470 has successfully built against this PR. (2025-05-25 14:10:34) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1e752b0a01bafdbcea6496ac4add09226b92aa99 --onto 2a1354b3cc1eb05e1b67c656d2172ada8f54a937. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-26 05:52:29)
  • 💥 Mathlib branch lean-pr-testing-8470 build failed against this PR. (2025-05-26 05:56:35) View Log

@kim-em
Copy link
Collaborator Author

kim-em commented May 25, 2025

I had expected this to break Mathlib, but apparently it is fine. I will run the simpNF linter from Batteries, to see what we might be able to eliminate from simp once these are added.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 26, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8470
ebb7fcb
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 26, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8470
20861d8
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 26, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8470
2c0b920
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 26, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8470
3b0bd8c
@kim-em kim-em marked this pull request as ready for review May 26, 2025 05:28
@kim-em kim-em requested a review from hargoniX as a code owner May 26, 2025 05:28
@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 May 26, 2025
@kim-em kim-em added this pull request to the merge queue May 27, 2025
Merged via the queue into master with commit eaa1bc1 May 27, 2025
21 checks passed
jcommelin pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025
@leanprover-community-mathlib4-bot @kim-em
@Vierkantor @Kha @eric-wieser @Rob23oba @jrr6
chore: adaptations for nightly-2025-06-04 (#25431)
3780f5f 
* Update lean-toolchain for testing leanprover/lean4#8347

* fixes for leanprover/lean4#8347

* Update lean-toolchain for testing leanprover/lean4#8397

* deprecations for leanprover/lean4#8397

* chore: bump to nightly-2025-05-19

* chore: adaptations for nightly-2025-05-19

* Trigger CI for leanprover/lean4#8347

* Update the style linter to use LinterOptions

* Fix test

* chore: adaptations for nightly-2025-05-19 (#25017)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>

* chore: bump to nightly-2025-05-20

* Merge master into nightly-testing

* feat: a `grind` test case (#25037)

Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test.

Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.)

* lake update

* fixes

* fixes

* fixes

* fixes

* fix

* fixes

* fixes

* shake --update

* chore: bump to nightly-2025-05-21

* Update lean-toolchain for testing leanprover/lean4#7352

* lake update

* Trigger CI for leanprover/lean4#7352

* chore: adaptations for nightly-2025-05-21

* chore: adaptations for nightly-2025-05-21 (#25079)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>

* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#8584

* chore: adaptations for nightly-2025-06-02

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* chore: bump to nightly-2025-06-04

* bump toolchain

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>
jcommelin added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2025
@leanprover-community-mathlib4-bot @kim-em
@eric-wieser @Rob23oba @jrr6 @Vierkantor @Kha @jcommelin @JovanGerb @nomeata
chore: adaptations for nightly-2025-06-05 (#25490)
5a9a408 
* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

* Update lean-toolchain for testing leanprover/lean4#8519

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* Trigger CI for leanprover/lean4#8519

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* chore: remove simp attribute when value of argument can not be inferred by simp

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#8584

* chore: adaptations for nightly-2025-06-02

* change phrasing of comments

* chore(Geometry/Manifold): two simp-lemmas can be proven by simp

* fix two lint problems

* Trigger CI for leanprover/lean4#8519

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* revert change in `Mathlib.Data.ZMOD.Basic`

* fix Mathlib/Data/List/EditDistance/Estimator.lean

* give specialized simp lemmas higher prio

* simp can prove these

* simp can prove these

* chore: bump to nightly-2025-06-04

* bump toolchain

* Adapt eqns

* Revert "Adapt eqns"

This reverts commit 34f1f7f.

* Simply remove check for now

* fix a bunch

* fixes?

* chore: adaptations for nightly-2025-06-04

* add `simp low` lemma `injOn_of_eq_iff_eq`

* wip

* wip

* wip

* fix

* Trigger CI for leanprover-community/batteries#1220

* Merge master into nightly-testing

* chore: bump to nightly-2025-06-05

* Kick CI

* Bump lean4-cli

* Bump import-graph

* Kick CI

* update lakefile

* chore: use more robust syntax quotation in Shake

* cleanup lakefile

---------

Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX 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-library Library 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

@kim-em @leanprover-community-bot