The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

I want to state (and prove) a lemma that conversion of
lists to vectors commutes with mapping.

Hence my lemma should look something like this:

Lemma vmap_map: forall  {A B}{f : A -> B}{ l: list A},
Vector.map f (Vector.of_list l) = Vector.of_list (map f l).

This lemma is not accepted by Coq because:

> The term "Vector.of_list (map f l)" has type "Vector.t B (length (map
f l))"
> while it is expected to have type "Vector.t B (length l)".

There's a lemma in the standard library, which proves the required
equality, namely map_length:

map_length
     : forall (A B : Type) (f : A -> B) (l : list A),
       length (map f l) = length l

But how can I tell Coq that it should accept my lemma due to map_length?

One thing I tried was to reformulate the lemma using an explicit auxiliary
congruence lemma:

Lemma eq_cong: forall {A} {x : A} {y : A} P, x = y -> P x -> P y.

With this auxiliary Lemma, I can reformulate map_vmap in such a way
that Coq accepts the lemma:

Lemma vmap_map: forall  {A B}{f : A -> B}{ v: list A},
Vector.map f (Vector.of_list v) = eq_cong (Vector.t B) (map_length f v)
(Vector.of_list (map f v)).

However, it's no longer the same lemma, and it's awkward to use.

Presumably I'm missing something very obvious, but I'd be grateful for
suggestions.

Klaus