我想知道如何在 Coq 中最好地处理这种情况:
假设我需要定义和证明关于任意结构的许多事情(为了讨论的目的，假设一个具有二元关系的集合)。当然，我总是可以提供集合和关系作为每个这样的定义/证明的参数:
Inductive star (X : Set) (R : X -> X -> Prop) := ...
Lemma star_trans (X : Set) (R : X -> X -> Prop) : ...
当然，一段时间后这会变得令人厌烦。我想做的是在代码的某些划定区域内将 X 和 R 作为本地参数，如下所示:
Parameter X : Set.
Parameter R : X -> X -> Prop.
Inductive star := ...
Lemma star_trans : ...
以这种方式，定义和定理在该代码区域之外使用时，会在通用量化下捕获 X 和 R 以便为它们提供正确的类型。例如，Check star 应该产生 star : forall X : Set, (X -> X -> Prop) -> X -> X -> Prop。
我认为这可能就是模块的用途，但我不知道如何在这种情况下使用它们。
最佳答案
这正是“部分机制”的作用:参见 https://coq.inria.fr/distrib/current/refman/Reference-Manual004.html#Section .
Section rel_star.
Variables (X : Set) (R : X -> X -> Prop).
Inductive star := ...
Lemma star_trans: ...
End rel_star.
关于coq - 如何在通用量化下捕获参数(使用模块？部分？)，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/40053229/