## Stream: Coq users

### Topic: Showing two types are equal inside theorem definition

#### Jordan Mitchell Barrett (May 11 2021 at 04:25):

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`?

#### Fabian Kunze (May 11 2021 at 08:01):

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

#### Fabian Kunze (May 11 2021 at 08:05):

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

#### Fabian Kunze (May 11 2021 at 08:07):

Last updated: Oct 03 2023 at 04:02 UTC