Coq's Prolog and application to defining semi-automatic tactics

Théo Zimmermann (1, 2) , Hugo Herbelin (1, 2)

1 PI.R2 - Design, study and implementation of languages for proofs and programs
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale

We report on a work-in-progress to re-implement Coq's apply tactic in order to embed some form of simple automation. We design it in a declarative way, relying on typeclasses eauto, a tactic which gives access to the proof-search mechanism behind type classes. We qualify this mechanism of " Coq's Prolog " and describe it in a generic way and explain how it can be used to support the construction of automatic and semi-automatic tactics.

Mots clés: apply; automation; Coq; proof assistant; reflection; type theory; views

Domaines: Théorie et langage formel [cs.FL]; Logiciel mathématique [cs.MS]; Logique en informatique [cs.LO]

Théo Zimmermann, Hugo Herbelin. Coq's Prolog and application to defining semi-automatic tactics. Type Theory Based Tools, Jan 2017, Paris, France. ⟨hal-01671994⟩