SMTCoq

Communication between Coq and SAT/SMT solvers

SMTCoq

Presentation

SMTCoq is a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:

Installation and use

SMTCoq is freely available as an opam package and on GitHub. See the INSTALL.md file for instructions on how to install SMTCoq and the supported provers.

See the examples to see how to use SMTCoq. More details are given in the USE.md file.

SMTCoq is distributed under the CeCILL-C license.

Community

If you have any question or remark, you are invited to join the SMTCoq forum.

Bugs can be reported on github.

Example

Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory.

From SMTCoq Require Import SMTCoq.

Section Group.
  Variable G : Type.
  (* We suppose that G has a decidable equality *)
  Variable HG : CompDec G.
  Variable op : G -> G -> G.
  Variable inv : G -> G.
  Variable e : G.

  Local Notation "a ==? b" := (@eqb_of_compdec G HG a b) (at level 60).

  (* We can prove automatically that we have a group if we only have the
     "left" versions of the axioms of a group *)
  Hypothesis associative :
    forall a b c : G, op a (op b c) ==? op (op a b) c.
  Hypothesis inverse :
    forall a : G, op (inv a) a ==? e.
  Hypothesis identity :
    forall a : G, op e a ==? a.
  Add_lemmas associative inverse identity.

  Lemma inverse' :
    forall a : G, op a (inv a) ==? e.
  Proof. smt. Qed.

  Lemma identity' :
    forall a : G, op a e ==? a.
  Proof. smt inverse'. Qed.

  Lemma unique_identity e':
    (forall z, op e' z ==? z) -> e' ==? e.
  Proof. intros pe'; smt pe'. Qed.

  Clear_lemmas.
End Group.

Extension of SMTCoq

A project called Sniper is currently developed to extend the number of Coq goals that SMTCoq is able to handle. It is based on small, compositional and certifying pre-processing transformations, combined together to translate some Coq goals into the logic handled by SMTCoq, the first-order logic. Have a look at the website !

Want to participate?

SMTCoq is an ambitious, collaborative project: everyone is welcome! There are many and varied enhancement to do: join the SMTCoq forum to discuss!

People

Current team

Past contributors

Publications

Reference

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin, CPP - Certified Programs and Proofs - First International Conference - 2011.

Other publications

  1. SMTCoq: A plug-in for integrating SMT solvers into Coq (Tool Paper), Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark, CAV - International Conference on Computer Aided Verification - 2017.
  2. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), Ekici, Burak; Katz, Guy; Keller, Chantal; Mebsout, Alain; Reynolds, Andrew; Tinelli, Cesare, HaTT - on Hammers for Type Theories - First International Workshop - 2016.
  3. Verifying SAT and SMT in Coq for a fully automated decision procedure, Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Werner, Benjamin, PSATTT - International Workshop on Proof-Search in Axiomatic Theories and Type Theories - 2011.
  4. SMTCoq : automatisation expressive et extensible dans Coq, Blot, Valentin; Bousalem, Amina; Garchery, Quentin; Keller, Chantal, JFLA - Journées Francophones des Langages Applicatifs - 2019.

Talk

Overview of SMTCoq (February, 2019)