The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Flávio Leonardo Cavalcanti de Moura wrote:
>         I defined the following recursive function:
>
> Fixpoint prod_in (n m:nat) {struct m} := ....
>
> "Eval compute in (prod_in 0 1)" returns 0, but if I declare a variable m
> of type nat
>
> "Eval compute in (prod_in 0 m)" doesn't evaluate to 0.
>    

As you guessed, the problem has to do with the fact that the 2nd 
argument is the recursive one.  Coq only beta-reduces [fix] expressions 
when they are applied to recursive arguments with known top-level 
structure.  It's actually a really good thing that this restriction is 
in place; otherwise, [fix] beta reduction could be applied in infinite 
descent, leading the type-checker to diverge (and possibly making the 
definitional equality undecidable)!