A language of patterns for subterm selection

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 sub expressions 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 sub expression of interest approximating the sub expression 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.
Type de document :
Communication dans un congrès
Lennart Beringer, Amy Felty. ITP, Aug 2012, Princeton, United States. Springer, 7406, pp.361-376, 2012, LNCS; Interactive Theorem Proving Interactive Theorem Proving. <10.1007/978-3-642-32347-8_25>
Liste complète des métadonnées


https://hal.inria.fr/hal-00652286
Contributeur : Enrico Tassi <>
Soumis le : lundi 13 février 2012 - 21:50:58
Dernière modification le : jeudi 9 février 2017 - 15:11:44
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 05:12:22

Fichier

rew.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Georges Gonthier, Enrico Tassi. A language of patterns for subterm selection. Lennart Beringer, Amy Felty. ITP, Aug 2012, Princeton, United States. Springer, 7406, pp.361-376, 2012, LNCS; Interactive Theorem Proving Interactive Theorem Proving. <10.1007/978-3-642-32347-8_25>. <hal-00652286v2>

Partager

Métriques

Consultations de
la notice

235

Téléchargements du document

155