## Stream: new members

### Topic: Non zero length vector

#### Mukesh Tiwari (Dec 16 2019 at 05:25):

def prod {F G : Type}(f : F → G → G) (g : G → G → G):
Π {n : ℕ},
vector G (n + 1) →
vector F (n + 1) → G
| .(0) (h :: _) (m :: _) :=  f m h
| .(n + 1)(vector.cons h hs) (vector.cons m ms) :=
g (f m h) (prod hs ms)


#### Mukesh Tiwari (Dec 16 2019 at 05:26):

Could some one please tell me what to change in this code to let Lean accept this definition?

#### Simon Hudon (Dec 16 2019 at 07:48):

What definition of vector do you use?

#### Simon Hudon (Dec 16 2019 at 07:50):

This works for me:

namespace hidden

inductive vector (α : Type) : ℕ → Type
| nil {} : vector 0
| cons {n} : α → vector n → vector (n+1)

def prod {F G : Type}(f : F → G → G) (g : G → G → G):
Π {n : ℕ},
vector G (n + 1) →
vector F (n + 1) → G
| (0) (vector.cons h hs) (vector.cons m ms) :=  f m h
| (n + 1)(vector.cons h hs) (vector.cons m ms) :=
g (f m h) (prod hs ms)

end hidden


#### YH (Dec 16 2019 at 07:52):

The definition in mathlib is like

def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n }


#### YH (Dec 16 2019 at 07:53):

I was wondering why this was the choice of vector earlier today. Still curious.

#### Kevin Buzzard (Dec 16 2019 at 08:51):

I think that mathlib somewhere has the recursive definition. Is it vector2 or vector3 or something?

#### Kevin Buzzard (Dec 16 2019 at 08:53):

There's also a recursive definition of fin somewhere. I guess the definition of vector is in core Lean not mathlib, so there's not much we can do about it.

#### Kevin Buzzard (Dec 16 2019 at 08:54):

vector3 seems to be in number_theory/dioph of all places, and uses fin2 from the same file.

#### Mukesh Tiwari (Dec 16 2019 at 11:10):

What definition of vector do you use?

Thanks for reply @Simon Hudon . Long time and nice to see your message :).
I have import bunch of libraries, and I do not know which one is importing the vector
import data.fintype data.nat.basic
data.zmod.basic algebra.group_power
tactic.omega

#### Mukesh Tiwari (Dec 16 2019 at 11:28):

The definition in mathlib is like

def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n }




If I understood this data type (it is a pair where the first one is list and second one is the length of list), then I can answer you from Coq perspective. In Coq, it is very difficult to work with length indexed vector datatype, so sometimes people encode the vectors in this way. This encoding makes life easier when dealing with vectors, but I am not sure why some one would adopt this approach for Lean.

#### Kevin Buzzard (Dec 16 2019 at 11:31):

We have both approaches.

#### Kevin Buzzard (Dec 16 2019 at 11:31):

The other is called vector3 for some reason.

Last updated: May 12 2021 at 04:19 UTC