我是Coq的新手,并试图根据我的研究开发一个框架.我的工作非常沉重,而且由于Coq似乎对待集合而我编码很困难.
有Type和Set,他们称之为"排序",我可以用它们来定义一个新的集合:
Variable X: Type.
然后有一个库编码(子)设置为' Ensembles ',它们是从一些Type到另一个的函数Prop.换句话说,它们是对a的谓词Type:
Variable Y: Ensemble X.
Ensemble感觉更像是适当的数学集合.此外,它们是由许多其他图书馆建立的.我已经尝试过关注它们:定义一个通用集U: Set,然后将自己限制在(子)Ensemble上U.但不是.Ensembles不能用作其他变量的类型,也不能用于定义新的子集:
Variable y: Y. (* Error *)
Variable Z: Ensemble Y. (* Error *)
现在,我知道有几种方法可以解决这个问题.问题" 子集参数 "提供了两个.两者都使用强制.第一个坚持Sets.第二个基本上使用Ensembles(虽然不是名字).但两者都需要相当多的机器才能完成如此简单的事情.
问题:一致(优雅)处理集的推荐方法是什么？
示例:以下是我想要做的示例:假设设置DD.定义一对dm =(D,<),其中D是DD的有限子集,而<是D上的严格偏序.
我敢肯定,通过强制修改或其他结构,我可以完成它; 但不是特别易读; 并没有很好的直觉,如何进一步操纵结构.例如,以下类型检查:
Record OrderedSet {DD: Set} : Type := …