[Merged by Bors] - feat(List/rotate): migrate to get, new lemmas, golf
#12171
Conversation
The goal is to drop `nth_le_tails` and `nth_le_inits` soon.
- Add `List.Nodup.rotate_congr_iff`, `List.cyclicPermutations_ne_nil`, `List.head?_cyclicPermutations`, `List.head_cyclicPermutations`, `List.cyclicPermutations_injective`, `List.cyclicPermutations_inj`. - Change `List.nthLe_cyclicPermutations` to `List.get_cyclicPermutations`. While the old lemma wasn't deprecated during port, the definition `List.nthLe` was, so I think that we can drop the lemma without a deprecation period.
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
There was a problem hiding this comment.
Thank you for doing this!
I verified that all existing lemmas are kept (sometimes moved); only changes are for nthLe -> in theorem statements. I did not scrutinize the new proofs carefully; they broadly look nicer than the old ones.
While there's no agreed policy on deprecations yet, not deprecating these lemmas for a while seems fine to me.
| simp [dropLast_eq_take, cyclicPermutations_of_ne_nil _ h, nthLe_take', | ||
| rotate_eq_drop_append_take hn.le] | ||
| #align list.nth_le_cyclic_permutations List.nthLe_cyclicPermutations | ||
| theorem cyclicPermutations_ne_nil : ∀ l : List α, cyclicPermutations l ≠ [] |
There was a problem hiding this comment.
Can l : List α be moved left of the colon?
There was a problem hiding this comment.
Why? This will make pattern matching a bit less convenient for no obvious (to me) gain.
There was a problem hiding this comment.
If you want to move it, then please push to this branch. Otherwise, just merge it, please.
bors d=grunweg
There was a problem hiding this comment.
That is a fair point. (I was trying to understand why "hypothesis left of colon" was not followed - sounds like you have a good reason. Thanks for educating me!)
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
- Add `List.Nodup.rotate_congr_iff`, `List.cyclicPermutations_ne_nil`, `List.head?_cyclicPermutations`, `List.head_cyclicPermutations`, `List.cyclicPermutations_injective`, `List.cyclicPermutations_inj`. - Change `List.nthLe_cyclicPermutations` to `List.get_cyclicPermutations`. While the old lemma wasn't deprecated during port, the definition `List.nthLe` was, so I think that we can drop the lemma without a deprecation period.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
get, new lemmas, golfget, new lemmas, golf
- Add `List.Nodup.rotate_congr_iff`, `List.cyclicPermutations_ne_nil`, `List.head?_cyclicPermutations`, `List.head_cyclicPermutations`, `List.cyclicPermutations_injective`, `List.cyclicPermutations_inj`. - Change `List.nthLe_cyclicPermutations` to `List.get_cyclicPermutations`. While the old lemma wasn't deprecated during port, the definition `List.nthLe` was, so I think that we can drop the lemma without a deprecation period.
- Add `List.Nodup.rotate_congr_iff`, `List.cyclicPermutations_ne_nil`, `List.head?_cyclicPermutations`, `List.head_cyclicPermutations`, `List.cyclicPermutations_injective`, `List.cyclicPermutations_inj`. - Change `List.nthLe_cyclicPermutations` to `List.get_cyclicPermutations`. While the old lemma wasn't deprecated during port, the definition `List.nthLe` was, so I think that we can drop the lemma without a deprecation period.
List.Nodup.rotate_congr_iff,List.cyclicPermutations_ne_nil,List.head?_cyclicPermutations,List.head_cyclicPermutations,List.cyclicPermutations_injective,List.cyclicPermutations_inj.List.nthLe_cyclicPermutationstoList.get_cyclicPermutations. While the old lemma wasn't deprecatedduring port, the definition
List.nthLewas,so I think that we can drop the lemma without a deprecation period.
get_tailsandget_inits#12170