feat: Add Array.scan{l,r,lM,rM}

[cmlsharp]

• Depends on: feat: add List.scanlM/scanrM #1588

This PR adds the Array equivalents of List.scan{l,r,L,R}. It was originally part of #1581.

• This PR provides both reference and efficient versions of Array.scanlM and Array.scanrM, and then defines Array.scanl and Array.scanr in terms of them. This is identical to how the standard library currently handles Array.fold*.
• Unlike the standard library, this PR attempts to make minimal use of unsafe in the implementations of the efficient versions. It defines an assumption (as Array.size_fits_usize) as well as an unsafe proof of this assumption (as Array.unsafe_size_fits_usize). These are currently public definitions. I could make them private, but they seem useful for writing other 'efficient' array functions.
• Array.scanlM is proven to be equivalent to its efficient implementation under the assumption that Array.size_fits_usize holds. The efficient version of Array.scanrM additionally uses this assumption when constructing the proofs for the bounds checks.
• I do not have a proof that the efficient version of Array.scanrM is equivalent to its efficient version under Array.size_fits_usize. It should be possible, but the structure of these two implementations differ more, so the proof is more difficult. With Array.scanlM the only difference between the implementations was the use of USize or Nat for the index, whereas the Array.scanrM reference implementation builds the array, then reverses it and the efficient implementation iterates over the array in reverse.

[cmlsharp]

WIP

[cmlsharp]

awaiting-review

[eric-wieser]

Suggested change

	theorem toList_drop (as: Array α) (n : Nat) :
	@[simp, grind =]
	theorem toList_drop (as: Array α) (n : Nat) :

to match toList_erase above.

[cmlsharp]

This doesn't work as a simp lemma because simp simplifies '(as.drop n).toList' to 'List.take (as.size - n) (List.drop n as.toList)`

[cmlsharp]

Fwiw I think this is very frustrating. Array.drop is automatically simplified to Array.extract. This over-eager simplification is why I wanted a toList_drop method to begin with.

[fgdorais]

There are way too many simp lemmas for my taste. Eric is very fond of them though and I respect his opinion. We (in general, including Eric and I) need a common language to talk about simp-normal-form. The Mathlib/Batteries concerns are a bit different.

[eric-wieser]

Thanks for starting the Zulip thread; indeed this can't be simp right now.

[fgdorais]

Can we resolve this or are we hoping to fix the simp issues upstream?

[eric-wieser]

I was going to claim that these should be simp, but having found #lean4 > Direction of List.map_toArray vs Array.toList_map @ 💬 I'm no longer sure.

[fgdorais]

Can we proceed without these simps?

[fgdorais]

Our Mathlib Testing CI is partly broken at this time. The last run has reported an error: https://github.com/leanprover-community/mathlib4-nightly-testing/tree/batteries-pr-testing-1589

Could you investigate to see whether there needs to be a Mathlib adaptation or whether this is a false negative?

[cmlsharp]

leanprover-community/mathlib4#35228

I opened a PR that fixes the issue. The problem was that I added List.reverse_singleton, but that was something that already existed in mathlib. The simple solution is to replace it.

[fgdorais]

Thanks! This is not the preferred way to make a Mathlib adaptation PR but I think we can work with it.

The preferred way is to edit the Mathlib Testing branch until CI works and then make a PR from that branch into Mathlib. I've added your fix to that branch and we will see what CI says, in case we need to add some additional fixes. If CI clears, then we can just use your Mathlib PR, otherwise we will revert to the preferred route.

@kim-em Could you give @cmlsharp write access to Mathlib Testing. (Is there a way to automate this?)

[cmlsharp]

Oh sorry about that! I will do that in the future. I just realized there was a commit I meant to push prior to making the PR (marking this lemma simp since it is marked that way in mathlib). I just pushed it.