request for refactoring around `List.enum`

Stream: mathlib4

[Kim Morrison]

I am replacing List.enum with List.zipIdx in lean#6800 (for uniformity with Array operations; Array.zipWithIndex is simultaneously being renamed to Array.zipIdx).

This generates pairs in the opposite order, so there are occasional fix ups required, which I'm performing on lean-pr-testing-6800.

There are a few spots I'd like to hand off, if possible.

First, docs#TrivSqZeroExt.snd_list_prod will need a rewrite --- it is a somewhat fragile proof with a long rw followed by a long simp_rw. This theorem is not actually used anywhere, so another alternative is perhaps deleting it. I'll ping @Eric Wieser and @Kenny Lau on the basis they are listed in the authors line. But anyone should feel free to jump in!

(For now, pushing fixes directly to lean-pr-testing-6800 is ideal.)

Second, there are some updates needed in Mathlib/Data/List/Indexes. Hopefully this is just a matter of following the deprecation warnings, and if need be renaming theorems (and adding deprecations for these renamings). As far as I can see this file is only used by Mathlib/Computability/, so it would be great if someone using these files could take this task on. I'll ping here everyone listed in an "Authors:" line of this or a downstream file: @Jannis Limperg, @Fox Thomson, @Chris Wong, @Yaël Dillies.

[Chris Wong]

Thanks Kim. At least for automata, I believe we only use Mathlib.Data.List.Indexes for the list_reverse_induction export, which looks to be unaffected by this change?

[Chris Wong]

To be honest I'm not sure why the induction principle is in that module and not the main one :sweat_smile:

[Kim Morrison]

Okay. It doesn't directly help with the deprecation warnings, but if you felt like moving the lemma you actually depend on elsewhere, then it makes it easier to argue that everything affected by this change is unused and can just itself be deprecated rather than fought with.

[Ruben Van de Velde]

It's just a worse version of docs#List.reverseRecOn too

[Ruben Van de Velde]

#21166

[Yakov Pechersky]

I pushed a TrivSqZeroExt.snd_list_prod fix, thanks to the new List.zipIdx_cons'

[Ruben Van de Velde]

I merged my change into the branch as well

[Kim Morrison]

Thanks very much for the assistance here!

[Kim Morrison]

The last stage is #21201:

As of 2025-01-29, these specification lemmas for List.mapIdx, List.mapIdxM, List.foldlIdx and List.foldrIdx are not used anywhere in Mathlib. Moreover, with List.enum and List.enumFrom being replaced by List.zipIdx in Lean's nightly-2025-01-29 release, they now use deprecated functions and theorems.

Rather than updating this unused material, we are deprecating it. Anyone wanting to restore this material is welcome to do so, but will need to update uses of List.enum and List.enumFrom to use List.zipIdx instead. However, note that this material will later be implemented in the Lean standard library.