coq - Coq 中的自由变量

Question

是否有任何函数/命令可以使用 Coq 获取/检查一个自由变量，比如 n:U，是否存在于术语/表达式 e 中？请分享。

例如，我想在 Coq 中声明这个“n 不会出现在 e 的自由名称中”。

谢谢，

维拉亚特

Answer 1

假设您在用Coq术语谈论自由变量：

处理一个基本的 Coq 证明（不使用任何外部），您操作的是，在证明上下文之外，一个封闭的术语，即一个只有绑定变量的术语。如果在证明模式下e，您的目标中的一个术语似乎有一个自由变量n（意味着该变量在您的证明上下文中的某处），您可以使用该策略n简单地使绑定显式（并关闭目标术语） 。generalize

在更高级的情况下，您的不太普通的证明可能涉及假设或参数形式的自由变量，在这种情况下，您可以使用Print Assumptions.

另一方面，如果您正在谈论使用 Coq 术语来表示特定语言中的术语概念（例如，您正在对这种语言进行形式化），您只需对您的语言的自由变量进行特殊处理。

如果您在语言术语的归纳定义中给它们一个特定的构造函数，那么应该很容易说明某个术语是否具有自由变量。如果您不熟悉表示替换和语言的自由变量的（不是那么微不足道的）概念，您会发现从TAPL到 BCPierce 的SF 课程再到POPLMark 挑战赛结果的精确度越来越高的指针。