The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Thursday 10 July 2008 15:21:24 Adam Chlipala wrote:
> 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. 

I thought there might be problems like this when I wasn't sure what I meant 
by "simple definition"...

> 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.

Yes, this could cause problems in some cases. As it is a heuristic though and 
I don't expect to be able to automate everything, as long the heuristic works 
in most cases, it should be helpful. I could do analysis of definitions first 
to avoid unfolding such problematic functions.

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

I have such a parameter already, but don't want to force the user to provide 
identifiers to unfold when it can be done automatically. Otherwise, the user 
is forced keep updating the simplifier to keep up with new definitions.

Thanks for the feedback!

Regards,

Sean