When writing tactics, there are situations where it would be useful to know
whether a term begins with a constructor. One possibility is to extract the
head of the term and use the is_constructor tactic.

GoalTrue. (* These calls succeed *) head_constructor 0. head_constructor 1. (* ...but this one fails *) Failhead_constructor (1 + 1). (*
The command has indeed failed with message:
In nested Ltac calls to "head_constructor" and "is_constructor", last call failed.
Tactic failure: not a constructor.
*) Abort.

As of version 8.8, the is_constructor tactic is undocumented, but this
should hopefully be fixed soon. Interestingly, we can achieve almost the
same effect without is_constructor, by observing that Coq does not reduce
a fixpoint unless it is applied to a term that begins with a constructor.

Unlike the previous version, this one reduces the term using cbn before
testing it. Thus, the following test succeeds, while the analogous one
before failed:

Coq views truth through the lens of provability. The hypotheses it
manipulates are not mere assertions of truth, but formal proofs of the
corresponding statements ─ data structures that can be inspected to build
other proofs. It is not a coincidence that function types and logical
implication use the same notation, A->B, because proofs of implication
in Coq are functions: they take proofs of the precondition as inputs and
return a proof of the consequent as the output. Such proofs are written
with the same language we use for programming in Coq; tactics are but
scripts that build such programs for us. A proof that implication is
transitive, for example, amounts to function composition.

Definitionimplication_is_transitive (ABC : Prop) :
(A -> B) -> (B -> C) -> (A -> C) := funHABHBCHA => HBC (HABHA).

Similarly, inductive propositions in Coq behave just like algebraic data
types in typical functional programming languages. With pattern matching,
we can check which constructor was used in a proof and act accordingly.

Definitionor_false_r (A : Prop) : A \/ False -> A := fun (H : A \/ False) => matchHwith
| or_introlHA => HA
| or_introrcontra => matchcontrawithend end.

Disjunction \/ is an inductive proposition with two constructors,
or_introl and or_intror, whose arguments are proofs of its left and
right sides. In other words, a proof of A\/B is either a proof of A
or a proof of B. Falsehood, on the other hand, is an inductive
proposition with no constructors. Matching on a proof of False does not
require us to consider any cases, thus allowing the expression to have any
type we please. This corresponds to the so-called principle of
explosion, which asserts that from a contradiction, anything follows.

The idea of viewing proofs as programs is known as the Curry-Howard
correspondence. It has been a fruitful source of inspiration for the
design of many other logics and programming languages beyond Coq, other
noteworthy examples including Agda
and Nuprl. I will
discuss a particular facet of this correspondence in Coq: the meaning of a
proof of equality.

Defining equality

The Coq standard library defines equality as an indexed inductive
proposition. (The familiar x=y syntax is provided by the standard
library using Coq's notation mechanism.)

This declaration says that the most basic way of showing x=y is when x
and y are the "same" term ─ not in the strict sense of syntactic
equality, but in the more lenient sense of equality "up to computation" used
in Coq's theory. For instance, we can use eq_refl to show that 1+1=2, because Coq can simplify the left-hand side using the definition of +
and arrive at the right-hand side.

To prove interesting facts about equality, we generally use the rewrite
tactic, which in turn is implemented by pattern matching. Matching on
proofs of equality is more complicated than for typical data types because
it is a non-uniform indexed proposition ─ that is, the value of its last
argument is not fixed for the whole declaration, but depends on the
constructor used. (This non-uniformity is what allows us to put two
occurrences of x on the type of eq_refl.)

Concretely, suppose that we have elements x and y of a type T, and a
predicate P:T->Prop. We want to prove that Py holds assuming that
x=y and Px hold. This can be done with the following program:

Compared to common match expressions, this one has two extra clauses. The
first, in_=z, allows us to provide a name to the non-uniform argument
of the type of p. The second, returnPz, allows us to declare what the
return type of the match expression is as a function of z. At the top
level, z corresponds to y, which means that the whole match has type
Py. When checking each individual branch, however, Coq requires proofs
of Pz using values of z that correspond to the constructors of that
branch. Inside the eq_refl branch, z corresponds to x, which means
that we have to provide a proof of Px. This is why the use of H there
is valid.

To illustrate, here are proofs of two basic facts about equality:
transitivity and symmetry.

Definitionetrans {T} {xyz : T} (p : x = y) (q : y = z) : x = z := matchpin_ = wreturnw = z -> x = zwith
| eq_refl => funq' : x = z => q' endq.

Definitionesym {T} {xy : T} (p : x = y) : y = x := matchpin_ = zreturnz = xwith
| eq_refl => eq_refl end.

Notice the return clause in the first proof, which uses a function type. We
cannot use w=z alone, as the final type of the expression would be y=z. The other reasonable guess, x=z, wouldn't work either, since we
would have nothing of that type to return in the branch ─ q has type y=z, and Coq does not automatically change it to x=z just because we know
that x and y ought to be equal inside the branch. The practice of
returning a function is so common when matching on dependent types that it
even has its own name: the convoy pattern, a term coined by Adam Chlipala
in his CDPT
book.

In addition to functions, pretty much any type expression can go in the
return clause of a match. This flexibility allows us to derive many basic
reasoning principles ─ for instance, the fact that constructors are
disjoint and injective.

Definitioneq_Sn_m (nm : nat) (p : Sn = m) := matchpin_ = kreturnmatchkwith
| 0 => False
| Sm' => n = m' endwith
| eq_refl => eq_refl end.

Definitionsucc_not_zeron : Sn <> 0 := eq_Sn_mn 0.

Definitionsucc_injnm : Sn = Sm -> n = m := eq_Sn_mn (Sm).

In the eq_refl branch, we know that k is of the form Sn. By
substituting this value in the return type, we find that the result of the
branch must have type n=n, which is why eq_refl is accepted. Since
this is only value of k we have to handle, it doesn't matter that False
appears in the return type of the match: that branch will never be used.
The more familiar lemmas succ_not_zero and succ_inj simply correspond to
special cases of eq_Sn_m. A similar trick can be used for many other
inductive types, such as booleans, lists, and so on.

Mixing proofs and computation

Proofs can be used not only to build other proofs, but also in more
conventional programs. If we know that a list is not empty, for example, we
can write a function that extracts its first element.

FrommathcompRequireImportseq.

Definitionfirst {T} (s : seqT) (Hs : s <> [::]) : T := matchsreturns <> [::] -> Twith
| [::] => funHs : [::] <> [::] => matchHseq_reflwithend
| x :: _ => fun_ => x endHs.

Here we see a slightly different use of dependent pattern matching: the
return type depends on the analyzed value s, not just on the indices of
its type. The rules for checking that this expression is valid are the
same: we substitute the pattern of each branch for s in the return type,
and ensure that it is compatible with the result it produces. On the first
branch, this gives a contradictory hypothesis [::]<>[::], which we can
discard by pattern matching as we did earlier. On the second branch, we can
just return the first element of the list.

Proofs can also be stored in regular data structures. Consider for instance
the subset type {x:T|Px}, which restricts the elements of the type
T to those that satisfy the predicate P. Elements of this type are of
the form existxH, where x is an element of T and H is a proof of
Px. Here is an alternative version of first, which expects the
arguments s and Hs packed as an element of a subset type.

Definitionfirst' {T} (s : {s : seqT | s <> [::]}) : T := matchswith
| existsHs => firstsHs end.

While powerful, this idiom comes with a price: when reasoning about a term
that mentions proofs, the proofs must be explicitly taken into account. For
instance, we cannot show that two elements existxH1 and existxH2 are
equal just by reflexivity; we must explicitly argue that the proofs H1 and
H2 are equal. Unfortunately, there are many cases in which this is not
possible ─ for example, two proofs of a disjunction A\/B need to use
the same constructor to be considered equal.

The situation is not as bad as it might sound, because Coq was designed to
allow a proof irrelevance axiom without compromising its soundness. This
axiom says that any two proofs of the same proposition are equal.

If we are willing to extend the theory with this axiom, much of the pain of
mixing proofs and computation goes away; nevertheless, it is a bit upsetting
that we need an extra axiom to make the use of proofs in computation
practical. Fortunately, much of this convenience is already built into
Coq's theory, thanks to the structure of proofs of equality.

Proof irrelevance and equality

A classical result of type theory says that equalities between elements of a
type T are proof irrelevant provided thatT has decidable equality.
Many useful properties can be expressed in this way; in particular, any
boolean function f:S->bool can be seen as a predicate S->Prop
defined as funx:S=>fx=true. Thus, if we restrict subset types to
computable predicates, we do not need to worry about the proofs that
appear in its elements.

You might wonder why any assumptions are needed in this result ─ after all,
the definition of equality only had a single constructor; how could two
proofs be different? Let us begin by trying to show the result without
relying on any extra assumptions. We can show that general proof irrelevance
can be reduced to irrelevance of "reflexive equality": all proofs of x=x
are equal to eq_reflx.

SectionIrrelevance.

VariableT : Type. ImplicitTypesxy : T.

Definitionalmost_irrelevance :
(forallx (p : x = x), p = eq_reflx) ->
(forallxy (pq : x = y), p = q) := funHxypq => matchqin_ = zreturnforallp' : x = z, p' = qwith
| eq_refl => funp' => Hxp' endp.

This proof uses the extended form of dependent pattern matching we have seen
in the definition of first: the return type mentions q, the very element
we are matching on. It also uses the convoy pattern to "update" the type of
p with the extra information gained by matching on q.

The almost_irrelevance lemma may look like progress, but it does not
actually get us anywhere, because there is no way of proving its premise
without assumptions. Here is a failed attempt.

Coq complains that the return clause is ill-typed: its right-hand side has
type x=x, but its left-hand side has type x=y. That is because when
checking the return type, Coq does not use the original type of p, but the
one obtained by generalizing the index of its type according to the in
clause.

It took many years to understand that, even though the inductive definition
of equality only mentions one constructor, it is possible to extend the type
theory to allow for provably different proofs of equality between two
elements. Homotopy type
theory, for example, introduced a univalence principle that says that
proofs of equality between two types correspond to isomorphisms between
them. Since there are often many different isomorphisms between two types,
irrelevance cannot hold in full generality.

To obtain an irrelevance result, we must assume that T has decidable
equality.

Hypothesiseq_dec : forallxy, x = y \/ x <> y.

The argument roughly proceeds as follows. We use decidable equality to
define a normalization procedure that takes a proof of equality as input and
produces a canonical proof of equality of the same type as output.
Crucially, the output of the procedure does not depend on its input. We
then show that the normalization procedure has an inverse, allowing us to
conclude ─ all proofs must be equal to the canonical one.

Here is the normalization procedure.

Definitionnormalize {xy} (p : x = y) : x = y := matcheq_decxywith
| or_introle => e
| or_intror_ => p end.

If x=y holds, eq_decxy must return something of the form or_introle, the other branch being contradictory. This implies that normalize is
constant.

This proof avoids the problem that we encountered in our failed proof of
irrelevance, resulting from generalizing the right-hand side of p. In
this return type, p*p^-1 has type x=x, which matches the one of
eq_reflx. Notice why the result of the eq_refl branch is valid: we
must produce something of type eq_reflx*(eq_reflx)^-1=eq_reflx, but
by the definitions of etrans and esym, the left-hand side computes
precisely to eq_reflx.

Armed with etransK, we can now relate normalize to its inverse, and
conclude the proof of irrelevance.

Lemmairrelevancexy (pq : x = y) : p = q. Proof. byrewrite -[LHS]normalizeK -[RHS]normalizeK (normalize_constpq). Qed.

EndIrrelevance.

Irrelevance of equality in practice

The Mathematical
Components library provides excellent support for types with decidable
equality in its eqtypemodule,
including a generic result of proof irrelevance like the one I gave above
(eq_irrelevance). The class structure used by eqtype makes it easy for
Coq to infer proofs of decidable equality, which considerably simplifies the
use of this and other lemmas. The Coq standard
library also provides a proof of this lemma (eq_proofs_unicity_on),
though it is a bit harder to use, since it does not make use of any
mechanisms for inferring results of decidable equality.

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!