Proofs involving Vector

Stream: batteries

[Alex Mobius]

Good day,
I'm a newcomer to Lean, so apologies in advance if I'm missing something obvious or cause any offense.
I've recently tried to use Batteries.Vector in my project, and found doing proofs with it extremely cumbersome. There's sore lack of basic theorems, like getElem_set, etc. I find myself writing unfolds of someone else's functions, which is probably not what I am supposed to be doing.
Is there a canonical way to do that? I feel that at least getElem_toArray would be very helpful.

[Yaël Dillies]

docs#Batteries.Vector is a recent addition. Furthermore, Batteries had a maintainer availability crisis until recently. I am not a Batteries maintainer, but I am sure that a PR adding those lemmas would be welcome :smile:

[Alex Mobius]

Right. I'll try to lemmafy my own code to remove unfold duplication, and whatever I end up with, I'll send upstream.
I wonder why mathlib's vector is a subtype of lists, not arrays; I guess it's better for induction.

[Shreyas Srinivas]

Where?

[Shreyas Srinivas]

Stdlib's vectors?

[Shreyas Srinivas]

As far as I know, what you say is true for Mathlib's vectors

[Alex Mobius]

Right :D I mean, what are you even doing without mathlib

[François G. Dorais]

There is a planned Batteries PR for many of these gaps for Vector. It's waiting for some Lean core changes right now, which I believe will all be part of the next release at the end of this week.

[Kim Morrison]

@François G. Dorais which changes are those? If you're waiting on something that is not yet merged, please let me know asap, as I have nothing further on my radar for the release cut.

[Kim Morrison]

@Alex Mobius, I would suggest treating Mathlib's Vector as vestigial. (Indeed, if it's possible to replace uses of it with Batteries' Vector, I'd be happy to see that happen.)

[Kim Morrison]

Currently Batteries.Vector is a "best effort" API. I still have a lot of work to do on the Array API in the Lean repository over the next month, but once that nears completion I will turn my attention to Vector. The closer people can get it to the Array API, the better (i.e. the less work for me later. :-)

[François G. Dorais]

The changes I need are already in for the next release. I just haven't checked carefully yet. Will do soon! It would help if there was a recent PR with a full toolchain for testing. (I use System 76 Pop! so elan doesn't allow me to grab the Ubuntu builds even though they probably would work just fine. I can also use Mac OS on my M2.)

[Henrik Böving]

Why does your Linux distro influence what downloads elan can make? I can just fetch all releases on my Fedora machine without troubles

[François G. Dorais]

lake build says error: binary package was not provided for 'linux' when I try to use the pr-release-5705 toolchain.

[Henrik Böving]

so if you run

[Henrik Böving]

λ lean +leanprover/lean4-pr-releases:pr-release-5705  --help

that doesn't work?

[François G. Dorais]

Ha! That does work! Why?

[Henrik Böving]

what's in your lean-toolchain file for that directory?

[François G. Dorais]

Hahaha! Thanks! I was missing the 4... lol!

[François G. Dorais]

All good now! Thanks Henrik!

[Shreyas Srinivas]

Btw, the Vector API is still incomplete

[Shreyas Srinivas]

I have a PR to port the monadic defs as well, but it has been in limbo dating back a few months, when batteries' status was unclear

[Shreyas Srinivas]

Alex Mobius said:

Right :D I mean, what are you even doing without mathlib

Loads of CS programming stuff and a lot of CS-ish stuff

[Shreyas Srinivas]

The PR is batteries#925 feel free to take it up and finish it. I don't expect to be able to touch it until January.

[Shreyas Srinivas]

There are only three sorrys to fix: in modifyM, mapM, and mapIdxM. Here's one of them

[Shreyas Srinivas]

@Alex Mobius : There is a getElem instance for Batteries.Vector. For the theorems you should be able to piggy-back off the corresponding array theorems for the moment

[Kim Morrison]

Oof, I just ran into the gaps in Vector this morning, it was pretty painful, nigh unusable. I've created batteries#1018 as a start, but there is a long way to go here.

[François G. Dorais]

@Kim Morrison I agree! Can this wait until I get my vector PR ready? I'll make sure it includes what you need. Now that Henrik figured out my silly typo :man_facepalming: , I can get that PR up before the upcoming Lean update.

[François G. Dorais]

It is actually easier to just merge batteries#1018 and wait for the next lean update before the bigger vector update.

[Kim Morrison]

Yes, nothing should ever wait unnecessarily. :-)