The Coq mailing list

[aurelien.pardon AT ens-lyon.fr]

Hello

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.

It's like the euclidian division where an integer greater than one is
substracted at each step.
I want to make something like a well_founded_co_induction.
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 application of the cofix hypothesis is refused by coq because my proof
doesn't show explicitly the contructor.

You can find the error in a simplified version of my problem  here
http://perso.ens-lyon.fr/aurelien.pardon/ ;(the lemma tata
cannot be proven)

Thank you
Aurelien Pardon