feat: add APIs around Array splitting

[hargoniX]

No description provided.

[fgdorais]

Code duplication.

[hargoniX]

Are there still issues with this branch @digama0?

[kim-em]

I am tempted to suggest that these functions should be returning Subarrays, so they can be 0(1).

However Subarray is rather underdeveloped, and has some issues, e.g. leanprover/lean4#2360, so I'm not sure.

[fgdorais]

Maybe Std should have its own Subarray with a better interface (leanprover/lean4#2164) and without a coercion to Array (leanprover/lean4#2360).

[hargoniX]

So what is the call here? Merge like this (possibly until a Subarray API exists)? Or shall I try to develop a Subarray API for std and then re-implement this in terms of the std Subarray API.

[fgdorais]

@hargoniX The smart call is: what do you actually need? It's definitely not a great for you to wait on a major array refactor. Do you need this now or can you wait another four or more months until something much better comes along?

[kim-em]

My preference would be, assuming that this PR is actually needed somewhere and the performance of this PR is sufficient for that purpose, that we add a comment suggesting that in future when there is a usable Subarray API that these functions be refactored to use it. And otherwise proceed as is.

[digama0]

We want the Subarray API to be similarly expansive to the Array API. But that doesn't affect this PR much, unless the author wants to write Subarray versions of these definitions. We can always do it later.

[hargoniX]

@hargoniX The smart call is: what do you actually need? It's definitely not a great for you to wait on a major array refactor. Do you need this now or can you wait another four or more months until something much better comes along?

I'm just adding APIs that I think could be useful I don't use them (yet).

[joehendrix]

I'd be inclined to not include these functions in stdlib. The performance of the split variants is O(n) and so probably not a great choice for code where performance matters. For theorem proving one would also want simplification theorems and related rules.

I'm separately partial to head instead of front since that's common in related libraries like the Haskell vector.

Expanding the subarray API (or theorems) would be great though.

[fgdorais]

Heartbeat check: is this PR still active? If it is then just give a thumbs up and I will delete this comment.

[hargoniX]

I'm not going to invest more time in it.

[fgdorais]

Understood. I'm removing awaiting-author and adding help-wanted to signal that this PR is "for adoption".