CoqHammer

Automation for Dependent Type Theory

Coq logo
Hammer logo
universitat innsbruck

We present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is "sufficiently" sound and complete to be of practical use for automated theorem provers. We also introduce a proof reconstruction mechanism based on an eauto-type algorithm combined with limited rewriting, congruence closure and some forward reasoning. The algorithm is able to reprove in the Coq logic most of the theorems established by the ATPs. Together with machine-learning based selection of relevant premises this constitutes a full hammer system. The performance of the overall procedure is evaluated in a bootstrapping scenario emulating the development of the Coq standard library. For each theorem in the library only the previous theorems and proofs can be used. We show that 40.8% of the theorems can be proved in a push-button mode in about 40 seconds of real time on a 8-CPU system.

Download Plugin

  • Download from github (Coq 8.8.2 and recent trunk)
  • Download the plugin source for Coq 8.7 and 8.7.1 and 8.7.2
  • or
  • Download the plugin source for Coq 8.6 and 8.6.1
  • Follow the instructions in the included README file, in particular make sure you have the correct "timeout" and ATP provers installed
  • Has been tested with Linux and MacOS X
  • The version for older Coq (8.5) is incomplete/outdated

Papers

  • Ł. Czajka and C. Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory. Submitted to JAR.
    [   PDF   ]
    Download TPTP input and result files corresponding to the experiments.
  • Ł. Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. Submitted to TYPES.
    [   PDF   ]