The Coq mailing list

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

I think this problem is the usual one when defining inductives
containing nested inductives (Vector of t1 inside defintion if t1).
There are lot of discussions about this in this list.

The syntactic guard condition of coq is not smart enough to "see" that
"(VectorUtils.traverse f1 x)" is actually a finite sequence of calls
to f1, each on a smaller or equal argument than x. This is not
necessarily true and depends on the definition of traverse (Suppose
for example that traverse f x = f (d3 x)..., you would create a
recursive loop). In some cases the guard condition detects such things
by unfolding but here it is not the case. And since it is not possible
in general you should adopt one of the two usual solutions I guess:

Either you encode your vectors as one more inductive in your inductive
family t1 t2, and then traverse is one more mutual functions in the
same mutual family than f1/f2.

Or you use a nested "fix" built to satisfy the guard condition instead
of traverse.

Hope this helps,
P.


2018-01-05 12:54 GMT+01:00 Merlin Göttlinger 
<megoettlinger AT gmail.com>:
> Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
>  schrieb am Fr., 5. Jan. 2018 um
> 12:01 Uhr:
>>
>> 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.
>
> Yes it is. This datatype represents a more general variant which allows more
> general arguments for those two "operators". The two fixpoints then
> transform the arguments into an allowed form (a kind of normal form).
>>
>>
>> Can you give the function you tried to write? I can't infer it from
>> what you gave.
>
>
> Fixpoint f1 f : list t1 :=
>   match f with
>   | d1 => [a1]
>   | d2 x x0 => f1 x ++ f1 x0
>   | d3 x => map a2 (VectorUtils.traverse (fun g => f1 g) x)
>   | d4 x => map a3 (VectorUtils.traverse f2 x)
>   end
> with f2 f : list t2 :=
>   match f with
>   | d1 => [b1]
>   | d2 x x0 => f2 x ++ f2 x0
>   | d3 x => map b2 (VectorUtils.traverse f1 x)
>   | d4 x => map b3 (VectorUtils.traverse f2 x)
>   end.
>
> The list part gets handeled in the conversion to t3 but the problem is in
> defining f1/f2.
>
> VectorUtils.traverse depends on a bunch of stuff I implemented and is the
> usual operation known from e.g. Haskell with signature G A -> (A -> F B) ->
> F (G B) where G is (fun T => Vector.t T n) and F is list in my case.
>
> Attatched stripped down versions of all necessary files in a gist for
> completeness:
> https://gist.github.com/mgttlinger/a80087e450a1e36963fa3c9cad4794ba
>
>>
>> > 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.
>
>  It probably does.
>
> Cheers,
> Merlin