How to turn an single unification variable into a goal, during proof

Question

I want to construct an existential variable interactively. I can't use Grab Existential Variables because I need to fill the existential before I complete the goal.

Minimal example Here is a minimal example (since it's simple, it has other solutions, but it illustrates my question)

Context (A: Type).
Parameter P Q: A -> Prop.
Definition filter: forall {a}, P a -> A := fun a Pa => a.
Lemma my_lemma:
  forall a b, Q b -> (Q b -> P a) ->
              exists a (H: P a), P (filter H).
forall a b : A,
Q b ->
(Q b -> P a) ->
exists (a0 : A) (H : P a0), P (filter H)
Proof.
forall a b : A,
Q b ->
(Q b -> P a) ->
exists (a0 : A) (H : P a0), P (filter H)
  intros ?? H H0.
a, b: A
H: Q b
H0: Q b -> P a
exists (a : A) (H : P a), P (filter H) do 2 eexists.
a, b: A
H: Q b
H0: Q b -> P a
P (filter ?H)

At this point, there are two solutions that don't answer my questions: (1) I could run (eauto) and then do Grab Existential Variables, but suppose that eauto doesn't succeed until I instantiate the unification variable; (2) I could just pass the proof term explicitly with instantiate (1 := H0 H) (or even instantiate (1:= ltac:(eauto))), but assume that the proof of the existential was tedious and we wished to do it interactively.

What else can we do? We can try to use cut or assert, like so:

  match goal with
  | [|- P (filter ?x)] =>
    match type of x with
    | ?T => assert (HH : T) by eauto
    end
  end.
a, b: A
H: Q b
H0: Q b -> P a
HH: P a
P (filter ?H)

But HH is not in the context of the unification variable, so it can't be instantiated.

  Fail instantiate (1 := HH).
The command has indeed failed with message:
Instance is not well-typed in the environment of ?H.

As far as I can tell, the only way to solve this is to use Show Existentials, see the type of the variable copy it by hand, roll back the proof to before the unification was introduced and construct the variable there. In the example it looks like this:

Lemma my_lemma:
  forall a b, Q b -> (Q b -> P a) ->
              exists a (H: P a), P (filter H).
forall a b : A,
Q b ->
(Q b -> P a) ->
exists (a0 : A) (H : P a0), P (filter H)
Proof.
forall a b : A,
Q b ->
(Q b -> P a) ->
exists (a0 : A) (H : P a0), P (filter H)
  intros ?? H H0.
a, b: A
H: Q b
H0: Q b -> P a
exists (a : A) (H : P a), P (filter H) do 2 eexists.
a, b: A
H: Q b
H0: Q b -> P a
P (filter ?H)
  Show Existentials.
Existential 1 =
?a : [a : A  b : A  H : Q b  H0 : Q b -> P a |- A] (shelved)
Existential 2 =
?H : [a : A  b : A  H : Q b  H0 : Q b -> P a |- P ?a] (shelved)
Existential 3 =
?Goal : [a : A  b : A  H : Q b  H0 : Q b -> P a
        |- P (filter ?H)]
a, b: A
H: Q b
H0: Q b -> P a
P (filter ?H)
  Restart.
forall a b : A,
Q b ->
(Q b -> P a) ->
exists (a0 : A) (H : P a0), P (filter H)
  (* This command restores the proof editing process to the original goal. *)
  intros ?? H H0.
a, b: A
H: Q b
H0: Q b -> P a
exists (a : A) (H : P a), P (filter H)
  assert (HH: P a) by eauto.
a, b: A
H: Q b
H0: Q b -> P a
HH: P a
exists (a : A) (H : P a), P (filter H)
  eexists.
a, b: A
H: Q b
H0: Q b -> P a
HH: P a
exists H1 : P ?a, P (filter H1) exists HH.
a, b: A
H: Q b
H0: Q b -> P a
HH: P a
P (filter HH) auto.
Qed.

Obviously, I would like to avoid this workflow. So, anyway to turn the existential variables into subgoals?

Answer

Your best bet is probably to avoid creating the existential variable as an evar in the first place. You don't have to construct the variable by hand to do this; if you can identify where it's created, you can wrap the offending tactic with unshelve t, which turns all evars created by t into goals. Where this might be difficult is if the relevant tactic is deep inside some automation and difficult to identify or change.