coqltac

Coq tactic for applying a concrete hypothesis to an existential goal

Consider the following example:

Theorem example: forall (P: nat->Prop), P (1+2+3) -> (exists x, P x).
Proof.
intros. 
apply H

The apply H fails with 

Unable to unify "P (1 + 2 + 3)" with "exists x : nat, P x".

So I know that I could use the tactic exists 1+2+3 to get apply to work here, or, based on this other stackoverflow question there is a more convoluted way to use forward reasoning on H to get it into an existential form.

But I would expect there is some smart tactic that can instantiate existential variables when it's unifying, without having to be explicit?

Solution

  • You don't need forward reasoning, you just want an evar:

    Theorem example: forall (P: nat->Prop), P (1+2+3) -> (exists x, P x).
Proof.
intros.
eexists.
apply H.

    You're being explicit here about creating an existential variable, and Coq is using unification to instantiate it.