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

【问题标题】：is there a `eapply`-like tactic that works on `exists` goals in Coq?在 Coq 中是否有类似 eapply 的策略适用于“exists”目标？
【发布时间】：2015-12-11 04:33:10
【问题描述】：

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

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

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

由于这是一个统一，因此不必在exists X. 中编写X 部分会很好。

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

【问题讨论】：

什么是eapply？

标签： coq coq-tactic

【解决方案1】：

存在这样一种策略，它被称为eexists。它完全符合您的预期。

https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic23

使用示例：

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.

【讨论】：

感谢您的回答。似乎eexists 与exists 相同。我还是要做eexists y. apply H，还需要搞清楚统一，即y我自己。如果我能做类似eexists H. 甚至只是eassumption 之类的事情来完成统一，那就太好了。
@tinlyx 我加了一个例子，你不需要指定y。
谢谢。一个额外的问题。有没有办法避免apply H 部分？我可以想象像eassumption 这样的东西会在每个假设上尝试apply。我尝试了assumption 并得到了Error: No such assumption.
@tinlyx eexists. eassumption. 非常适合上述示例。 eauto. 也可以，顺便说一句。