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. |

Published: 16th July 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.337.5 | bibtex | |

Comments and questions to: eptcs@eptcs.org |

For website issues: webmaster@eptcs.org |