The Coq mailing list

[Balazs Vegvari <balazs.vegvari AT gmail.com>]

Thanks, I thought there should be a more elegant solution.

 

Regads,

Balazs

On Fri, May 4, 2012 at 1:59 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Balazs Vegvari wrote:

I have defined a simple indexed list type as follows:

Inductive nlist : nat ->  Set :=
| nnil : nlist O
| ncon : forall k, nat ->  nlist k ->  nlist (S k).

I am trying to write a function called nzip, which 'zips' two lists: from (1,2,3) and (4,5,6) it makes (1,4,2,5,3,6).

For a more thorough treatment of dependent container types than is feasible to get by asking questions on coq-club, I suggest reading Chapter 9 (and maybe the rest of ;]) CPDT:
   http://adam.chlipala.net/cpdt/

Here's a much nicer solution, which is compatible with your specification, save for the use of a dedicated function for doubling numbers.


Require Import DepList.

Fixpoint times2 (n : nat) :=
 match n with
   | O => O
   | S n' => S (S (times2 n'))
 end.

Fixpoint zip (n : nat) : ilist nat n -> ilist nat n -> ilist nat (times2 n) :=
 match n with
   | O => fun _ _ => INil
   | _ => fun l1 l2 => ICons (hd l1) (ICons (hd l2) (zip _ (tl l1) (tl l2)))
 end.

Implicit Arguments zip [n].

Eval compute in zip (ICons 1 (ICons 2 INil)) (ICons 3 (ICons 4 INil)).
(* = ICons 1 (ICons 3 (ICons 2 (ICons 4 INil))) *)