The Coq mailing list

[Robert R Schneck-McConnell <schneck AT math.berkeley.edu>]

> I'm trying to make a proof on a coinductive type but I get the error
> "Recursive definition of H is ill-formed".
> My proof doesn't destruct the infinite object once but several times.
>
> I don't use my cofix hypothesis on the tail of my streams but on the tail^k
> (the tail of the tail of tail ... k times), which seems to be good because 
> the
> term is (intellectually) in guarded form.

The real problem, from your simplified version, is that you don't actually
apply the coinductive constructor directly as a guard, but instead apply a
lemma (ifleche_trans), which itself is a fixpoint over a case analysis
where each case is guarded.  The error message given by "Guarded" is very
explicit on this.  Coq can't figure out that that's good enough
as a guard.

I don't know what the right workaround is; one option might be to add
ifleche_trans as an extra coinductive constructor, and then separately
prove that the new predicate is equivalent to the original (in that it
holds of the same arguments; of course the proofs are different).

Robert