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.
-
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 thehammer
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.
-
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 thesauto
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 tosauto
, the current main limitation ofhammer
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:
- Vampire: https://vprover.github.io.
- CVC4: http://cvc4.cs.stanford.edu. CVC4 needs to be version 1.6 or later. Earlier versions do not fully support the TPTP format. It is recommended to have the better-performing GPL version of CVC4 instead of the BSD version.
- Eprover: http://www.eprover.org.
- Z3:
https://github.com/Z3Prover/z3/releases. Note
that the default version of Z3 does not support the TPTP format. You
need to compile the TPTP frontend located in
examples/tptp
in the Z3 source package.
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:
- solvers:
sdone
,strivial
,qauto
,hauto
,sauto
; - simplifiers:
simp_hyps
,sintuition
,qsimpl
,ssimpl
.
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
.
-
use: <term-list>
Add the listed lemmas at the top of the context. Default:
use: -
. -
inv: <ind-list>
Try performing inversion (case reasoning) on values of the listed inductive types. Default:
inv: *
.This does not affect inversion for the inductive types representing logical connectives. Use
inv: never
to prevent inversion for logical connectives. -
ctrs: <ind-list>
Try using constructors of listed inductive types. Default:
ctrs: *
.This does not affect constructors of the inductive types representing logical connectives. Use
ctrs: never
to prevent using constructors of logical connectives. -
unfold: <const-list>
Try unfolding the listed definitions based on heuristic criteria. Default:
unfold: -
.This does not affect
iff
andnot
which are treated specially and always unfolded. Useunfold: never
to prevent this behaviour. -
unfold!: <const-list>
Always unfold the listed definitions. A primitive version of
unfold:
without heuristics. Default:unfold!: -
. -
db: <db-list>
Use the listed hint databases (accepts both
auto
andautorewrite
hint databases). Default:db: -
. -
hint:db: <db-list>
Use the listed
auto
hint databases. Default:hint:db: -
. -
rew:db: <db-list>
Use the listed
autorewrite
hint databases. Default:rew:db: -
. -
cases: <ind-list>
Eliminate discriminees in case expressions when the discriminee has one of the listed inductive types. If
ecases: on
then elimination of match disciminees is performed eagerly, otherwise with backtracking. Default:cases: *
,ecases: on
. -
split: <sind-list>
Eagerly apply constructors of the listed “simple” inductive types. An inductive type is “simple” if it is non-recursive with exactly one constructor, and such that the application of the constructor does not introduce new existential variables. Default:
split: -
.This does not affect inductive types representing logical connectives. Use
split: never
to prevent eager applications of constructors of “simple” inductive types representing logical connectives (i.e., conjunction and existential quantification). -
limit: <number>
Limit the cost of the entire proof tree. Note that this does not directly limit the depth of proof search, but only the cost of the whole proof tree, according to the cost model built into
sauto
. Default:limit: 1000
. -
depth: <number>
Directly limit the depth of proof search. Cancels the
limit:
option. -
time: <number>
(since 1.3.1)Set the timeout in seconds. Currently, this is meaningful only for the
best
tactic where the default is 1 second. -
finish: <tactic>
Set a tactic to use at the leaves of the proof search tree. Default:
finish: (sfinal sdone)
. -
final: <tactic>
Shorthand for
finish: (sfinal <tactic>)
. Default:final: sdone
. -
simp: <tactic>
Set a tactic for additional simplification after context change. This option is for additional simplification - it has no impact on other simplifications performed by
sauto
. The defaultsimp:
tactic does not actually simplify but tries to fully solve the goal. Default:simp: (sfinal sdone)
. -
simp+: <tactic>
Add a tactic for additional simplification after context change, keeping all previously registered
simp:
tactics. -
ssimp: <tactic>
Set a tactic for additional strong simplification in
ssimpl
andqsimpl
. Default:ssimp: ssolve
. -
ssimp+: <tactic>
Add a tactic for additional strong simplification in
ssimpl
andqsimpl
, keeping all previously registeredssimp:
tactics. -
solve: <tactic>
Set a solver tactic to run at each node of the proof search tree. For instance, for goals involving real numbers one might use
solve: lra
. Default:solve: -
. -
solve+: <tactic>
Add a solver tactic to run at each node of the proof search tree, keeping all previously registered
solve:
tactics. -
fwd: <bopt>
Controls whether to perform limited forward reasoning. Default:
fwd: on
. -
ecases: <bopt>
Controls whether elimination of discriminees in case expressions is performed eagerly. Default:
ecases: on
. -
sinv: <bopt>
Controls whether to use the “simple inverting” heuristic. This heuristic eagerly inverts all hypotheses
H : I
withI
inductive when the number of subgoals generated by the inversion is at most one. Default:sinv: on
. -
einv: <bopt>
Controls whether to use the “eager simple elimination restriction”, i.e., eagerly invert all hypotheses which have a non-recursive inductive type with arguments (parameters or indices). Default:
einv: on
. -
ered: <bopt>
Controls whether reduction (with
simpl
) is performed eagerly. Default:ered: on
. -
red: <bopt>
Controls whether to perform reduction with
simpl
. Whenred: on
, it depends on theered:
option if reduction is performed eagerly or with backtracking. Default:red: on
. -
erew: <bopt>
Controls whether directed rewriting is performed eagerly. Directed rewriting means rewriting with hypotheses orientable with LPO. If
erew: off
butdrew: on
, directed rewriting is still performed but with backtracking. Default:erew: on
. -
drew: <bopt>
Controls whether to perform directed rewriting. Default:
drew: on
. -
urew: <bopt>
Controls whether to perform undirected rewriting. Default:
urew: on
. -
rew: <bopt>
This is a compound option which controls the
drew
andurew
options. Settingdrew: on
impliesdrew: on
andurew: on
. Settingrew: off
impliesdrew: off
andurew: off
. Default:rew: on
. brefl: <bopt>
-
b: <bopt>
(since 1.3.1)Controls whether to perform boolean reflection, i.e., convert elements of
bool
applied tois_true
into statements inProp
. Settingbrefl: on
impliesecases: off
- usebrefl!:
to prevent this behaviour. You may also re-enableecases:
by providingecases: on
afterbrefl: on
. Default:brefl: off
.See also the Boolean reflection section.
brefl!: <bopt>
-
b!: <bopt>
(since 1.3.1)A primitive version of
brefl:
which when enabled does not automatically disableecases:
. -
sapp: <bopt>
Controls whether to use the
sapply
tactic for application. Thesapply
tactic performs application modulo simple equational reasoning. This increases the success rate, but decreases speed. Default:sapp: on
. -
exh: <bopt>
Controls whether to perform backtracking on instantiations of existential variables. Default:
exh: off
. -
lia: <bopt>
Controls whether to try the
lia
tactic for arithmetic subgoals. Default:lia: on
.Note that invoking
lia
is done via the defaultsimp:
andfinish:
tactics - if these tactics are changed thenlia:
has no effect. To re-enablelia
usesolve: lia
orsolve+: lia
. -
sig: <bopt>
Controls whether to (eagerly) perform simplifications for sigma-types (using the
simpl_sigma
tactic). Default:sig: on
. -
prf: <bopt>
Controls whether to (eagerly) generalize proof terms occurring in the goal or in one of the hypotheses. Default:
prf: off
. -
dep: <bopt>
Enhanced support for dependent types. When
on
, thedepelim
tactic from the Program module is used for inversion. This may negatively impact speed and introduce dependencies on some axioms equivalent to Uniqueness of Identity Proofs. Settingdep: on
impliesprf: on
,einv: off
andsinv: off
- usedep!:
to prevent this behaviour. You can also change theprf:
,einv:
andsinv:
options separately by setting them afterdep: on
. Default:dep: off
. -
dep!: <bopt>
A primitive version of
dep:
which when enabled does not affectprf:
,einv:
orsinv:
. eager: <bopt>
-
e: <bopt>
This is a compound option which controls multiple other options:
ered
,erew
,ecases
,einv
,sinv
,sig
. Settingeager: on
(ore: on
) has the effect of enabling all these options. Settingeager: off
disables all of the listed options. lazy: <bopt>
-
l: <bopt>
The exact opposite of
eager:
, i.e.,lazy: on
is justeager: off
, andlazy: off
is justeager: on
. quick: <bopt>
-
q: <bopt>
Setting
quick: on
(orq: on
) has the same effect as setting:sapp: off simp: idtac finish: sdone lia: off
Setting
quick: off
has no effect. -
lq: <bopt>
Settting
lq: on
has the same effect as settinglazy: on
andquick: on
. Settinglq: off
has no effect. lqb: <bopt>
(since 1.3.1)qb: <bopt>
(since 1.3.1)-
lb: <bopt>
(since 1.3.1)Compound options analogous to
lq:
.
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
.
-
sdestruct t
Destruct
t
in the “right” way, introducing appropriate hypotheses into the context and handling boolean terms correctly (automatically performing boolean reflection). -
dep_destruct t
Dependent destruction of
t
. A simple wrapper around thedependent destruction
tactic from the Program module. -
sinvert t
Inversion of the conclusion of
t
. The type oft
may be quantified - then new existential variables are introduced or new subgoals are generated for the arguments. -
sdepinvert t
Dependent inversion of the conclusion of
t
. The same assinvert t
but may use thedepelim
tactic for inversion. -
sapply t
Apply
t
modulo simple heuristic equational reasoning. See thesapp:
option. -
bool_reflect
Boolean reflection in the goal and in all hypotheses. See the Boolean reflection section.
-
use lem1, .., lemn
Add the listed lemmas at the top of the context and simplify them.
-
srun tac <sauto-options>
The
srun
tactical first interprets sauto options (see Options for sauto) and performssauto
initialisation, then runsunshelve solve [ tac ]
, and then tries to solve the unshelved subgoals withauto
,easy
anddo 10 constructor
.Only the following options are interpreted by
srun
:use:
,unfold:
,unfold!:
,brefl:
,brefl!:
,red:
,ered:
,sig:
. Other options have no effect.The
sauto
initialisation performed bysrun
executes the actions corresponding to the options listed here. The default values of the options are like forsauto
. -
sfinal tac
Perform “final” simplifications of the goal (simplifying hypotheses, eliminating universally quantified disjunctions and existentials) and solve all the resulting subgoals with
tac
. Thesfinal tac
tactic invocation fails iftac
does not solve some of the resulting subgoals. -
forwarding
Limited forward reasoning corresponding to the
fwd:
option. -
forward_reasoning n
Repeated forward reasoning with repetition limit
n
. This is similar to but not exactly the same asdo n forwarding
. -
simpl_sigma
Simplifications for sigma-types. Composed of two tactics:
destruct_sigma
which eagerly destructs all elements of subset types occurring as arguments to the first projection, andinvert_sigma
which is a faster but weaker version ofinversion_sigma
from the standard library. Thesimpl_sigma
tactic corresponds to thesig:
option. generalize proofs
generalize proofs in H
-
generalize proofs in *
Generalizes by proof terms occurring in the goal and/or a hypothesis. Corresponds to the
prf:
option. -
srewriting
Directed rewriting with the hypotheses which may be oriented using LPO. See the
drew:
anderew:
options. simple_inverting
-
simple_inverting_dep
Perform “simple inversion” corresponding to the
sinv:
option. The_dep
version may use thedepelim
tactic. eager_inverting
-
eager_inverting_dep
Perform “eager simple elimination” corresponding to the
einv:
option. The_dep
version may use thedepelim
tactic. case_split
-
case_split_dep
Eliminate one discriminee of a match expression occurring in the goal or in a hypothesis. The
_dep
version may use thedepelim
tactic. case_splitting
-
case_splitting_dep
Eagerly eliminate all discriminees of match expressions occurring in the goal or in a hypothesis. This corresponds to the action enabled by setting
cases: *
andecases: on
. The_dep
version may use thedepelim
tactic. -
simple_splitting
Eagerly apply constructors of “simple” inductive types - non-recursive inductive types with exactly one constructor such that application of the constructor does not introduce new existential variables. This corresponds to
split: *
. -
simple_splitting logic
Simple splitting for logical connectives only.
-
ssolve
The
ssolve
tactic is justsolve [ (intuition auto); try sfinal sdone; try congruence 24; try easy; try solve [ econstructor; sfinal sdone ] ].
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.
breflect
breflect in H
-
breflect in *
Perform boolean reflection - convert boolean statements (arguments of
is_true
) into propositions inProp
, and boolean comparisons (on basic types from the standard library) into the corresponding inductive types.The
breflect
tactic just performs generalised top-down rewriting (also under binders) with thebrefl
rewrite hint database. This allows for easy customisation of boolean reflection by adding lemmas expressing reflection of user-defined boolean predicates. For instance, suppose you have a boolean predicatesortedb : list nat -> bool
and a corresponding inductive predicate
sorted : list nat -> Prop
and a lemma
sortedb_sorted_iff : forall l : list nat, is_true (sortedb l) <-> sorted l
Then adding the rewrite hint
Hint Rewrite -> sortedb_sorted_iff : brefl.
will result in
breflect
automatically convertingis_true (sortedb l)
tosorted l
. This will then also be done bybool_reflect
and bysauto
withbrefl: on
, because these tactics internally usebreflect
. breify
breify in H
-
breify in *
The reverse of
breflect
. Uses thebreif
rewrite hint database. bsimpl
bsimpl in H
-
bsimpl in *
Simplify boolean expressions. This is just generalised top-down rewriting with the
bsimpl
database. bdestruct t
-
bdestruct t as H
Destruct a boolean term
t
in the “right” way, introducing an appropriate hypothesis into the context and automatically performing boolean reflection on it. The second form of the tactic provides an explicit name for the introduced hypothesis. A successful run ofbdestruct
always results in two subgoals with one new hypothesis in each. -
blia
Perform boolean reflection and then run
lia
.
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
Set/Unset Hammer Debug.
-
Set Hammer GSMode n.
The hammer may operate in one of two modes: gs-mode or the ordinary mode. If GSMode is set to n > 0 then n best strategies (combination of prover, prediction method and number of predictions) are run in parallel. Otherwise, if n = 0, then the ordinary mode is active and the number of machine-learning dependency predictions, the prediction method and whether to run the ATPs in parallel are determined by the options below (Hammer Predictions, Hammer PredictMethod and Hammer Parallel). It is advisable to set GSMode to the number of cores your machine has, plus/minus one. Default: 8.
-
Set Hammer Predictions n.
The number of predictions for machine-learning dependency prediction. Irrelevant if GSMode > 0. Default: 1024.
-
Set Hammer PredictMethod "knn"/"nbayes".
Irrelevant if GSMode > 0. Default: “knn”.
-
Set/Unset Hammer Parallel.
Run ATPs in parallel. Irrelevant if GSMode > 0. Default: on.
-
Set Hammer ATPLimit n.
ATP time limit in seconds. Default: 20s.
-
Set Hammer ReconstrLimit n.
Time limit for proof reconstruction. Default: 5s.
-
Set Hammer SAutoLimit n.
Before invoking external ATPs the hammer first tries to solve the goal using the
sauto
tactic with a time limit ofn
seconds. Default: 1s. -
Set/Unset Hammer Vampire/CVC4/Eprover/Z3.
-
Set Hammer PredictPath "/path/to/predict".
Default: “predict”.
-
Set/Unset Hammer FilterProgram.
Ignore dependencies from
Coq.Program.*
. Default: on. -
Set/Unset Hammer FilterClasses.
Ignore dependencies from
Coq.Classes.*
. Default: on. -
Set/Unset Hammer FilterHurkens.
Ignore dependencies from
Coq.Logic.Hurkens.*
. Default: on. -
Set Hammer MinimizationThreshold n.
The minimum number of dependencies returned by an ATP for which minimization is performed. Default: 8.
-
Set/Unset Hammer SearchBlacklist.
Ignore dependencies blacklisted with the
Search Blacklist
vernacular command. Default: on. -
Add/Remove Hammer Filter module.
Ignore dependencies from the given module. Since version 1.3.2.
-
Test Hammer Filter.
Print the currently ignored modules. Since version 1.3.2.
-
Set/Unset Hammer ClosureGuards.
Should guards be generated for types of free variables? Setting this to “on” typically harms the hammer success rate, but it may help with functional extensionality. Set this to “on” if you use functional extensionality and get many unreconstructible proofs. Default: off.
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
-
Ł. 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. -
Ł. Czajka, Practical proof search for Coq by type inhabitation, IJCAR 2020
This paper is the main reference for the
sauto
tactic. -
Ł. 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. -
Ł. Czajka, B. Ekici, C. Kaliszyk, Concrete Semantics with Coq and CoqHammer, CICM 2018
Related projects
-
SMTCoq connects Coq with external SAT and SMT solvers. In contrast, CoqHammer’s target external tools are general automated theorem provers (ATPs). CoqHammer never uses the “modulo theory” facilities of the SMT solvers it supports (CVC4 and Z3), effectively treating them as if they were general ATPs. If what you need is predominantly SMT theory reasoning (e.g. reasoning about linear arithmetic, bit vectors, arrays) then you might want to try SMTCoq.
-
Tactician is a tactic learner and prover for Coq. It uses machine learning methods to synthesise tactic scripts. In contrast, CoqHammer searches for proof terms directly in the logic of Coq. A limitation of CoqHammer (particularly of the
hammer
tactic which relies on first-order ATPs) is that it might perform poorly on some fragments of Coq’s logic. An approach based on tactic script synthesis is not directly limited in this way.In particular, by design CoqHammer never tries induction. If you are interested in automatically finding inductive proofs or in interactive tactic recommendation, then you might want to try Tactician. On the other hand, we expect CoqHammer to be generally stronger on the fragments of Coq’s logic that it can handle well (non-inductive, “close to” first-order, goal-directed proofs).
Copyright and license
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.