有沒有類似eapply的策略可以用於Coq中存在的目標？

在目標是存在的證明中，我有以下幾點：目標屬性是假設之一。有沒有類似eapply的策略可以用於Coq中存在的目標？

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

我知道我可以做證明，當前的目標，但我想知道，如果有，可以直接使用的假設來這裏證明存在的目標，像eapply H更智能的戰術？

由於這是一個統一，所以不必編寫exists X.中的X部分。

如果這種策略不存在，我該怎麼寫？

2015-12-11 tinlyx

存在這樣的策略，它被稱爲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.

2015-12-11 09:29:42 Ptival

感謝您的回答。看起來'eexists'和'exists'是一樣的。我仍然必須做'存在'。應用H'，並且需要弄清楚統一，也就是我自己。如果我能做一些像'e存在H.'甚至只是'eassumption'來完成統一的事情，那將是很好的。 – tinlyx

@tinlyx我加了一個例子，你不需要指定'y'。 – Ptival

謝謝。一個額外的問題。有沒有辦法避免'應用H'部分？我可以想像像'eassumption'這樣的東西，它試圖在每個假設上應用'。我試過'假設'並得到了'錯誤：沒有這樣的假設。' – tinlyx

回答