Reflexive tactics for algebra, revisited

TL;DR

This paper develops reflexive tactics that support packed classes and homomorphisms in proof assistants, enhancing automation in algebraic structure reasoning and formal proofs like the irrationality of zeta(3).

Contribution

It introduces methods to implement reflexive tactics compatible with packed classes and homomorphisms, improving proof automation in dependent type theory.

Findings

Successfully adapted ring and field tactics in Coq.

Enhanced proof automation for algebraic structures.

Applied tactics to prove irrationality of zeta(3).

Abstract

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 $\zeta(3)$ by Chyzak, Mahboubi, and Sibut-Pinote, to bring more proof automation.