POPL 2016 was just held a few weeks ago in Saint Petersburg, Florida, bringing together many researchers in programming languages to learn about the latest developments in the field. As usual, it was an exciting event for the Coq community. Early in the week, Robert Rand and I led an introductory Coq tutorial. Later, there was a special meeting to announce DeepSpec, an ambitious research effort to develop and integrate several verified software components, many of which use Coq. Near the end, Xavier Leroy received an award for the most influential POPL paper of 2006, for Formal Verification of a Compiler Back-end, where he introduced the CompCert verified C compiler.

Besides all these events, this year also featured the second edition of the CoqPL workshop. Its main attraction may have been the release of the long-awaited Coq 8.5. Matthieu Sozeau and Maxime Dénès gave a detailed presentation of its main new features, which include asynchronous proof checking and editing, universe polymorphism, and a new tactic engine. Congratulations to the Coq team for the great work!

Another fun talk was by Clément Pit-Claudel, where he announced company-coq, a set of Proof General extensions brings many nice editing features for Coq code in Emacs. These include: automatically prettifying code (for instance, replacing forall by ∀), auto-completion, code folding, and improved error messages, among many others. If you work with Coq under Emacs, you should definitely give it a try!

One important aspect of Coq's logic is the special status given to
computation: while some systems require one to apply explicit
deductive steps to show that two given terms are equal, Coq's logic
considers any two terms that evaluate to the same result to be equal
automatically, without the need for additional reasoning.

Without getting into too much detail, we can illustrate this idea with
some simple examples. Russell and Whitehead's seminal Principia
Mathematica had to develop hundreds
of pages of foundational mathematics before being able to prove
that 1+1=2. In contrast, here's what this proof looks like in
Coq:

erefl is the only constructor of the eq type; its type,
forallA(a:A),a=a, tells us that we can use it to prove that
given term a is equal to itself. Coq accepts one_plus_one as a
valid proof because, even though the two sides of the equation are not
syntactically the same, it is able to use the definition of + to
compute the left-hand side and check that the result is the same as
the right-hand side. This also works for some statements with
variables in them, for instance

The same principle applies here: + is defined by case analysis
on its first argument, and doesn't even need to inspect the second
one. Since the first argument on the left-hand side is a constructor
(0), Coq can reduce the expression and conclude that both sides are
equal.

Unfortunately, not every equality is a direct consequence of
computation. For example, this proof attempt is rejected:

What happened here? As mentioned before, + is defined by case
analysis on the first argument; since the first argument of the
left-hand side doesn't start with a constructor, Coq doesn't know how
to compute there. As it turns out, one actually needs an inductive
argument to prove this result, which might end up looking like this,
if we were to check the proof term that Coq produces:

It seems that, although interesting, computation inside Coq isn't
of much use when proving something. Or is it?

In this post, I will show how computation in Coq can be used to write
certified automation tactics with a technique known as proof by
reflection. Reflection is extensively used in Coq and in other proof
assistants as well; it is at the core of powerful automation tactics
such as ring, and played an important role in the formalization of
the Four-color
theorem. As a matter of fact, the name Ssreflect stands for
small-scale reflection, due to the library's pervasive use of
reflection and computation.

Let's see how reflection works by means of a basic (but interesting)
example: a tactic for checking equalities between simple expressions
involving natural numbers.

Arithmetic with reflection

Imagine that we were in the middle of a proof and needed to show that
two natural numbers are equal:

ring is powerful enough to solve this goal by itself, but just
for the sake of the example, suppose that we had to prove it by
hand. We could write something like

This was not terribly complicated, but there's certainly room for
improvement. In a paper proof, a mathematician would probably assume
that the reader is capable of verifying this result on their own,
without any additional detail. But how exactly would the reader
proceed?

In the case of the simple arithmetic expression above, it suffices to
apply the distributivity law as long as possible, until both
expressions become a sum of monomials. Then, thanks to associativity
and commutativity, we just have to reorder the factors and terms and
check that both sides of the equation match.

The idea of proof by reflection is to reduce a the validity of a
logical statement to a symbolic computation, usually by proving a
theorem of the form thm:b=true->P with b:bool. If b can
be computed explicitly and reduces to true, then Coq recognizes
erefl as a proof of b=true, which means that thmerefl becomes
a proof of P.

To make things concrete, let's go back to our example. The idea that
we described above for checking whether two numbers are equal can be
used whenever we have expressions involving addition, multiplication,
and variables. We will define a Coq data type for representing such
expressions, as we will need to compute with them:

Variables are represented by natural numbers using the Var
constructor, and Add and Mul can be used to combine
expressions. The following term, for instance, represents the
expression n*(m+n):

Here, each monomial is represented by a list enumerating all
variables that occur in it, counting their multiplicities. Hence, a
sum of monomials is represented as a list of lists. For example,
here's the result of normalizing expr_ex:

To prove that monoms has the intended behavior, we show that the
value of an expression is preserved by it. By using the big operations
\sum and \prod from the MathComp library, we can compute the value
of a sum of monomials very easily:

Hence, to check that two expressions are equivalent, it suffices
to compare the results of monoms, modulo the ordering. We can do
this by sorting the variable names on each monomial and then testing
whether one list of monomials is a permutation of the other:

The first argument to our lemma assigns "real" variables to
variable numbers: 0 corresponds to n (the first element of the
list), 1 to m, and 2 to p. The second and third argument are
symbolic representations of the left and right-hand sides of our
equation. The fourth argument is the most interesting one: the
expr_eq was defined as a boolean function that returns true when
its two arguments are equivalent expressions. As we've seen above,
this means that whenever expr_eqe1e2 computes to true, erefl
is a valid proof of it. Finally, when Coq tries to check whether the
conclusion of expr_eqP can be used on our goal, it computes
nat_of_expr on both sides, realizing that the conclusion and the
goal are exactly the same. For instance:

Of course, expr_eqP doesn't force its first argument to always
return actual Coq variables, so it can be applied even in some cases
where the expressions contain other operators besides + and *:

At this point, it may seem that we haven't gained much from using
expr_eqP, since the second proof of our example was much bigger than
the first one. This is just an illusion, however, as the proof term
produced on the first case is actually quite big:

lem = funnmp : nat =>
(fun_evar_0_ : n * p + m * p = p * m + p * n => eq_ind_r (eq^~ (p * m + p * n)) _evar_0_ (mulnDlnmp))
((fun_evar_0_ : p * n + m * p = p * m + p * n => eq_ind_r
(fun_pattern_value_ : nat => _pattern_value_ + m * p = p * m + p * n) _evar_0_ (mulnCnp))
((fun_evar_0_ : p * n + p * m = p * m + p * n => eq_ind_r
(fun_pattern_value_ : nat => p * n + _pattern_value_ = p * m + p * n) _evar_0_
(mulnCmp))
((fun_evar_0_ : p * m + p * n = p * m + p * n => eq_ind_r (eq^~ (p * m + p * n)) _evar_0_ (addnC (p * n) (p * m)))
(erefl (p * m + p * n)))))
: forallnmp : nat, (n + m) * p = p * m + p * n

By using reflection, we were able to transform the explicit reasoning
steps of the first proof into implicit computation that is carried out
by the proof assistant. And since proof terms have to be stored in
memory or included into the compiled vo file, it is good to make
them smaller if we can.

Nevertheless, even with a smaller proof term, having to manually type
in that proof term is not very convenient. The problem is that Coq's
unification engine is not smart enough to infer the symbolic form of
an expression, forcing us to provide it ourselves. Fortunately, we can
use some code to fill in the missing bits.

Reification

To reify something means to produce a representation of that object
that can be directly manipulated in computation. In our case, that
object is a Gallina expression of type nat, and the representation
we are producing is a term of type expr.

Reification is ubiquitous in proofs by reflection. The Coq standard
library comes with a plugin
for reifying formulas, but it is not general enough to accommodate our
use case. Therefore, we will program our own reification tactic in
ltac.

We will begin by writing a function that looks for a variable on a
list and returns its position. If the variable is not present, we add
it to the end of the list and return the updated list as well:

Notice the call to evalsimpl on the first branch of
loop. Remember that in ltac everything is matched almost purely
syntactically, so we have to explicitly evaluate a term when we are
just interested on its value, and not on how it is written.

We can now write a tactic for reifying an expression. reify_expr
takes two arguments: a list vars to be used with intern for
reifying variables, plus the expression e to be reified. It returns
a pair (e',vars') contained the reified expression e' and an
updated variable list vars'.

Again, because this is an ltac function, we can traverse our
Gallina expression syntactically, as if it were a data
structure. Notice how we thread though the updated variable lists
after each call; this is done to ensure that variables are named
consistently.

Finally, using reify_expr, we can write solve_nat_eq, which
reifies both sides of the equation on the goal and applies expr_eqP
with the appropriate arguments.

We have seen how we can use internal computation in Coq to write
powerful tactics. Besides generating small proof terms, tactics that
use reflection have another important benefit: they are mostly written
in Gallina, a typed language, and come with correctness proofs. This
contrasts with most custom tactics written in ltac, which tend to
break quite often due to the lack of static guarantees (and to how
unstructure the tactic language is). For solve_nat_eq, we only had
to write the reification engine in ltac, which results in a more
manageable code base.

If you want to learn more about reflection, Adam Chlipala's CPDT book has an entire
chapter devoted to the subject, which I highly recommend.

Guillaume Claret, a Ph.D. student in Paris, has also a blog devoted to Coq. You can find some good articles in there, such as this one, explaining how to use OPAM as a package manager for Coq.

Ömer’s blog has a lot of general programming-languages and functional-programming material. This post, for instance, presents a simple exercise in dependently typed programming.