The Coq mailing list

[Dimitur Krustev <dkrustev AT gmail.com>]

Robert Dockins <robdockins <at> fastmail.fm> writes:

> 
> I'm playing around with representations for graphs, and I've run into 
difficulty stating a definition I
> want.  I'd like to prove some results relating graphs represented via 
successor lists to a representation
> via an infinite "spanning tree," but Coq will not accept a cofixpoint 
definition that seems productive to
> me. The following is a simplified form.  Coq 8.3pl1 and 8.4 give the same 
error (reproduced below).
> 
> I think this definition ought to be accepted, but it runs afoul of the 
guardness checker.  Apparently you
> cannot have fixpoints nested inside cofixpoints?  Is there any nice way to 
> get 
around this?
> 
> Thanks,
> Rob Dockins
> 

Hi Robert,

When I recently stumbled upon a similar problem, I found the ideas from the 
following paper useful:

- C Picard, R Matthes, "Mixing induction and co-induction in Coq: a case 
study 
for lists", 2010

Briefly, the main trick is to avoid mixing induction and co-induction 
altogether: replace the nested use of the inductive [list] with an isomorphic 
non-inductive definition, such as [fun A => { length: nat & Fin length -> A 
}] 
(using your favorite definition of [Fin]). The advantage is that many 
functions 
(especially [map]) have non-recursive definitions for this version of finite 
lists, which makes it easier for Coq to "see" that certain co-inductive 
definitions are productive.

I am not sure how well this would work in your particular setting, but it 
might 
be worth to try.

Best regards,
Dimitur