The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Hey Balazs,
the problem is that "(S b + S b)" and "(S (S (b + b)))" are not convertible.
You need to prove that they are equal and then use this proof with eq_rect to 
cast your list of type "nlist (S (S (b + b)))" to a list of type 
"nlist (S b + S b)".
Hope this helps,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France


On Friday 04 May 2012 08:56:51 Balazs Vegvari wrote:
> 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