Тактика 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, чтобы получить здесь работуили, основываясь на этом другом вопросе о потоке стека , существует более запутанный способ использовать прямое рассуждение на H, чтобы привести его в экзистенциальную форму.

Но я ожидаю, что есть некоторыеумная тактика, которая может создавать экземпляры экзистенциальных переменных при их объединении, без необходимости явного указания?

Answer 1

Тебе не нужны предварительные рассуждения, ты просто хочешь получить evar:

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

Здесь вы явно говорите о создании экзистенциальной переменной, а Coq использует унификацию для ее создания.