We are happy to announce the release of CoqHammer 1.2.1 for Coq 8.10 and Coq 8.11.
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., sauto and scrush):
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 hammer.
For the best experience using the hammer, users should install all supported automated provers (Vampire, CVC4, Eprover, and Z3) according to the instructions.