coq - 在 Coq 中执行通用实例化的最佳方式

Question

假设我在上下文中有一个假设H : forall ( x : X ), P x和一个变量。x : X我想执行通用实例化并获得一个新的假设H' : P x。做到这一点最无痛的方法是什么？显然apply H in x不起作用。assert ( P x )其次是apply Hdoes，但如果P很复杂，它会变得非常混乱。

有一个类似的问题似乎有些相关。不过，不确定它是否可以在这里应用。

Answer 1

pose proof (H x) as H'.

括号是可选的。

Answer 2

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

assert (H' := H x).

如果可以替换现有假设

specialize (H x).

Answer 3

您可以使用类似generalize (H x); intros Hx:的generalize内容(H x)作为当前目标前面的新含义，intros并将其放入您的假设中。