Using vectors in Coq

Using Coq
1

Hi all, I’m kind of new to using vectors in Coq and trying to understand things.
I want to use vectors that contain multiple lists of nat, for eg I want Vnat to be a vector that contains 1 list of nat [1;2]:
Definition Vnat := Vector.cons (list nat) [1;2] 1.
The previous definition works, but a Print outputs:
Vnat = Vector.cons (list nat) [1;2] 1
: t (list nat) 1 → t (list nat) 2
When I want to see: t (list nat) 1.
Can you help me understand better this constructor and how to achieve what I want.
Thanks

2

What you want is the following:

Definition Vnat := Vector.cons (list nat) [1;2] 0 (Vector.nil _).
Check Vnat.
(* 
   Vnat : t (list nat) 1
*)
1 Like
3

Yes, exactly what I want, thank you :slight_smile:

My next step is to use a parameter n that represents the size of the vector, for example with n=2, the definition would be this way (if I’m correct):
Definition Vnat2 := Vector.cons (list nat) [1;2] 1 (Vector.cons (list nat) [1;2] 0 (Vector.nil _)).
Is there a more general way to get a vector of n elements directly, because using this previous method means I need to know n before constructing the vector.

Thanks again !

4

You can take full advantage of the type inference mechanism by leaving _ holes behind:

Definition Vnat2 := Vector.cons _ [1;2] _ (Vector.cons _ [1;2] _ (Vector.nil _)).

5

The inference is really helpful when I know the Vector size, but if it is some unknown parameter n, I will have to construct the vector with Vector.cons called n-1 times.

For example:
Definition n := 2.
Definition Vnat2 := Vector.cons _ [1;2] (n-1) (Vector.cons _ [1;2] _ (Vector.nil _)).
This works, but if I happen to change the value of n, Vnat2 will no longer fit.

Isn’t there a way to do it more directly, through a function maybe?

6
7

This would do the trick if I wanted a vector that only contains constants “a” of some type A but my elements are different from each other :frowning: