Intro Tutorial Installation Sauto   Options   Tactics   Reflection Hammer   Options   Debugging Papers Related About

CoqHammer is an automated reasoning tool for Coq. It helps in your search for Coq proofs.

Since version 1.3, the CoqHammer system consists of two major separate components.

  1. The sauto general proof search tactic for the Calculus of Inductive Construction.

    A “super” version of auto. The underlying proof search procedure is based on a fairly general inhabitation procedure for the Calculus of Inductive Constructions. While it is in theory complete only for a “first-order” fragment of CIC, in practice it can handle a much larger part of Coq’s logic. In contrast to the hammer tactic, sauto can use only explicitly provided lemmas and it does not invoke any external ATPs. For effective use, sauto typically needs some configuration by providing appropriate options.

    See the Sauto section below.

  2. The hammer automated reasoning tool which combines learning from previous proofs with the translation of problems to the logics of external automated systems and the reconstruction of successfully found proofs with the sauto procedure.

    A typical use is to prove relatively simple goals using available lemmas. The problem is to find appropriate lemmas in a large collection of all accessible lemmas and combine them to prove the goal. The advantage of a hammer is that it is a general tool not depending on any domain-specific knowledge and not requiring configuration by the user. The hammer tactic may use all currently accessible lemmas, including those proven earlier in a given formalization, not only the lemmas from predefined libraries or hint databases. At present, however, best results are achieved for statements “close to” first-order logic and lemmas from the standard library or similar. In comparison to sauto, the current main limitation of hammer is its poor effectiveness on problems heavily dependent on non-first-order features of Coq’s logic (e.g. higher-order functions, boolean reflection or sophisticated uses of dependent types).

    See the Hammer section below.

Tutorial

CoqHammer video tutorial: part 1 (sauto), part 2 (hammer).

The tutorial files are available here.

Most useful sauto options: use:, inv:, ctrs:, unfold:, db:, l:, q:, lq:, brefl:, dep:. Use your browser’s “find” function to search for their descriptions in the Options for sauto section of this page.

The best tactic (since 1.3.1) automatically finds the best options for sauto. It doesn’t, however, find the dependencies: lemmas (use:), inversions (inv:), constructors (ctrs:), or unfoldings (unfold:). The hammer tactic tries to find the dependencies automatically.

Note that sauto or hammer never perform induction. When induction is needed, it must be done manually.

See also a formalisation of various sorting algorithms with sauto: https://github.com/lukaszcz/sortalgs.

Installation

CoqHammer can be installed via opam (recommended) or from source. To use the hammer tactic you also need to install some provers.

CoqHammer has been tested on Linux and Mac OS X.

Note that some old versions of Proof General encounter problems with the plugin. If you use Proof General you might need the most recent version obtained directly from https://proofgeneral.github.io.

Opam installation

The latest release of CoqHammer is most easily installed via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-hammer

If you are only interested in sauto and related tactics, they can be installed standalone (without the hammer plugin) via OPAM after adding the coq-released repository as above:

opam install coq-hammer-tactics

Manual installation

To instead build and install CoqHammer manually, download the latest CoqHammer release from GitHub, unpack it and run make followed by make install. Then optionally run make tests to check if everything works. Some of the tests may fail if your machine is not fast enough or you do not have all provers installed.

To instead build and install the tactics manually, use make tactics followed by make install-tactics. The tactics may be tested with make test-tactics.

The command make install tries to install the predict and htimeout programs into the directory specified by the COQBIN environment variable. If this variable is not set then a binary directory is guessed basing on the Coq library directory.

Installation of first-order provers

To use the hammer tactic you need at least one of the following ATPs available in the path (under the command name in brackets): Vampire (vampire), CVC4 (cvc4), Eprover (eprover), Z3 (z3_tptp). It is recommended to have all four ATPs, or at least Vampire and CVC4.

The websites for the provers are:

Sauto

The Tactics module contains sauto and related tactics. These tactics are used by the hammer tool for proof reconstruction. To use them directly in your proof scripts first include:

From Hammer Require Import Tactics.

The easiest way to use sauto is via the best tactic (since 1.3.1). The best tactic tries a number of sauto variants with different options (see Options for sauto). However, familiarity with different tactics from the Tactics module and with various sauto options often results in more effective use.

Note that sauto and related tactics never perform induction. When induction is needed, it must be done manually.

The Tactics module provides “solvers” which either solve the goal or fail, and “simplifiers” which simplify the goal but do not perform backtracking proof search. The simplifiers never fail. The solvers are based on variants of the sauto tactic or its sub-components. The simplifiers are based on variants of the heuristics and simplifications performed by sauto upon context change.

Below we list the solvers and the simplifiers in the order of increasing strength and decreasing speed:

The hauto tactic is just sauto inv: - ctrs: -. The qauto tactic is just hauto quick: on limit: 100 finish: (eauto; congruence 400).

See the Options for sauto section for an explanation of these options.

The sdone tactic is used by sauto as the final tactic at the leaves of the proof search tree (see the final: and finish: options). The strivial tactic is just srun (sfinal sdone). The srun and sfinal tactics are described in the Extra tactics section.

Additional variants of the solvers are used in the reconstruction backend of the hammer tactic. The solvers listed here are the ones most suited for standalone use.

Some examples are available here.

Options for sauto

Most useful sauto options: use:, inv:, ctrs:, unfold:, db:, l:, q:, lq:, brefl:, dep:. Use your browser’s “find” function to search for their descriptions in this section.

The best tactic (since 1.3.1) automatically finds the best options for sauto. It doesn’t, however, find the dependencies: lemmas (use:), inversions (inv:), constructors (ctrs:), or unfoldings (unfold:). The hammer tactic tries to find the dependencies automatically.

The best tactic accepts the same options as sauto - the provided options are appended to the options of the tried variants of sauto, possibly overriding them. For example, if you want to automatically find the best variant of sauto which performs search up to depth 3 and uses lemma lem1 then write:

best depth: 3 use: lem1

Note that immediately upon success you are supposed to replace the best tactic with the tactic shown in the response window.

The sauto options take arguments specified by:

<bopt> ::= on | off
<db> ::= <hintDb> | <rewDb>
<X-list> ::= <X>, .., <X> | - | *

Additionaly, <number> denotes a natural number, <term> a Coq term, <const> a Coq constant, <ind> an inductive type, <hintDb> a hint database, <rewDb> a rewriting hint database, <tactic> a tactic. For a list, - denotes the empty list, * denotes the list of all available objects of a given type (e.g., * for <ind-list> denotes the list of all inductive types).

Below is a list of options for sauto and its variants. The defaults are for sauto.

Extra tactics

In addition to the solvers and the simplifiers listed above, the Tactics module contains a number of handy tactics which are used internally by sauto.

Boolean reflection

Importing the Reflect module with

From Hammer Require Import Reflect.

declares is_true as a coercion and makes available the following tactics related to boolean reflection.

Hammer

In your Coq file editor or toplevel (e.g., coqide or coqtop), first load the hammer plugin:

From Hammer Require Import Hammer.

The available commands are:

command description
hammer Runs the hammer tactic.
predict n Prints n dependencies for the current goal predicted by the machine-learning premise selection.
Hammer_version Prints the version of CoqHammer.
Hammer_cleanup Resets the hammer cache.

This directory contains some examples.

The intended use of the hammer tactic is to replace it upon success with the reconstruction tactic shown in the response window. This reconstruction tactic has no time limits and makes no calls to external ATPs. The success of the hammer tactic itself is not guaranteed to be reproducible. If all uses of hammer in a file have been replaced with reconstruction tactics, it is recommended to ensure that only the Tactics module is loaded and not the hammer plugin.

Note that hammer never performs induction. If induction is needed, it must be done manually before invoking hammer.

Hammer options

Debugging hammer

The following commands are useful for debugging the hammer tactic.

command description
Set Hammer Debug Makes hammer print diagnostic info.
Hammer_print "name" Prints object name in hhterm format.
Hammer_transl "name" Prints all axioms resulting from the translation of name in the intermediate coqterm format accepted by the tptp_out.ml module.
hammer_transl Prints all axioms resulting from the translation of the current goal.
Hammer_features "name" Prints the features of name, bypassing the cache.
Hammer_features_cached "name" Prints the features of name, using and possibly modifying the cache.
hammer_features Prints the features of the current goal.
Hammer_objects Prints the number of accessible objects.

Papers about CoqHammer

  1. Ł. Czajka, C. Kaliszyk, Hammer for Coq: Automation for Dependent Type Theory, Journal of Automated Reasoning, 2018

    This paper is the main reference for the hammer tactic.

  2. Ł. Czajka, Practical proof search for Coq by type inhabitation, IJCAR 2020

    This paper is the main reference for the sauto tactic.

  3. Ł. Czajka, A Shallow Embedding of Pure Type Systems into First-order Logic, TYPES 2016

    This paper proves soundness of a core version of the translation used by the hammer tactic.

  4. Ł. Czajka, B. Ekici, C. Kaliszyk, Concrete Semantics with Coq and CoqHammer, CICM 2018

Copyright (c) 2017-2021, Lukasz Czajka, TU Dortmund University.
Copyright (c) 2017-2018, Cezary Kaliszyk, University of Innsbruck.

Distributed under the terms of LGPL 2.1.

See CREDITS for a full list of contributors.