Abstract
We present a complete mechanized proof of the result in homological algebra known as basic perturbation lemma. The proof has been carried out in the proof assistant Isabelle, more concretely, in the implementation of higher-order logic (HOL) available in the system. We report on the difficulties found when dealing with abstract algebra in HOL, and also on the ongoing stages of our project to give a certified version of some of the algorithms present in the Kenzo symbolic computation system.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Aransay, J.: Mechanized reasoning in homological algebra. Ph.D. Thesis, Universidad de La Rioja. http://www.unirioja.es/servicios/sp/tesis/tesis34.shtml (2006)
Aransay, J.: A formalized proof of the basic perturbation lemma in Isabelle/HOL. http://www.unirioja.es/cu/jearansa/BPL/index.html (2007)
Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Log. (2008)
Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003, 3rd International Workshop on Types for Proofs and Programs, Torino, Italy, May 2003. Lecture Notes in Computer Science, vol. 3085, pp. 34–50. Springer (2004)
Ballarin, C.: Interpretation of locales in Isabelle: managing dependencies between locales. Technical Report TUM-I0607, Technische Universität München. http://www4.in.tum.de/~ballarin/publications/TUM-I0607.pdf (2006a)
Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006, 5th International Conference on Mathematical Knowledge Management, Wokingham, UK, August 2006. Lecture Notes in Artificial Intelligence, vol. 4108, pp. 31–43. Springer (2006b)
Ballarin, C., Kammüller, F., Paulson, L.: The Isabelle/HOL algebra library. http://isabelle.in.tum.de/library/HOL/HOL-Algebra/document.pdf (2005)
Barnes, D., Lambe, L.: Fixed point approach to homological perturbation theory. Proc. Am. Math. Soc. 112(3), 881–892 (1991)
Bauer, G., Wenzel, M.: Computer-assisted mathematics at work (the Hahn–Banach theorem in Isabelle/Isar). In: Coquand, T., Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES’99, Types for Proofs and Programs International Workshop, Lökeberg, Sweden, June 1999. Lecture Notes in Computer Science, vol. 1956, pp. 61–76. Springer (2000)
Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002, 2nd International Workshop on Types for Proofs and Programs, Berg en Dal, The Netherlands, April 2002. Lecture Notes in Computer Science, vol. 2646, pp. 21–38. Springer (2003a)
Berghofer, S.: Proofs, programs and executable specifications in higher order logic. Ph.D. Thesis, Technische Universität München (2003b)
Berghofer, S.: Answer to Tom Ridge. Available at the mail list isabelle-users@cl.cam.ac.uk, February 18. http://www.cl.cam.ac.uk/users/lcp/archive/ (2005)
Bertot, Y., Castéran, P.: Interactive theorem proving and program development. In: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, vol. 25. Springer (2004)
Calmet, J.: Some grand mathematical challenges in mechanized mathematics. In: Hardin, T., Rioboo, R. (eds.) Calculemus 2003, 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Rome, Italy, September 2003, pp. 137–141. Aracne Editrice S.R.L. (2003)
Coquand, T., Lombardi, H.: A logical approach to abstract algebra. Math. Struct. Comput. Sci. 16(5), 885–900 (2006)
Coquand, T., Spiwack, A.: Towards constructive homological algebra in type theory. In: Kauers, R.M.M., Kerber, M., Windsteiger, W. (eds.) 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 2007. Lecture Notes in Computer Science, vol. 4573, pp. 40–54. Springer (2007)
Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo program. http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/ (1999)
Gugenheim, V.K.A.M.: On the chain complex of a fibration. Ill. J. Math. 16(3), 398–414 (1972)
Jacobson, N.: Basic Algebra 2, 2nd edn. W.H. Freeman and Company (1989)
Johnstone, P.T.: Notes on Logic and Set Theory. Cambridge University Press (1987)
Kammüller, F., Paulson, L.C.: A formal proof of Sylow’s theorem – an experiment in abstract algebra with Isabelle/HOL. J. Autom. Reason. 23(3), 235–264 (1999)
Kobayashi, H., Suzuki, H., Ono, Y.: Formalization of Hensel’s lemma. In: Hurd, J., Smith, E., Darbari, A. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings. Oxford University Computing Laboratory (2005)
Mac Lane, S.: Homology. Springer (1963)
Markov, A.A.: On constructive mathematics. Am. Math. Soc. Transl. 2(98), 1–9 (1971)
Müller, O., Slind, K.: Treating partiality in a logic of total functions. Comput. J. 40(10), 640–652 (1997)
Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Grundy, J., Newey, M. (eds.) TPHOLs’98, 11th International Conference on Theorem Proving in Higher Order Logics, Canberra, Australia, September 1998. Lecture Notes in Computer Science. vol. 1479, pp. 349–366. Springer (1998)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher order logic. Lecture Notes in Computer Science, vol. 2283. Springer (2002)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle’s logics: HOL. http://isabelle.in.tum.de/dist/Isabelle/doc/logics-HOL.pdf (2005)
Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363–397 (1989)
Paulson, L.C.: A formulation of the simple theory of types (for Isabelle). In: Martin-Löf, P., Mints, G. (eds.) COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988. Lecture Notes in Computer Science, vol. 417, pp. 246–274. Springer (1990a)
Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press (1990b)
Rubio, J., Sergeraert, F.: Constructive algebraic topology. Lecture Notes Summer School in Fundamental Algebraic Topology, Institut Fourier. http://www-fourier.ujf-grenoble.fr/~sergerar/Summer-School/ (1997)
Rubio, J., Sergeraert, F.: Constructive algebraic topology. Bulletin des Sciences Mathématiques 126(5), 389–412 (2002)
Thompson, S.: Type Theory and Functional Programming. Addison-Wesley (1991)
Troelstra, A., van Dalen, D.: Constructivism in Mathematics, vol. 2. Studies in Logic and the Foundations of Mathematics, vol. 123. North-Holland Press (1988)
Wenzel, M.: Isabelle/Isar – a versatile environment for human-readable formal proof documents. Ph.D. Thesis, Technische Universität München (2002)
Author information
Authors and Affiliations
Corresponding author
Additional information
J. Aransay was partially supported by Ministerio de Educación y Ciencia, MTM2006/06513, and by Gobierno de La Rioja ANGI2005/19 and J. Rubio was partially supported by Ministerio de Educación y Ciencia, MTM2006/06513, and by Gobierno de La Rioja ANGI2005/19.
Rights and permissions
About this article
Cite this article
Aransay, J., Ballarin, C. & Rubio, J. A Mechanized Proof of the Basic Perturbation Lemma. J Autom Reasoning 40, 271–292 (2008). https://doi.org/10.1007/s10817-007-9094-x
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-007-9094-x