SMTCoq: Mixing Automatic and Interactive Proof Technologies

SMTCoq is a plugin for the Coq interactive theorem prover to work in conjunction with automated theorem provers based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), in an efficient and expressive way. As such, it allows one to formally establish, in a proof assistant, mathematical results relying on large combinatorial properties that require automatic Boolean reasoning. To this end, the huge SAT proofs coming from such problems can be safely checked in Coq and combined with standard mathematical Coq developments in a generic and modular way, for instance to obtain a formal proof of the Erdős Discrepancy Conjecture. To achieve this objective with the same degree of safety as Coq itself, SMTCoq communicates with SAT and SMT solvers that, in addition to a yes/no answer, can output traces of their internal proof search. The heart of SMTCoq is thus a certified, efficient and modular checker for such traces expressed in a format that can encompass most aspects of SMT reasoning. Preprocessors—that need not be certified—for proof traces coming from the state-of-the-art SMT solvers CVC4 and veriT and SAT solvers zChaff and Glucose are implemented. Coq can thus work in conjunction with widely used provers. From a proof assistant perspective, SMTCoq also provides a mechanism to let Coq users enjoy automation provided by external provers.