The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

simplified I have the following mutualy inductive type:

Inductive t1 : Set :=

| a1 : t1

| a2 {n} : Vector.t t1 n -> t1

| a3 {n} : Vector.t t2 n -> t1

with t2 : Set :=

     | b1 : t2

     | b2 {n} : Vector.t t1 n -> t2

     | b3 {n} : Vector.t t2 n -> t2.

I also have two other inductive types:

Inductive t3 : Set :=

| c1 : t3 -> t3 -> t3 

| c2 {n} : Vector.t t1 n -> t3

| c3 {n} : Vector.t t2 n -> t3.

Inductive t4 : Set :=

| d1 : t4

| d2 : t4 -> t4 -> t4

| d3 {n} : Vector.t t4 n -> t4

| d4 {n} : Vector.t t4 n -> t4.

The problem I'm having is I am trying to convert t4 into t3 (its a kind of normalization). The issue comes with handling the cases d3 and d4 which corrspond to c2 and c3 respectively. There I essentially need to map a function converting to t1/t2 over the vector. Given that t1 and t2 are recursive and mutual these functions have to be mutual fixpoints (lets call those f1 : t4 -> t1 and f2 : f4 -> t2).

I have played around with this for a while now and I can't get coq to accept my definitions for these mutual fixpoints. When I try to map f2 over the input vector in the definition of f1, coq produces somewhat strange errors like "Not enough arguments" which if i write (fun f => f2 f) turns into a complaint that I apply f2 to something which should rather be the whole vector (to which it can't even be applied for typing reasons).

Is there some trick how to do this or is this again a case where using vector completely screws you over (or makes things so complicated that you'd rather not do that)?

Cheers,

Merlin