feat: scan combinators for Vectors

[cmlsharp]

This depends on #1589

In conjunction with #1590 and #1589, this should conclude the project of bringing the 'scan' combinator to parity across List, Array, iterator, and Vector.

This takes a basically analogous approach to Array. In principle Array could be implemented in terms of Vector, except the Vector methods do not have the optional 'start' 'stop' parameters (which also keeps the return type of these functions much simpler). This is inline with the standard library's Vector methods.

[ghost]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1643 has successfully built against this PR. (2026-01-30 14:48:43) View Log

[fgdorais]

I think this is nearly next in the queue. Could you merge main now that #1589 has been merged?

[cmlsharp]

Done. right now some of the usize logic in Vector is duplicated with that in Array. Maybe there should be some shared Batteries.Data.USize for these theorems?

[fgdorais]

Yes, please make a quick PR to add the USize lemmas you need to Batteries.Data.UInt.

[cmlsharp]

Additionally, something I noticed while writing these is that the default stop/start parameters can make proof automation a bit annoying. E.g. consider

@[grind =]
theorem Vector.scanl_push {f : β → α → β} {as : Vector α n} {a : α} :
    (as.push a).scanl f init = (as.scanl f init).push (f (as.foldl f init) a) := by
  apply toArray_inj.mp
  simp only [toArray_scanl, toArray_push, Array.scanl_push, foldl]

simp only is required here because otherwise Vector.size_toArray and Array.size_push will cause

⊢ Array.scanl f init (as.toArray.push a) 0 (as.toArray.push a).size  ...

to simplify to

⊢ Array.scanl f init (as.toArray.push a) 0 n  ...

which then causes Array.scanl_push to fail to unify.

In the standard library, they seem to solve this issue (for e.g. Array.foldl) by having two versions of many such lemmas. E.g.

theorem Array.foldl_push {f : β → α → β} {init : β} {xs : Array α} {a : α} :
    (xs.push a).foldl f init = f (xs.foldl f init) a

and

@[simp, grind =]
theorem Array.foldl_push' {f : β → α → β} {init : β} {xs : Array α} {a : α} {stop : Nat}
    (h : stop = xs.size + 1) :
    (xs.push a).foldl f init 0 stop = f (xs.foldl f init) a

(there are many of these pairs e.g. Array.foldl_map and Array.foldl_map')
where if any, the latter is the one that gets the simp/grind annotations. We could do the same for Array.scan*.

[cmlsharp]

Yes, please make a quick PR to add the USize lemmas you need to Batteries.Data.UInt.

Done #1673. this additionally moves one (unshared) lemma from this implementation to Batteries.Data.UInt, because it seems like it might be more generally useful