Use `Vector` more?

Stream: mathlib4

[Yury G. Kudryashov]

Should we use Vector instead of Fin n -> X in more cases? E.g., for matrices?

[Yury G. Kudryashov]

The downside is that we can't use index types other than Fin n, so this may be a bad idea for proofs, even though it's good for computation.

[Weiyi Wang]

Such a coincidence that I was just refactoring my own code to replace Fin n -> X with Vector to get better computability. Though I am not sure about Mathlib itself. I think I still see it mainly as a library for proofs so I probably prefer keeping Fin n -> X? As long as there are enough API to convert between these

[Weiyi Wang]

btw I just discovered there is no AddMonoid (Vector _ _) even though there is Add (Vector _ _)

[Weiyi Wang]

There is Lean.Grind.AddCommMonoid (Vector α n) though :melting_face:

[Jakub Nowak]

Maybe we should have a VectorLike class so that the user can choose whether they want Fin n -> X or Vector n?

[Wrenna Robson]

A related point: in some places we use the "Tuple" namespace, but we don't actually define "Tuple" anywhere. I think we could do worse than at the very least defining "Tuple A n" as an abbreviation for Fin n -> A.

[Wrenna Robson]

Don't forget we also have List.Vector in mathlib. I wish we didn't, but we do.

[Wrenna Robson]

Having had a good deal of experience with this sort of thing, I do think you want to keep Fin n -> A as that is often a much nicer and natural way to state things (whether under the Fin name or otherwise).

[Wrenna Robson]

I assume when people talk about computability, they don't mean computability so much as performance (Fin n -> A is perfectly computable, it just sometimes has bad performance).

[Wrenna Robson]

(Perhaps more accurately because it is a function Lean does just treat it differently to a Vector which is kind of more of a static block object.)

[Wrenna Robson]

It can especially be useful to use Fin n -> A when using Equiv, I find.

[Yury G. Kudryashov]

Wrenna Robson said:

I assume when people talk about computability, they don't mean computability so much as performance (Fin n -> A is perfectly computable, it just sometimes has bad performance).

When I said that Vector is good for computation, I meant performance.

[Yury G. Kudryashov]

Wrenna Robson said:

Don't forget we also have List.Vector in mathlib. I wish we didn't, but we do.

IMHO, we should deprecate it.

[Wrenna Robson]

Yury G. Kudryashov said:

Wrenna Robson said:

Don't forget we also have List.Vector in mathlib. I wish we didn't, but we do.

IMHO, we should deprecate it.

I strongly agree but I do not have the energy or the community clout to make it happen.

[Wrenna Robson]

Yury G. Kudryashov said:

When I said that Vector is good for computation, I meant performance.

[Wrenna Robson]

Yeah I figured you did.

[Eric Wieser]

What's the argument for dropping List.Vector?

[Yury G. Kudryashov]

Mathematically, it's the same as Vector, which is in core. If there are computational reasons to have it, then IMHO it belongs in CSLib, not Mathlib.

[Eric Wieser]

Couldn't the same argument be used to say that List shouldn't exist, only Array should?

[Yury G. Kudryashov]

The main difference is that List already has lots of API & uses in Mathlib.

[Yury G. Kudryashov]

Also, pattern matching defs are nice.

[Eric Wieser]

I guess I'd claim that the pattern matching argument applies to List.Vector too

[Yury G. Kudryashov]

My opinion is that

• we should choose one of List/Array for Mathlib;
• we should choose one of List.Vector/Vector for Mathlib;
• the choices don't have to match;
• I may prefer Array/Vector, but this may be a side effect of me writing some code in Lean as a programming language.

[Robin Carlier]

I would be very sad if List gets out of Mathlib: I think almost every formalization project that I have or had use them and their API quite extensively in a way or an other.

[Eric Wieser]

On your last point, is this because you've tried to verify your Array code and found that results you need are stated about List instead?

[Eric Wieser]

Or just because the Array APi is more in your muscle memory?

[Yury G. Kudryashov]

It's because I've started caring more about performance since I've started writing code in Lean.

[Yury G. Kudryashov]

But I with Mathlib hat on understand that this may not be what we want for proofs in Mathlib, so if there is a vote, then I'm going to abstain.

[Yury G. Kudryashov]

E.g., I think that some of our code that uses Finsets would become faster if we used Arrays. Also, if we had a way to override DecidableEq on Finsets for LinearOrders to just sort both sides and compare...

[Yury G. Kudryashov]

UPD: I meant, on Multisets. We can speedup it on Finsets by using something like s = t \iff s.card = t.card \and s \sub t instead of relying on List.isPerm.
UPD2: the current algorithm is not much worse. It takes elements from LHS one by one, verifies that they're there in the RHS and removes them from there. At least, it runs in a polynomial time.

[Yury G. Kudryashov]

Note: it looks like I don't understand something important about performance in Lean. I've tried to write List.offDiag with lists and arrays, and the array version turned out to be slower.

[Lua Viana Reis]

I think some methods like Array.eraseIdx are worse than the List version because the List version only has to change a single pointer, while for Array it needs to move all the next ones

[Yury G. Kudryashov]

I tried to use Array.ofFn and failed.

[Yury G. Kudryashov]

This is a definition for List:

/-- List.offDiag l` is the product `l.product l` with the diagonal removed. -/
def List.offDiag {α} (l : List α) : List (α × α) :=
  l.zipIdx.flatMap fun (x, n) ↦ map (Prod.mk x) <| l.eraseIdx n

A similar definition for Arrays is ~2x worse on List.range 5000, while this one is ~4x worse:

def offDiag (l : Array α) : Array (α × α) :=
  (l.mapIdx fun i x => l.mapIdx fun j y ↦ if i = j then none else some (x, y)).flatten.reduceOption

[Shreyas Srinivas]

Yury G. Kudryashov said:

E.g., I think that some of our code that uses Finsets would become faster if we used Arrays. Also, if we had a way to override DecidableEq on Finsets for LinearOrders to just sort both sides and compare...

You want a map to bitvec and back for finsets rather than arrays

[Shreyas Srinivas]

Arrays don't guarantee Nodup, and I know a few problems where combining some lean formalisation work with some bv_decide calls might lead to interesting results (despite its downside of expanding the trusted code base).

[Lua Viana Reis]

I think Array.flatten has a similar problem, List.flatMap only needs to update the pointer at the end of each list in the list, while Array.flatten has to copy/resize a lot of data

[Lua Viana Reis]

@Yury G. Kudryashov how can I test this? #eval (List.range 257).offDiag crashes the Lean server for me

perhaps

def offDiag' (l : Array α) : Array (α × α) := Id.run do
  let mut s : Array (α × α) := Array.emptyWithCapacity (l.size * (l.size - 1))
  for x in l, i in [:l.size] do
    for y in l, j in [:l.size] do
      if i != j then
        s := s.push (x,y)
  return s

is more performant but I cannot test

[Yury G. Kudryashov]

I've tested with #eval (List.range 5000).offDiag.length so that it doesn't have to pretty print a long list.

[Lua Viana Reis]

(deleted)

[Yury G. Kudryashov]

Can we please stop discussing matrix-free definitions in this thread? I'm totally fine with this discussion happening in another thread, but it's offtopic for this one.

[Kevin Buzzard]

(moving them) (edit: done. Sorry for contributing to the noise. Now back to your scheduled programming)

[Violeta Hernández]

Sorry, back to topic. What are the places where List.Vector is currently used, and how reasonable would it be to remove it from them?

[Ruben Van de Velde]

Loogle finds a handful of places: Mathlib.Data.Sym.Basic, Mathlib.GroupTheory.Perm.Cycle.Type, Mathlib.Computability.Primrec

[Jakub Nowak]

IMO we should prefer List.Vector over Vector in mathlib, just like we prefer List over Array. The only downside is that List.Vector API is underdeveloped.