General Automation in Coq through Modular Transformations - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Electronic Proceedings in Theoretical Computer Science Année : 2021

General Automation in Coq through Modular Transformations

Résumé

Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible.
Fichier principal
Vignette du fichier
main.pdf (323.98 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03328935 , version 1 (30-08-2021)

Identifiants

Citer

Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial. General Automation in Coq through Modular Transformations. Seventh Workshop on Proof Exchange in Theorem Proving, Jul 2021, Pittsburgh, United States. ⟨10.4204/EPTCS.336.3⟩. ⟨hal-03328935⟩
115 Consultations
110 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More