coq - 在 Coq 中是否有类似 eapply 的策略适用于“exists”目标？

Question

在目标是存在的证明中，我有以下内容，并且目标属性是假设之一。

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

我知道我可以exists y. apply H.证明当前的目标，但我想知道是否有更智能的策略可以直接使用假设来证明这里的存在目标，比如eapply H？

由于这是一个统一，因此不必将X部分写入exists X..

如果不存在这样的策略，我该如何编写？

score 4 · Accepted Answer

有这样一种战术，叫做eexists。它完全符合您的预期。

示例使用：

Variable T : Type.
Variable R : T -> T -> Prop.

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

1 回答 1