The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear all,

If one has constructors that are like "nil" and "cons" one can build
something that is like lists. This can be made more precise. A
generalized list is

Record list_type (A: Type): Type
:= mk_list_type
   { LT: Type;
     list_nil: LT;
     list_cons: A -> LT -> LT;
     list_cons_injective:
        forall a a': A,
        forall l l': LT,
        list_cons a l = list_cons a' l' ->
        (a = a' /\ l = l');
     list_cons_discrimination:
        forall a: A,
        forall l: LT,
        list_nil <> list_cons a l;
     list_induction:
        forall P: LT -> Type,
        P list_nil ->
        (forall a: A, forall l: LT, P l -> P (list_cons a l)) ->
        forall l: LT,
        P l
   }.

Once I wrote a forall_list predicate. It looked like

Inductive forall_list (A: Type) (P: A -> Type)
   : list A -> Type
   := | forall_nil: forall_list P nil
      | forall_cons:
           forall a: A,
           forall l: list A,
           P a ->
           forall_list P l ->
              forall_list P (a :: l).

A nice thing to have, really. It can also be written for the
generalized lists given above as

Inductive forall_list_type (A: Type) (L: list_type A) (P: A -> Type):
LT L -> Type
:= | forall_type_nil:
        forall_list_type L P (list_nil L)
   | forall_type_cons:
        forall a: A,
        forall l: LT L,
        P a ->
        forall_list_type L P l ->
        forall_list_type L P ((list_cons L) a l).

The standard library provides the nice function "map". Also that can
be generalized into

Definition map_list_type (A: Type) (B: Type) (ltA: list_type A) (ltB:
list_type B)
      (f: A -> B):
   LT ltA -> LT ltB
:= list_induction
      ltA
      (fun l: LT ltA => LT ltB)
      (list_nil ltB)
      (fun a: A =>
       fun tailA: LT ltA =>
       fun tailB: LT ltB =>
       (list_cons ltB) (f a) tailB).

It seems writing records like list_type is about the same as writing
Modules. Moreover, they are first class citizens in the Coq language,
being Inductives with some extra destructor names for convenience. So,
why was the basic Coq language polluted with the seemingly useless
concept of modules?

All the best,
Chris