Is there a eapply-like tactic that works on exists goals in Coq?

Link:: https://stackoverflow.com/q/34216180

Display all goals and responses

Question

I have the following during a proof where the goal is an existential, and the target property is one of the assumptions.

H : x ==> y
...
______________________________________(1/2)
exists t : tm, x ==> t

I know I can do exists y. apply H. to prove the current goal, but I am wondering if there is a more intelligent tactic that can use the assumption directly to prove the existential goal here, like eapply H?

Since this is one unification away, it would be nice not having to write the X part in exists X..

If such a tactic does not exist, how do I write one?

Answer

There exists such a tactic and it is called eexists. It does exactly what you seem to expect.

https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic23

Example use:

Variable T : Type.Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]
Variable R : T -> T -> Prop.Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]

Theorem test : forall x y, R x y -> exists t, R x t.forall x y : T, R x y -> exists t : T, R x t
Proof.forall x y : T, R x y -> exists t : T, R x t
  intros.x, y: T
H: R x y
exists t : T, R x t eexists.x, y: T
H: R x y
R x ?t apply H.
Qed.

Q: Thanks. An extra question. Is there a way to avoid the apply H part? I can imagine something like eassumption that tries apply on every assumption. I tried assumption and got Error: No such assumption.

A: eexists. eassumption. works perfectly for the above example. eauto. works too, btw.