如何在通用量化下捕获参数（使用Modules？Sections？）

Question

我想知道在 Coq 中如何最好地处理这种情况：

假设我需要定义和证明关于任意结构的一些事情（为了讨论的目的，假设一个具有二元关系的集合）。当然，我总是可以提供集合和关系作为每个 definition/proof:

的参数

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.

我想这可能就是模块的用途，但我不知道如何在这种情况下使用它们。

Answer 1

Section rel_star.

Variables (X : Set) (R : X -> X -> Prop).

Inductive star := ...
Lemma star_trans: ...

End rel_star.

How to capture parameters under universal quantification (using Modules? Sections?)