Lists and vector basics

Stream: mathlib4

[Robert]

Hey! So I can't figure out how to create a vector in Mathlib, is it just this?

![1, 2,3]

```quote
structure test (n: ℕ) where
x: Vector Float n

def test1: test (2) := {x:= ![1.2,2.3]

but then i get the error saying type mismatch ![1.2, 2.3] has type Fin (Nat.succ 0).succ → ?m.1099 : Type ?u.1098 but is expected to have type Mathlib.Vector Float 2 : Type

im so confused, the documentation is so unclear about data structures, if i work with lists above and change it to say x: List Float and make everything dynamic then it all works, but then I dont know how to compute the dot product between two lists , cause Matrix.dotProduct takes in two vectors, and so I tried converting the list into a vector but it got some error as well.

so just a general question, is it better to use lists or vectors? if so lists are better how does one compute the dot product between the lists or convert lists into vectors so i can use the vector operations directly in lean? also why doesn't this work,

def x1 := [1, 2]

def x2 := [3, 4]

def x3 := ∑ i in [0, 1], x1[i] * x2[i]```

this gives me application type mismatch Finset.sum [0, 1] argument [0, 1] has type List ?m.445 : Type ?u.364 but is expected to have type Finset ?m.365 : Type ?u.364

im so confused, i would assume straightforward computations like this would be relatively easy in Lean. Sorry for too many questions, its just hard to get even basic lists or vectors working without so many issues: ( i wish the documentation or textbook had more info on just data structures and how to use them

[Matt Diamond]

Could you provide a #mwe? The formatting in your comment is messed up which makes it hard to understand what you're asking.

[Matt Diamond]

I would recommend reading through this page if you haven't already: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fin/VecNotation.html

[Matt Diamond]

I think part of your confusion is coming from the assumption that vector math is done with the Mathlib.Vector type... that's not the right type in this context

[Matt Diamond]

they're represented by functions from indices to values

[Matt Diamond]

import Mathlib

open Matrix

#check (![1,2,3] : Fin 3 → ℕ)

#eval ![1,2,3] ⬝ᵥ ![4,5,6]

[Robert]

Matt Diamond
sure here is a mwe

structure test (n: ℕ) where
x: Mathlib.Vector Float n

def test1: test (2) := {x:= ![1.2,2.3]}

but then i get the error saying type mismatch
![1.2, 2.3]
has type
Fin (Nat.succ 0).succ → ?m.1099 : Type ?u.1098
but is expected to have type
Mathlib.Vector Float 2 : Type

so not sure how to even create a new vector and also is there a way to convert a list into a vector cause its easier to work with lists, but then i don't know how to properly compute the dot product. I did this and it worked but is it the best way

def product_list (v w: List Float):=
  (List.zipWith (· * ·) v w).foldl (· + ·) 0
``` and this worked well.

[Matt Diamond]

Don't use Mathlib.Vector, that's not the right type

[Matt Diamond]

import Mathlib

structure test (n: ℕ) where
  x : Fin n → Float

def test1: test (2) := {x:= ![1.2,2.3]}

[Matt Diamond]

If you look at my earlier example above, I showed how you could compute the dot product using the ⬝ᵥ operator

[Robert]

Oh thanks Matt, I see now,! Also for computations i would assume its more efficient to use vectors compared to lists? also i see that you can convert a vector into a list but i assume the other way is not possible as vectors are fixed size and lists are dynamic correct? cause if i could convert a list into a vector for efficiency that would be great cause then i can do the dot product etc and use other operations with vectors.

[Matt Diamond]

In theory you could convert a single-dimensional array to a vector using docs#List.get, but why do you find it easier to work with lists?

[Matt Diamond]

There are functions that allow you to manipulate vectors in much the same way that you would manipulate lists

[Kim Morrison]

Note that there are two different versions of Vector: Mathlib.Vector, which is based on List, and Batteries.Vector (soon to be just Vector) which is based on Array.

If you're actually doing computations you should surely be using the Array backed version.

[Kim Morrison]

I'd suggest we actually rename Mathlib.Vector to Mathlib.ListWithLength, but I'm not putting my hand up. :-)

[Robert]

Oh thanks Matt! Oh it just was easier to follow and create/do operations with list compared to the vectors (im still learning and found lists to be easier to work with), plus i wasnt sure how to use vectors properly. but i will try to move to using vectors.

[Robert]

oh @Kim Morrison why is that i should use the array backed version? is the syntax the same as what Matt wrote before ie Fin n -> Float? or is it different

[Robert]

also is there documentation like a paper or some guide for it? I came across batteries and it seems to be mainly focussed on data structures, is that correct?

[Robert]

Thanks for all your help!

[Eric Wieser]

Kim Morrison said:

If you're actually doing computations you should surely be using the Array backed version.

In theory you can use this at the same time as the abstract version Matt describes, as

import Mathlib

def myDotProduct (x y : Batteries.Vector Rat 3) : Rat :=
  Matrix.dotProduct x.get y.get  -- this works on the `Fin _ → _`-style vectors

#eval myDotProduct ⟨#[1, 2, 3], rfl⟩ ⟨#[4, 5, 6], rfl⟩

[Eric Wieser]

(unfortunately this doesn't work on Float because addition is not associative, and so the order that you do the summation matters!)

[Robert]

I see that makes sense! Thanks, ill just stick to lists for now then, unless I need to change to vectors

[Kim Morrison]

Robert said:

oh Kim Morrison why is that i should use the array backed version? is the syntax the same as what Matt wrote before ie Fin n -> Float? or is it different

If you're doing proofs, then Fin n → X is surely going to be best. If you're programming, then Vector will be best. If you're doing both, then you'll need to convert!