在Coq中執行通用實例化的最佳方法

Question

假設我在上下文中有一個假設H : forall (x : X), P x和一個變量x : X。我想執行通用實例化並獲得一個新的假設H' : P x。什麼是最無痛的方式來做到這一點？顯然apply H in x不起作用。 assert (P x)其次是apply H呢，但是如果P很複雜，會變得非常混亂。

有一個似乎有點相關的similar question。不知道是否可以在這裏應用。

Answer 1

pose proof (H x) as H'.

括號是可選的。

Answer 2

您可以使用類似generalize (H x); intros Hx：generalize將在目前的目標前加上(H x)作爲一種新的含義，並intros將放在你的假說。

Answer 3

如果你想新的假說，你可以使用@ Ptival的答案，或者

assert (H' := H x). 

如果它是確定替代現有的假說

specialize (H x).