Achieve parity between Array and List lemmas

[mpenciak]

In order to encourage std4 users to write verifiable code with arrays, we should aim to have a similar set of lemmas for arrays (https://github.com/leanprover/std4/blob/main/Std/Data/Array/Lemmas.lean) as we do for lists (https://github.com/leanprover/std4/blob/main/Std/Data/List/Lemmas.lean).

[Vtec234]

A trick I learned from @digama0 is to liberally apply Array → List transfer theorems which reduce problems about Arrays to problems about Lists. For example foldl_eq_foldl_data. This works very well because functions on Lists usually have a simple inductive structure whereas functions on Arrays tend not to (using indexed accesses and so on), so the List-based proofs are often simpler. So from this perspective, it is actually better not to have those lemmas and rather encourage applying transfer whenever possible. The lemmas that are still necessary are those for when you really need to reason about something involving indices. For example, foldl_induction.

[ammkrn]

There may be other ones, but some of the remaining incongruities between the List and Array interfaces:

List	Array	notes
List.replicate	Array.mkArray	Mathlib also defines List.repeat
List.modifyNth	Array.modify
List.insertNth	Array.insertAt(!)	These have sort of a confusing relationship
List.length	Array.size	This seems purposeful, but it may be helpful to document it
List.splitOn/List.splitAt	Array.split	They're different, so I guess the goal is to have splitOn, splitAt and split for both types?

It may be helpful to document the difference (if any) between functions like .elem/.contains and Array.modify/Array.modifyOp as well.

@digama0 if at some point you decide any changes are appropriate, let me know if I can help.

[jeremysalwen]

I am doing some "practical program" proving with lean4, and I have found the following lemma really helpful

lemma Array.data_injective : Function.Injective (Array.data (α:=α)) := by sorry

If I want to prove some equality of arrays, I use apply Array.data_injective; simp which works pretty well.

However, it still feels like something is missing, because if I have some List subexpression in my goal, simp will simplify it away no problem, but if I have some Array subexpression, it won't.

I need to manually use this technique on each Array subexpression to get it to simplify. It feels like this could probably be automated some way?

[pcpthm]

lemma Array.data_injective : Function.Injective (Array.data (α:=α)) := by sorry

That is Array.ext' already defined in the prelude.