Countability of Inductive Types Formalized in the Object-Logic Level

TL;DR

This paper formalizes the countability of inductive types within Coq, providing a proof method and tools to automatically verify countability of various inductive definitions without relying on meta-language proof generators.

Contribution

It introduces a dependently typed Coq proof for countability of inductive types and provides automated tactics and libraries for practical verification.

Findings

Successfully formalized countability of inductive types in Coq

Developed an automatic Coq tactic for countability proofs

Created reusable Coq libraries for inductive syntax and countability

Abstract

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.