The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Sean Wilson wrote:
> As a simple example of what I need, given this definition:
>
> Definition f x y := plus x y.
>
> The following is true:
>
> Goal forall x y, f x y = f y x.
>
> My proof automation can prove this goal but only if "f" is unfolded first.

It seems dubious that you can even describe a general tactic for this 
kind of thing.  [plus] is no more privileged as a "primitive definition" 
than your [f], as far as Coq is concerned.  The heuristic you suggest 
for not unfolding recursive function definitions might work, but you 
might run up against a library function that you want to consider 
"primitive" that happens to be defined in terms of a recursive helper 
function, and then (if I understand you) the heuristic wouldn't do what 
you want.

I recommend parameterizing your automation on a simplification tactic, 
which could just be an [unfold] with a long list of identifiers.