refactor: move theorems about lists from mathlib #756
Merged
Conversation
This file contains 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
|
awaiting-review |
github-actions
bot
added
the
awaiting-review
chabulhwi
force-pushed
the
list-theorems
branch
2 times, most recently
from
23a45f4
to
075ff99
Compare
This was referenced Apr 19, 2024
|
Is there a Mathlib adaptation PR ready? A lot of things are in flight at the moment so I'd like to be confident that after merging I can get everything working quickly. See e.g. what Yury did at #758. |
kim-em
added
awaiting-author
chabulhwi
force-pushed
the
list-theorems
branch
2 times, most recently
from
64e8be0
to
5e535c8
Compare
chabulhwi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 30, 2024
* `List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. * `List.cons_prefix_iff` is from `Mathlib.Data.List.Infix`. * We need these theorems to prove `String.splitOn_of_valid`. See leanprover-community/batteries#756.
3 tasks
@semorrison I opened a Mathlib PR that removes the theorems I brought to |
|
awaiting-review |
github-actions
bot
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
merge-conflict
github-actions
bot
added
awaiting-review
|
I resolved merge conflicts. |
leanprover-community-mathlib4-bot
removed
the
merge-conflict
kim-em
reviewed
May 3, 2024
kim-em
reviewed
May 3, 2024
kim-em
reviewed
May 3, 2024
kim-em
reviewed
May 3, 2024
kim-em
reviewed
May 3, 2024
kim-em
reviewed
May 3, 2024
chabulhwi
added a commit
to chabulhwi/batteries
that referenced
this pull request
Jun 15, 2024
* `List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. I removed the `simp` priority and `nolint` attribute from `modifyHead_modifyHead` because we don't need them anymore. * `List.cons_prefix_cons` is from `Mathlib.Data.List.Infix`. Its previous name was `List.cons_prefix_iff`. We need these theorems to prove `String.splitOn_of_valid`. See leanprover-community#756. Co-authored-by: Kim Morrison <[email protected]>
leanprover-community-mathlib4-bot
added
the
merge-conflict
chabulhwi
added a commit
to chabulhwi/batteries
that referenced
this pull request
Sep 3, 2024
`List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. I removed the `simp` priority and `nolint` attribute from `modifyHead_modifyHead` because we don't need them anymore. We need these theorems to prove `String.splitOn_of_valid`. See leanprover-community#756. Co-authored-by: Kim Morrison <[email protected]>
chabulhwi
force-pushed
the
list-theorems
branch
from
6a7a92f
to
6fb4f5e
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
chabulhwi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 3, 2024
The simplifier used to always unfold the definition of the function `List.modifyHead` because it had the `simp` attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the `simp` priority in the theorem `List.modifyHead_modifyHead` is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.
chabulhwi
force-pushed
the
list-theorems
branch
from
6fb4f5e
to
4cb9841
Compare
chabulhwi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 3, 2024
`List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. We need these theorems to prove `String.splitOn_of_valid`. See leanprover-community/batteries#743. This is a Batteries bump PR corresponding to leanprover-community/batteries#756.
chabulhwi
force-pushed
the
list-theorems
branch
from
4cb9841
to
b6a0c53
Compare
chabulhwi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 3, 2024
`List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. We need these theorems to prove `String.splitOn_of_valid`. See leanprover-community/batteries#743. Corresponding Batteries PR: leanprover-community/batteries#756
`List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from `Mathlib.Data.List.Basic`. We need these theorems to prove `String.splitOn_of_valid`. See leanprover-community#743. Batteries bump PR in Mathlib: leanprover-community/mathlib4#12540 Co-authored-by: Kim Morrison <[email protected]>
chabulhwi
force-pushed
the
list-theorems
branch
from
b6a0c53
to
f6e0091
Compare
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 4, 2024
The simplifier used to always unfold the definition of the function `List.modifyHead` because it had the `simp` attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the `simp` priority in the theorem `List.modifyHead_modifyHead` is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 5, 2024
The simplifier used to always unfold the definition of the function `List.modifyHead` because it had the `simp` attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the `simp` priority in the theorem `List.modifyHead_modifyHead` is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 9, 2024
The simplifier used to always unfold the definition of the function `List.modifyHead` because it had the `simp` attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the `simp` priority in the theorem `List.modifyHead_modifyHead` is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 9, 2024
The simplifier used to always unfold the definition of the function `List.modifyHead` because it had the `simp` attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the `simp` priority in the theorem `List.modifyHead_modifyHead` is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 12, 2024
The simplifier used to always unfold the definition of the function `List.modifyHead` because it had the `simp` attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the `simp` priority in the theorem `List.modifyHead_modifyHead` is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
Merged
via the queue into
leanprover-community:main
with commit Oct 14, 2024
405f949
2 checks passed
chabulhwi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 14, 2024
`List.modifyHead_modifyHead` is from `Mathlib.Data.List.Basic`. I need it to prove `String.splitOn_of_valid`. See leanprover-community/batteries#743. Corresponding Batteries PR: leanprover-community/batteries#756
chabulhwi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 14, 2024
`List.modifyHead_modifyHead` is from `Mathlib.Data.List.Basic`. I need it to prove `String.splitOn_of_valid`. See leanprover-community/batteries#743. Corresponding Batteries PR: leanprover-community/batteries#756
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 14, 2024
`List.modifyHead_modifyHead` is from `Mathlib.Data.List.Basic`. I need it to prove `String.splitOn_of_valid`. See leanprover-community/batteries#743. Corresponding Batteries PR: leanprover-community/batteries#756 Co-authored-by: Kim Morrison <[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.
List.isEmpty_iff_eq_nilandList.modifyHead_modifyHeadare fromMathlib.Data.List.Basic. We need these theorems to proveString.splitOn_of_valid. See#743.
Batteries bump PR in Mathlib: leanprover-community/mathlib4#12540
Co-authored-by: Kim Morrison [email protected]
@[simp]fromList.modifyHead#790