Inductive Proof Automation for Coq - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Inductive Proof Automation for Coq

Sean Wilson
  • Fonction : Auteur
  • PersonId : 871787
Jacques Fleuriot
  • Fonction : Auteur
  • PersonId : 871788
Alan Smaill
  • Fonction : Auteur
  • PersonId : 871789

Résumé

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.
Fichier principal
Vignette du fichier
paper_2.pdf (128.12 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00489496 , version 1 (05-06-2010)

Identifiants

  • HAL Id : inria-00489496 , version 1

Citer

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

Collections

COQ2010
274 Consultations
318 Téléchargements

Partager

Gmail Facebook X LinkedIn More