feat: add String.splitOn_of_valid
#743
Open
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
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
4 times, most recently
from
2df1e65
to
3699b5d
Compare
|
awaiting-review |
github-actions
bot
added
the
awaiting-review
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
4 times, most recently
from
75b032f
to
dd5f11a
Compare
|
This is doing too many things at once. Can you split out the preliminary steps (upstreaming from Mathlib) as separate PRs? |
semorrison
added
awaiting-author
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
4 times, most recently
from
e6b2836
to
cf96e0e
Compare
@semorrison I've split these commits into separate PRs. |
|
awaiting-review |
github-actions
bot
added
awaiting-review
chabulhwi
changed the title
String.splitOn_of_valid
semorrison
added
depends on another PR
leanprover-community-mathlib4-bot
added
the
merge-conflict
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
from
cf96e0e
to
55046a9
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
from
55046a9
to
4af3b7e
Compare
|
I resolved merge conflicts. |
semorrison
reviewed
May 3, 2024
semorrison
reviewed
May 3, 2024
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
9 times, most recently
from
2c75571
to
d080155
Compare
|
@semorrison I resolved all the conversations. |
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
from
d080155
to
91413c1
Compare
leanprover-community-mathlib4-bot
added
the
merge-conflict
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
from
91413c1
to
6911f78
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
* `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 <kim@tqft.net>
Most of these lemmas are needed to prove `String.splitOn_of_valid`.
* `List.splitOnceP` returns `(l₁, l₂)` for the first split `l = l₁ ++ l₂` such that `P l₂` returns true. * `List.splitOnList` splits a list at every occurrence of a separator list. The separators are not in the result. * `List.splitOnListAux` is an auxiliary definition for proving `String.splitOnAux_of_valid`. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Add `String.splitOnAux_of_valid` and `String.splitOn_of_valid`.
chabulhwi
force-pushed
the
String.splitOn_of_valid_v3
branch
from
6911f78
to
32bf83b
Compare
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.
String.splitOn_of_validis the first of the eleven unproved theoremsabout strings. I added the following to prove it:
Nat.addand listsBatteries.Data.List.SplitOnListString.splitOnAux_of_validThis is the third version of #495 and includes #531. The second version is #719.
Function.id_deffrom mathlib #755