Hello,

I am trying to define a simple function that, given a vector of integers, returns a new vector with the same values and as many zeros at the end as elements the given vector contains. My problem comes from the fact that the return type of the vector (t Z 2*n) where n is the number of elements of the first vector, is a parameter, and Coq doesn't seem to be able to reason that 2*0 equals 0. Here is my code:

```
Fixpoint add_zeros {n_var} : t Z n_var -> t Z (2*n_var) :=
match n_var with
| 0%nat => fun _ => []
| S n_var' => fun v => (hd v) :: (add_zeros (tl v)) ++ [0]
end.
```

The error that arises is:

```
Error:
In environment
add_zeros : forall n_var : nat, Vector.t Z n_var -> Vector.t Z (2 * n_var)
n_var : nat
t : t Z ?n@{n0:=0}
The term "[]" has type "Vector.t Z 0" while it is expected to have type
"Vector.t Z (2 * ?n0@{n0:=0})".
```

Hope you can give a hand. Thanks in advance.

Are you using vector because you want to have fun struggling with dependent elimination or just because you want fixed-size lists? (i.e. have you read the comment on top of https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v )

Last updated: Oct 08 2024 at 14:01 UTC