I've defined a type family `vec`

which is essentially a `list`

that carries its length around with it:

```
Inductive vec: Type -> nat -> Type :=
| vnil : forall (A:Type), vec A 0
| vcons : forall (A:Type) (n:nat) (a:A) (v: vec A n), vec A (S n).
```

I've also defined functions

```
inject {A:Type}(ls: list A) : vec A (length ls)
unject {A:Type}{n: nat} : vec A n -> list A
```

going back and forth between these two representations.

Now, I want to prove

```
Theorem inject_inverse2 : forall (A:Type) (n:nat) (ls: vec A n),
inject A (unject A n ls) = ls.
```

but this won't typecheck - Coq complains that `ls`

has type `vec A n`

, while it is expected to have type `vec A (length (unject A n ls))`

.

I can prove

```
Theorem inject_inverse2a : forall (A:Type) (n:nat) (ls: vec A n),
length (unject A n ls) = n.
```

Now, does it follow from `inject_inverse2a`

that `vec A n = vec A (length (unject A n ls))`

? If so, how can I use this in the statement of `inject_inverse2`

? If not, is it possible to prove `inject_inverse2`

?

One pointer would be CPDT, chapter http://adam.chlipala.net/cpdt/html/Equality.html , starting from "Type-Casts in Theorem Statements"

note that the other equation, `unject .. (inject ..) = ls`

is more easily stated, so if it is possible/useful to talk about lists instead, that would make things easier

Or look at https://stackoverflow.com/questions/63017478/some-help-dealing-with-inject-unject-and-vector-types

Last updated: Oct 03 2023 at 04:02 UTC