Generic Automation for the Coq Proof Assistant: Design and Principles

Pierre Corbineau
(Verimag UMR 5104, Université Grenoble Alpes, France)

Proof-editing in the Coq proof assistant is conducted using a wide variety of procedures called tactics. Several of these tactics host automated proof-search procedures addressing generic or specific logical problems.

Generic automation tactics try to provide help without relying on the existence of a specific theory or axiom, whereas specialised tactics address logical problems expressed in specific object-level theories such as linear arithmetic, rings, fields...

In this talk, we will focus on several examples of generic automation procedures. We will first describe how they work, and then show how they can interact with each other and other Coq features. Finally we will discuss their usefulness and weaknesses, and the pertinence of the generic approach.

In Jasmin Christian Blanchette and Cezary Kaliszyk: Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016), Coimbra, Portugal, July 1, 2016, Electronic Proceedings in Theoretical Computer Science 210, pp. 1–1.
Published: 17th June 2016.

http://dx.doi.org/10.4204/EPTCS.210.1 bibtex

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org