Validating Mathematical Structures
Validating Mathematical Structures
复制标题
DOI：
10.1007/978-3-030-51054-1_8
复制
发表时间：
2020-06-06
期刊：
影响因子：
--
通讯作者：
Sakaguchi K
中科院分区：
文献类型：
--
作者：
Sakaguchi K
在数学结构（如群和环）的继承层次中共享符号和理论，对于证明助手形式化数学时的生产力是重要的。打包类方法是一种通用设计模式，用于定义和组合依赖类型理论中的数学结构和记录。当与隐式强制和统一提示机制结合使用时，打包类可以在层次结构中实现自动结构推理和子类型，例如，可以使用环代替组。然而，基于打包类的大型层次结构很难实现和维护。我们确定了两个层次不变量，以确保推理的模块化和可预测性与包装类的推理，并提出了算法来检查这些不变量。我们将我们的算法作为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.
登录
查看更多内容
影响因子：
0.8
作者：
Boldo, Sylvie;Lelay, Catherine;Melquiond, Guillaume
通讯作者：
Melquiond, Guillaume
影响因子：
0.7
作者：
Geuvers, H;Pollack, R;Zwanenburg, J
通讯作者：
Zwanenburg, J
影响因子：
0.6
作者：
Cohen, Cyril;Mahboubi, Assia
通讯作者：
Mahboubi, Assia
影响因子：
1
作者：
COQUAND, T;HUET, G
通讯作者：
HUET, G
DOI：
10.1007/978-3-030-51054-1_1
发表时间：
2020-06-06
期刊：
Automated Reasoning
影响因子：
--
作者：
Affeldt R;Cohen C;Kerjean M;Mahboubi A;Rouhling D;Sakaguchi K
通讯作者：
Sakaguchi K