Skip to main content
SpringerLink
Log in

A Language of Patterns for Subterm Selection

  • Conference paper
Interactive Theorem Proving (ITP 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7406))

Included in the following conference series:

Abstract

This paper describes the language of patterns that equips the SSReflect proof shell extension for the Coq system. Patterns are used to focus proof commands on subexpressions of the conjecture under analysis in a declarative manner. They are designed to ease the writing of proof scripts and to increase their readability and maintainability.

A pattern can identify the subexpression of interest approximating the subexpression itself, or its enclosing context or both. The user is free to choose the most convenient option.

Patterns are matched following an extremely precise and predictable discipline, that is carefully designed to admit an efficient implementation.

In this paper we report on the language of patterns, its matching algorithm and its usage in the formal library developed by the Mathematical Components team to support the verification of the Odd Order Theorem.

The research leading to these results has received funding from the European Union’s 7th Framework Programme under grant agreement nr. 243847 (ForMath).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Mathematical Components website, http://www.msr-inria.inria.fr/Projects/math-components/ , http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/

  2. Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending COQ with Imperative Features and Its Application to SAT Verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 83–98. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Journal of Automated Reasoning 39(2), 109–139 (2007)

    Article  MATH  Google Scholar 

  4. Bender, H., Glauberman, G.: Local analysis for the Odd Order Theorem. London Mathematical Society Lecture Note Series, vol. 188. Cambridge University Press (1994)

    Google Scholar 

  5. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: the Calculus of Inductive Constructions. Springer (2004)

    Google Scholar 

  6. Braibant, T., Pous, D.: An Efficient COQ Tactic for Deciding Kleene Algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 163–178. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Braibant, T., Pous, D.: Tactics for Reasoning Modulo AC in COQ. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 167–182. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection extension for the COQ system. INRIA Technical report, 00258384

    Google Scholar 

  10. Gonthier, G.: Formal proof – the four color theorem. Notices of the American Mathematical Society 55, 1382–1394 (2008)

    MathSciNet  MATH  Google Scholar 

  11. Grégoire, B., Mahboubi, A.: Proving Equalities in a Commutative Ring Done Right in COQ. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Huppert, B., Blackburn, N.: Finite groups II. Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, vol. 2. Springer (1982)

    Google Scholar 

  13. The COQ development team. The COQ proof assistant reference manual, Version 8.3 (2011)

    Google Scholar 

  14. Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning 5, 363–397 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  15. Pollack, R.: Dependently typed records in type theory. Formal Aspects of Computing 13, 386–402 (2002)

    Article  MATH  Google Scholar 

  16. Sacerdoti Coen, C., Tassi, E.: Working with Mathematical Structures in Type Theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 157–172. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21, 1–31 (2011)

    Article  Google Scholar 

  18. Théry, L., Hanrot, G.: Primality Proving with Elliptic Curves. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 319–333. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Wenzel, M.T.: Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–184. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Georges Gonthier

  2. INRIA - Microsoft Research Joint Centre, France

    Georges Gonthier & Enrico Tassi

  3. Laboratoire d’Informatique de l’Ecole Polytechnique, INRIA, France

    Enrico Tassi

Authors
  1. Georges Gonthier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Enrico Tassi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Princeton University, 35 Olden Street, 08540, Princeton, NJ, USA

    Lennart Beringer

  2. School of Electrical Engineering and Computer Science, University of Ottawa, 800 King Edward Ave., K1N 6N5, Ottawa, ON, Canada

    Amy Felty

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gonthier, G., Tassi, E. (2012). A Language of Patterns for Subterm Selection. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32347-8_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32346-1

  • Online ISBN: 978-3-642-32347-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation