feat: migrate List lemmas from mathlib

[AdrienChampion]

Integrates a few of Mathlib's lemmas over Lists. Some proofs have been slightly simplified

[AdrienChampion]

Solved simp-normal form issues, but I'm not sure what to do with

@[simp 1100] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by
  -- ...

I commented the simp 1100 as the linter complains with

List.modifyHead_modifyHead.{u_1} Left-hand side simplifies from
  List.modifyHead g (List.modifyHead f l)
to
  match
  match l with
  | [] => []
  | a :: l => f a :: l with
| [] => []
| a :: l => g a :: l
using
  simp only [@List.modifyHead]
Try to change the left-hand side to the simplified term!

since List.modifyHead is @[simp], but I don't want to use the simplified term :/

[digama0]

List.modifyHead should not be simp. I think most of those are mistakes, that kind of thing used to work in lean 3 but in lean 4 it unfolds directly to the match statement which is almost never what you want.

[AdrienChampion]

List.modifyHead should not be simp. I think most of those are mistakes, that kind of thing used to work in lean 3 but in lean 4 it unfolds directly to the match statement which is almost never what you want.

So should I remove the simp on List.modifyHead then? Or just leave it like this?

[digama0]

So should I remove the simp on List.modifyHead then?

👍

[AdrienChampion]

Done, I made modifyHead_modifyHead just be simp instead of simp 1100 since the linter authorized me

[fgdorais]

Would it make sense to split this PR into sections? Everything looks good and many parts deserve an immediate all clear review (e.g. the concat lemmas) but they are bogged down by tiny issues (e.g. is there a common use case for length_eq_three?)

[AdrienChampion]

I'm fine with splitting this PR if you let me know what does (not) deserve to be merged immediately.

Regarding length_eq_three I don't have an argument for it, it's only here because it can be migrated from mathlib. From what I can see it's used in only one place there:

❯ rg length_eq_three
Mathlib/Data/Multiset/Basic.lean
801:      (List.length_eq_three.mp h).imp fun _a =>

Mathlib/Data/List/Basic.lean
223:theorem length_eq_three {l : List α} : l.length = 3 ↔ ∃ a b c, l = [a, b, c] :=
225:#align list.length_eq_three List.length_eq_three

[fgdorais]

I was thinking about splitting per section header but that's perhaps too much detail. Here is what I'm thinking:

• The head and tail stuff can go together, perhaps combined with concat, these parts are really straightforward. Length and get stuff can go in there too but it might be easier to split them since the use cases are rare.
• The pure, map, bind stuff should be separate since there is a need to discuss (not necessarily in this PR) whether to make the List functor an applicative, an alternative, and/or a monad. It's lawful for all but there are other issues. The outcome of this decision will cause the syntax of the lemmas to change.

It's a matter of taste whether to split into smaller parts than these two.

[fgdorais]

Got part way...

[semorrison]

Is there a matching Mathlib PR? It would be nice to be able to verify that Mathlib can be updated cleanly.

(Maybe you know this already, but you can just make a Mathlib branch in which the lakefile points to this branch.)

[AdrienChampion]

Is there a matching Mathlib PR? It would be nice to be able to verify that Mathlib can be updated cleanly.

(Maybe you know this already, but you can just make a Mathlib branch in which the lakefile points to this branch.)

I can do that, I did not know about the lakefile-pointer bit but I can probably figure it out.

But I'd rather wait for the review process to be completed on this PR first, so that I know what will actually end up being merged.

[AdrienChampion]

On that note, this PR is awaiting reviews, not author, could you change the label back @semorrison please?

[semorrison]

@AdrienChampion, in fact anyone can change labels, by writing a message solely containing one of awaiting-author, awaiting-review, or WIP!

[AdrienChampion]

Is there something blocking this PR on my end?

Is it maybe the mathlib PR, should I open one to move on on this one?

[fgdorais]

Golfing.

[fgdorais]

There was a recent discussion on Zulip that is relevant to this PR: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.2Econcat.20and.20List.2Eappend

[fgdorais]

From a quick experiment, this seems to be mostly absorbed by core and other PRs. Should we close?

[AdrienChampion]

I think so, thank you for pointing it out