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

【问题标题】：Best way to perform universal instantiation in Coq在 Coq 中执行通用实例化的最佳方式
【发布时间】：2014-10-30 12:45:11
【问题描述】：

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

有一个similar question 似乎有些相关。不过不确定是否可以在这里应用。

【问题讨论】：

标签： coq quantifiers

【解决方案1】：

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

assert (H' := H x).

如果可以替换现有假设

specialize (H x).

【讨论】：

【解决方案2】：

pose proof (H x) as H'.

括号是可选的。

【讨论】：

【解决方案3】：

您可以使用generalize (H x); intros Hx 之类的东西：generalize 将在当前目标前面添加(H x) 作为新含义，intros 会将其放入您的假设中。

【讨论】：