feat: add list function and lemmas #987
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
add-more-list-lemmas
branch
2 times, most recently
from
f9d2745 to
20de1c3
Compare
|
awaiting-review |
github-actions
bot
added
the
awaiting-review
2 tasks
eric-wieser
reviewed
Oct 14, 2024
eric-wieser
reviewed
Oct 14, 2024
fgdorais
reviewed
Oct 15, 2024
I need these lemmas to prove `String.splitOn_of_valid`.
These are 'leftover' lemmas I created while trying to prove `String.splitOn_of_valid`. See leanprover-community#743.
Using the `@` symbol is a bit old-fashioned. Co-authored-by: François G. Dorais <[email protected]>
The function `List.commonPrefix` returns the longest common prefix of two lists.
* Remove the "_exists" part from the theorem's name. * Remove the existential quantifiers from the theorem's statement and add new hypotheses.
chabulhwi
force-pushed
the
add-more-list-lemmas
branch
from
df77496 to
ce38099
Compare
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
chabulhwi
commented
Oct 15, 2024
Move `List.commonPrefix` to `Batteries.Data.List.Basic`.
chabulhwi
changed the title
chabulhwi
changed the title
kmill
reviewed
Oct 15, 2024
kmill
reviewed
Oct 15, 2024
chabulhwi
force-pushed
the
add-more-list-lemmas
branch
from
2152acb to
7311737
Compare
chabulhwi
force-pushed
the
add-more-list-lemmas
branch
from
6ed7df8 to
b794e10
Compare
This theorem will simplify the proof of the theorem `List.commonPrefix_prefix_right`. Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
chabulhwi
force-pushed
the
add-more-list-lemmas
branch
from
b794e10 to
d257184
Compare
|
The |
|
Don't close this one! We want to keep the review history for the other parts. Just delete the parts that are moved to the other PR. |
This was referenced Oct 16, 2024
|
Yes. Thank you! |
This reverts commit d257184.
This reverts commit 9e0d971.
This reverts commit ab8e65a.
This reverts commit 6b7c0e4.
This reverts commit ce38099.
This reverts commit 6b39d44.
This reverts commit 2d30498.
This reverts commit f39e00a.
I moved the theorem to another pull request: leanprover-community#994.
leanprover-community-mathlib4-bot
added
the
merge-conflict
fgdorais
requested changes
Oct 27, 2024
Comment on lines
+499
to
+501
| theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by | ||
| intro heq | ||
| simp [heq, nil_prefix] at h |
There was a problem hiding this comment.
Suggested change
| theorem ne_nil_of_not_prefix (h : ¬l₁ <+: l₂) : l₁ ≠ [] := by | |
| intro heq | |
| simp [heq, nil_prefix] at h | |
| theorem ne_nil_of_not_prefix : ¬l₁ <+: l₂ → l₁ ≠ [] := by | |
| apply mt; intro h; simp [h] |
fgdorais
added
awaiting-author
leanprover-community-mathlib4-bot
added
merge-conflict
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.
These are 'leftover' lemmas I created while trying to prove
String.splitOn_of_valid. See#743.
Co-authored-by: François G. Dorais [email protected]
I split this pull request in two: #993 and #994.