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

Question

假设我在上下文中有一个假设H : forall ( x : X ), P x和一个变量x : X。我想进行通用实例化并获得一个新的假设H' : P x。最无痛的方法是什么？显然apply H in x不起作用。assert ( P x )之后是apply H，但如果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将其放入您的假设中。