change to simp normal form for `List` lookup

Stream: nightly-testing

[Kim Morrison]

This is giving everyone a heads-up that I'd like to implement a significant change to simp normal forms, and that this will include changes to Lean / Batteries / Mathlib.

We want L[i] (which is implicitly L[i]'h, where h : i < L.length) to be the simp normal form for List lookup, rather than L.get ⟨i, h⟩. We think this is a much better experience for new users, and aligns better with the Array normal forms.

I've implemented this as lean#4400, and the corresponding patches to Batteries and Mathlib are at

• batteries#843
• #13815

You'll notice upon looking at these diffs that I have replaced many functions involving get?/get with functions involving L[i]?/L[i], and in nearly all cases I have deprecated the old functions. I am willing to remove some (or even many) of these deprecations if there is a case for it --- they were useful to me to help make more thorough changes. I will note that (perhaps with one or two exceptions, I'll have to double check) all of these deprecations are actually respected (i.e. no longer used at all), and so in the interests in minimising the explosion of the API surface area I do prefer that we keep as many of these deprecations as possible.

[François G. Dorais]

I haven't looked through all of it yet but this feels like a breath of fresh air! :fresh_air:

[Kim Morrison]

I'm hoping that the fact that all the downstream consequences work out okay means we can proceed on this pretty soon. Obviously once #4400 is merged we're setting a big train in motion.

[François G. Dorais]

I'm in favor of keeping all the deprecations. That will help me and others update their code to the new normal.

[François G. Dorais]

Are you looking for optimizations or just a checkmark?

[Kim Morrison]

Very happy to have suggested changes to any of the 3 PRs. But mostly just giving notice before we actually set things in motion. :-)

[Kim Morrison]

Integrated CI has now succeeded, so I'll plan to start merging over the weekend.

[Yaël Dillies]

What's the performance cost?

[James Gallicchio]

I was updating LeanColls to a new version today and ran into a deprecation -- List.get_append_left. I rely pretty heavily on List.get because I want Lean to infer Fin L.length often.

If that is no longer going to be a supported simp normal form then I'd maybe prefer List.get be deprecated too, since otherwise we will be left with a function with no API... (I was surprised that List.get_append_left was deprecated and went on a search to figure out why!)

[Kim Morrison]

I'm actually pretty happy to roll back some (many!) of these deprecations on theorems.

We're not going to deprecate List.get itself, certainly. It's not too hard to find places in Mathlib where we're trying to do some Fin indexed combinatorics and get is the right tool. However generally I've been finding that while it's useful in the definitions, in proofs the new simp normal form means we rarely need the theorems directly about get.

[Kim Morrison]

It's usually fine to have "a function with no API" as long as there's a simp lemma that immediately rewrites it to a function that does have API.

[Kim Morrison]

I'd love to see a more concrete description of what goes wrong for your use case if you switch to using GetElem.

[James Gallicchio]

Makes sense. I was able to rewrite my proofs without too much headache (the diff isn't too helpful)

[Mario Carneiro]

Kim Morrison said:

I've been finding that while it's useful in the definitions, in proofs the new simp normal form means we rarely need the theorems directly about get.

I don't think this is sufficient reason for deprecation, this just means it shouldn't be a simp lemma

[Mario Carneiro]

it's also not cool to upstream lemmas from batteries and then deprecate/remove them; just put them back where they came from if you are going to do that

[Kim Morrison]

It is certainly useful to at least temporarily have the @[deprecated] on all these lemmas: it's really helpful when switching over downstream libraries to use the new preferred API to have warnings on all the places where proofs are detouring back via the old API.

But I agree that in the long run the lemmas should not actually be deleted while List.get still exists (which I think should be forever!).

How about I leave these as @[deprecated] for now, in the hope that helps people switch, but when it is "time to delete" them in core I will instead drop them back into Batteries?