The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

A slightly different way to approach this would be to identify things you don't want to have unfolded using cbv:

    cbv beta delta -[plus].

The drawback of this is that I can't think of any way (offhand) to compose more than one of these tactics, so you would have to define it once and for all.

On Thu, Jul 10, 2008 at 7:21 AM, Adam Chlipala <adamc AT hcoop.net> 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.  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.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club