coq - 将具体假设应用于存在目标的 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 正在使用统一来实例化它。