Inductive Proof Automation for Coq

Abstract : We introduce inductive proof automation for Coq that supports reasoning about inductively defined data types and recursively defined functions. This includes support for proofs involving case splits and multiple inductive hypotheses. The automation makes use of the rippling heuristic to guide step case proofs as well as heuristics for generalising goals. We include features for caching lemmas that are found during proof search, where these lemmas can be reused in future proof attempts. We show that the techniques we present provide a high-level of automation for inductive proofs which improves upon what is already available in Coq. We also discuss an algorithm that, by inspecting finished proofs, can identify and then remove irrelevant subformulae from cached lemmas, making the latter more reusable. Finally, we compare our work to related research in the field.
Type de document :
Communication dans un congrès
Yves Bertot. Second Coq Workshop, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00489496
Contributeur : Yves Bertot <>
Soumis le : samedi 5 juin 2010 - 09:21:47
Dernière modification le : jeudi 26 octobre 2017 - 16:34:02
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 15:36:19

Fichier

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

Identifiants

  • HAL Id : inria-00489496, version 1

Collections

Citation

Sean Wilson, Jacques Fleuriot, Alan Smaill. Inductive Proof Automation for Coq. Yves Bertot. Second Coq Workshop, Jul 2010, Edinburgh, United Kingdom. 2010. 〈inria-00489496〉

Partager

Métriques

Consultations de la notice

249

Téléchargements de fichiers

260