Countability of Inductive Types Formalized in the Object-Logic Level

Qinxiang Cao
(John Hopcroft Center of Computer Science, Shanghai Jiao Tong University; Shanghai Key Laboratory of Trustworthy Computing, East China Normal University)
Xiwei Wu
(Shanghai Jiao Tong University)

The set of integer number lists with finite length, and the set of binary trees with integer labels are both countably infinite. Many inductively defined types also have countably many elements. In this paper, we formalize the syntax of first order inductive definitions in Coq and prove them countable, under some side conditions. Instead of writing a proof generator in a meta language, we develop an axiom-free proof in the Coq object logic. In other words, our proof is a dependently typed Coq function from the syntax of the inductive definition to the countability of the type. Based on this proof, we provide a Coq tactic to automatically prove the countability of concrete inductive types. We also developed Coq libraries for countability and for the syntax of inductive definitions, which have value on their own.

In Elaine Pimentel and Enrico Tassi: Proceedings Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2021), Pittsburgh, USA, 16th July 2021, Electronic Proceedings in Theoretical Computer Science 337, pp. 55–70.
Published: 16th July 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: