论文标题
验证数学结构
Validating Mathematical Structures
论文作者
论文摘要
在数学结构的继承层次结构中共享符号和理论，例如组和戒指，对于证明助手的数学形式化时，对生产力很重要。包装的类方法是一种通用设计模式，可以在依赖类型理论中定义和将数学结构与记录相结合。当与隐式胁迫和统一提示的机制结合使用时，包装的类可实现自动结构的推理和层次结构中的亚型，例如，可以使用一个环代替组。但是，基于包装类的大型层次结构在实施和维护方面具有挑战性。我们确定了两个层次结构不变性，以确保推理的模块化和用包装类别的推理的可预测性，并提出算法检查这些不变性。我们将算法作为COQ证明助手的工具实施，并表明它们显着改善了数学组成部分的开发过程，这是用于形式化数学的库。
Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a generic design pattern to define and combine mathematical structures in a dependent type theory with records. When combined with mechanisms for implicit coercions and unification hints, packed classes enable automated structure inference and subtyping in hierarchies, e.g., that a ring can be used in place of a group. However, large hierarchies based on packed classes are challenging to implement and maintain. We identify two hierarchy invariants that ensure modularity of reasoning and predictability of inference with packed classes, and propose algorithms to check these invariants. We implement our algorithms as tools for the Coq proof assistant, and show that they significantly improve the development process of Mathematical Components, a library for formalized mathematics.
