These releases include new automated reasoning tactics based on a general proof search procedure for the Calculus of Inductive Constructions, as described in a paper to appear in the proceedings of IJCAR 2020. The procedure is shown to be superior to many other general procedures, such as Coq’s
firstorder tactic, on a diverse set of problems derived from Coq libraries and CompCert.
To install only the standalone CoqHammer reconstruction tactics (e.g.,
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-hammer-tactics
These tactics can then be used in Coq files by including:
From Hammer Require Import Tactics.
To install the full hammer, including both the reconstruction tactics and the hammer plugin:
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-hammer
The hammer is then exposed through the
hammer tactic, which becomes available by including the following in Coq files:
From Hammer Require Import Hammer.
In a typical workflow, the user first tries the
hammer tactic which invokes one or more automated provers, and, if successful, prints a sequence of calls to reconstruction tactics that are meant to replace
For the best experience using the hammer, users should install all supported automated provers (Vampire, CVC4, Eprover, and Z3) according to the instructions.