Julin S (Nov 26 2021 at 05:55): 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
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…
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