Experience Implementing a Performant Category-Theory Library in Coq
Experience Implementing a Performant Category-Theory Library in Coq
复制标题
在 Coq 中实现高性能类别理论库的经验
DOI：
10.1007/978-3-319-08970-6_18
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
David I. Spivak
中科院分区：
文献类型：
--
作者：
Jason Gross;A. Chlipala;David I. Spivak
我们描述了在Coq中实施广泛的范畴理论库的经验。范畴理论和计算性能通常不会被相提并论，但我们需要大量的工程努力来教Coq科普大型范畴结构，而不会令人无法接受地减慢证明脚本处理。在本文中，我们分享了我们所学到的关于如何在Coq中表示非常抽象的数学对象和参数的经验教训，以及如何设计未来的证明助手来更好地支持这种推理。一个特殊的编码技巧，我们提请注意允许范畴理论的论点，涉及对偶性内在的柯克的逻辑与定义的平等。我们的可能是迄今为止最大的Coq开发，使用同伦类型理论家开发的相对较新的Coq版本，我们反思哪些新功能特别有用。
We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to cope with large categorical constructions without slowing proof script processing unacceptably. In this paper, we share the lessons we have learned about how to represent very abstract mathematical objects and arguments in Coq and how future proof assistants might be designed to better support such reasoning. One particular encoding trick to which we draw attention allows category-theoretic arguments involving duality to be internalized in Coq’s logic with definitional equality. Ours may be the largest Coq development to date that uses the relatively new Coq version developed by homotopy type theorists, and we reflect on which new features were especially helpful.