Non zero length vector

Stream: new members

[Mukesh Tiwari]

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]

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

[Simon Hudon]

What definition of vector do you use?

[Simon Hudon]

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]

The definition in mathlib is like

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

[YH]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mukesh Tiwari]

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]

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]

We have both approaches.

[Kevin Buzzard]

The other is called vector3 for some reason.