The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 7 Apr 2012 17:42:39 -0700,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> If, for some reason, you can't recast the inductive definition, you
> could also use the following:
> 
> Definition map {A B:Type} (f:A->B) (l:List A) : List B :=
> List_rect (fun A' _ => A = A' -> List B)
>   (fun _ _ => nil B)
>   (fun A' (a:A') (l':List A') (recval: A=A' -> List B)
>      (e: A = A') =>
>    cons B
>      (f (match e in (_ = T) return (T -> A) with
>          | eq_refl => fun a' => a'
>          end a))
>      (recval e))
>   A l (eq_refl A).
> 
> The fundamental idea here is that P A' l reduces to "A = A' -> List
> B", and then you use the equality hypothesis to cast a from type A' to
> A.
> 
> As you can probably see, rewriting the inductive definition as
> guillaume suggested is much simpler...

In fact there is more simple than using the eq type:

Definition map : forall (A B:Type)(F:A->B) (l:List A), List B.
intros.
revert F.
refine (List_rect (fun A0 _ => (A0 -> B) -> List B) _ _ A l).
intros _ _.
left.
intros.
right.
now apply X0.
now apply X.
Defined.
Print map.

Gives this definition of map:

Definition map (A B : Type) (F : A -> B) (l : List A) : List B :=
List_rect
  (fun A0 _ => (A0 -> B) -> List B)
  (fun _ _ => nil B)
  (fun A0 a _ (Rec : (A0 -> B) -> List B) f => cons B (f a) (Rec f))
  A
  l
  F.

You can even write this function as:
Definition map (A B : Type) (F : A -> B) (l : List A) : List B :=
List_rect _ (fun _ _ => nil _)
            (fun _ a _ Rec f => cons _ (f a) (Rec f))
            _ l F.
if you want to be concise.

The trick here is to pass the F function into the recursive calls (as f
here).
But of course gallais answer is still better ^^