The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Patricia,

If you slightly modify your definition of List to highlight
the fact that the type of the elements is a parameter,
List_rect is less general and map is then easy to write.

================================

Inductive List (A:Type) : Type :=
  | nil : List A
  | cons : forall (a:A)(l:(List A)),List A.

Check List_rect.

(*
List_rect
     : forall (A : Type) (P : List A -> Type),
       P (nil A) ->
       (forall (a : A) (l : List A), P l -> P (cons A a l)) ->
       forall l : List A, P l
*)

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

================================

Cheers,

--
guillaume



On 7 April 2012 18:00, Patricia Peratto 
<psperatto AT adinet.com.uy>
 wrote:
> Hello, I have defined the list inductive set in the following way:
>
> Inductive List :forall(A:Type),Type :=
> |nil : forall(A:Type),List A
> |cons :forall(A:Type)(a:A)(l:(List A)),List A.
>
> The corresponding recursive operator is
>
> List_rect : forall P: forall A:Type, List A -> Type,
>             (forall A:Type, P A (nil A)) ->
>             (forall (A:Type) (a:A)(l:List A), P A l -> P A (cons A a l)) ->
>             forall (A:Type)(l:List A), P A l
>
> I want to define the function map using List_rect and with
> the type that I show below:
>
> Definition map : forall (A B:Type)(F:A->B)
> (l:List A), List B :- ............
>
> I have tried different ways but I couldn´t define it.
>
> Can someone help me with this definition?
>
> Regards,
> Patricia Peratto