The Coq mailing list

[CJ Bell <siegebell+coq AT gmail.com>]

So far so good.  But now, try to represent the naive Fibonacci function as a naive user who doesn't know it will actually terminate:

[...]

Coq won't accept this because of the occurrence of fib in the notation-produced function bodies (and I understand there are good reasons for rejecting such definitions).  In fact, I'm convinced that to produce a version that will be accepted, you'll essentially have to encode a runtime stack for the execution yourself - which isn't what you would have "signed up for" starting the exercise.

This example is due to Adam Chlipala.

The above example uses Capretta's encoding ("thunks"). Adam also shows an alternative encoding (from Megacz) that *does* work for the Fibonacci example and is (in my opinion) easy to work with. True, the user has to think about which encoding they use to avoid such problems, but that's kind of a running theme in Coq and it's certainly not limited to coinductive types.

see: [http://adam.chlipala.net/cpdt/html/GeneralRec.html]

The main difficulty I've had with Coq's limited guardedness checker is for coinductive proofs using the cofix tactic.

Anyone running into problems with the cofix tactic should try the Paco library (http://plv.mpi-sws.org/paco/) instead, which provides a coinduction tactic that feels similar to induction and makes it easy to write incremental and modular coinductive proofs (e.g. separate proofs for mutually corecursive functions). It uses greatest fixed-point representations of coinductive types, which is fairly easy to prove equivalent w.r.t. a CoInductive encoding.

-cj