feat: add Vector.tail API batteries#1234

Stream: batteries

[Kim Morrison]

I would not have merged batteries#1234, @François G. Dorais . I mean, I understand it is my own fault for not deprecating Vector.tail already, but it seems the obvious conclusion to "what should I do about Vector.tail not having API" should be to complain that it's pointless API surface area that should be removed.

While I'm at it, it was merged with terminal simp only [...]s that should have just been simp [...], which promptly broke on nightly-testing --- this is why we prefer to avoid terminal simp only, because they are fragile!

lean#8445 adds the simp lemma converting Vector.tail into Vector.extract (analogous to the existing lemmas for take and drop). Hopefully the simpNF linter will complain on the next Batteries nightly.

[Mario Carneiro]

A recent relevant discussion (about cons not tail but the idea is similar): #mathlib4 > ✔ List.Vector - could we just remove it? @ 💬

[Mario Carneiro]

I think for simp purposes extract is not better than tail, since the latter has a better defeq than extract could ever have

[Mario Carneiro]

but it seems the obvious conclusion to "what should I do about Vector.tail not having API" should be to complain that it's pointless API surface area that should be removed.

Also I really don't agree with this kind of argument. Maybe the functions exist because they are useful? Not having lemmas says only that they haven't been a priority for the FRO

[Mario Carneiro]

I consider lean#8445 actively harmful, and would prefer you just removed the operation from lean core and put it in batteries

[Mario Carneiro]

actually extract looks like the worst of all of these operations in terms of its signature. It has optional arguments that will make rewrites painful, and a messy type which requires casts. The take and drop simp lemmas should not be simp lemmas, they should all just be simp normal

[Mario Carneiro]

in particular, (v.take n).toList = v.toList.take n should be a simp lemma and the take_eq_extract lemma will surely leave the LHS here in a mess

[Mario Carneiro]

Kim Morrison said:

While I'm at it, it was merged with terminal simp only [...]s that should have just been simp [...], which promptly broke on nightly-testing --- this is why we prefer to avoid terminal simp only, because they are fragile!

What broke exactly? It's a short simp only containing only a few lemmas, did the statements of these lemmas change?

[Mario Carneiro]

The issue seems to be that on current batteries main, { toArray := #[], size_toArray := ⋯ }.toList is reduced to [] by simp only (no lemmas), while on the nightly-testing version it is not reduced but there is a toList_mk simp lemma. What changed?

[Mario Carneiro]

This makes some sense since it's pure constructor reasoning. Is the flag of simp for doing constructor reduction no longer enabled by default?

[Mario Carneiro]

The reason for the discrepancy is not a change to simp, but a change in the statements of some theorems, because .toList here changed from being syntax sugar for .toArray.toList (which displayed as .toList because it was a stack of parent projections) to being an actual function Vector.toList, which needs unfolding and is not unfolded by simp only. (Maybe it should be an abbrev...)

[François G. Dorais]

Kim Morrison said:

I would not have merged batteries#1234, @François G. Dorais . I mean, I understand it is my own fault for not deprecating Vector.tail already, but it seems the obvious conclusion to "what should I do about Vector.tail not having API" should be to complain that it's pointless API surface area that should be removed.

I see that Mario said much of this in his own words...

That was exactly my first thought about batteries#1234. However, I changed my mind after realizing that the alternatives Vector.eraseIdx and Vector.extract both have unnecessarily complex API and a simpler API for Vector.tail makes sense in Batteries.

I was actually surprised that Vector.tail was in core at all since Array.tail does not exist. I imagined that this was an oversight and it would soon disappear from core and we could add it to Batteries (along with Array.tail) instead.

Is there a reason to keep Vector.tail in core?

[Kim Morrison]

Consulting internally about whether we want to keep Vector.tail/take/drop as is, or deprecate/move downstream. I'll reply here when ready.