在Coq中执行通用实例化的最佳方法 [英] Best way to perform universal instantiation in Coq

问题描述

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

Suppose I have an hypothesis H : forall ( x : X ), P x and a variable x : X in the context. I want to perform universal instantiation and obtain a new hypothesis H' : P x. What is the most painless way to do this? Apparently apply H in x does not work. assert ( P x ) followed by apply H does, but it can get very messy if P is complex.

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

There's a similar question that seems somewhat related. Not sure if it can be applied here, though.

推荐答案

pose proof (H x) as H'.

括号是可选的.

这篇关于在Coq中执行通用实例化的最佳方法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！