The Coq mailing list

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

Thanks for the quick answers.

 

@Conor: to me, this just popped up as I tried to educate myself in Coq. Not a real-life problem (at least for now :) ). But I'll think go over your suggestions as I am definitely not a functional programmer and maybe I should think more 'functionally'. Thanks for the ideas.

 

Nevertheless, reasoning about the equality of the two terms helped. I ended up with this:

 

Theorem lengths_equal : forall n, S (S (n + n)) = S n + S n.
intros.
omega.
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 zz) return zz=0 -> (nlist zz) 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 zz) return (S a)=zz -> nlist (zz+zz) with
            | nnil => fun h => False_rec (nlist 0) (discriminate_S_O h)
            | ncon b mx ms => fun h =>

(eq_rec (S (S b + b)) (fun v : nat => nlist v)
(ncon lx (ncon mx (nzip b (eq_rec (S a) (fun v:nat => nlist (pred v)) ls (S b) h) ms)))
(S b + S b) (lengths_equal b))

            end (refl_equal (S a)))
end.

 

Implicit Arguments nzip [k].

 

But when I evaluate the function:

 

Eval compute in (nzip (ncon 1 (ncon 2 (ncon 3 nnil))) (ncon 4 (ncon 5 (ncon 6 nnil)))).

The result is:

 

     = match lengths_equal 2 in (_ = y) return (nlist y) with
       | eq_refl =>
           ncon 1
             (ncon 4
                match lengths_equal 1 in (_ = y) return (nlist y) with
                | eq_refl =>
                    ncon 2
                      (ncon 5
                         match
                           lengths_equal 0 in (_ = y) return (nlist y)
                         with
                         | eq_refl => ncon 3 (ncon 6 nnil)
                         end)
                end)
       end
     : nlist (3 + 3)

So it seems ok but a bit unreadable. Is it because I should be smarter about how to use eq_rec properly?

I would expect something like (ncon 1 (ncon 4 (ncon 2 (ncon 5 (ncon 3 (ncon 6 nnil)))))).

 

 

Thanks,

Balazs

 

On Fri, May 4, 2012 at 9:31 AM, Paolo Herms <paolo.herms AT cea.fr> wrote:

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