The Coq mailing list

["Jonas B. Jensen" <jobr AT itu.dk>]

Hi Gregory

On Tue, May 31, 2011 at 03:20, Gregory Malecha
<gmalecha AT eecs.harvard.edu>
 wrote:
> Is there any way to tell autorewrite to treat existentials as "atomic," i.e.
> not be able to expand them arbitrarily?

We've had the same type of problem in our development recently. The
quick-fix was to do pre- and post-processing steps to make the
existentials opaque. Here's your code with this hack applied:

Require Import Plus.

Ltac ugly_evar_hack_create :=
  repeat (match goal with
            [ |- context[?x]] => is_evar x; let l := fresh "l" in
remember x as l
          end).

Ltac ugly_evar_hack_restore :=
  repeat (match goal with
             | [H : (?l = ?evar) |- ?p] => is_evar evar; subst l
          end).

Hint Rewrite <- plus_assoc : test.

Goal exists x, x + 0 = x.
eexists.
do 3 rewrite <- plus_assoc. (** produces a bunch of existentials **)
ugly_evar_hack_create; autorewrite with test; ugly_evar_hack_restore.

These tactics can certainly be made more robust and easy to work with.
And I hope somebody else has a better solution.

Cheers,
Jonas