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
append vec padding.
```

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] *)
pad 4 [false].
(* [false; false; false; false] *)
```

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…

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.

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.

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

Last updated: Oct 13 2024 at 01:02 UTC