MapM for List.Vector

Stream: new members

[Scott Buckley]

Hi there, apologies if this is not the right place to ask such a question.

I'm just wondering why there isn't a List.Vector.MapM? I wondered if it is perhaps because there is a more general implementation of this somewhere that I should be using?

My particular use-case, if it helps, is that I have a List.Vector (List.Vector α n) n, and a function α → Option β, and I want to create an Option (List.Vector (List.Vector β n) n). This was simple with (non List) Vector.mapM, but I am switching over to List.Vector to make a lot of other proofs much simpler.

Thanks in advance!

[Jakub Nowak]

I think it's missing and we should have it. In fact, it looks like List.Vector API is missing quite a lot e.g. mapM, forM, zip, zipWithM, fold{l,r}{,M}.

[Scott Buckley]

Ok, good to know! I have already implemented List.Vector.MapM for my own satisfaction, I'd very much like to be involved in adding these to the library, if that is possible! I'm studying existing implementations for other types to try to match the approach.

[Jakub Nowak]

Sure! Check out #contrib.

[Shreyas Srinivas]

List.Vector has limited API for good reason. It got superseded by Vector for almost all uses.

[Shreyas Srinivas]

It was kept around because someone felt that they were still useful in some cases like PL contexts. I am not sure this is true anymore, since Finvec might work better and Vector can be used like Lists if absolutely needed.

[Jakub Nowak]

Why not supersede List with Array?

[Shreyas Srinivas]

Operations that are efficient for arrays are not natural for lists and vice versa

[Jakub Nowak]

Exactly, that's why there's List.Vector and Vector. It's just List and Array with length as index parameter.

[Shreyas Srinivas]

Yes except when you find a definition missing in list.vector, it is worthwhile trying the Vector version.

[Shreyas Srinivas]

I think list.vector was saved by one member of the community. And they had very specific uses in mind

[Jakub Nowak]

In my opinion it's better to deprecate something then have a half-baked API. But if @Scott Buckley wishes to contribute to List.Vector then I see no reason to not have it.

[Jakub Nowak]

Are there many uses for Vector though? I never used it, and I would prefer to just use arr.size = n : Prop if there's a need for it.

[Shreyas Srinivas]

There’s prior discussion on this in the mathlib4 channel

[Scott Buckley]

Shreyas Srinivas said:

There’s prior discussion on this in the mathlib4 channel

Could you point me to this discussion please? I did a search before posting but wasn't able to find it.

[Shreyas Srinivas]

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20Vector.20namespace/near/440588550

[Shreyas Srinivas]

Basically nobody except Mario was defending its continued existence

[Shreyas Srinivas]

And Mario’s objection to deleting it rested on List.Vector being useful for something because it doesn’t have array underneath.

[Scott Buckley]

It seems to me that it is a fair bit more useful for writing proofs (which is what I am usually doing). However, if there was a nice way to do case destruction and induction in a list-like manner on the array-based Vector, that would also suit my needs I guess!

[Scott Buckley]

Regardless, it does exist as of now. Purely as an exercise I would be happy to implement some of the features mentioned above for it, and it would be fine if they ended up being thrown away if List.Vector is thrown away - it is good practice for me nonetheless.

[Shreyas Srinivas]

Convert the vector to a list of course

[Jakub Nowak]

I've looked through usages of Array in mathlib4, and it's not being used in any definition. It's only being used internally in a few functions for List (as an optimization). Vector is not being used in mathlib4 at all.
There are some usages of List.Vector though.

[Jakub Nowak]

There is no lemma of the form arr = .empty ∨ arr = arr'.push a, nor there is eliminator for these two cases for neither Array nor Vector. This is because, for this kind of induction style use, List and List.Vector are better suited.

[Jakub Nowak]

There is no performance gain of using Array over List in kernel. It only matters for compiled programs.

[Eric Wieser]

Jakub Nowak said:

There is no lemma of the form arr = .empty ∨ arr = arr'.push a

Note that these lemmas are generally worthless anyway; they should be expressed as induction principles not as compound expressions with Exists and Or

[Jakub Nowak]

Eric Wieser said:

Jakub Nowak said:

There is no lemma of the form arr = .empty ∨ arr = arr'.push a

Note that these lemmas are generally worthless anyway; they should be expressed as induction principles not as compound expressions with Exists and Or

Hm, why exactly do you think they would be worthless?

[Scott Buckley]

Is there an induction principle for Vector similar to List.Vector.inductionOn?

[Jakub Nowak]

Scott Buckley said:

Is there an induction principle for Vector similar to List.Vector.inductionOn?

There isn't, I think you could write one, but Eric seems to disagree?

[Jakub Nowak]

Ah, wait, no. Sorry, I've misread your message Eric.

[Jakub Nowak]

You could use obtain \<h, h\> := on a lemma expressed with Or. So I don't think it's worthless.

[Eric Wieser]

Why is that better than using induction though?

[Jakub Nowak]

It isn't.

[Eric Wieser]

In the end your ⟨ ⟩ has far more things in the braces than that, and you end up using the induction principle for Eq, Or, and Exists instead of more directly using the one for your specific type

[Eric Wieser]

We should definitely have an Array.recPush definition with the analgous statement

[Jakub Nowak]

I'm not so sure we should. If you need to prove something about your implementation that uses Array, wouldn't it be easier to just convert your Array to List at the very start of the proof?

[Eric Wieser]

That is

@[elab_as_elim]
def Array.recPush
    {α : Type u}
    {motive : Array α → Sort*}
    (empty : motive #[])
    (push : ∀ (as : Array α) (a : α), motive as → motive (as.push a))
    (arr : Array α) : motive arr :=
  match h : arr.size with
  | 0 => cast (congrArg motive <| by simp_all) empty
  | n + 1 => cast (congrArg motive <| by simp_all; sorry) <| push arr.pop arr.back (Array.recPush empty push arr.pop)
termination_by arr.size

[Scott Buckley]

I played a bit with a definition for List.Vector.mapM today. It can be a little tricky with the length proof obligation hanging around. I got the following working using tactic mode:

def List.Vector.mapM [Monad m] (f : α → m β) (l : List.Vector α n) : m (List.Vector β n) := by
  cases l using List.Vector.casesOn with
  | nil => exact pure (List.Vector.nil)
  | cons a l => exact return (List.Vector.cons (← f a) (← List.Vector.mapM f l))

I tried to implement the above using List.Vector.casesOn outside of tactic mode, which is doable, but will require some fiddling with specifying the right motive I guess - I'm new to this "motive" structure.

[Scott Buckley]

The following feels like a more "natural" definition to me, but does not compile:

def List.Vector.mapM [Monad m] (f : α → m β) : List.Vector α n → m (List.Vector β n)
  | ⟨[], h⟩ => pure ⟨[], h⟩
  | ⟨a :: v, h⟩ => return (List.Vector.cons (← f a) (← List.Vector.mapM f v))

The issue here is that List.Vector.cons creates a List.Vector of length Nat.succ n', which needs to match against n - intuitively we know that the length n in the cons case is non-zero and therefore unifies with some Nat.succ n', but cramming that knowledge/logic into this definition might get a bit unwieldy.

Any tips?

[Eric Wieser]

The tactic one looks fine to me

[Eric Wieser]

You could otherwise invoke casesOn directly without using cases, if you want to stay in term mode

[Eric Wieser]

I woner if something like docs#Array.size_mapM (but for List) is useful here

[Eric Wieser]

Maybe @Sebastian Graf can comment on whether mvcgen's machinery replaces SatisfiesM

[Jakub Nowak]

@Scott Buckley Matching on index parameters often helps.

import Mathlib

def List.Vector.mapM [Monad m] (f : α → m β) : {n : Nat} → List.Vector α n → m (List.Vector β n)
  | 0, ⟨[], h⟩ => pure ⟨[], h⟩
  | n + 1, ⟨a :: v, h⟩ => return (List.Vector.cons (← f a) (← List.Vector.mapM f ⟨v, by grind⟩))

[Scott Buckley]

@Jakub Nowak very nice! And Lean is clever enough here to not require the two invalid cases? very clever :)

[Jakub Nowak]

This is because the type of ⟨[], h⟩ is Vector α 0 and the type of ⟨a :: v, h⟩ is Vector α (Nat.succ n).
https://github.com/leanprover-community/mathlib4/blob/7478ffb26bdb1d28e594d5de3c49a170e30404cf/Mathlib/Data/Vector/Defs.lean#L44-L53