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

refactor: move theorems about lists from mathlib #756

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

refactor: move theorems about lists from mathlib #756

wants to merge 1 commit into from

Conversation

chabulhwi
Copy link
Contributor

@chabulhwi chabulhwi commented Apr 19, 2024 •
edited

  • 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
#756.

Co-authored-by: Kim Morrison kim@tqft.net

Batteries bump PR in Mathlib: leanprover-community/mathlib4#12540

@chabulhwi
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Apr 19, 2024
@chabulhwi chabulhwi force-pushed the list-theorems branch 2 times, most recently from 23a45f4 to 075ff99 Compare April 19, 2024 14:20
This was referenced Apr 19, 2024
Closed
Open
@semorrison
Copy link
Collaborator

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.

@semorrison semorrison added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Apr 30, 2024
@chabulhwi chabulhwi force-pushed the list-theorems branch 2 times, most recently from 64e8be0 to 5e535c8 Compare April 30, 2024 07:35
chabulhwi added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 30, 2024
@chabulhwi
refactor: move theorems about lists to std
f1d64b0 
* `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.
@chabulhwi chabulhwi mentioned this pull request Apr 30, 2024
Open
1 task
@chabulhwi
Copy link
Contributor Author

chabulhwi commented Apr 30, 2024 •
edited

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.

@semorrison I opened a Mathlib PR that removes the theorems I brought to Std Batteries. See leanprover-community/mathlib4#12540.

@chabulhwi
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Apr 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 2, 2024
@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels May 3, 2024
@chabulhwi
Copy link
Contributor Author

I resolved merge conflicts.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 3, 2024
@semorrison semorrison added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels May 6, 2024
@chabulhwi
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels May 6, 2024
chabulhwi added a commit to leanprover-community/mathlib4 that referenced this pull request May 6, 2024
@chabulhwi
refactor: move theorems about lists to std
dc8b368 
* `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.
chabulhwi added a commit to leanprover-community/mathlib4 that referenced this pull request May 7, 2024
@chabulhwi
refactor: move theorems about lists to batteries
a8076b9 
* `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.
@eric-wieser
Copy link
Member

The PR description should be a coherent summary, not a list of commit messages. If the commit messages are largely separate, then this should be separate PRs; for instance, perhaps the porting note cleanup and renames can happen in mathlib before you move things.

@chabulhwi
Copy link
Contributor Author

chabulhwi commented May 9, 2024 •
edited

@eric-wieser I see. I can make separate pull requests from the later commits suggested by @semorrison. I'll do it until tomorrow. Thanks for pointing that out!

@chabulhwi
Copy link
Contributor Author

chabulhwi commented May 9, 2024 •
edited

The PR description should be a coherent summary, not a list of commit messages. If the commit messages are largely separate, then this should be separate PRs; for instance, perhaps the porting note cleanup and renames can happen in mathlib before you move things.

@semorrison @eric-wieser I made a new PR from a commit and squashed the rest of the commits.

@chabulhwi chabulhwi force-pushed the list-theorems branch 3 times, most recently from 2b8a859 to 3b0a7fc Compare May 9, 2024 17:01
chabulhwi added a commit to chabulhwi/batteries that referenced this pull request May 9, 2024
@chabulhwi @semorrison
refactor: move theorems about lists from mathlib
39685d9 
* `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 it
  anymore.
* `List.cons_prefix_cons` is from `Mathlib.Data.List.Infix` and was
  renamed `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>
chabulhwi added a commit to leanprover-community/mathlib4 that referenced this pull request May 9, 2024
@chabulhwi
refactor: move theorems about lists to batteries
0a4fda3 
* `List.isEmpty_iff_eq_nil` and `List.modifyHead_modifyHead` are from
  `Mathlib.Data.List.Basic`. I removed the `simp` priority and the
  `nolint` attribute from `modifyHead_modifyHead` because we don't need
  it anymore.
* `List.cons_prefix_cons` is from `Mathlib.Data.List.Infix` and was
  renamed `List.cons_prefix_iff`.

We need these theorems to prove `String.splitOn_of_valid`. See
leanprover-community/batteries#756.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 9, 2024
chabulhwi added a commit to chabulhwi/batteries that referenced this pull request May 10, 2024
@chabulhwi @semorrison
refactor: move theorems about lists from mathlib
a6552b7 
* `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 it
  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>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 10, 2024
chabulhwi added a commit to chabulhwi/batteries that referenced this pull request May 10, 2024
@chabulhwi @semorrison
refactor: move theorems about lists to batteries
64b1647 
* `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>
chabulhwi added a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2024
@chabulhwi
refactor: move theorems about lists to batteries
8ea0b9d 
* `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/batteries#756.
chabulhwi added a commit to chabulhwi/batteries that referenced this pull request May 23, 2024
@chabulhwi @semorrison
refactor: move theorems about lists to batteries
6abc979 
* `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>
@chabulhwi @semorrison
refactor: move theorems about lists from mathlib
df9f54c 
* `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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@chabulhwi @semorrison @eric-wieser @leanprover-community-mathlib4-bot