Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description)
Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description)
复制标题
DOI：
10.4230/lipics.fscd.2020.34
复制
发表时间：
2020-05
期刊：
影响因子：
--
通讯作者：
C. Cohen;Kazuhiko Sakaguchi;Enrico Tassi
中科院分区：
文献类型：
--
作者：
C. Cohen;Kazuhiko Sakaguchi;Enrico Tassi
现在习惯于围绕代数结构的层次结构组织机器检查证明库[2，6，8，16，18，23，27]。一个有影响力的例子是Mathematical Components库，在其之上，奇阶定理的冗长而复杂的证明可以完全形式化[14]。尽管如此，在Coq [9]这样的证明助手中构建代数层次结构需要大量的手工劳动，并且通常需要证明器内部的深厚专业知识[13，17]。此外，根据我们的经验[26]，在不破坏客户端代码的情况下使层次结构进化也同样棘手：即使是简单的重构，例如将一个结构分成两个更简单的结构，也很难做到正确。在本文中，我们描述HB，一个高级语言，建立层次结构的代数结构，并使这些层次结构的演变，而不破坏用户代码。关键的概念是工厂、构建器和缩写，它们让层次结构开发人员为他们的库描述一个实际的接口。在该接口后面，开发人员可以提供适当的代码来确保追溯兼容性。我们使用Elpi [11，28]扩展语言在Coq系统的分层构建器插件中实现HB语言。
It is nowadays customary to organize libraries of machine checked proofs around hierarchies of algebraic structures [2, 6, 8, 16, 18, 23, 27]. One influential example is the Mathematical Components library on top of which the long and intricate proof of the Odd Order Theorem could be fully formalized [14]. Still, building algebraic hierarchies in a proof assistant such as Coq [9] requires a lot of manual labor and often a deep expertise in the internals of the prover [13, 17]. Moreover, according to our experience [26], making a hierarchy evolve without causing breakage in client code is equally tricky: even a simple refactoring such as splitting a structure into two simpler ones is hard to get right. In this paper we describe HB, a high level language to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure retro compatibility. We implement the HB language in the hierarchy-builder addon for the Coq system using the Elpi [11, 28] extension language.