This PR takes Array-specific lemmas at the end of `Array/Lemmas.lean`
(i.e. material that does not have exact correspondences with
`List/Lemmas.lean`) and moves them to more appropriate homes. More to
come.
This PR adds `Array.replace` and `Vector.replace`, proves the
correspondences with `List.replace`, and reproduces the basic API. In
order to do so, it fills in some gaps in the `List.findX` APIs.
This PR moves away from using `List.get` / `List.get?` / `List.get!` and
`Array.get!`, in favour of using the `GetElem` mediated getters. In
particular it deprecates `List.get?`, `List.get!` and `Array.get?`. Also
adds `Array.back`, taking a proof, matching `List.getLast`.
This PR adds `LawfulBEq` instances for `Array` and `Vector`.
(Note this replaces a contribution of @mehbark to Batteries for the
LawfulBEq instance for Vector, which was dropped during the release
process due to conflicts. Thanks for that contribution!)
This PR aligns current coverage of `find`-type theorems across
`List`/`Array`/`Vector`. There are still quite a few holes in this API,
which will be filled later.
This PR completes the alignment of lemmas about monadic functions on
`List/Array/Vector`. Amongst other changes, we change the simp normal
form from `List.forM` to `ForM.forM`, and correct the definition of
`List.flatMapM`, which previously was returning results in the incorrect
order. There remain many gaps in the verification lemmas for monadic
functions; this PR only makes the lemmas uniform across
`List/Array/Vector`.
This PR makes `take`/`drop`/`extract` available for each of
`List`/`Array`/`Vector`. The simp normal forms differ, however: in
`List`, we simplify `extract` to `take+drop`, while in `Array` and
`Vector` we simplify `take` and `drop` to `extract`. We also provide
`Array/Vector.shrink`, which simplifies to `take`, but is implemented by
repeatedly popping. Verification lemmas for `Array/Vector.extract` to
follow in a subsequent PR.
This PR makes the signatures of `find` functions across
`List`/`Array`/`Vector` consistent. Verification lemmas will follow in
subsequent PRs.
We were previously quite inconsistent about the signature of
`indexOf`/`findIdx` functions across `List` and `Array`. Moreover, there
are still quite large gaps in the verification lemma coverage for these
even at the `List` level.
My intention is to make the signatures consistent by providing:
`findIdx` / `findIdx?` / `findFinIdx?` (these all take a predicate, and
return respectively a `Nat`, `Option Nat`, `Option (Fin l.length)`) and
similarly `idxOf` / `idxOf?` / `finIdxOf?` (which look for an element)
for each of List/Array/Vector. I've seen enough examples by now where
each variant is genuinely the most convenient at the call-site, so I'm
going to accept the cost of having many closely related functions.
*Hopefully* for the verification lemmas we can simp all of these into
"projections" of the `Option (Fin l.length)` versions, and then only
have to specify that.
However, I will not plan on immediately either filling in the missing
verification lemmas (or even deciding what the simp normal forms
relating these operations are), and just reach parity amongst
List/Array/Vector for what is already there.
This PR adds missing monadic higher order functions on
`List`/`Array`/`Vector`. Only the most basic verification lemmas
(relating the operations on the three container types) are provided for
now.
This PR remove simp priorities that are not needed. Some of these will
probably cause complaints from the `simpNF` linter downstream in
Batteries, which I will re-address separately.
This PR uniformizes the naming of `enum`/`enumFrom` (on `List`) and
`zipWithIndex` (on `Array` on `Vector`), replacing all with `zipIdx`. At
the same time, we generalize to add an optional `Nat` parameter for the
initial value of the index (which previously existed, only for `List`,
as the separate function `enumFrom`).
This PR lowers the simp priority of `List/Array/Vector.mem_map`, as
downstream in Mathlib many lemmas currently need their priority raised
to fire before this.
This PR defines `Vector.flatMap`, changes the order of arguments in
`List.flatMap` for consistency, and aligns the lemmas for
`List`/`Array`/`Vector` `flatMap`.
This PR completes aligning `List`/`Array`/`Vector` lemmas about
`flatten`. `Vector.flatten` was previously missing, and has been added
(for rectangular sizes only). A small number of missing `Option` lemmas
were also need to get the proofs to go through.
