The Coq mailing list

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

Is there any way to affect the way rewrite instantiates existential variables?

I have a database of autorewrite rules for simplifying terms, that are along the lines of this:

Axiom Assoc : forall x y z, x + (y + z) = x + z + y.
Hint Rewrite Assoc : Simpl.

The problem is that rewrite aggressively instantiates existential variables.

Consider the following:

Goal exists x, x = 0.
econstructor.

In this case, doing "rewrite Assoc" changes the goal from
    ?1 = 0
to
    ?2 + ?3 + ?4 = 0
...and of course, "rewrite Assoc" can be done again on this goal.

The result of this is attempting to do "autorewrite with Simpl" on this goal causes an infinite loop.

Is there any better solution than manually instantiating all existential variables before autorewriting?

I'm also curious if there are cases where one might actually want to instantiate existential variables while doing rewriting.

Thanks,

Andrew McCreight