在 Coq 中参数化模块

Question

有没有一种方法可以将类型变量作为参数传递给 Coq 中的模块，这样我就不必重复声明类型变量了？

我的意思是：我想证明关于集合论的一些基本事实。让我们从德摩根定律的一部分开始。使用标准库中的 Ensemble，我有：

Require Import Ensembles.

Variable U : Type.

Lemma demorgan1: forall A B: Ensemble U, 
    Included U 
        (Intersection U (Complement U A) (Complement U B)) 
        (Complement U (Union U A B)).

这行得通，但是到处都是这些 U 真的很烦人。

有没有一种方法可以将 U 作为参数传递给 Ensembles 模块，这样从它导入的所有对象都会自动将 U 作为第一个传递争论？

Answer 1

Ensembles 库因历史原因保留，但如今已基本过时。直接使用谓词 U -> Prop 通常更容易，这就是 Ensemble U 展开的结果。但是回到你的问题，你可以通过使用 implicit arguments:

来实现你想要的

Require Import Ensembles.

Variable U : Type.

Arguments Included {U} _ _.
Arguments Intersection {U} _ _.
Arguments Union {U} _ _.
Arguments Complement {U} _.

Lemma demorgan1: forall A B: Ensemble U,
    Included
        (Intersection (Complement A) (Complement B))
        (Complement (Union A B)).

隐式参数是在 Arguments 声明或定义头中的花括号中指定的参数。 Coq 尝试根据其他参数的类型自动推断这些隐式参数应该用什么来实例化。在这种情况下，它知道这些函数的第一个参数应该是 U 因为 A、B 等的类型是 Ensemble U.

一般来说，覆盖其他人的定义中隐含的参数不是一个好主意：这个选择是库接口的一部分，最好按照作者的意图使用它。一个设计良好的现代图书馆通常会提供明智的隐式参数选择。但对于 Ensembles 等遗留库，覆盖它们可能是有意义的。

在 Coq 中参数化模块

Parametrizing a Module in Coq

proof

coq