Coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
Install / Use
/learn @lukaszcz/CoqhammerREADME
CoqHammer (dev) for Rocq 9.1 (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.
-
The
sautogeneral proof search tactic for the Calculus of Inductive Construction. -
The
hammerautomated 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 thesautoprocedure.
See the CoqHammer webpage for documentation and installation instructions.
Requirements
Copyright and license
Copyright (c) 2017-2025, 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.
Related Skills
imsg
337.7kiMessage/SMS CLI for listing chats, history, and sending messages via Messages.app.
node-connect
337.7kDiagnose OpenClaw node connection and pairing failures for Android, iOS, and macOS companion apps
oracle
337.7kBest practices for using the oracle CLI (prompt + file bundling, engines, sessions, and file attachment patterns).
lobster
337.7kLobster Lobster executes multi-step workflows with approval checkpoints. Use it when: - User wants a repeatable automation (triage, monitor, sync) - Actions need human approval before executing (s
