The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 27/04/2015 12:44, Matej Kosik wrote:

> I can work with those values normally.
> E.g.:
>
>         Definition is_empty (A:Type) (l : list1 A) :=
>           match l with
>           | nil1 _ => true
>           | cons1 _ _ _ => false
>           end.
>
>         Compute is_empty nat (nil1 nat).
>         Compute is_empty nat (cons1 nat 5 (nil1 nat)).
>
>
> I am curious, why is "list1" as defined above inferior to "list" as it 
> appears in the standard library?

That is because you chose a function that is way too simple. Try instead 
to define a function of type (list1 A -> option A). You can no longer do 
a simple match, you have to use type-dependent pattern-matching.

Definition head {A} (l : list1 A) : option A :=
  match l in list1 H return option H with
  | nil1 _ => None
  | cons1 _ h _ => Some h
  end.

Even worse, try to define the map function. The f function can no longer 
be applied to the head element of your list because it does not have the 
correct type, a priori. This forces you to write the following code.

Fixpoint map {A B} (f : A -> B) (l : list1 A) : list1 B :=
  match l in list1 H return (H -> B) -> list1 B with
  | nil1 _ => fun _ => nil1 _
  | cons1 _ h t => fun f => cons1 _ (f h) (map f t)
  end f.

Best regards,

Guillaume