将具体假设应用于存在目标的Coq策略

Question

考虑以下示例：

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

apply H出现故障

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

所以我知道我可以使用策略exists 1+2+3来应用于这里的工作，或者，基于另一个stackoverflow问题，有一种更复杂的方法可以在H上使用正向推理来将其转化为存在形式。

但我希望有一些聪明的策略可以在统一时实例化存在变量，而不必显式？

Answer 1

你不需要正向推理，你只需要一个evar:

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

您在这里明确地介绍了创建一个存在变量，而Coq正在使用统一来实例化它