The Coq mailing list

[Frederic.Blanqui AT loria.fr]

Selon Venanzio Capretta 
<Venanzio.Capretta AT mathstat.uottawa.ca>:

> Yes, replacing the mutual definition with a function works, but I was
> wandering what's wrong with the "CoFixpoint ... with ..." construction.
> It seems to be a problem with the reduction tactics: If you give the
> proof of the unfolding lemma directly instead of using tactics, you
> don't get any error. See the attached file.
>
> To Frederic: the problem doesn't seem to be related with the fact that
> you don't get the correct induction principle for mutual inductive
> types, since here you define mutual functions, not types.

in theory, the generated (co)induction principles are the basic -functions- 
(not
types) by which the user-defined functions are implemented. so, if there is 
some
problem in the implementation of reduction rules for generated principles (in
case of a mutual coinductive type), it can appear later in a user-defined
function. but, as you say, the problem seems related more to tactics than to
reduction rules for generated principles since it works if you don't use
tactics.