feat: statically sized Vector type

[Shreyas4991]

This PR adds a static vector type to batteries akin to Mathlib.Data.Vector with a key difference: It is based on Array instead of List and is designed for efficient operations with while offering a static size . The PR attempts to make the API of Batteries.Data.Vector isomorphic to Mathlib.Data.Vector to the maximum possible extent.

EDIT: This PR also extends all the Array API to Vector
For discussion see this Zulip thread

EDIT: After consideration of the magnitude of the task, I limit this PR itself to porting non-monadic functions from Init.Data.Array.Basic and some surrounding API, as well as the extension theorem. I will create further PRs for adapting monadic functions, relevant theorems, and elements of the Array API already present in Batteries and Init

Depends on

• feat: size lemmas for Array.shrink #801
• feat: Array lemma for empty map added #877 : Later Vector.map_empty needs to be changed to use the lemma introduced there.

[nomeata]

Thanks! Looking forward to having that. I wonder how soon we'd like to have it (or a private copy) in core. I certainly wrote code there where I thought it would be easier with this…

I noticed that not all operations are backed by Array operations; at least not all that could be. It seems like it should be the case, shouldn't it?

Can we also get nice #[a,b,c] syntax for terms and patterns? Especially in patterns its nice if that is then a complete pattern.

[Shreyas4991]

Changing all operations to array operations is my next goal. This causes quite a bit of proof breakage that will have to be fixed. It doesn't make sense to turn operations like head and cons into array operations I suppose?

[nomeata]

It doesn't make sense to turn operations like head and cons into array operations I suppose?

head certainly! Not sure about cons. Maybe it shouldn't be there? Or at least with a warning.

[nomeata]

(also I should mention that I'm just offering unsolicited opinions here, the maintainers have authority here)

[Shreyas4991]

I have started porting the large Array API under Init.Data.Array.Basic. This is a very large file, so I expect this to take some time.

[Shreyas4991]

This latest commit also adds a number of docstrings, which should be reviewed

[Shreyas4991]

I would like to merge this PR after taking care of any new reviews in order to avoid putting too many things together. Subsequent PRs will:

1. Add a separate file for monadic defs and their dependents.
2. Port Array lemmas.
3. Add insertion and sort defs.

[fgdorais]

First pass on Vector.Basic.

[fgdorais]

Review Vector.Lemmas.

[fgdorais]

Ready for community review.

[Shreyas4991]

awaiting-review

[semorrison]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/style.20guide.20for.20comments.3F/near/438709035

[Shreyas4991]

Done

[YaelDillies]

Could you explicitly indicate in the docstrings the cost of each operation? See List.map for what I mean.

[Shreyas4991]

Could you explicitly indicate in the docstrings the cost of each operation? See List.map for what I mean.

We maintained those complexity annotations where the corresponding Array docstring stated the complexity. For the rest, at some point, we just agreed that predicting whether an operation is an in-place edit is not trivial.