## Stream: Coq users

### Topic: Letting coq know that 2 `Vector.t` types are same

#### Julin S (Nov 26 2021 at 05:55):

I was trying to make a function that would make an argument `Vector.t bool` to be of a specific length by 'padding' the required `false` values at the end of it.

So I tried:

``````Definition pad {n : nat} (size : nat) (vec : Vector.t bool n) : Vector.t bool size :=
let padding := Vector.const false (size - n) in
``````

where `size` is the size of the (padded) return value and `n` is the length of the input vector `vec`.

But I got an error saying

``````In environment
n : nat
size : nat
vec : t bool n
padding := const false (size - n) : t bool (size - n)
The term "vec ++ padding" has type "t bool (n + (size - n))"
while it is expected to have type "t bool size".
``````

It seems that we need a way to let coq know that `t bool (n + (size - n))` is same as `t bool size`. How can we do that?

What I was aiming at was something like:

``````pad 5 [true; true].
(* [true; true; false; false; false] *)

(* [false; false; false; false] *)
``````

#### Meven Lennon-Bertrand (Nov 26 2021 at 09:46):

In general for natural numbers it is not true that `n + (m - n) = m`, because if `n` is larger than `m` the subtraction is equal to `0` and does not cancel. In your case, if `n` is larger than `size`, you cannot make `vec` of size `size` by padding, because it is too large…

#### Meven Lennon-Bertrand (Nov 26 2021 at 09:51):

But setting this aside, if you have a vector of a given length and want to get another one of a length that is only propositionally equal (as in your example), you will need some kind of equational reasoning, but how to set this up depends wildly on the use for your function, I think.

#### Meven Lennon-Bertrand (Nov 26 2021 at 09:54):

An "easy" way out would be to define a general function `cast {A m n} (m = n) : Vector.t A m -> Vector.t A n` and use it in your definition, but this might prove annoying if you want to compute.

#### Paolo Giarrusso (Nov 26 2021 at 10:49):

If you want to compute, math-comp's tuple n is better - basically, { l : list A | length A = n }

Last updated: Oct 03 2023 at 21:01 UTC