In a theorem prover like Coq, mathematical concepts can be implemented in several ways. Their different representations can be either efficient for computing or well-suited to carry out proofs easily. In this paper, we present improved techniques to deal with changes of data representation within Coq. We propose a smart handling of case analysis and definitions together with some general methods to transfer recursion operators and their reduction rules from one setting to another. Once we have built a formal correspondence between two settings, we can translate automatically properties obtained in the initial setting into new properties in the target setting. We successfully experiment with changing Peano's numbers into binary numbers for the whole Arith library of Coq as well as with changing polymorphic lists into reversed (snoc) lists. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Magaud, N. (2003). Changing data representation within the Coq system. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2758, 87–102. https://doi.org/10.1007/10930755_6
Mendeley helps you to discover research relevant for your work.