The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

When proving a goal with an existential, it matters when
eexists is used. For instance, with

Inductive foo : Set :=
  | bar : forall n, n = 7 -> foo.

the following proof works

Goal foo -> exists {n:nat}, n=7.
intros. destruct H. eexists. exact(e). Defined.

but this one yields a "cannot instantiate ... not in scope" error

Goal foo -> exists {n:nat}, n=7.
intros.  eexists. destruct H. exact(e).

It's easy to correct this error in a manual proof, but it is not clear to
me how to deal with such goals in (goal-direct) proof automation.

In principle, I could automate proofs like that using something like

Hint Extern 1 (?n = 7) =>
      match goal with
        | [ H : foo |- ?n = 7 ] => destruct H
      end.

but the hint won't fire until I used "eexists" first - but I need to use
eexists _after_ the "destruct".

Is there a way to solve this conundrum?

Klaus