如何解决在 Coq 中参数化模块
有没有一种方法可以将类型变量作为参数传递给 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
作为第一个参数传递?
解决方法
Ensembles
库是出于历史原因保留的,但现在它基本上已经过时了。通常直接使用谓词 U -> Prop
更容易,这就是 Ensemble U
无论如何展开的。但是回到你的问题,你可以通过使用隐式参数来实现你想要的:
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
等遗留库,覆盖它们可能是有意义的。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。