Stream: Coq users

Topic: Problem reasoning with the return type of a vector function

view this post on Zulip Pablo (Apr 22 2024 at 14:56):

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 2n) 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 20 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.

view this post on Zulip Pierre Roux (Apr 22 2024 at 14:59):

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