The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi Nils,

> Mixing Induction and Coinduction
> http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html

Thanks for the reference to this interesting paper. I've tried to port  
your fib example to Coq; as far as I know, there is no (easy?) way to  
mix induction and coinduction in Coq, so I used a nat to nesting depth  
of ZipWith instead (https://www.cs.tcd.ie/Edsko.de.Vries/fib.v) --  
same effect though. If there is a nicer way to achieve this I'd be  
interested to hear it. (I don't really understand what it even means  
to mix induction and coinduction; how does Agda verify that your  
definition of fibP is correct? At least in my Coq version, I have to  
specify the appropriate integers myself; and presumably if I can't,  
then that's a good indication that perhaps I'm doing something bold :)

I had tried to use this approach (using a nat) with my problem but  
didn't manage and gave up because it seemed messy.. But now that I'v  
eseen that other people do it too I might give it a go again :)

Thanks,

Edsko