论文标题
对代数的反身策略，重新审视
Reflexive tactics for algebra, revisited
论文作者
论文摘要
计算反射使我们能够将经过验证的决策程序转变为证明助手的有效自动推理工具。这种方法的典型应用包括具有可决定理论片段的数学结构，例如通勤环和晶格的方程式理论。但是，已知这种现有工具不与包装类别合作，这是一种定义依赖类型理论的数学结构的方法，可以在整个继承层次结构中共享词汇。此外，此类工具不支持域和代码域类型可能不同的同态。本文演示了如何实施支持包装类和同构的反身策略。作为我们方法论的应用，我们将Coq的环和现场策略调整到了数学组件库的交换环和现场结构中，并将结果策略应用于Chyzak，Mahboubi和Sibut-Pinote的正式证明$ζ（3）$的正式证明，以带来更多的证明自动化。
Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology include mathematical structures that have decidable theory fragments, e.g., equational theories of commutative rings and lattices. However, such existing tools are known not to cooperate with packed classes, a methodology to define mathematical structures in dependent type theory, that allows for the sharing of vocabulary across the inheritance hierarchy. Additionally, such tools do not support homomorphisms whose domain and codomain types may differ. This paper demonstrates how to implement reflexive tactics that support packed classes and homomorphisms. As applications of our methodology, we adapt the ring and field tactics of Coq to the commutative ring and field structures of the Mathematical Components library, and apply the resulting tactics to the formal proof of the irrationality of $ζ(3)$ by Chyzak, Mahboubi, and Sibut-Pinote, to bring more proof automation.
