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):

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