2026-07-25T12:51:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16731 2024-03-06T10:58:10Z ddc:004 open_access

Computational Back-And-Forth Arguments in Constructive Type Theory Kirst, Dominik back-and-forth method computable isomorphisms Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dominik Kirst 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.22 urn:nbn:de:0030-drops-167311 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.22 eng https://creativecommons.org/licenses/by/4.0/legalcode