The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2018-01-05 10:29 GMT+01:00 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.

is it really Vector.t t4 n in d3 and d4? Given you comments I would
have expected Vector.t t1 n and Vector.t t2 n.

Can you give the function you tried to write? I can't infer it from
what you gave.

> 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).

Maybe the problem comes more from the fact that your types use
Vector.t in a nested way. Using list would be a problem too.

P.

> 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