The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Note this trick, though:

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

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

What that did: the evar generated by eexists has its own subgoal, which 
is shelved.  The instantiate tactic has the interesting feature of being 
able to run another tactic in an evar's subgoal, even though instantiate 
itself is not called within that subgoal. Hence that second "destruct H" 
runs in the evar's subgoal.  That second "destruct H" keeps the 
evolution of the two subgoals in step with respect to the new variables 
(n and e) revealed by the destruction, in just the same way as if that 
destruction had been done prior to the eexists.

WIthout instantiate, this can be done using unshelve to add the evar's 
subgoal to the proof focus, as in:

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

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

Coincidentally, I am writing a draft of something I might make into a 
CEP about just this.  It is an extension of the discussion with Hugo in 
bug https://coq.inria.fr/bugs/show_bug.cgi?id=3918 that he recently 
prompted me to look at again.  My point in this draft will be that in 
many cases, the above trick keeps proofs solvable, whereas otherwise 
they become unsolvable - and so perhaps there should be a setting that 
makes this happen automatically when possible.

-- Jonathan