HOLyHammer for HOL Light and HOL4, Sledgehammer for Isabelle/HOL, and other similar tools can have a huge impact on user productivity. These integrate automatic theorem provers (including SMT solvers) with proof assistants. However, users of proof assistants based on type theories, such as Agda, Coq, Lean, and Matita, currently miss out on this convenience. The expressive, constructive logic is often seen as an insurmountable obstacle, but large developments, including the CompCert compiler, typically postulate the classical axioms and use dependent types sparingly.
There has been some work in the direction of a hammer for Coq, but nothing that has really reached end users. Here is a partial list of relevant work:
- The SMTCoq integration of the SMT solver veriT, and ongoing work on extending this to CVC4, is perhaps the most serious integration of an automatic prover in a proof assistant based on type theory, but it is restricted to first-order logic.
- The why3 tactic in Coq integrates first-order provers with a first-order fragment of the calculus of inductive constructions extended with the classical axioms.
- The higher-order automatic theorem prover Satallax can produce Coq proof terms and scripts that rely on the classical axioms.
- A prototypical advisor, or relevance filter, has been developed and evaluated for Coq, yielding similar results as with other proof assistants.
- Although Mizar is based on set theory, it has a notion of dependent types, and there exists an encoding into classical first-order logic.
- An unpublished translation from the dependently typed F* dialect of ML to SMT-LIB has been developed.
- There is some ongoing work on adapting the OCaml version of the leanCoP prover to deliver intuitionistic proofs.
The HaTT workshop aims at gathering researchers working on these and other aspects of “hammer-style” automation for type theories, to exchange experiences and foster collaborations, to finally reach end users.
