The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Ups... sorry for the malformed post. It should read:
--------------

(*

   Dear list,

  I'm working with heterogenous lists, as defined in Adam Chlipala's 

book CPDT. I'd like to define a function that takes a list of lists

[xs_1; ... xs_n] and produces a list containing all the lists of

the form [x_1; ... x_n] where [In x_1 xs_1 /\ ... /\ In x_n xs_n].

  For 'regular' lists this function can be straightforwardly defined 

as:

*)

Require Import List Program.

Set Implicit Arguments.

Section List_prods.

  Variable A : Type.

  (* [list_combine [x_1; ... x_n] [y_1; ... y_n] = [x_1::y_1; ... x_n::y_n; x_2::y_1 ... x_n::y_n]] *)

  Fixpoint list_combine (l : list A) (l' : list (list A)) : list (list A) :=

    match l with

    | [] => []

    | x::xs => List.map (fun y_i => x::y_i) l' ++ list_combine xs l'

    end.

  (* list_prod_tuple [xs_1; ... xs_n] gives a list containing every 

     list of the form [x_1; ... x_n] where [In x_1 xs_1], ... [In x_n xs_n].

   *)

  Fixpoint list_prod_tuple (elts : list (list A)) : list (list A) :=

    match elts with

    | [] => []

    | [x] => List.map (fun i => [i]) x

    | x::xs => list_combine x (list_prod_tuple xs)

    end.

End List_prods.

Eval vm_compute in list_prod_tuple [[1;2]; [3;4]].

(*

 >  = [[1; 3]; [1; 4]; [2; 3]; [2; 4]]

 >  : list (list nat)

*)

(*

    However, when I try to generalize this to heterogenous lists I hit

  two problems (the listing is a tad longer so I attach it to this mail):

  1) Coq does not recognize that the principal argument is decreasing

     in the recursive call (although clearly it does).

  2) even when we forget about this, I run into Universe inconsistency 

     problem... 

   Any help appreciated,

    Adam

*)

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [15 rue Berlier, 75013 Paris, France]
Sent from Montrouge, France