Coq证明助手中沿同构的定理自动透明迁移
计算机科学中的逻辑
2015-07-10 v4 数学软件
摘要
在数学中，对同一对象有多种构造是常见做法。数学家会模同构地识别它们，并且之后不必担心使用哪种构造，因为为一个构造证明的定理对所有构造都有效。在使用证明助手时，也常见多个数据类型表示同一对象。本工作旨在使多个同构构造的使用如同数学中非形式化操作一样简单和透明。这需要自动推断缺失的证明步骤。我们正在设计一种寻找并填充这些缺失证明步骤的算法，并将其实现为 Coq 的插件。
引用
@article{arxiv.1505.05028,
title = {Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant},
author = {Théo Zimmermann and Hugo Herbelin},
journal= {arXiv preprint arXiv:1505.05028},
year = {2015}
}