The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 03/03/2014 22:57, Ömer Sinan Ağacan wrote:
> Hi all,
>
> I have this term as goal: http://lpaste.net/100661 and it looks
> solvable once I can simplify it by doing beta-reduction and then
> simplifying `match n with ...` term(it will become `match 0 with` once
> beta-reduction is done) ..
>
> Any ideas why I can't simplify this term, and what should I do to simplify it?

Coq never reduces a fix construct, unless the argument at the 
structurally-decreasing position is a constructor. (Otherwise, you would 
build an infinite sequence of reductions, which is bad.) So you have to 
destruct e sooner or later, so as to make a constructor appear there and 
reduce the fix.

Two approaches: either you destruct e and finish the proof for each of 
its constructors, or you replace the fix term by the reduced term you 
expect, and prove the equality by destructing e. Which approach to 
choose depends on which is the less painful: replicating the final proof 
8 times or typing the replacing term.

Best regards,

Guillaume