Publication details

Saarland University Computer Science

Computational Back-and-Forth Arguments in Constructive Type Theory

Dominik Kirst

13th International Conference on Interactive Theorem Proving (ITP 2022), Haifa, Israel, 2022

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.

Project page

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy