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.22
URN: urn:nbn:de:0030-drops-167311
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16731/
Go to the corresponding LIPIcs Volume Portal

Kirst, Dominik

Computational Back-And-Forth Arguments in Constructive Type Theory

pdf-format:
LIPIcs-ITP-2022-22.pdf (0.7 MB)

Abstract

The back-and-forth method is a well-known technique to establish isomorphisms of countable structures. In this proof pearl, we formalise this method abstractly in the framework of constructive type theory, emphasising the computational interpretation of the constructed isomorphisms. As prominent instances, we then deduce Cantor’s and Myhill’s isomorphism theorems on dense linear orders and one-one interreducible sets, respectively. By exploiting the symmetry of the abstract argument, our approach yields a particularly compact mechanisation of the method itself as well as its two instantiations, all implemented using the Coq proof assistant. As adequate for a proof pearl, we attempt to make the text and mechanisation accessible for a general mathematical audience.

BibTeX - Entry

@InProceedings{kirst:LIPIcs.ITP.2022.22,
  author =	{Kirst, Dominik},
  title =	{{Computational Back-And-Forth Arguments in Constructive Type Theory}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{22:1--22:12},
  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/16731},
  URN =		{urn:nbn:de:0030-drops-167311},
  doi =		{10.4230/LIPIcs.ITP.2022.22},
  annote =	{Keywords: back-and-forth method, computable isomorphisms, Coq}
}

Keywords: back-and-forth method, computable isomorphisms, Coq
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: https://www.ps.uni-saarland.de/extras/back-and-forth

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