Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Balaa, A., Bertot, Y.: Fix-point Equations for Well-Founded Recursion in Type Theory. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 1–16. Springer, Heidelberg (2000)
Barthe, G., Pons, O.: Type Isomorphisms and Proof Reuse in Dependent Type Theory. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 57–71. Springer, Heidelberg (2001)
Bertot, Y., Casteran, P.: Le Coq’Art (2003) (to appear)
Chrzaszcz, J.: Implementation of Modules in the Coq System. Draft (February 2003)
Coq development team, INRIA and LRI. The Coq Proof Assistant Reference Manual, Version 7.3 (May 2002)
Cornes, C., Terrasse, D.: Automatizing Inversion of Inductive Predicates in Coq. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158. Springer, Heidelberg (1996)
Delahaye, D., Mayero, M.: Field: une procédure de décision pour les nombres réels en Coq. In: Castéran, P. (ed.) Journées Francophones des Langages Applicatifs, Pontarlier, Janvier. INRIA (2001)
Dybjer, P.: Inductive Families. Formal Aspects of Computing 6(4), 440–465 (1994)
Dybjer, P.: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65(2) (2000)
Hofmann, M.: Conservativity of Equality Reflection over Intensional Type Theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 153–165. Springer, Heidelberg (1996)
Luo, Z., Soloviev, S.: Dependent Coercions. In: 8th Inter. Conf. on Category Theory in Computer Science (CTCS 1999), Edinburgh, Scotland. ENTCS, vol. 29, pp. 23–34. Elsevier, Amsterdam (1999)
Magaud, N., Bertot, Y.: Changing Data Structures in Type Theory:A Study of Natural Numbers. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 181–196. Springer, Heidelberg (2002)
McBride, C., McKinna, J.: The View from the Left. Journal of Functional Programming, Special Issue: Dependent Type Theory meets Programming Practice (2002) (submitted)
Miquel, A.: Axiom ∀P,Q: Prop (P \(\leftrightarrow\) Q)→(P==Q) is safe. Communication in the coq-club list (November 2002)
Paulin-Mohring, C.: Inductive Definitions in the System Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993); LIP research report 92–49
Saïbi, A.: Typing Algorithm in Type Theory with Inheritance. In: POPL 1997. ACM, New York (1997)
Wadler, P.: Views: A Way for Pattern Matching to Cohabit with Data Abstraction. In: POPL 1987. ACM, New York (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Magaud, N. (2003). Changing Data Representation within the Coq System. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_6
Download citation
DOI: https://doi.org/10.1007/10930755_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40664-8
Online ISBN: 978-3-540-45130-3
eBook Packages: Springer Book Archive