The Coq mailing list

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

Hi,
 
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). It makes one single list (not a 
list of pairs) so the length of the result is the sum of the two inputs. 
Following some examples in the Coq' Art book, I ended up with the code bellow:
 
Theorem discriminate_S_O : forall p, S p=0 -> False.
Proof.
 intros;discriminate.
Qed.
 
Fixpoint nzip k (l : nlist k) : nlist k -> nlist (k+k) :=
match l in (nlist z) return (nlist z) -> (nlist (z+z)) with
| nnil => fun m : nlist 0 => 
            match m in (nlist v) return v=0 -> (nlist v) with
            | nnil => (fun h => nnil)
            | ncon q _ _ => (fun h => False_rec (nlist (S q)) 
(discriminate_S_O h))
            end (refl_equal 0)
| ncon a lx ls => (fun m : nlist (S a) => 
            match m in (nlist v) return (S a)=v -> nlist (v+v) with
            | nnil => fun h => False_rec (nlist 0) (discriminate_S_O h)
            | ncon b mx ms => fun h => ncon lx (ncon mx (nzip b (eq_rec (S a) 
(fun v:nat => nlist (pred v)) ls (S b) (h:S a=S b)) ms))
            end (refl_equal (S a)))
end.
 
Unfortunately Coq says:
 
The term
 "ncon lx
    (ncon mx
       (nzip b
          (eq_rec (S a) (fun v : nat => nlist (pred v)) ls (S b)
             (h:S a = S b)) ms))" has type "nlist (S (S (b + b)))"
 while it is expected to have type "nlist (S b + S b)".
 
 
Could some one please explain what the problem is and how to get this 
function done in the correct way?
 
 
Thanks in advance,
Balazs