License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.29
URN: urn:nbn:de:0030-drops-167385
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16738/
Go to the corresponding LIPIcs Volume Portal

Sakaguchi, Kazuhiko

Reflexive Tactics for Algebra, Revisited

pdf-format:
LIPIcs-ITP-2022-29.pdf (0.8 MB)

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 decidable algebraic theories such as 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. Moreover, 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. As a result, the lines of code in the proof scripts have been reduced by 8%, and the time required for proof checking has been decreased by 27%.

BibTeX - Entry

@InProceedings{sakaguchi:LIPIcs.ITP.2022.29,
  author =	{Sakaguchi, Kazuhiko},
  title =	{{Reflexive Tactics for Algebra, Revisited}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16738},
  URN =		{urn:nbn:de:0030-drops-167385},
  doi =		{10.4230/LIPIcs.ITP.2022.29},
  annote =	{Keywords: Coq, Elpi, \lambdaProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection}
}

Keywords: Coq, Elpi, λProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software: https://doi.org/10.5281/zenodo.6487597

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI