[Bubbler-4]

This PR adds reverse iterators for Array and Vector.

This change was split out of #15233 into a separate PR, as per the comments there.

[datokrat]

Thanks for helping us out with the iterator API!

I noticed that the verification API for the reverse iterators is still missing (under Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean etc.). It would be very helpful to have the verification API already in this PR. Besides the benefit of proving that the iterator does what it should, I believe that writing it would have caught some of the things I remarked, e.g. the missing Finite and IteratorLoop instance

[datokrat]

Typo: Should be ArrayRevIterator. toList, as in your tests, works, but you wouldn't be able to use it in proofs without the Finite instance. There's the same type in instIteratorLoop below.

[datokrat]

Something that will bite us in the lemmas (iterRevFromIdxM is the natural thing to induct over):
For non-empty arrays, iterRevFromIdxM cannot represent the exhausted state pos := 0.

I also don't think that the match_pattern will work here because of min; this is also something that would become apparent when writing the lemmas.

I think we could address both issues by instead providing an iterator iterRevFromRevIdxM, where the last element of the iterator gets position 0. Then the exhausted state becomes representable and we can get rid of the min. What do you think? Alternatively, we could provide both iterRevFromRevIdxM, the more well-behaved one, and iterRevFromIdxM, the more intuitive one.

[Bubbler-4]

iterRevFromRevIdxM sounds like a good idea indeed. It should also help with formalizing the equivalence with the forward iterator too. That said, how would I actually write down the statement that "iterRevFromRevIdxM is equivalent to iterFromIdxM on the reversed array"?

[datokrat]

It would already be great to show that applying toList to both yields the same result. The more general, but also more difficult, theorem would be to show that these iterators are equivalent. Although it would be great to have such a lemma, I think the toList-based lemma would be sufficient for now (except, of course, if you are willing to prove the general equivalence, that would be great).