SMTCoq

Communication between Coq and SAT/SMT solvers

C API for SMTCoq - Tutorial

Start with installing the API and reading the introductory example of the documentation (no need to read the “Advanced details” section or the full documentation of the API at this stage).

Tip: When doing the exercises, if you observe that the certified checker answers false, do not hesitate to use the debugging checker.

Propositional logic

(*) Exercise 1

Modify the introductory example of the documentation so that, instead of asserting a ∧ ¬a, there are two assertions: a and ¬a. Modify the certificate accordingly.

Tip

Fewer rule kinds are needed for the certificate.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();
  FUNSYM asymb = funsym("a", 0, NULL, sort("Bool"));
  declare_fun(asymb);
  EXPR a = efun(asymb, NULL);

  /* Two assertions instead of one */
  assertf(a);
  assertf(enot(a));

  /* The two assumptions already prove steps 2 and 3 */
  CERTIF step2 = cassume("step2", 0);   // Proves the clause `a`
  CERTIF step3 = cassume("step3", 1);   // Proves the clause `¬a`
  CERTIF clauses[2] = {step2, step3};
  CERTIF step4 = cresolution("step4", 2, clauses);   // Proves the empty clause
  assert(check_proof(step4));
  return 0;
}

(*) Exercise 2

Check a proof of the unsatisfiability of the conjunction of the two assertions a ∧ ¬b and ¬a ∧ b.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* The two variables */
  FUNSYM asymb = funsym("a", 0, NULL, sort("Bool"));
  declare_fun(asymb);
  EXPR a = efun(asymb, NULL);
  FUNSYM bsymb = funsym("b", 0, NULL, sort("Bool"));
  declare_fun(bsymb);
  EXPR b = efun(bsymb, NULL);

  /* The two assertions */
  EXPR args1[2] = {a, enot(b)};
  assertf(eand(2, args1));
  EXPR args2[2] = {enot(a), b};
  assertf(eand(2, args2));

  /* Certificate: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);

  /* Certificate: only one side of each conjunction is useful */
  CERTIF and0 = cand("and0", ass0, 1);
  CERTIF and1 = cand("and1", ass1, 1);

  /* Certificate: resolution */
  CERTIF res[2] = {and0, and1};
  CERTIF proof = cresolution("proof", 2, res);

  /* Proof checking */
  assert(check_proof(proof));
  return 0;
}

(*) Exercise 3

Read the documentation about disjunctive expressions and the or rule.

Check a proof of the unsatisfiability of the conjunction of the two assertions a ∧ ¬b and ¬a ∨ b.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* The two variables */
  FUNSYM asymb = funsym("a", 0, NULL, sort("Bool"));
  declare_fun(asymb);
  EXPR a = efun(asymb, NULL);
  FUNSYM bsymb = funsym("b", 0, NULL, sort("Bool"));
  declare_fun(bsymb);
  EXPR b = efun(bsymb, NULL);

  /* The two assertions */
  EXPR args1[2] = {a, enot(b)};
  assertf(eand(2, args1));
  EXPR args2[2] = {enot(a), b};
  assertf(eor(2, args2));

  /* Certificate: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);

  /* Certificate: both sides of the conjunction of the first assertion
     are useful */
  CERTIF and0 = cand("and0", ass0, 1);
  CERTIF and1 = cand("and1", ass0, 2);

  /* Certificate: decompose the disjunction of the second assertion */
  CERTIF or = cor("or", ass1);

  /* Certificate: resolution */
  CERTIF res[3] = {or, and0, and1};
  CERTIF proof = cresolution("proof", 3, res);

  /* Proof checking */
  assert(check_proof(proof));
  return 0;
}

(**) Exercise 4

Read the Wikipedia page of the pigeonhole principle. State the principle for 1 hole and 2 pigeons, and prove that it is unsatisfiable.

Tip 1

One can use 2 Boolean variables: xi represents the fact that pigeon i is in the hole.

Tip 2

There are two conditions:

  1. every pigeon must be in the hole
  2. the hole cannot contain two pigeons
Tip 3

The two conditions can be translated as:

  1. x1 and x2 are true
  2. ¬x1 ∨ ¬x2 is true
Tip 4

The proof consists in destroying the disjunction in condition 2, then resolving with the two conditions 1.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* The 2 variables */
  FUNSYM x1symb = funsym("x1", 0, NULL, sort("Bool"));
  FUNSYM x2symb = funsym("x2", 0, NULL, sort("Bool"));
  declare_fun(x1symb);
  declare_fun(x2symb);
  EXPR x1 = efun(x1symb, NULL);
  EXPR x2 = efun(x2symb, NULL);

  /* Every pigeon is in the hole */
  assertf(x1);
  assertf(x2);

  /* The hole cannot contain more than one pigeon */
  EXPR args[2] = {enot(x1), enot(x2)};
  assertf(eor(2, args));

  /* Certif: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);
  CERTIF ass2 = cassume("ass2", 2);

  /* Certif: or rule */
  CERTIF or = cor("or", ass2);

  /* Certif: resolution */
  CERTIF res[3] = {or, ass0, ass1};
  CERTIF proof = cresolution("proof", 3, res);

  /* Check the proof */
  assert(check_proof(proof));
  return 0;
}

(***) Exercise 5

State the pigeonhole principle for 2 holes and 3 pigeons, and prove that it is unsatisfiable.

Tip 1

Again, one can use 6 Boolean variables: xij represents the fact that pigeon i is in hole j. The conditions are similar to Exercise 4.

Tip 2

First prove that pigeon 1 is in hole 1.

Tip 3

Then deduce that pigeon 2 cannot be in hole 1, and that pigeon 3 cannot be in hole 1.

Tip 4

Then deduce that pigeon 2 must be in hole 2, and that pigeon 3 must also be in hole 2. Conclude.

Tip 5

Do not forget to break ors first.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* The 6 variables */
  FUNSYM x11symb = funsym("x11", 0, NULL, sort("Bool"));
  FUNSYM x12symb = funsym("x12", 0, NULL, sort("Bool"));
  FUNSYM x21symb = funsym("x21", 0, NULL, sort("Bool"));
  FUNSYM x22symb = funsym("x22", 0, NULL, sort("Bool"));
  FUNSYM x31symb = funsym("x31", 0, NULL, sort("Bool"));
  FUNSYM x32symb = funsym("x32", 0, NULL, sort("Bool"));
  declare_fun(x11symb);
  declare_fun(x12symb);
  declare_fun(x21symb);
  declare_fun(x22symb);
  declare_fun(x31symb);
  declare_fun(x32symb);
  EXPR x11 = efun(x11symb, NULL);
  EXPR x12 = efun(x12symb, NULL);
  EXPR x21 = efun(x21symb, NULL);
  EXPR x22 = efun(x22symb, NULL);
  EXPR x31 = efun(x31symb, NULL);
  EXPR x32 = efun(x32symb, NULL);

  /* Every pigeon is in a hole */
  EXPR p1[2] = {x11, x12};
  assertf(eor(2, p1));
  EXPR p2[2] = {x21, x22};
  assertf(eor(2, p2));
  EXPR p3[2] = {x31, x32};
  assertf(eor(2, p3));

  /* A hole cannot contain more than one pigeon */
  EXPR h1[2] = {enot(x11), enot(x21)};
  assertf(eor(2, h1));
  EXPR h2[2] = {enot(x11), enot(x31)};
  assertf(eor(2, h2));
  EXPR h3[2] = {enot(x21), enot(x31)};
  assertf(eor(2, h3));
  EXPR h4[2] = {enot(x12), enot(x22)};
  assertf(eor(2, h4));
  EXPR h5[2] = {enot(x12), enot(x32)};
  assertf(eor(2, h5));
  EXPR h6[2] = {enot(x22), enot(x32)};
  assertf(eor(2, h6));

  /* Certif: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);
  CERTIF ass2 = cassume("ass2", 2);
  CERTIF ass3 = cassume("ass3", 3);
  CERTIF ass4 = cassume("ass4", 4);
  CERTIF ass5 = cassume("ass5", 5);
  CERTIF ass6 = cassume("ass6", 6);
  CERTIF ass7 = cassume("ass7", 7);
  CERTIF ass8 = cassume("ass8", 8);

  /* Certif: or rules */
  CERTIF or0 = cor("or0", ass0);
  CERTIF or1 = cor("or1", ass1);
  CERTIF or2 = cor("or2", ass2);
  CERTIF or3 = cor("or3", ass3);
  CERTIF or4 = cor("or4", ass4);
  CERTIF or5 = cor("or5", ass5);
  CERTIF or6 = cor("or6", ass6);
  CERTIF or7 = cor("or7", ass7);
  CERTIF or8 = cor("or8", ass8);

  /* Certif: prove that pigeon 1 is in hole 1 */
  CERTIF res1[4] = {or0, or6, or1, or5};
  CERTIF reso1 = cresolution("reso1", 4, res1);
  CERTIF res2[4] = {or0, or7, or2, reso1};
  CERTIF reso2 = cresolution("reso2", 4, res2);

  /* Certif: deduce that pigeon 2 cannot be in hole 1, and that pigeon 3
     cannot be in hole 1 */
  CERTIF res3[2] = {reso2, or3};
  CERTIF reso3 = cresolution("reso3", 2, res3);
  CERTIF res4[2] = {reso2, or4};
  CERTIF reso4 = cresolution("reso4", 2, res4);

  /* Certif: deduce that pigeon 2 must be in hole 2, and that pigeon 3
     must also be in hole 2 */
  CERTIF res5[2] = {reso3, or1};
  CERTIF reso5 = cresolution("reso5", 2, res5);
  CERTIF res6[2] = {reso4, or2};
  CERTIF reso6 = cresolution("reso6", 2, res6);

  /* Conclude */
  CERTIF resp[3] = {or8, reso5, reso6};
  CERTIF proof = cresolution("proof", 3, resp);

  assert(check_proof(proof));
  return 0;
}

Equality

The theory of equality adds the = symbol and states that it is reflexive, symmetric, transitive, and congruent with respect to function and predicate symbols, independently of types.

Read the documentation about equality in expressions and defining new uninterpreted sorts.

(*) Exercise 6

Test the following program:

int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* An uninterpreted sort */
  SORT u = sort("U");
  declare_sort(u);

  /* Two variables of this sort */
  FUNSYM asymb = funsym("a", 0, NULL, u);
  declare_fun(asymb);
  EXPR a = efun(asymb, NULL);
  FUNSYM bsymb = funsym("b", 0, NULL, u);
  declare_fun(bsymb);
  EXPR b = efun(bsymb, NULL);

  /* Assert that `a = b` and `¬(b = a)` */
  assertf(eeq(a, b));
  assertf(enot(eeq(b, a)));

  /* Certificate: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);

  /* Certificate: resolution */
  CERTIF res[2] = {ass0, ass1};
  CERTIF proof = cresolution("proof", 2, res);

  /* Proof checking */
  assert(check_proof(proof));
  return 0;
}

What can you deduce from the way the SMTCoq checker treats symmetry of equality?

(**) Exercise 7

Read the documentation about the rules of reflexivity, transitivity, congruence with function symbols, and congruence with predicate symbols (and its variant).

Given an uninterpreted sort U, a variable a of type U, and a function symbol f : U → U, prove that the conjunction of x = f(x) and ¬(f(f(x)) = x) is unsatisfiable.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* The uninterpreted sort */
  SORT u = sort("U");
  declare_sort(u);

  /* A variable of this sort */
  FUNSYM asymb = funsym("a", 0, NULL, u);
  declare_fun(asymb);
  EXPR a = efun(asymb, NULL);

  /* A function symbol of type U → U */
  FUNSYM fsymb = funsym("f", 1, &u, u);
  declare_fun(fsymb);
  EXPR fa = efun(fsymb, &a);
  EXPR ffa = efun(fsymb, &fa);

  /* The two assertions */
  assertf(eeq(a, fa));
  assertf(enot(eeq(ffa, a)));

  /* Certificate: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);

  /* Certificate: congruence */
  EXPR clause[2] = {enot(eeq(a, fa)), eeq(fa, ffa)};
  CERTIF congr = ceq_congruent("congr", 2, clause);

  /* Certificate: transitivity */
  EXPR es[3] = {a, fa, ffa};
  CERTIF trans = ceq_transitive("trans", 3, es);

  /* Certificate: resolution */
  CERTIF res[4] = {congr, trans, ass0, ass1};
  CERTIF proof = cresolution("proof", 4, res);

  /* Proof checking */
  assert(check_proof(proof));
  return 0;
}

Other rules for equality

Read the documentation about the rules of reflexivity and congruence with predicate symbols, version 1 and version 2.

Linear integer arithmetic

Finally, the theory of linear integer arithmetic adds the sort "Int", integers, and operations on them. We refer the reader to the documentation of the expressions to visualize them.

SMTCoq’s checker integrates a powerful certifying linear arithmetic solver called Micromega, designed and implemented by Frédéric Besson. Thus, there is a single rule for this theory: lia_generic.

Note: The literals in the clause given to lia_generic may belong to multiple theories, but the proof that it is a tautology must use only linear integer arithmetic reasoning.

(**) Exercise 8

Given a function symbol f of type Int → Int, and two variable x and y of type Int, prove that the conjunction of y = x+1 and ¬(f(x) = f(y-1)) is unsatisfiable.

Tip

Remember that the sort "Int” is interpreted and can be defined using sort("Int"), as presented in the documentation about sorts.

Solution 
int main(int argc, char ** argv)
{
  caml_startup(argv);
  start_smt2();

  /* The two variables */
  SORT s = sort("Int");
  FUNSYM xsymb = funsym("x", 0, NULL, s);
  declare_fun(xsymb);
  EXPR x = efun(xsymb, NULL);
  FUNSYM ysymb = funsym("y", 0, NULL, s);
  declare_fun(ysymb);
  EXPR y = efun(ysymb, NULL);

  /* A function symbol of type Int → Int */
  FUNSYM fsymb = funsym("f", 1, &s, s);
  declare_fun(fsymb);
  EXPR fx = efun(fsymb, &x);
  EXPR yminone = eminus(y, eint(1));
  EXPR fyminone = efun(fsymb, &yminone);

  /* The two assertions */
  assertf(eeq(y, eadd(x, eint(1))));
  assertf(enot(eeq(fx, fyminone)));

  /* Certificate: assertions */
  CERTIF ass0 = cassume("ass0", 0);
  CERTIF ass1 = cassume("ass1", 1);

  /* Certificate: LIA */
  EXPR clauselia[2] = {enot(eeq(y, eadd(x, eint(1)))), eeq(x, eminus(y, eint(1)))};
  CERTIF lia = clia_generic("lia", 2, clauselia);

  /* Certificate: congruence */
  EXPR clause[2] = {enot(eeq(x, eminus(y, eint(1)))), eeq(fx, fyminone)};
  CERTIF congr = ceq_congruent("congr", 2, clause);

  /* Certificate: resolution */
  CERTIF res[4] = {congr, lia, ass0, ass1};
  CERTIF proof = cresolution("proof", 4, res);

  /* Proof checking */
  assert(check_proof(proof));
  return 0;
}