[Agda] vs++[]==vs for vectors

[Kenichi Asai]

Dear all,

I want to prove that vs ++ [] == vs for a vector vs of length n.
Simply writing this statement results in a type error, because the
left-hand side has type Vec N (n + 0) while the right-hand side
Vec N n. The problem is similar to the associativity of vector append
that I asked years ago:

https://lists.chalmers.se/pipermail/agda/2014/007282.html

This time, I am trying to prove it using subst found in
Relation.Binary.PropositionalEquality, and formulated the statement as:

subst (Vec N) (+-right-identity n) (vs ++ []) == vs

But I could not prove it. How can I prove it? It seems I don't
understand how I can pattern match on (+-right-identity n), so that
subst is unfolded.

Thanks in advance.

Sincerely,

[Roman]

Hi Kenichi,

see https://lists.chalmers.se/pipermail/agda/2016/009069.html for how
associativity of vectors (and `vs ++ [] == vs` as well) can be proven
without the need for `subst` or `rewrite`.