Abstract
We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.: The semantics of reflected proof. In: Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia, Pennsylvania, pp. 195–197. IEEE Computer Society Press, Los Alamitos (1990)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Coq’Art: the Calculus of Inductive Constructions. Texts in Theoretical Computer Science (2004)
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: TACS, pp. 515–529 (1997)
Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. LNCS, vol. 33, pp. 134–183. Springer, Berlin (1975)
Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 85–95. Springer, Heidelberg (2000), http://cedric.cnam.fr/~delahaye/publications/LPAR2000-ltac.ps.gz
Delahaye, D., Mayero, M.: Field: une procédure de décision pour les nombres réels en Coq. In Journees Francophones des Langages Applicatifs, Pontarlier, INRIA Janvier 2001 (2001), http://cedric.cnam.fr/~delahaye/publications/JFLA2000-Field.ps.gz
Barthe, V.C.G., Pons, O.: Setoids in type theory. Journal of Functional Programming 13(2), 261–293 (2003)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming 2002, pp. 235–246. ACM Press, New York (2002)
Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. Journal of Automated Reasoning 21, 279–294 (1998)
Hofmann, M.: A simple model for quotient types. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 216–234. Springer, Heidelberg (1995)
Narboux, J.: A decision procedure for geometry in coq. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 225–240. Springer, Heidelberg (2004)
The Coq development team. The coq proof assistant reference manual v7.2. Technical Report 255, INRIA, France, mars (2002), http://coq.inria.fr/doc8/main.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grégoire, B., Mahboubi, A. (2005). Proving Equalities in a Commutative Ring Done Right in Coq. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_7
Download citation
DOI: https://doi.org/10.1007/11541868_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)