A few questions about contributing within `List.Vector`

Stream: general

[Scott Buckley]

As per a previous conversation #new members > MapM for List.Vector , I am building out a lot of the missing api for List.Vector. I plan to submit this as a PR, but I have a few questions about how best to approach this task.

The main things i'm implementing so far are definitions like mapM, mapIdx, mapFinIdx, mapFinIdxM, range', range, as well as lemmas about these utilities, for example mapM_append, range_append, get_mapFinIdx, etc.

Question 1: What to add
Finding which definitions to add seems easy, but knowing which lemmas to add seems tricky. List and Vector both have map and mapFinIdx, but they don't have the same utility lemmas proved for them. Right now i'm just taking a guess at what seems the most useful to have, but are there any more structured approaches to this I should take?

Question 2: How best to define things
Let's take mapFinIdx as an example. I could define this as essentially a lift of List.mapFinIdx, and then all of the associated lemmas would probably have the similar approach, relying on lemmas from about List.mapFinIdx. Alternatively, I could define mapFinIdx in terms of List.Vectors natively, and then prove this equivalent to a lifted version of List.mapFinIdx. The second approach is more fun, so it's what I'm doing first, but I wonder if the community has an opinion on which is better? Some example definitions below (in the List.Vector namespace):

-- `mapFinIdx` defined specifically for Vectors.
@[inline, expose] def mapFinIdx (as : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) : Vector β n :=
  match n, as with
  | 0, ⟨[], _⟩ => nil
  | i+1, ⟨a :: l, h⟩ => f 0 a (by omega) ::ᵥ mapFinIdx ⟨l, by simp_all⟩ (fun i a h ↦ f (i+1) a (by omega))

-- `mapFinIdx` defined using `List.mapFinIdx`
@[inline, expose] def mapFinIdx' (as : List.Vector α n) (f : (i : Nat) → α → (h : i < n) → β) : List.Vector β n :=
  match as with
  | ⟨l, h⟩ => ⟨l.mapFinIdx fun i a h ↦ f i a (by omega), (by simp [h])⟩

Question 3: How to annotate things
I have read through the mathlib style guidelines and i'm trying to stick to them. I have intuition about what should be added to simp and what shouldn't, but some documentation about this would also be helpful, if somebody could point me in the right direction. The same goes for things like grind, inline, etc.
Alternatively, should I just write it all up on my own and then sort these details out as part of the PR approval process?

A note on List.Vector
I know a few people will say that this is not useful work, as List.Vector may be deprecated, but it's a bit of fun for me to do this, and i'll still be happy to get a PR approved even if the work is later deleted.

A note on casting
There are some lemmas that seem obvious / important to have implemented for List.Vector. For example append_assoc:

abbrev cast_length {n m : Nat} (as : Vector α n) (h_eq : n = m) : Vector α m :=
  ⟨as.1, by simp only [length_val, h_eq]⟩

lemma append_assoc (as : Vector α n) (bs : Vector α m) (cs : Vector α k) :
    as ++ (bs ++ cs) = (as ++ bs ++ cs).cast_length (by omega) := by ...

This is a useful lemma, but can't really exist without some kind of casting. For now i'm using my own abbreviation cast_length that casts only the lengths of Vectors, it's a system that's working pretty well, but I'd definitely want to chat to somebody about it before including them in a PR.

Sorry for the long message, and thanks in advance for any advice :)

[Aaron Liu]

I really thought there would be an already existing cast function for List.Vector, like how we have docs#Fin.cast for Fin

[Yury G. Kudryashov]

It exists for docs#Vector

[Yury G. Kudryashov]

docs#Vector.append_assoc

[Yury G. Kudryashov]

Note that we're indeed trying to decide whether to deprecate List.Vector.

[Violeta Hernández]

Where is List.Vector currently used? And how hard is it to replace it within those files?

[Wrenna Robson]

I think this is nice work to do even if I think it'll be useless and it should be deprecated: it's good for your soul if nothing else to do this kind of thing.

[Jakub Nowak]

Yury G. Kudryashov said:

Note that we're indeed trying to decide whether to deprecate List.Vector.

You mean internally, or is there a discussion on Zulip I missed? Apart from #new members > MapM for List.Vector and #mathlib4 > Use `Vector` more?, but neither topic is about depreciation.

[Jakub Nowak]

Violeta Hernández said:

Where is List.Vector currently used? And how hard is it to replace it within those files?

It's not used much, just a few places. Vector is not used at all (I'm not counting implementations of tactics etc.)

[Jakub Nowak]

Scott Buckley said:

This is a useful lemma, but can't really exist without some kind of casting. For now i'm using my own abbreviation cast_length that casts only the lengths of Vectors.

There's List.Vector.congr. We might want to rename it to cast to be in-line with Vector.cast.

[cmlsharp]

Jakub Nowak said:

Violeta Hernández said:

Where is List.Vector currently used? And how hard is it to replace it within those files?

It's not used much, just a few places. Vector is not used at all (I'm not counting implementations of tactics etc.)

Vector is used in the implementation of Batteries.BinaryHeap (specifically the implementations of heapifyDown and heapifyUp)

[Jakub Nowak]

Ah, sorry, I only checked mathlib and forgot batteries.
I should specify, we should absolutely not replace Vector with List.Vector in implementations, because of performance. But we should keep using List.Vector and not Vector in proofs.

[cmlsharp]

In hindsight this might have made my verification PR of BinaryHeap somewhat easier. Because of the implementation of heapifyDown and heapifyUp, the wellformedness condition is specified in terms of Vector but it might have been easier if it had been specified in terms of List.Vector (were List.Vector available in Batteries of course)

[Scott Buckley]

Wrenna Robson said:

it's good for your soul if nothing else to do this kind of thing.

Yeah my thoughts exactly. It feels so good to write and prove all these simple (and occasionally slightly less simple) interconnected theorems.

[Scott Buckley]

Jakub Nowak said:

Scott Buckley said:

This is a useful lemma, but can't really exist without some kind of casting. For now i'm using my own abbreviation cast_length that casts only the lengths of Vectors.

There's List.Vector.congr. We might want to rename it to cast to be in-line with Vector.cast.

Thanks for pointing out List.Vector.congr, I hadn't seen that! I need to get better at searching for things like this.

About renaming to cast, would it make sense to just write cast in my fork, adjust congr to be marked as deprecated, and include that in the PR? Or would something like that be discussed here first? There's a similar issue with List.Vector.mmap which I think should be named mapM (although somebody suggested it should actually be mapA).

[Eric Wieser]

That sounds fine to just make as a PR

[Eric Wieser]

(perhaps a separate one for each)

[Peter Pfaffelhuber]

Please keep up your work on List.Vector. Recently, I work on a way to implement discrete probability. There, I exactly need List.Vector, since

• it is simple to do induction over List.Vector (not true for Vector, which should be avoided in proofs anyway, as far as I can tell);
• List.Vector α n is a Fintype, if α is a Fintype (not true for List);
• it has a Traversable instance, allowing to use sequence for mapping over a List.Vector. (Here, it is particular beneficial that the result knows about its own dimension in comparison with List, which leads to annoying trivial cases.)

[Wrenna Robson]

It could be simple to do proofs over Vector, and I do actually do it a lot.

[Wrenna Robson]

List.Vector doesn't particularly have an advantage over it in that sense.

[Jakub Nowak]

Wrenna Robson said:

List.Vector doesn't particularly have an advantage over it in that sense.

Yes, but exactly the same argument can be used to argument that one could use Array instead of List.

[Wrenna Robson]

Well, no, I think the fact that List is a relatively simple inductive type (which List.Vector is not!) does make it useful to work with.

[Wrenna Robson]

One could imagine a world in which List.Vector was defined as:

namespace List

inductive Vector (α : Type u) : ℕ → Type u
  | nil : Vector α 0
  | cons : α → Vector α n → Vector α (n + 1)

end List

[Wrenna Robson]

And actually... I would like this more honestly! That is the "honest" inductive definition of List.Vector.

[Wrenna Robson]

Then you add:

namespace Vector

def toList {n : Nat} : Vector α n → List α
  | nil => []
  | cons a l => a :: l.toList

def mk {n : Nat} : (l : List α) → l.length = n → Vector α n
  | [], h => h ▸ .nil
  | a :: l, h => h ▸ .cons a (mk l rfl)

end Vector

[Henrik Böving]

Wrenna Robson said:

And actually... I would like this more honestly! That is the "honest" inductive definition of List.Vector.

This definition is not chosen on purpose because it wastes memory compared to the subtype definition. And requires you to rebuild massive amounts of proofs.

[Wrenna Robson]

Array is fundamentally not constructed in the same way that List is - even though on a logical level it's a wrapper for List, List.cons is "fast" on lists and not on Arrays, but Arrays are faster in general (especially for arbitrary accesses).

[Wrenna Robson]

Henrik Böving said:

Wrenna Robson said:

And actually... I would like this more honestly! That is the "honest" inductive definition of List.Vector.

This definition is not chosen on purpose because it wastes memory compared to the subtype definition.

Right - what I don't understand is why we care about performance for List.Vector.

[Wrenna Robson]

I mean to be clear I think the definition of Vector is clearly the right one.

[Wrenna Robson]

But if we want to keep List.Vector - and honestly as I've said before I am not really a strong advocate for that - I think an implementation that exhibits the inductive construction would be better than one that prioritises performance.

[Henrik Böving]

Why would you not care about performance for such a simple type? It's also not very fun to rebuild all of the proof infrastructure that has been done for List from scratch. All of the lemmas from https://leanprover-community.github.io/mathlib4_docs/Init/Data/List.html would have to be reproven from scratch.

[Wrenna Robson]

Ah, you see, I would find that extremely fun :)

[Wrenna Robson]

I would argue that List.Vector already rebuilds a lot of proof infrastructure (I don't like that it exists).

[Wrenna Robson]

Why does List.Vector.inductionOn exist, for instance, if we would rather people use the proof infrastructure of List?

[Wrenna Robson]

I think it makes sense that Array exists and Vector exists though I do wish they had inductive principles - I accept the reasons they don't though.

[Wrenna Robson]

If the goal in Mathlib of List.Vector is to be "the Vector you do proofs on", I would argue you should choose the definition for proof reasons (and I like the inductive definition better for that) and not for performance reasons.

[Henrik Böving]

Wrenna Robson said:

Why does List.Vector.inductionOn exist, for instance, if we would rather people use the proof infrastructure of List?

We want people to use the proof infrastructure for list to build a minimal layer that exposes the proof infrastructure of List + length assumptions instead of having to go through all of the list nonsense again. The end goal of List.Vector as a data type is of course not that people still rely on the List API most of the time, the question is how the Vector API is built and that is simply easier with all that we have for lists already. There is about 16k LoC in Init.Data.List, nobody should have to replicate this for an invariant as trivial as "the list has a certain length"

[Wrenna Robson]

Mmm - honestly I was not really clear on the purpose of List.Vector (as opposed to Vector).

[Wrenna Robson]

Given the file that defines it suggests it could be deprecated I wouldn't say that Mathlib defines it very strongly currently. But I agree - nobody should have to replicate that.

[Wrenna Robson]

(You mention the Vector API but to be clear I am not talking about Vector but List.Vector - I think this is what you meant, though the List.Vector API is sorely in need of updates.)

[Jakub Nowak]

Why is it ok to replicate List API for Array and Vector, but not for List.Vector? Is it just because the former two are more commonly used, so it's worth the effort?

[Henrik Böving]

Neither Array or Vector rebuild the List API. Array functions behave usually quite differently from their respective List friends so it is not possible to just reuse the lemmas that we have proven about say List.foldl to do proofs about Array.foldl. On the other hand doing proofs about Vector by just using the Array API is easy so the Vector API is built upon the Array API without doing massive amounts of proofs on their own again. You do of course want to replicate the available API surface, the thing you do not want to replicate is the proofs which are almost all trivial in the respective Vector versions. When you go from a subtype to an inductive encoding of List.Vector you suddenly do have to do all proofs from scratch though

[Jakub Nowak]

I don't think you would have to do all proofs from scratch. You only need extensionality and proofs that the definitions coincide, so theorems like List.Vector.foldl f x v = List.foldl f x v.toList or List.Vector.reverse v |>.toList = List.reverse v.toList. And you can than reuse proofs from List API by rewriting with these equalities.

[Peter Pfaffelhuber]

Currently, and as I said above, I am working with List.Vector since I find most tools that I need. (It is a Traversable, has an induction principle, is a Fintype, etc.) I wonder why List.Vector.count {n : ℕ} (a : α) : (l : List.Vector α n) → Fin (n + 1) does not exist. (Also Vector.count maps to ℕ, which I do not understand. Wouldn't it be better to e.g. know that count maps to a Fintype?

def List.Vector.count [BEq α] {n : ℕ} (a : α) : (l : List.Vector α n) → Fin (n + 1) := fun l ↦
  ⟨l.val.count a, lt_of_le_of_lt l.val.count_le_length (lt_of_le_of_lt l.prop.le (lt_add_one n))⟩

[Jakub Nowak]

For symmetry with Vector we probably want List.Vector.count map to Nat. But we can consider adding Vector.countFin and List.Vector.countFin.