CoqHammer (dev) for Rocq 9.2 (use other branches for other versions of Rocq)

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

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.

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.

See the CoqHammer webpage for documentation and installation instructions.

Premise selection options

• Set Hammer DefinitionPremises K. reserves bounded slots within each predictor premise budget for accessible definitions referenced by the goal or hypotheses (including grouped inductives and constructors). Candidates are ordered by rarity, then size and name. At most K and one eighth of the budget (rounded up) are reserved; the predictor fills the remaining slots, so these definitions do not increase the budget. The default is 32; 0 disables reserved definition premises.
• Set Hammer DefinitionFeatures G. expands the predictor query with the plain constant dependencies taken from definitions of rare seed constants mentioned by the goal or hypotheses. A seed constant is expanded when at most G accessible definitions refer to it. The default is 16; 0 disables definition-feature expansion.

Unset Hammer DefinitionPremises. and Unset Hammer DefinitionFeatures. restore their respective defaults.

Requirements

• Rocq 9.2
• for hammer: automated provers (Vampire, CVC4, Eprover, and/or Z3)

Copyright and license

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

Distributed under the terms of LGPL 2.1, see the file LICENSE.

See CREDITS for a full list of contributors.