Zulip Chat Archive

Stream: new members

Topic: Non zero length vector


view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Dec 16 2019 at 07:48):

What definition of vector do you use?

view this post on Zulip 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

view this post on Zulip YH (Dec 16 2019 at 07:52):

The definition in mathlib is like

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

view this post on Zulip YH (Dec 16 2019 at 07:53):

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

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 08:51):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 16 2019 at 11:31):

We have both approaches.

view this post on Zulip 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