Mathematical Components: Assia Mahboubi and Enrico Tassi
Mathematical Components: Assia Mahboubi and Enrico Tassi
Mathematical Components: Assia Mahboubi and Enrico Tassi
https://math-comp.github.io/mcb/
Mathematical Components is the name of a library of formalized mathematics for the Coq
system. It covers a variety of topics, from the theory of basic data structures (e.g., numbers,
lists, finite sets) to advanced results in various flavors of algebra. This library constitutes
the infrastructure for the machine-checked proofs of the Four Color Theorem [Gon08] and
of the Odd Order Theorem [Gon+13a].
The reason of existence of this book is to break down the barriers to entry. While there
are several books around covering the usage of the Coq system [BC04; Chl14; Pie+15] and
the theory it is based on [Coq, chapter 4][Pau15; Uni13], the Mathematical Components
library is built in an unconventional way. As a consequence, this book provides a non-
standard presentation of Coq, putting upfront the formalization choices and the proof
style that are the pillars of the library.
This books targets two classes of public. On the one hand, newcomers, even the more
mathematically inclined ones, find a soft introduction to the programming language of
Coq, Gallina, and the SSReflect proof language. On the other hand accustomed Coq
users find a substantial account of the formalization style that made the Mathematical
Components library possible.
By no means does this book pretend to be a complete description of Coq or SSReflect:
both tools already come with a comprehensive user manual [Coq; GMT15]. In the course
of the book, the reader is nevertheless invited to experiment with a large library of
formalized concepts and she is given as soon as possible sufficient tools to prove non-trivial
mathematical results by reusing parts of the library. By the end of the first part, the reader
has learned how to prove formally the infinitude of prime numbers, or the correctness of
the Euclidean’s division algorithm, in a few lines of proof text.
Acknowledgments.
The authors wish to thank Reynald Affeldt, Guillaume Allais, Sophie Bernard, Alain
Giorgetti, Laurence Rideau, Lionel Rieg, Damien Rouhling, Michael Soegtrop for their
comments on earlier versions of this text. They are specially grateful to Pierre Jouvelot,
Darij Grinberg, Michael Nahas, Anton Trunov and Yamamoto Mitsuharu for their careful
proofreading and for their suggestions. Many thanks to Hanna for the illustrations.
Coq code is in typewriter font and (surrounded by parentheses) when it occurs in the
middle of the text. Longer snippets are in boxes with line numbers like the following one:
Code snippets are often accompanied by the goal status printed by Coq.
n : nat
IHn : \sum_(0 <= i < n.+1) i = (n * n.+1) %/ 2
============================
\sum_(0 <= i < n.+2) i = (n.+1 * n.+2) %/ 2
Names of components one can Require in Coq are written like ssreflect or fintype.
The first line actually instructs the Coq system to load the first level of the Mathematical
Components library. More advanced levels are available under names all fingroup, all algebra,
all solvable, all field, and all character. While the first chapters of this book rely mainly on
the first level, later chapters will rely on the other levels. This will be clearly stated as the
topics evolve.
Contents
3 Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.1 Terms, types, proofs 73
3.1.1 Propositions as types, proofs as programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.1.2 First types, terms and computations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
3.1.3 Inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.1.4 More connectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
3.2 A script language for interactive proving 81
3.2.1 Proof commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
3.2.2 Goals as stacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
3.2.3 Inductive reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
3.2.4 Application: strengthening induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
3.3 On the status of Axioms 90
4 Boolean Reflection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
4.1 Reflection views 94
4.1.1 Relating statements in bool and Prop . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
4.1.2 Proving reflection views . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
4.1.3 Using views in intro patterns . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
4.1.4 Using views with tactics . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
4.2 Advanced, practical, statements 100
4.2.1 Inductive specs with indices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
4.3 Real proofs, finally! 103
4.3.1 Primes, a never ending story . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
4.3.2 Order and max, a matter of symmetry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
4.3.3 Euclidean division, simple and correct . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
4.4 Notational aspects of specifications 109
4.5 Exercises 111
4.5.1 Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
II Formalization Techniques
6 Sub-Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
6.1 n-tuples, lists with an invariant on the length 138
6.2 n-tuples, a sub-type of sequences 140
6.2.1 The sub-type kit ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
6.2.2 A note on boolean Σ-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
6.3 Finite types and their theory 144
6.4 The ordinal subtype 145
6.5 Finite functions 146
6.6 Finite sets 148
6.7 Permutations 149
6.8 Matrix 150
6.8.1 Example: matrix product commutes under trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
6.8.2 Block operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152
6.8.3 Size casts ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
7 Organizing Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
7.1 Structure interface 155
7.2 Telescopes 158
7.3 Packed classes ? 160
7.4 Parameters and constructors ?? 164
7.5 Linking a custom data type to the library 167
III Synopsis
Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
I
Basics for Formal Mathematics
3 Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.1 Terms, types, proofs
3.2 A script language for interactive proving
3.3 On the status of Axioms
4 Boolean Reflection . . . . . . . . . . . . . . . . . . . 93
4.1 Reflection views
4.2 Advanced, practical, statements
4.3 Real proofs, finally!
4.4 Notational aspects of specifications
4.5 Exercises
1. Functions and Computation
In the formalism underlying the Coq system, functions play a central role akin to the
one of sets in set theory. In this chapter, we give a flavor of how to define functions
in Coq, how to perform computations and how to define basic mathematical objects in
this formalism. Readers with a mathematical background will need to get accustomed
to the fact that functions are different in nature from the functions encountered in the
mathematical tradition of set theory.
1.1 Functions
Before being more precise about the logical foundations of the Coq system in chapter 3,
we review in this section some vocabulary and notations associated with functions. We
will use the words function and operation interchangeably. Sometimes, we will also use the
word program to talk about functions described in an effective way, i.e. by a code that can
be executed. As a consequence we borrow from computer science some jargon, like input
or return. For example we say that an operation takes as input a number and returns
its double to mean that the corresponding program computes or outputs the double of
its input, or that the function maps a number to its double. We study many examples
involving natural numbers. In the Coq language, we casually use nat to refer to the
collection of natural numbers and the infix symbol + (resp. * ) to denote the addition (resp.
product) operation on natural numbers, before providing their actual formal definition
in section 1.2.2. We will also assume implicitly that numerals 0, 1, 2, . . . denote natural
numbers, represented by their analogue 0, 1, 2, . . . in the Coq language.
+ in the expression
2+1
This expression represents a natural number, obtained as the result of an operation applied
to its arguments. More precisely, it is the result of the binary operation of addition, applied
to two natural numbers 2 and 1. The same expression can also represent the result of
the unary operation of adding one on the right to a natural number, applied to a natural
number 2.
In Coq, the operation of adding one on the right to a natural number is written in the
following manner:
1 fun n => n + 1
1 (fun n => n + 1) 2
Note that applying a function to an argument is represented simply by writing the function
on the left of the argument, with a separating space but not necessarily with parentheses
around the argument; we will come back to this later in the present section. As a first
approximation, we can see that expressions in the language of Coq, also called terms,
are either variables, constants, functions of the form (fun x => e) , where e is itself an
expression, or the application (e1 e2) of an expression e1 to another expression e2. However,
just like with pen and paper, the addition operation is denoted in the Coq language
using an infix notation + . The transformation we just detailed, from expression (2 + 1) to
expression (fun n => n + 1) 2 , is called abstracting 2 in (2 + 1) . As a contrast to traditional
set-theoretic approaches, abstraction is essentially the only way to define a function in this
language. A function is never described by providing extensively the graph as a subset of
the cartesian product of the input and the output.
While expression (fun n => n + 1) describes an operation without giving it a name, the
usual mathematical practice would be to rely on a sentence like consider the function f
from N to N which maps n to n + 1, or on a written definition like:
N → N
f: (1.1)
n 7→ n + 1
In Coq, the user can also associate a name with the operation (fun n => n + 1) , in the
following manner:
An alternative syntax for exactly the same definition is as follows and this alternative is
actually preferred.
1.1 Functions 15
1 Definition f n := n + 1.
In this syntax, the name of the argument n is provided on the left of the separating
:=,to be then referenced on the right of the separating :=, in the actual definition of the
function. The code of the actual definition is hence enclosed between the := symbol and
the terminating dot.
The information on the domain and codomain of f, as in f : N → N, is provided using
the nat label to annotate the argument and the output in the Coq definition:
The label nat is actually called a type. We refer once again to chapter 3 for a more accurate
description of types: in the present chapter we rely on the loose intuition that a type refers
to a collection of objects that can be treated in a uniform way. A type annotation has the
shape (t : T) , where a colon : surrounded by two spaces separates an expression t on its
left from the type T itself on the right. For instance in (n : nat) , the argument n of the
function f is annotated with type nat.
The other occurrence of nat, visible in ... : nat := ..., annotates the output of the
function and indicates that this output is of type nat. In other words, the type of any
expression made of f applied to an argument is nat.
Coq provides a command to retrieve relevant information about the definitions done
so far. Here is the response to a query about f:
which confirms the type information about the domain and codomain of f: the arrow ->
separates the type of the input of f from the type of its output.
We can be more inquisitive in our requests for information about f, and ask also for
the value behind this name f:
The output of this Print query has some similarities with the mathematical notation
in (1.1) and provides both the actual definition of f and its type information. Actually
the way the definition is printed also features a type annotation of the arguments of the
function, in the fragment “fun n : nat =>”.
Types are used in particular to avoid confusion and rule out ill-formed expressions.
Coq provides a command to check whether an expression is well typed.
For example the function f we just defined can only be applied to a natural number, i.e.,
a term of type nat. Therefore this first query succeeds, as 3 is a natural number:
1 Check f 3. f 3 : nat
But f cannot be applied to something that is not a natural number, like for example a
function:
16 Chapter 1. Functions and Computation
Error:
1 Check f (fun x : nat => x + 1).
The term "(fun x : nat => x + 1)"
2
has type "nat -> nat" while it is
3
expected to be "nat".
As expected, it makes little sense to compute the addition between a function and 1.
Expressions that are well typed can be computed by Coq, meaning that they are
reduced to a “simpler” form, also called a normal form. For example computing (f 3)
returns value 4:
As a simple explanation, we can observe that the argument 3 has been substituted
for the argument variable in the definition of function f and that the addition has been
evaluated. Although this capability of Coq plays a crucial role in the Mathematical
Components library, as we will see in chapter 2, it is too early to be more precise about
this normalization strategy. This would require at least describing in more details the
formalism underlying the Coq system, which we do only in chapter 3. The interested
reader should actually refer to [Coq, section 8.7.1] for the official documentation of compute.
For now, we suggest to keep only the intuition that this normalization procedure provides
the “expected value” of a computation.
In fact, for the sake of compactness, contiguous arguments of one and the same type can be
grouped and share the same type annotation, so that the above definition is better written:
This asserts firstly (by the (n m : nat) type annotation) that both arguments n and m have
type nat, and secondly that the output of the function also has type nat, as prescribed by
the ... : nat := ... type annotation. Again, the About command provides information on
the type of the arguments and values of g:
The first two occurrences of nat in the response nat -> nat -> nat assert that function g
has two arguments, both of type nat; the last occurrence refers to the type of the output.
This response actually reads nat -> (nat -> nat), as the -> symbol associates to the right.
Otherwise said, a multiple argument function is a single argument function that returns
a function. This idea that multiple argument functions can be represented using single
argument functions (rather, for instance, than tuples of arguments) is called currying and
will play a special role in chapter 3. For now, let us just insist on the fact that in Coq,
functions with several arguments are not represented with a tuple of arguments.
1.1 Functions 17
Back to our example, here is an alternative definition h which has a single argument n
of type nat and returns a function of one argument as a result:
If we go further in our scrutiny and ask the Coq system to print the definitions
associated to names g and h, we see that these definitions are exactly the same: The Coq
system does not make any difference between these two ways of describing a two-argument
function.
Term (g 2 3) actually reads ((g 2) 3) and features three nested sub-expressions. The
symbol g is the deepest sub-expression and it is applied to 2 in (g 2) . The value of this
sub-expression is a function, which can be written:
1 fun m => 2 + m * 2
Finally, (g 2 3) is in turn the application of the latter function to 3, which results in:
1 2 + 3 * 2
instance, the following definition introduces a function that takes a function from nat to
nat and produces a new function from nat to nat, by iterating its argument.
Once again, let us scrutinize this Coq statement. The first line asserts that the name of
the function to be defined is repeat_twice. We also see that it has one argument, a function
of type nat -> nat. For later reference in the definition of repeat_twice, the argument is
given the name g. Finally we see that the value produced by the function repeat_twice is
itself a function from nat to nat.
Reading the second line of this statement, we see that the value of repeat_twice when
applied to one argument is a new function, described using the “fun .. => ..” construct.
The argument of that function is called x. After the => sign, we find the ultimate value of
this function. This fragment of text, g (g x), also deserves some explanation. It describes
the application of function g to an expression (g x) . In turn, the fragment (g x) describes
the application of function g to x. Remember that the application of a function to an
argument is denoted by juxtaposing the function (on the left) and the argument (on the
right), separated by a space. Moreover, application associates to the left: expressions made
with several sub-expressions side by side should be read as if there were parentheses around
the subgroups on the left. Parentheses are only added when they are needed to resolve
ambiguities. For instance, the inner (g x) in (g (g x)) needs surrounding parentheses
because expression (g g x) reads ((g g) x) . The latter expression would be ill-formed
because it contains the sub-expression (g g) where g receives a function as argument, while
it is expected to receive an argument of type nat.
We can play a similar game as in section 1.1.2, and scrutinize the expression obtained
by applying the function repeat_twice to the function f and the number 2. Let us compute
the resulting value of this application:
Now looking at the type of repeat_twice and adding redundant parentheses we obtain
((:nat -> nat) -> (nat -> nat)) : once the first argument (f : nat
::::::::::
-> nat) is passed, we obtain
:::::::::
a term the type of which is the right hand side of the main arrow, that is (nat -> nat) .
By passing another argument, like (2 : nat) , we obtain an expression the type of which
is, again, the right hand side of the main arrow, here nat. Remark that each function has
an arrow type and that the type of its argument matches the left hand side of this arrow
1.2 Data types, first examples 19
(as depicted with different underline styles). When this is not the case, Coq issues a type
error.
1 let x := B in
2 x + x + x
In this expression the variable x is bound and can be used in the text that comes after
the in keyword. Variants of this syntax make it possible to state the type ascribed to the
variable x, which may come handy when the code has to be very explicit about the nature
of the values being abbreviated. Here is an example of usage of this syntax:
1 Eval compute in
2 let n := 33 : nat in
= 297 : nat
3 let e := n + n + n in
4 e + e + e.
When it comes to comparing the values of computations, a local definition has the same
result as the expression where all occurrences of the bound variable are replaced by the
corresponding expression. Thus, the example expression above has exactly the same value
as:
(> ∨ ⊥) ∧ b
20 Chapter 1. Functions and Computation
0 + x × (S 0)
is a well formed expression in the language {0, S, +, ×} of Peano arithmetic. These languages
are usually equipped with behavior rules, expressed in the form of equality axioms, like
In practice, these axioms confer a distinctive status on the symbols > and ⊥ for booleans,
and to the symbols 0 and S for natural numbers. More precisely, any variable-free boolean
expression is equal to either > or ⊥ modulo these axioms, and any variable-free expression
in Peano arithmetic is equal either to 0 or to an iterated application of the symbol S to 0.
In both cases, the other symbols in the signature represent functions, whose computational
content is prescribed by the axioms. In what follows, we shall call the distinctive symbols
constructors. So the constructors of boolean arithmetic are > and ⊥ and the constructors
of Peano arithmetic are 0 and S.
In Coq, such languages are represented using a data type, whose definition provides in
a first single declaration the name of the type and the constructors, plus some rules on
how to define maps on these data types or prove theorems about their elements. The other
operations are then derived from these rules.
The first single declarations of data types are introduced by the means of inductive
type definitions. One can then explicitly define more operations on the elements of the type
by describing how they compute on a given argument in the type using a case analaysis or
a recursive definition on the shape of this argument. This approach is used in a systematic
way to define a variety of basic types, among which boolean values, natural numbers, pairs
or sequences of values are among the most prominent examples.
In the following sections, we introduce basic types bool for boolean values and nat
for natural numbers, taking the opportunity to describe various constructs of the Coq
language as they become relevant. These sections serve simultaneously as an introduction
to the data types bool and nat and to the Coq language constructs that are used to define
new data types and describe operations on these data types.
It is actually one of the simplest possible inductive definitions, with only base cases, and
no inductive cases. This declaration states explicitly that there are exactly two elements in
type bool: the distinct constants true and false, called the constructors of type bool.
In practice, this means that we can build a well-formed expression of type bool by using
either true or false.
More generally, we can define a function that takes a boolean value as input and returns
one of two possible natural numbers in the following manner:
As illustrated on this example, the compute command rewrites any term of the shape
if true then t1 else t2 into t1 and of the shape if false then t1 else t2 into t2.
We can then use this basic operation to describe the other elements that we usually
consider as parts of the boolean language, usually at least conjunction, written && and
disjunction, written ||. We first define these as functions, as follows:
and then the notations && and || are attached to these two functions, respectively.
For any choice of values b1, b2, and b3 it appends that the expressions b1 && (b2 && b3)
and (b1 && b2) && b3 always compute to the same result. In this sense, the conjunction
operation is associative. We shall see in chapter 2 that this known property can be stated
explicitely. For a mathematical reader, this associativity is often included in the reading
process, so that the two forms of three-argument conjunctions are often identified. However,
when manipulating boolean expressions of the Coq language, there is a clear distinction
between these two forms of conjunctions of three values, and the notation conventions
make sure that the two forms appear differently on the screen. We will come back to this
question in section 1.7.
The Mathematical Components library provides a collection of boolean operations that
mirror reasoning steps on truth values. The functions are called negb, orb, andb, and implyb,
with notations ~~ , ||, &&, and ==>, respectively (the last three operators are infix, i.e., they
appear between the arguments, as in b1 && b2). Note that the symbol ~~ uses two characters
~ : it should not be confused with two consecutive occurrences of the one-character symbol
~ , which would normally be written with a separating space. The latter has a meaning in
Coq, but is almost never used in the Mathematical Components library.
This inductive definition of the expressions of type nat has one base case, the constant
O, and one inductive case, for the natural numbers obtained using the successor function at
least once: therefore O has type nat, (S O) has type nat, so does (S (S O)) , and so on, and
any natural number has this shape. The constant O and the function S are the constructors
of type nat.
When interacting with Coq, we will often see decimal notations, but these are only
a parsing and display facility provided to the user for readability: O is displayed 0, (S O)
is displayed 1, etc. Users can also type decimal numbers to describe values in type nat:
these are automatically translated into terms built (only) with O and S. In the rest of this
chapter, we call such a term a numeral.
The Mathematical Components library provides a few notations to make the use of
the constructor S more intuitive to read. In particular, if x is a value of type nat, x.+1 is
another way to write (S x) . The “.+1” notation binds stronger than function application,
rendering some parentheses unnecessary: assuming that f is a function of type nat -> nat
the expression (f n.+1) reads (f (S n)) . Notations are also provided for S (S n), written
n.+2, and so on until n.+4.
1 Check fun n => f n.+1. fun n : nat => f n.+1 : nat -> nat
be better to start When defining functions that operate on natural numbers, we can proceed by case
h a function that analysis, as was done in the previous section for boolean values. Here again, there are
ests equality to 0 two cases: either the natural number used in the computation is O or it is p.+1 for some p,
and the value of p may be used to describe the computations to be performed. This case
analysis can be seen as matching against patterns: if the data fits one of the patterns, then
the computation proceeds with the expression in the corresponding branch. Such a case
analysis is therefore also called pattern matching. Here is an example:
The function predn returns the predecessor of a natural number when it exists, and 0
otherwise. In this definition p.+1 is a pattern. The value bound to the name p mentioned
in this pattern is not known in advance; it is actually computed at the moment the n is
matched against the pattern. For instance:
The compute command rewrites any term of the shape if 0 is p.+1 then t1 else t2 into
t2 and any term of the shape if k.+1 is p.+1 then t1 else t2 into t1 where all occurrences
of p have been replaced by k. In our example, as the value of k.+1 is 5, k and hence p and
t1 are 4.
The symbols that are allowed in a pattern are essentially restricted to the constructors,
here O and S, and to variable names. Thanks to notations however, a pattern can also
contain occurrences of the notation “.+1” which represents S, and decimal numbers, which
represent the corresponding terms built with S and O. When a variable name occurs, this
variable can be reused in the result part.
1.2 Data types, first examples 23
Observe that we did omit the type of the input n. We can omit this type because
matching n against the p.+1 pattern imposes that n has type nat, as the S constructor
belongs to exactly one inductive definition, namely the one of nat.
The pattern used in the if statement can be composed of several nested levels of the
.+1 pattern. For instance, if we want to write a function that returns n − 5 for every input
n larger than or equal to 5 and 0 for every input smaller than 5, we can write the following
definition:
1 Definition pred5 n :=
2 if n is u.+1.+1.+1.+1.+1 then u else 0.
On the other hand, if we want to describe a different computation for three different cases
and use variables in more than one case, we need the more general “match .. with .. end”
syntax. Here is an example:
1 Definition three_patterns n :=
2 match n with
3 u.+1.+1.+1.+1.+1 => u
4 | v.+1 => v
5 | 0 => n
6 end.
This function maps any number n larger than or equal to 5 to n − 5, any number
n ∈ {1, . . . , 4} to n − 1, and 0 to 0.
The pattern matching construct “match .. with .. end” may contain an arbitrarily large
number of pattern matching rules of the form “pattern =>result” separated by the | symbol.
Optionally one can prefix the first pattern matching rule with |, in order to make each line
begin with |. Each pattern matching rule results in a new rewrite rule available to the
compute command. All the pattern matching rules are tried successively against the input.
The patterns may overlap, but the result is given by the first pattern that matches. For
instance with the function three_patterns, if the input is 2, in other words 0.+1.+1, the first
rule cannot match, because this would require that 0 matches u.+1.+1.+1 and we know that
0 is not the successor of any natural number; when it comes to the second rule 0.+1.+1
matches v.+1, because the rightmost .+1 in the value of 2 matches the rightmost .+1 part
in the pattern and 0.+1 matches the v part in the pattern.
A fundamental principle is enforced by Coq on case analysis: exhaustiveness. The
patterns must cover all constructors of the inductive type. For example, the following
definition is rejected by Coq.
1 Definition same_bool b1 b2 :=
2 match b1, b2 with
3 | true, true => true
24 Chapter 1. Functions and Computation
Here, the reserved word _ stands for a “throwaway variable”, i.e., a variable that we
choose to give no name because we are not going to reference it (for example, the constant
function fun (n : nat) => 2 can also be written fun (_ : nat) => 2).
The above code defining same_bool is parsed as follows:
1 Definition same_bool b1 b2 :=
2 match b1 with
3 | true => match b2 with true => true | _ => false end
4 | false => match b2 with true => false | _ => true end
5 end.
1 Fixpoint addn n m :=
2 if n is p.+1 then (addn p m).+1 else m.
As this example illustrates, the keyword for defining a recursive function in Coq is Fixpoint:
the function being defined, here called addn, is used in the definition of the function addn
itself. This text expresses that the value of (addn p.+1 m) is (addn p m).+1 and that the value
(addn 0 m) is m. This first equality may seem redundant, but there is progress when reading
this equality from left to right: an addition with p.+1 as the first argument is explained
with the help of addition with p as the first argument, and p is a smaller number than
p.+1. When considering the expression (addn 2 3) , we can know the value by performing
the following computation:
When the computation finishes, the symbol addn disappears. In this sense, the recursive
definition is really a definition. Remark that the (addn n m) program simply stacks n times
the successor symbol on top of m.
If we reflect again on the discussion of Peano arithmetic, as in Section 1.2, we see that
addition is provided by the definition of addn, and the usual axioms of Peano arithmetic,
namely:
S x + y = S(x + y) 0+x = x
are actually provided by the computation behavior of the function, namely by the “then”
branch and the “else” branch respectively. Therefore, Peano arithmetic is really provided
by Coq in two steps, first by providing the type of natural numbers and its constructors
thanks to an inductive type definition, and then by providing the operations as defined
functions (usually recursive functions as in the case of addition). The axioms are not
1.2 Data types, first examples 25
constructed explicitly, but they appear as part of the behavior of the addition function. In
practice, it will be possible to create theorems whose statements are exactly the axioms of
Peano arithmetic, using the tools provided in Chapter 2. The fact that the computation of
addn 2 3 ends in an expression where the addn symbol does not appear is consistent with the
fact that O (also noted 0) and S (also noted .+1) are the constructors of natural numbers.
An alternative way of writing addn is to provide explicitly the rules of the pattern-
matching at stake instead of relying on an if statement. This can be written as follows:
1 Fixpoint addn n m :=
2 match n with
3 | 0 => m
4 | p.+1 => (addn p m).+1
5 end.
With this way of writing the recursive function, it becomes obvious that pattern-matching
rules describe equalities between two symbolic expressions, but these equalities are always
used from left to right during computations.
When writing recursive functions, the Coq system imposes the constraint that the
described computation must be guaranteed to terminate. The reason for this requirement
is sketched in section 3.2.3. This guarantee is obtained by analyzing the description of
the function, making sure that recursive calls always happen on a given argument that
decreases. Termination is obvious when the recursive calls happen only on “syntactically
smaller arguments”. For instance, in our example addn, the function is defined by matching
its first argument n against the patterns p.+1 and 0; in the branch corrsponding to the
pattern p.+1, the recursive call happens on p, a strict subterm of p.+1. Had we matched the
argument n against the pattern p.+1.+1, then the recursive call would have been allowed on
arguments p or p.+1, but not p.+1.+1. The way Coq verifies that recursive functions will
terminate is explained in more detail in the reference manual [Coq] or in the Coq’Art book
[BC04].
An erroneous, in the sense of non-terminating, definition is rejected by Coq:
We have seen that addition is implemented by repeating the operation of applying .+1
to one of the arguments. Conversely, comparing two natural numbers is implemented by
repeating the operation of fetching a subterm. Consider two terms m and n representing
the natural numbers m and n respectively. Then m is larger than n if and only if m has k
more constructors than n for some k ≥ 0, which measures the distance between m and n.
Comparison is thus implemented in terms of an auxiliary truncated subtraction, which is
again easily expressed using pattern matching constructs:
Number m is less or equal to number n if and only if (subn m n) is zero. Here as well, this
subtraction is already defined in the libraries, but we play the game of re-defining our
26 Chapter 1. Functions and Computation
own version. The second pattern matching rule indicates that when any argument of the
subtraction is 0, then the result is the first argument. This rule thus also covers the case
where the second argument is non-zero while the first argument is 0: in that case, the
result of the function is zero. Another possible view on subn it to see it as a subtraction
operation on natural numbers, made total by providing a default value in the “exceptional”
cases. We shall discuss totality of functions in more detail in Section ??.
We can also write a recursive function with two arguments of type nat, that returns
true exactly when the two arguments are equal:
1 Fixpoint eqn m n :=
2 match m, n with
3 | 0, 0 => true
4 | p.+1, q.+1 => eqn p q
5 | _, _ => false
6 end.
The last rule in the code of this function actually covers two cases : 0, _.+1 and _.+1, 0 .
For equality test functions, it is useful to add a more intuitive notation. For instance
we can attach a notation to eqn in the following manner:
Now that we have programmed this equality test function, we can verify that the Coq
system really identifies various ways to write the same natural number.
1 Definition leq m n := m - n == 0.
2 Notation "m <= n" := (leq m n).
Note that this definition crucially relies on the fact that subtraction computes to 0
whenever the first argument is less than or equal to the second argument.
The Mathematical Components library also provides concepts that make sense only for
the nat data type, like the test functions identifying prime and odd numbers. In that case,
1.3 Containers 27
R Each file in the Mathematical Components library starts with a banner describing all
the concepts and associated notations introduced by the file. There is no better way
to browse the library than reading these banners.
1.3 Containers
A container is a data type which describes a collection of objects grouped together so that
they can be manipulated as a single object. For instance, we might want to compute the
sequence of all predecessors or all divisors of a number. We could define the following data
type for this purpose:
The elements of this data type constitue a possible description of lists of zero or more
natural numbers; the first constructor niln builds the empty list, whereas the second
constructor consn builds a nonempty list by combining a natural number hd with an already
existing list tl. For example:
This approach is problematic for two reasons. First, every time we write a function
that manipulates a list, we have to decide a priori if the list holds numbers or booleans,
even if the program does not really use the objects held in the list. A concrete example
is the function that computes the size of the list; in the current setting such a function
has to be written twice. Worse, starting from the next chapter we will prove properties of
programs, and given that the two size functions are “different”, we would have to prove
such properties twice.
However it is clear that the two data types we just defined follow a similar schema, and
so do the two functions for computing the size of a list or the theorems we may prove about
these functions. Hence, one would want to be able to write something like the following,
where α is a schematic variable:
1 http://math-comp.github.io/math-comp/htmldoc/libgraph.html
28 Chapter 1. Functions and Computation
This may look familiar jargon to some readers. In the present context however, we would
rather like to avoid appealing to any notion of schema, that would somehow be added on
top of the Coq language. This way, we will make possible the writing of formal sentences
with arbitrary quantifications on this parameter α.
The name seq refers to (finite) “sequences”, also called “lists”. This definition actually
describes the type of lists as a polymorphic type. This means that there is a different type
(seq A) for each possible choice of type A. For example (seq nat) is the type of sequences of
natural numbers, while (seq bool) is the type of sequences of booleans. The type (seq A)
has two constructors, named nil and cons. Constructor nil represents the empty sequence.
The type of the constructor cons is devised specifically to describe how to produce a new
list of type (seq A) by combining an element of A, the head of the sequence, and an existing
list of type (seq A) , the tail of the sequence. This also means that this data-type does not
allow users to construct lists where the first element would be a boolean value and the
second element would be a natural number.
In the declaration of seq, the keyword Type denotes the type of all data types. For
example nat and bool are of type Type, and can be used in place of A. In other words seq
is a function of type (Type -> Type) , sometimes called a type constructor. The symbol seq
alone does not denote a data type, but if one passes to it a data type, then it builds one.
Remark that this also means that (seq (seq nat)) is a valid data type (namely, the type of
lists of lists of natural numbers), and that the construction can be iterated. Types again
avoid confusion: it is not licit to form the type (seq 3) , since the argument 3 has type nat,
while the function seq expects an argument of type Type.2
In principle, the constructors of such a polymorphic data type feature a type argument:
nil is a function that takes a type A as argument and returns an empty list of type (seq A) .
The type of the output of this function hence depends on the value of this input. The type
of nil is thus not displayed with the arrow notation “.. -> ..” that we have used so far for
lanation of the ∀ the type of functions. It is rather written as follows:
l and the forall
keyword. 1 ∀ A : Type, seq A
so as to bind the value A of the argument in the type of the output. The same goes for the
other constructor of seq, named cons. This function actually takes three arguments: a type
A, a value in this type, and a value in the type (seq A) . The type of cons is thus written as
follows:
2 For historical reasons Coq may display the type of nat or bool as Set and not Type. We beg the reader
to ignore this detail, which plays no role in the Mathematical Components library.
1.3 Containers 29
Since the type of the output does not depend on the second and third arguments of
cons, respectively of type A and (seq A) , the type of cons features two arrow separators for
these. Altogether, we conclude that the sequence holding a single element 2 : nat can be
constructed as (cons nat 2 (nil nat)) . Actually, the two occurrences of type nat in this
term are redundant: the tail of a sequence is a sequence with elements of the same type.
Better yet, this type can be inferred from the type of the given element 2. One can thus
write the sequence as (cons _ 2 (nil _)) , using the placeholder _ to denote a subterm, here
a type to be inferred by Coq. In the case of cons, however, one can be even more concise.
Let us ask for information about cons using the command About:
The Coq system provides a mechanism to avoid that users need to give the type
argument to the cons function when it can be inferred. This is the information meant
by the message “Argument A is implicit and ..”. Every time users write cons, the system
automatically inserts an argument in place of A, so that this argument does not need
to be written (the argument is implicit). It is then the job of the Coq system to guess
what this argument is when looking at the first explicit argument given to the function.
The same happens to the type argument of nil in the built-in version of seq provided by
the Mathematical Components library. In the end, this ensures that users can write the
following expression.
This example shows that the function cons is only applied explicitly to two arguments (the
two arguments effectively declared for cons in the inductive type declaration). The first
argument, which is implicit, has been guessed so that it matches the actual type of 2. Also
for nil the argument has been guessed to match the constraints that it is used in a place
where a list of type (seq nat) is expected.
To locally disable the status of implicit arguments, one can prefix the name of a constant
with @ and pass all arguments explicitly, as in (@cons nat 2 nil) or (@cons nat 2 (@nil nat))
or even (@cons _ 2 (@nil _)) .
This example, and the following ones, also show that Coq and the Mathematical
Components library provide a collection of notations for lists.
In particular Coq provides the infix notation :: for cons. The Mathematical Components
library follows a general pattern for n-ary operations obtained by the (right-associative)
iteration of a single binary one. In particular [:: begins the repetition of :: and ] ends it.
Elements are separated by , (comma) but for the last one separated by &. For example, the
above [:: 1, 2, 3 & l] stands for 1 :: (2 :: (3 :: l)). For another example, one can write
30 Chapter 1. Functions and Computation
the boolean conjunction of three terms as [&& true, false & true].3 For sequences that
are nil-terminated, a very frequent case, the Mathematical Components library provides
an additional notation where all elements are separated by ; (semi-colon) and the last
element, nil, is omitted.
Pattern matching can be used to define functions on sequences, like the following
example which computes the first element of a non-empty sequence, with a default value
for the empty case:
During computation on a given sequence, this function traverses the whole sequence,
incrementing the result for every cons that is encountered. Note that in this definition,
the function size is described as a two argument function, but the recursive call (size tl)
is done by providing explicitly only one argument, tl. Remember that the Coq system
makes arguments of functions that can be guessed from the type of the following arguments
automatically implicit, and A is implicit here. This feature is already active in the expression
defining size.
Another example of recursive function on sequences is a function that constructs a new
sequence whose entries are values of a given function applied to the elements of an input
sequence. This function can be defined as:
This function provides an interesting case study for the definition of appropriate notations.
For instance, we will add a notation that makes it more apparent that the result is the
sequence of all expressions f (i) for i taken from another sequence.
For instance, with this notation we write the computation of successors for a given sequence
of natural numbers as follows:
3 Some n-ary notations use a different, but more evocative, last separator. For example one writes
In addition to the function map and the associated notation we describe here, the Mathe-
matical Components library provides a large collection of useful functions and notations to
work on sequences, as described in the header of the file seq. For instance [seq i <- s | p]
filters the sequence s keeping only the values selected by the boolean test p. Another
useful function for sequences is cat (with infix notation ++ ) that is used to concatenate two
sequences together.
Akin to a pointed version of A, type (option A) contains a copy of all the elements of A,
built using the Some constructor, plus an extra element given by the constructor None. It
may be used to represent the output of a partial function or of a filtering operation, using
None as a default element.
For example, function only_odd “filters” natural numbers, keeping the odd ones and
replacing the even ones by the None default value:
Similarly, one can use the option type to define a partial function which computes the
head of a non-empty list:
See also the sub-type kit presented in chapter 6, which makes use of the option type to
describe a partial injection.
Another typical polymorphic data type is the one of pairs, that lets one put together
any two values:
The type pair has two type parameters, A and B, so that it can be used to form any
instance of pairs: (pair nat bool) is the type of pairs with an element of type nat in its
first component and one of type bool in its second, but we can also form (pair bool nat) ,
(pair bool bool) , etc. The type pair is denoted by an infix * symbol, as in (nat * bool) .
This inductive type has a single constructor mk_pair. It takes over the two polymorphic
parameters, that become its two first, implicit arguments. The constructor mk_pair has
two more explicit arguments which are the data stored in the pair. This constructor
is associated with a notation so that (a, b) builds the pair of a and b, and (a, b) has
32 Chapter 1. Functions and Computation
type (pair A B) . For a given pair, we can extract its first element, and we can provide a
polymorphic definition of this projection:
As one expects, pairs can be nested. Coq provides a slightly more complex notation
for pairs, which makes it possible to write (3,true,4) for ((3,true),4) . In this example, the
value true is the second component of this tuple, or more precisely the second component
of its first component: it can thus be obtained as (3,true,4).1.2 . This may be a drawback,
consequence of representing tuples as nested pairs. If tuples of a certain fixed length are
pervasive to a development, one may consider defining another specific container type for
this purpose. See for instance exercise 1 for the definition of triples.
We conclude this example with a remark on notations. After declaring such a notation
for the type of pairs, the expression (a * b) becomes “ambiguous”, in the sense that the same
infix * symbol can be used to multiply two natural numbers as in (1 * 2) but also to write
the type of pairs (nat * bool) . Such an ambiguity is somewhat justified by the fact that
the pair data type can be seen as the (Cartesian) product of the arguments. The ambiguity
can be resolved by annotating the expression with a specific label: (a * b)%N interprets the
infix * as multiplication of natural numbers, while (a * b)%type would interpret * as the
pair data type constructor. The %N and %type labels are said to be notation scope delimiters
(for more details see [Coq, section 12.2]).
This line of code defines an inductive type point, with no parameter and with a single
constructor Point, which has three arguments each of type nat. Otherwise said, this type is:
Using the Record version of this definition instead of its equivalent Inductive allows us
to declare names for the projections at the time of the definition. In our example, the
record point defines three projections, named x, y and z respectively. In the case where
1.4 The Section mechanism 33
they come from a record definition, these projections are also called fields of the record.
One can thus write:
When an inductive type has a single constructor, like in the case of pair or for records,
the name of this constructor is not relevant in pattern matching, as the “case analysis” has
a single, irrefutable, branch. There is a specific syntax for irrefutable patterns, letting one
rewrite the definition above as follows:
Record types are as expressive as inductive types with one constructor: they can be
polymorphic, they can package data with specifications, etc. In particular, they will be
central to the formalization techniques presented in Part II.
1 Section iterators.
2
3 Variables (T : Type) (A : Type).
4 Variables (f : T -> A -> A).
5
6 Implicit Type x : T.
7
8 Fixpoint iter n op x :=
9 if n is p.+1 then op (iter p op x) else x.
10
11 Fixpoint foldr a s :=
12 if s is y :: ys then f y (foldr a ys) else a.
13
14 End iterators.
The Section and End keywords delimit a scope in which the types T and A and the function
f are given as parameters: T, A and f are called section variables. These variables are used
in the definition of iter and foldr.
The Implicit Type annotation tells Coq that, whenever we name an input x (or x’, or
x1, . . . ), its type is supposed to be T. Concretely, it lets us omit an explicit type annotation
in the definition of programs using x, such as iter. The Implicit Type command is used
34 Chapter 1. Functions and Computation
frequently in the Mathematical Components library; the reader can refer to [Coq, section
2.7.18] for a more detailed documentation of it.
When the section is closed (using the End command), these variables are abstracted:
i.e., from then on, they start appearing as arguments to the various functions that use
them in the very same order in which they are declared. Variables that are not actually
used in a given definition are omitted. For example, f plays no role in the definition of
iter, and thus does not become an argument of iter outside the section. This process is
called an abstraction mechanism.
Concretely, the definitions written inside the section are elaborated to the following
ones.
Finally, remark that T and A are implicit arguments; hence they are not explicitly passed
to iter and fold in the recursive calls.
We can now use iter to compute, for example, the subtraction of 5 from 7, or foldr to
compute the sum of all numbers in [:: 1; 2]:
1 Section iterators.
2
3 Variables (T : Type) (A : Type).
4 Variables (f : T -> A -> A).
5
6 Fixpoint foldr a s :=
7 if s is x :: xs then f x (foldr a xs) else a.
If we ask for the type of foldr in the middle of the section, we see that it is not a
polymorphic function (yet).
We hence postulate a term of type A and two of type T in order to apply foldr to a
two-element list, and we ask Coq to compute this expression.
1 Variable init : A.
2 Variables x1 x2 : T.
3 Eval compute in foldr init [:: x1; x2]. = f x1 (f x2 init) : A
The symbols f, x1, x2 and init are inert: They represent unknown values, hence compu-
tation cannot proceed any further. Still Coq has developed the expression symbolically.
To convince ourselves that such an expression is meaningful we can try to substitute f,
x1, x2 and init with the values we used at the end of the last section to play with foldr,
namely addn, 1, 2 and 0:
The expression, which now contains no inert symbols, computes to the numeral 3, the
very same result we obtained by computing (foldr addn 0 [:: 1; 2]) directly.
The way functions are described as programs has an impact on the way symbolic
computations unfold. For example, recall from section 1.2.3 the way we defined an addition
operation on elements of type nat. It was defined using the if .. is .. then .. else ..
syntax:
Both are sensible definitions, and we can show that the two addition functions compute
the same results when applied to numerals. Still, their computational behavior may differ
when computing on arbitrary symbolic values. In order to highlight this, we will use
another normalization strategy to perform computation, the simpl evaluation strategy. One
difference between the simpl and compute strategies is that the simpl one usually leaves
expressions in nicer forms whenever they contain variables. Here again we point the
interested reader to [Coq, section 8.7.1] for more details. predn has a nota
attached to it
1 Variable n : nat.
= (add n 8).-1 : nat
2 Eval simpl in (add n.+1 7).-1.
= addn n 7 : nat
3 Eval simpl in (addn n.+1 7).-1.
Here we see the impact of the difference in the definitions of addn and add: the add
variant transfers the number of pebbles (represented by the successor S symbol) given as I think it is
first argument to its second argument before resorting to its base case, whereas in the addn counter-producti
variant, the resulting stack of pebbles is constructed top down. An intermediate expression use the pebble m
in the computation of (addn n m) exposes as many successors as recursive calls have been here, because it w
performed so far. Since bits of the final result are exposed early, the predn function can introduced befor
eventually compute, and it cancels the .+1 coming out of the sum. On the other hand, add
36 Chapter 1. Functions and Computation
does not expose a successor when a recursive call is performed; hence symbolic computation
in predn is stuck.
As chapter 2 illustrates, symbolic computation plays an important role in formal proofs,
and this kind of difference matters. For instance the addn variant helps showing that
(addn n.+1 7) is different from 0 because by computation Coq would automatically expose
a S symbol and no natural number of the form (S ..) is equal to 0. For a worked out
example, see also the proof of muln_eq0 in section 2.2.2.
and, more generally, in order to make explicit the meaning of the capital notations like
Tn n
i=1 Ai , ∏i=1 ui , . . . , we need to decribe an iteration procedure akin to the foldr program.
We illustrate this on the example of the summation symbol (for a finite sum):
The iota function generates the list [:: m; m+1; ...; m+n-1] of natural numbers cor-
responding to the range of the summation. Then the notation defines expressions with
shape \sum_ (m <= i < n) F , with F a sub-expression featuring variable i, the one used for
the index. For instance, once the above notation is granted and for any natural number
(n : nat) , one may write the Coq expression (\sum_(1 <= i < n) i) to represent the sum
n−1
∑ i. The name i is really used as a binder name here and we may substitute i with any
i=1
other name we may find more convenient, as in (\sum_(1 <= j < n) j) , without actually
changing the expression4 .
The notation represents an instance of the foldr program, iterating a function of type
nat -> nat -> nat: the two type parameters of foldr are set to nat in this case. The first
explicit argument given to foldr is hence a function of type nat -> nat -> nat, which is
created by abstracting the variable i in the expression F, as mentioned in section 1.1.1. The
name of the second argument of the function, called a here, should not appear in expression
F in order for the notation to be meaningful. Crucially, the foldr iterator takes as input
a functional argument that is able to represent faithfully any general term. As a second
explicit argument to foldr, we also provide the neutral element 0 for the addition: this is
the initial value of the iteration, corresponding to an empty index range.
Let us perform a few examples of computations with these iterated sums.
4 Although this change results in two syntactically different expressions, they have the same meaning for
Coq
1.7 Notations, abbreviations 37
Behind the scenes, iteration happens following the order of the list, as we observed
in section 1.5. In the present case the operation we iterate, addition, is commutative, so
this order does not impact the final result. But it may not be the case, for example if the
iterated operation is the product of matrices.
Defining the meaning of this family of notations using a generic program foldr, which
manipulates functions, is not only useful for providing notations, but it also facilitates
the design of the corpus of properties of these expressions. This corpus comprises lemmas
derived from the generic properties of foldr, which do not depend on the function iterated.
By assuming further properties linking the iterated operation to the initial value, like
forming a monoid, we will be able to provide a generic theory of iterated operations in
section 5.7.
For infix notations, which are meant to be printed between two arguments of the
operator (like addition in 2 + 3), we advise to always include space around the infix
operator, so that notations don’t get mixed up with potential notations occurring in the
arguments.
Similarly, the comparison relation leq on type nat comes with an infix notation <= which
can be defined as:
where the rightmost annotations, between parentheses, indicate a precedence level and
an associativity rule so as to avoid parsing ambiguities. A lower level binds more than a
higher level. A comprehensive description of the Notation command goes behind the scope
of this book; the interested reader shall refer to [Coq, chapter 12].
A notation can denote an arbitrary expression, not just a single constant. Here is for
instance the definition of the infix notation < , for the strict comparison of two natural
numbers: it denotes the composition of the comparison _ <= _ (which refers to the constant
leq) with the successor _.+1 (which refers to the constructor S) on its first argument:
38 Chapter 1. Functions and Computation
R There is no function testing if a natural number is strictly smaller than another one.
(a < b) is just an alternative syntax for (a.+1 <= b)
The converse relation (n > m) is defined as a notation for (m < n) . However, it is only
accepted in input, and is always printed as (m < n) , thanks to the following declaration:
1 Notation succn := S.
The notation _.+1 we have been using so far is defined on top of this abbreviation, as:
The Locate command can be used to reveal the actual term represented by a notation.
In order to understand the meaning of an unknown notation like for instance (a <= b <= c) ,
one can use the Locate command to uncover the symbols it involves.
1 Locate "<=".
Notation Scope
"m <= n <= p" := andb (leq m n) (leq n p) : nat_scope
"m <= n < p" := andb (leq m n) (leq (S n) p) : nat_scope
"m <= n" := leq m n : nat_scope
The only difficulty in using Locate comes from the fact that one has to provide a
complete symbol. A symbol is composed of one or more non-blank characters and its first
character is necessarily a non-alphanumerical one. The converse is not true: a sequence of
characters is recognized as a symbol only if it is used in a previously declared notation.
For example 3.+1.+1 is parsed as a number followed by two occurrences of the .+1 symbol,
even if .+1.+1 could, in principle, be a single symbol.
Moreover substrings of a symbol are not necessarily symbols. As a consequence
Locate "=" does not find notations like the ones above, since <= is a different symbol even
if it contains = as a substring. For the same reason Locate ".+" returns an empty answer
since .+ is not a (complete) symbol.
We mention here some notational conventions adopted throughout the Mathematical
Components library.
• Concepts that are typically denoted with a letter, like N(G) for the normalizer of
the group G, are represented by symbols beginning with ’ as in ’N(G) , where ’N is a
symbol.
1.7 Notations, abbreviations 39
• At the time of writing, notations for numerical constants are specially handled by
the system. The algebraic part of the library overrides specific cases, like binding 1
and 0 to ring elements.
• Postfix notations begin with ., as in .+1 and .-group to let one write (p.-group G) .
There is one exception for the postfix notation of the factorial, which starts with ‘ ,
as in m‘!.
• Taking inspiration from LATEX some symbols begin with \ , like \in , \matrix , \sum , . . .
• Arguments typically written as subscripts appear after a symbol which ends with an
underscore like ’N_ in ’N_G(H) .
• N-ary notations begin with [ followed by the symbol of the operation being repeated,
as in [&& true, false & false].
• Bracket notations are also used for operations building data, as in [seq .. | .. ].
• Curly braces notations like {poly R} are used for data types with parameters.
• Curly braces are also used to write localized statements such as {in A, injective f} ,
which means that the restriction of f to A is injective.
Each file in the Mathematical Components library comes with a header documenting
all concepts and associated notations it provides.
40 Chapter 1. Functions and Computation
1.8 Exercises
Remark that the triple data type has to be polymorphic in order to be applicable to
each of these combinations of natural numbers and booleans.
Exercise 2 Addition with iteration
Define a program computing the sum of two natural numbers using iter.
1 Eval compute in = 11
2 nth 99 [:: 3; 7; 11; 22] 2. : nat
3 Eval compute in = 99
4 nth 99 [:: 3; 7; 11; 22] 7. : nat
1.8.1 Solutions
Answer of exercise 1
1 Inductive triple (A B C : Type) := mk_triple (a : A) (b : B) (c : C).
2 Notation "( a , b , c )" := (mk_triple a b c).
3 Definition fst A B C (p : triple A B C) := let: (a, _, _) := p in a.
4 Definition snd A B C (p : triple A B C) := let: (_, b, _) := p in b.
5 Definition thrd A B C (p : triple A B C) := let: (_, _, c) := p in c.
Answer of exercise 2
Answer of exercise 3
Answer of exercise 4
Answer of exercise 5
Answer of exercise 6
Answer of exercise 7
42 Chapter 1. Functions and Computation
In this chapter, we explain how to use the Coq system to state and prove theorems,
focusing on simple statements and basic proof commands. In the course of this book,
we will see that choosing the right way to state a proposition formally can be a rather
delicate matter. For equivalent wordings of one and the same proposition, some can be
much simpler to prove, and some can be more convenient to invoke inside the proof of
another theorem. This chapter emphasizes the use of computable definitions and equational
reasoning whenever possible, an approach that will be developed fully in chapter 4.
1 Check 3 = 3. 3 = 3 : Prop
2 Check false && true = false. false && true = false : Prop
Let’s anatomize the two above examples. Indeed, just like Coq’s type system prevents
us from applying functions to arguments of a wrong nature, it also enforces a certain
nature of well-formedness at the time we enunciate sentences that are candidate theorems.
44 Chapter 2. First Steps in Formal Proofs
Indeed, formal statements in Coq are themselves terms and as such they have a type and
their subterms obey type constraints. An equality statement in particular is obtained by
applying the constant eq to two arguments of the same type. This application results in a
well-formed term of type Prop, for proposition.
Throughout this book, we will use the word proposition for a term of type Prop, typically
something one wants to prove.
The About vernacular command provides information on a constant: its type, the list of
arguments of the constant that are implicit, . . . . For instance we can learn more about the
constant eq:
The constant eq is a predicate, i.e., a function that outputs a proposition. The equality
predicate is polymorphic: exactly like we have seen in the previous chapter, the ∀ quantifier
is used to make the (implicit) parameter A range over types. Both examples 3 = 3 and
false && true = false thus use the same equality constant, but with different values (respec-
tively, nat and bool) for the type parameter A. Since the first argument of eq is implicit, it is
not part of the infix notation and its value is not provided by the user. This value can indeed
be inferred from the type of the two sides of the identity: (3 = 3) unfolds to (eq _ 3 3) , and
the missing value must be nat, the type of 3. Similarly, (false && true = false) unfolds to
(eq _ (false && true) false) and the missing value is bool, the common type of false and
(false && true) .
As the Coq system checks the well-typedness of statements, the two sides of a well-
formed equality should have the same type:
1 Check 3 = [:: 3]. Error: The term [:: 3] has type seq nat
2 while it is expected to have type nat.
1 Check 3 = 4. 3 = 4 : Prop
In order to establish that a certain equality holds, the user should first announce that
she is going to prove a sentence, using a special command like Lemma. This command has
several variants Theorem, Remark, Corollary,. . . which are all synonyms for what matters here.
A Lemma keyword is followed by the name chosen for the lemma and then by the statement
itself. Command Lemma and its siblings are in fact a variant of the Definition syntax we
used in chapter 1: everything we mentioned about it also applies here. The Proof command
marks the beginning of the proof text, which ends either with Qed or Admitted. After the
command Proof is executed, the system displays the current state of the formal proof in a
dedicated window.
Indeed, Coq is now in its so-called proof mode: we can execute new commands to
construct a proof and inspect the current state of a proof in progress, but some other
commands, like opening sections, are no longer available. At any stage of the proof
construction, Coq displays the current state of the (sub)proof currently pending: a list of
named hypotheses forms the current context and is printed on top of the horizontal bar
(empty here), whereas the statement of the current goal (the conjecture to be proved) is
below the bar.
We will explain how to proceed with such a proof in section 2.2.1. For now, let us just
admit this result, using the Admitted command.
1 Lemma my_first_lemma : 3 = 3.
2 Proof.
3 Admitted.
Although we have not (yet) provided a proof for this lemma, a new definition has been
added to our environment:
In the rest of the chapter, we will often omit the Admitted proof terminator, and simply
reproduce the statement of some lemmas in order to discuss their formulation.
2.1.2 Identities
Ground equalities are a very special case of mathematical statements called identities.
An identity is an equality relation A = B that holds regardless of the values that are
substituted for the variables in A and B. Let us state for instance the identity expressing
the associativity of the addition operation on natural numbers:
Note that in the statement of addnA, the right hand side does not feature any parentheses
but should be read ((m + n) + k) : This is due to the left-associativity of the infix + notation,
which was prescribed back when this notation was defined (see section 1.7). Command
Lemma, just like Definition, allows for dropping the type annotations of parameters if these
types can be inferred from the statement itself:
1 Lemma addnA n m k : m + (n + k) = m + n + k.
Boolean identities play a central role in the Mathematical Components library. They
state equalities between boolean expressions (possibly with parameters). For instance,
the orbT statement expresses that true is right absorbing for the boolean disjunction
operation orb. Recall from section 1.2.1 that orb is equipped with the || infix notation:
More precisely, lemma orbT expresses that the truth table of the boolean formula
(b || true)coincides with the (constant) one of true: otherwise said, that the two proposi-
tional formulas are equivalent, or that (b || true) is a propositional tautology. Below, we
provide some other examples of such propositional equivalences stated as boolean identities.
46 Chapter 2. First Steps in Formal Proofs
Proving these identities (once we have learned to provide proofs) is left as an exercise (see
exercise 8).
As a general fact, boolean identities express that two boolean statements are equivalent.
We already encountered special cases of such equivalence with propositional tautologies
in section 2.1.2. Here are a few more examples involving boolean predicates on natural
numbers that we have defined in chapter 1: the equality test == and its negation !=, the
order relation < and its large version <= , and the divisibility predicate %|, with (a %| b)
meaning a divides b. Note that we omit the type of the parameters; they are all of type
nat, as enforced by the type of the operators involved in the statements:
This arrow -> is the same as the one we used in chapter 1 in order to represent function
types. This is no accident, but we postpone further comments on the meaning of this
arrow to section 3.1. For now let us only stress that -> is right-associative, and therefore a
succession of arrows expresses a conjunction of conditions:
1 Lemma my_first_lemma : 3 = 3.
2 Proof.
3 Admitted.
In the Coq system, the user builds a formal proof by providing, interactively, instructions
to the Coq system that describe the gradual construction of the proof she has in mind.
This list of instructions is called a proof script, and the instructions it is made of are called
proof commands, or more traditionally tactics. The language of tactic we use is called
SSReflect.
1 Lemma my_first_lemma : 3 = 3.
2 Proof.
3 (* your finished proof script comes here *)
4 Qed.
Once the proof is complete, we can replace the Admitted command by the Qed one. This
command calls the proof checker part of the Coq system, which validates a posteriori that
the formal proof that has been built so far is actually a complete and correct proof of the
statement, here 3 = 3.
In this section, we will review different kinds of proof steps and the corresponding
tactics.
1 Lemma my_first_lemma : 3 = 3.
2 Proof. by []. No more subgoals.
Indeed, this statement holds trivially, because the two sides of the equality are syntacti-
cally the same. The tactic “by []” is the command that implements this nature of trivial
48 Chapter 2. First Steps in Formal Proofs
proof step. The proof command by typically prefixes another tactic (or a list thereof): it is
a tactical. The by prefix checks that the following tactic trivializes the goal. But in our
case, no extra work is needed to solve the goal, so we pass an empty list of tactics to the
tactical by, represented by the empty bracket [].
The system then informs the user that the proof looks complete. We can hence
confidently conclude our first proof by the Qed command:
Just like when it was Admitted, this script results in a new definition being added in our
context, which can then be reused in future proofs under the name my_first_lemma. Except
that this time we have a machine checked proof of the statement of my_first_lemma. By
contrast Admitted happily accepts false statements. . .
What makes the by [] tactic interesting is that it can be used not only when both sides
of an equality coincide syntactically, but also when they are equal modulo the evaluation of
programs used in the formal sentence to be proved. For instance, let us prove that 2 + 1 = 3.
1 Lemma my_second_lemma : 2 + 1 = 3.
2 Proof. by []. Qed.
Indeed, this statement holds because the two sides of the equality are the same, once
the definition of the addn function, hidden behind the infix + notation, is unfolded, and
once the calculation is performed. In a similar way, we can prove the statement (0 <= 1) ,
or (odd 5) , because both expressions compute to true.
As we have seen in chapter 1, computation is not limited to ground terms; it is really
about using the rules of the pattern matching describing the code of the function. For
instance the proof of the addSn identity:
is trivial as well because it is a direct consequence of the definition of the addn function:
This function is defined by pattern matching, with one of the branches stating exactly this
identity. Statements like (0 + n = n) or (0 < n.+1) can be proved in a similar way, but also
(2 + n = n.+2) , which requires several steps of computation.
Last, the by tactical turns its argument into a terminating tactic — and thus by [] is
such a terminating tactic. A tactic is said to be terminating if, whenever it does not solve
the goal completely, it fails and stops Coq from processing the proof script. A terminating
tactic is colored in red so that the eye can immediately spot that a proof, or more commonly
a subproof, ends there.
Indeed, proving this identity requires more than a simple unfolding of the definition of
negb:
One also needs to perform a case analysis on the boolean value of the parameter b and
notice that the two sides coincide in both cases. The tactic case implements this action:
More precisely, the tactic “case: b” indicates that we want to perform a case analysis
on term b, whose name follows the separator :. The Coq system displays the state of
the proof after this command: The proof now has two subcases, treated in two parallel
branches, one in which the parameter b takes the value true and one in which the parameter
b takes the value false. More generally, the case: t tactic only works when t belongs to an
inductive type. This tactic then performs a case analysis on (the shape of) a term t. As
any inhabitant of an inductive type is necessarily built from one of its constructors, this
tactic creates as many branches in the proof as the type has constructors, in the order in
which they appear in the definition of the type. In our example, the branch for true comes
first, because this constructor comes first in the definition of type bool.
We shall thus provide two distinct pieces of script, one for each subproof to be con-
structed, starting with the branch associated with the true value. In order to help the
reader identify the two parts of the proof script, we indent the first one.
Once the case analysis has substituted a concrete value for the parameter b, the proof
becomes trivial, in both cases: We are in a similar situation as in the proofs of section 2.2.1
and the tactic by [] applies successfully:
Once the first goal is solved, we only have one subgoal left, and we solve it using the
same tactic.
However, as we mentioned earlier, we can also use the by tactical as a prefix for any
tactic (not just an empty list of tactics), and have the system check that after the case
tactic, the proof actually becomes trivial, in both branches of the case analysis. This way,
50 Chapter 2. First Steps in Formal Proofs
n : nat
1 Lemma leqn0 n : (n <= 0) = (n == 0).
=====================
2 Proof.
(n <= 0) = (n == 0)
Both comparison operations <= and == are defined by case analysis on their first argument,
independently of the shape of the second. The proof of leq0n thus goes by case analysis
on term (n : nat) , as it appears as a first argument to both these comparison operators.
Remember that the inductive type nat is defined as:
with two constructors, O which has no argument and S which has one (recursive) argument.
A case analysis on term (n : nat) thus has two branches: one in which n is 0 and one in
which n is (S k) , denoted k.+1, for some (k : nat) . We hence need a variant of the case
tactic, in order to name the parameter k that appears in the second branch as the argument
of the S constructor of type nat:
The tactic “case: n => [|k]” can be decomposed into two components, separated by
the arrow =>. The left block “case: n” indicates that we perform a case analysis action,
on term (n : nat) , while the right block “[|k]” is an introduction pattern. The brackets
surround slots separated by vertical pipes, and each slot allows to name the parameters to
be introduced in each subgoal created by the case analysis, in order.
As type nat has two constructors, the introduction pattern [|k] of our case analysis
command uses two slots: the last one introduces the name k in the second subgoal and
the first one is empty. Indeed, in the first subgoal (first branch of the case analysis), n is
substituted with 0. In the second one, we can observe that n has been substituted with
k.+1. As hinted in the first chapter, the term (k.+1 <= 0) is displayed as (k < 0) .
The first goal can easily be solved by computation, as both sides of the equality evaluate
to true.
The second and now only remaining goal corresponds to the case when n is the successor
of k. Note that (k < 0) is a superseding notation for (k.+1 <= 0) , as mentioned in section
1.7. This goal can also be solved by computation, as both sides of the equality evaluate to
false. The final proof script is hence:
We will use a last example of boolean equivalence to introduce more advanced proof
techniques, leading to less verbose proof scripts. Remember from chapter 1 that the
product of two natural numbers is defined as a function (muln : nat -> nat -> nat) . From
this definition, we prove that the product of two (natural) numbers is zero if and only if
one of the numbers is zero:
In the case when m is zero (whatever value n takes), both sides of the equality evaluate to
true: the left hand side is equal modulo computation to (0 == 0) , which itself computes
to true, and the right hand side is equal modulo computation to ((0 == 0) || (n == 0)) ,
hence to (true || (n == 0)) and finally to true because the boolean disjunction (_ || _) is
defined by case analysis on its first argument.
1 Lemma muln_eq0 m n :
n, m : nat
2 (m * n == 0) = (m == 0) || (n == 0).
=========================
3 Proof.
(m.+1 * n == 0) =
4 case: m => [|m].
(m.+1 == 0) || (n == 0)
5 by [].
In this script, we used the name m for the argument of the constructor in the second
branch of the case analysis. There is no ambiguity here and this proof step reads: either m
is zero, or it is of the form m.+1 (for a new m).
By default, the successor case is treated in the second subgoal, according to the order
of constructors in the definition of type nat. If we want to treat it first, we can use the
“; last first” tactic suffix:
It is a good practice to get rid of the easy subgoal first: since we are going to indent
the text of its subproof, it better be the shortest one. In this way the reader can easily
skip over the simple case, that is likely to be less interesting than the hard one.
Here the successor case is such an easy subgoal: when n is of the form k.+1, it is easy to
see that the right hand side of the equality evaluates to false, as both arguments of the
52 Chapter 2. First Steps in Formal Proofs
boolean disjunction do. Now the left hand side evaluates to false too: by the definition
of muln, the term (m.+1 * k.+1) evaluates to (k.+1 + (m * k.+1)) , and by definition of the
addition addn, this in turn reduces to (k + (m * k.+1)).+1 . The left hand side term hence
is of the form t.+1 == 0, where t stands for (k + (m * k.+1)) , and this reduces to false. In
consequence, the successor branch of the second case analysis is trivial by computation.
1 Lemma muln_eq0 m n :
1 subgoal
2 (m * n == 0) = (m == 0) || (n == 0).
3 Proof.
m : nat
4 case: m => [|m].
=========================
5 by [].
(m.+1 * 0 == 0) =
6 case: n => [|k]; last first.
(m.+1 == 0) || (0 == 0)
7 by [].
This proof script can actually be made more compact and, more importantly, more
linear by using extra features of the introduction patterns. It is indeed possible, although
optional, to inspect the subgoals created by a case analysis and to solve the trivial ones on
the fly, as the by [] tactic would do, except that in this case no failure happens in the case
some, or even all, subgoals remain. For instance in our case, we can add the optional //
simplify switch to the introduction pattern of the first case analysis:
Only the first generated subgoal is trivial: Thus, it has been closed and we are left with
the second one. Similarly, we can get rid of the second goal produced by the case analysis
on n:
1 Lemma muln_eq0 m n :
m : nat
2 (m * n == 0) = (m == 0) || (n == 0).
=========================
3 Proof.
(m.+1 * 0 == 0) =
4 case: m => [|m] //.
(m.+1 == 0) || (0 == 0)
5 case: n => [|k] //.
This // switch can be used in more general contexts than just this special case of
introduction patterns: It can actually punctuate more complex combinations of tactics,
avoiding spurious branching in proofs in a similar manner [GMT15, section 5.4].
The last remaining goal cannot be solved by computation. The right hand side evaluates
to true, as the left argument of the disjunction is false (modulo computation) and the
right one is true. However, we need more than symbolic computation to show that the left
hand side is true as well: the fact that 0 is a right absorbing element for multiplication
indeed requires reasoning by induction (see section 2.3.4).
To conclude the proof we need one more proof command, the rewrite tactic, that lets
us appeal to an already existing lemma.
2.2.3 Rewriting
This section explains how to locally replace certain subterms of a goal with other terms
during the course of a formal proof. In other words, we explain how to perform a rewrite
2.2 Formal proofs 53
proof step, thanks to the eponymous rewrite tactic. Such a replacement is licit when the
original subterm is equal to the final one, up to computation or because of a proved identity.
The rewrite tactic comes with several options for an accurate specification of the operation
to be performed.
Let us start with a simple example and come back to the proof that we left unfinished
at the end of the previous section:
1 Lemma muln_eq0 m n :
m : nat
2 (m * n == 0) = (m == 0) || (n == 0).
=======================
3 Proof.
(m.+1 * 0 == 0) =
4 case: m => [|m] //.
(m.+1 == 0) || (0 == 0)
5 case: n => [|k] //.
1 (0 == 0) = (m.+1 == 0) || (0 == 0)
which is equal modulo computation to (true = true) , hence trivial. But since the definition
of muln proceeded by pattern matching on its first argument, (m.+1 * 0) does not evaluate
symbolically to 0: This equality holds but requires a proof by induction, as explained in
section 2.3.4. For now, let us instead derive (m.+1 * 0 = 0) from a lemma. Indeed, the
Mathematical Components library provides a systematic review of the properties of the
operations it defines. The lemma we need is available in the library as:
1 Lemma muln0 n : n * 0 = 0.
As a side remark, being able to find the “right” lemma is of paramount importance for
writing modular libraries of formal proofs. See section 2.5 which is dedicated to this topic.
Back to our example, we use the rewrite tactic with lemma muln0, in order to perform
the desired replacement.
1 Lemma muln_eq0 m n :
2 (m * n == 0) = (m == 0) || (n == 0). m : nat
3 Proof. =======================
4 case: m => [|m] //. (0 == 0) =
5 case: n => [|k] //. (m.+1 == 0) || (0 == 0)
6 rewrite muln0.
The rewrite tactic uses the muln0 lemma in the following way: It replaces an instance of
the left hand side of this identity with the corresponding instance of the right hand side.
The left hand side of muln0 can be read as a pattern (_ * 0) , where _ denotes a wildcard:
The identity is valid for any value of its parameter n. The tactic automatically finds where
in the goal the replacement should take place, by searching for a subterm matching the
pattern (_ * 0) . In the present case, there is only one such subterm, (m.+1 * 0) , for which
the parameter (or the wild-card) takes the value m.+1. This subterm is hence replaced by 0,
the right hand side of muln0, which does not depend on the value of the pattern. We can
now conclude the proof script, using the prenex by tactical1 :
1 Passing a single tactic to by requires no brackets; i.e., we can write by rewrite muln0 instead of
by [rewrite muln0].
54 Chapter 2. First Steps in Formal Proofs
Arguments to the rewrite tactic are typically called rewrite rules and can be prefixed
by flags tuning the behavior of the tactic.
The proof goes as follows: The left hand side can equivalently be written as (m * n1 - m * n2 == 0) ,
which factors into (m * (n1 - n2) == 0) . But this is equivalent to one of the arguments of
the product being zero. And (n1 - n2 == 0) means (n1 <= n2) .
The first step is performed using the following equation:
The proof of this identity is trivial, as the right hand side is the definition of the leq
relation, denoted by the <= infix notation. Rewriting with this equation turns the left hand
side of our goal into a subtraction:
The command rewrite leqE only affects the first occurrence of <= , but we would like to
substitute both. In order to rewrite all the possible instances of the rule in the goal, we
may use a repetition flag, which is !:
Now the definition of <= has been exposed everywhere in the goal, i.e., at both its
occurrences in the initial goal. We can now factor out m on the left, according to the
appropriate distributivity property:
1 Lemma mulnBr n m p : n * (m - p) = n * m - n * p.
2.3 Quantifiers 55
This time we need to perform a right-to-left rewriting of the mulnBr lemma (instead of
the default left-to-right). The rewriting step first finds in the goal an instance of pattern
(_ * _ - _ * _) , where the terms matched by the first and the third wildcards coincide.
The syntax for right-to-left rewriting consists in prefixing the name of the rewrite rule with
a minus - :
The last step of the proof uses lemma muln_eq0 to align the left and the right hand sides of
the identity.
The proof can now be completed by prefixing the tactic with the by tactical.
We only provided here some hints on the basic features of the rewrite tactic. Section 2.4.1
gives more details on the matching algorithm and on the flags supported by rewrite. The
complete description of the features of this tactic is found in the manual [GMT15].
2.3 Quantifiers
2.3.1 Universal quantification, first examples
Let us compare an example of a function we defined in chapter 1:
1 Definition leq n m := m - n == 0.
We recall, as seen in chapter 1, that this concise syntax for defining leq stands for:
The curious reader might already have tested the answer of the About command on
some parametric lemmas:
She has thus observed that Coq’s output features a prenex forall quantifier. This
universal quantifier binds a natural number, and expresses — as expected — that the
equation holds for any natural number. In fact, the types of the lemmas and theorems
with parameters all feature prenex universal quantifiers:
Quantifiers may also occur elsewhere in a statement, and not only in prenex position.
In the following example, we use the function nth, extracting the element of a sequence at
a given position, which was the object of exercise 4. This statement expresses that two
sequences with the same size and whose n-th elements coincide for any n are the same.
The second hypothesis, about the elements, is itself a quantified formula:
Observe that in the above statement of size_map, we have used a compact notation for
successive universal quantifications: “∀ (f : T1 -> T2) (s : seq T1), ...” is syntactic sugar
for “∀ f : T1 -> T2, ∀ s : seq T1, ...”. However, in this case of prenex quantification, we
could just as well write:
and the lemma stating the commutativity of the addn operation is in fact:
The Mathematical Components library defines several such predicates, which are used
as templates in order to state standard properties in a consistent and compact way. We
provide below a few examples:
1 Section StandardPredicates.
2 Variable T : Type.
3 Implicit Types (op add : T -> T -> T).
4 Definition associative op := ∀ x y z, op x (op y z) = op (op x y) z.
5 Definition left_distributive op add :=
6 ∀ x y z, op (add x y) z = add (op x z) (op y z).
7 Definition left_id e op := ∀ x, op e x = x.
8 End StandardPredicates.
Beside the standardization of the statements through these predicates, the Mathematical
Components library uses a systematic naming policy for the lemmas that are instances of
these predicates. A common suffix C is used for commutativity properties like addnC or mulnC.
Such naming conventions are also useful to search the library, as detailed in section 2.5.
Another class of predicates typically describes usual properties of functions; these
usually feature quantifiers in their definitions:
1 Section MoreStandardPredicates.
2 Variables rT aT : Type.
3 Implicit Types (f : aT -> rT).
4 Definition injective f := ∀ x1 x2, f x1 = f x2 -> x1 = x2.
5 Definition cancel f g := ∀ x, g (f x) = x.
6 Definition pcancel f g := ∀ x, g (f x) = Some x.
7 End MoreStandardPredicates.
1 Check 3 = 3. 3 = 3 : Prop
2 Check (commutative addn). commutative addn : Prop
1 Section Chinese.
2
3 Variables m1 m2 : nat.
4 Hypothesis co_m12 : coprime m1 m2.
5
6 Lemma chinese_remainder x y :
7 (x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
8 Proof.
9 ...
10 End.
11
12 End Chinese.
The part of this excerpt up to the beginning of the lemma corresponds to a mathematical
sentence of the form: In this section, m1 and m2 are two coprime natural numbers. . . .
Within the scope of this section, the parameters m1 and m2 are fixed and the hypothesis
co_m12 is assumed to hold. Outside the scope of the section (i.e., after the End Chinese
command), these variables and the hypotheses are generalized, so that the statement of
chinese_remainder becomes:
Note that the syntax to start a Lemma lets one name not only parameters such as m1 and m2,
but also assumptions such as co_m12.
In general, when a section ends, the types of the constants and the statements of the
lemmas change to include those section variables and hypotheses that are actually used in
their definitions or proofs.
In order to save the effort of explicitly mentioning trivial steps in the proof script, we can
extend the power of the by terminator to make it aware of some lemmas available in the
library. The Hint Resolve command is used to tag these lemmas, as in:
1 (* This line belongs to the file where leqnn is stated and proved.*)
2 Hint Resolve leqnn.
3 Lemma example a b : a + b <= a + b.
2.3 Quantifiers 59
Observe that the goal is now closed without a mention of leqnn, although it has been used
by the system to conclude the proof.
In order to illustrate more proof techniques related to the use of lemmas inside proofs,
let us scrutinize a formal proof that a prime number which divides m! + 1 for a certain
integer m has to be greater than m. This lemma is a key step in a proof that there are
infinitely many primes, which will be studied in section 4.3.1. The proof of the lemma goes
by contraposition: If p is a prime number smaller than m, then it divides m! and thus it
cannot divide m! + 1 as it does not divide 1. We first state this lemma as follows:
where p %| m‘! stands for “p divides the factorial of m”. there is a proble
The first step of our formal proof will be to give a name to the hypothesis (prime p) , the factorial nota
which means that we add it to the current context of the goal. The dedicated tactic for this the beginning of
naming step is move=> followed by the name given to the hypothesis, because the hypothesis
moves from under the bar to above the bar:
The second step of the proof is to transform the current goal into its contrapositive.
This means that we use the lemma
which describes (one direction of) the contraposition law (namely, that an implication
between booleans can be derived from its contraposition). The apply: contraLR tactic finds
the appropriate values of the premise and conclusion and instantiates the law, leaving us
with the task of proving that p is not a divisor of (m ‘! + 1) under the assumption that p is
not greater than m:
More precisely, the values chosen by the tactic for the two parameters c, b of lemma
contraLR are (m < p) and (p %| m ‘! + 1) . They have been found by comparing the statement
to be proved with the conclusion (b -> c) of the statement of the lemma contraLR. The new
statement of the goal is the corresponding instance of the premise (~~ c -> ~~ b) of lemma
contraLR.
The next steps in our formal proof are to improve the shape of the hypothesis ~~ (m < p)
(using rewrite -leqNgt) and to give it a name (using move=> leq_p_m):
60 Chapter 2. First Steps in Formal Proofs
Observe the second goal at the bottom of the buffer, which displays the statement of
the side condition to be proved later. The context of this subgoal is omitted but we do not
really need to see it: We know that statement p %| m‘! holds because p <= m and because
we can combine the following lemmas:
Notice that the expression 0 < m <= n in dvdn_fact is really an abbreviation for (0 < m) && (m <= n) .
The first goal is also easy to solve, using the following basic facts:
For brevity, we record the goal solved by a tactic in a comment after this tactic. Before
improving this script a comment is due: the goal after line 12, 0 < p <= m, is really an
abbreviation for (0 < p) && (p <= m) . The subsequent rewrite command replaces (0 < p)
with true: after all the conclusion of prime_gt0 is an equation. We explain such tricks in
details later on.
We shall improve this script in two steps. First, we take advantage of rewrite sim-
plification flags. It is quite common for an equation to be conditional, hence for rewrite
to generate side conditions. We have already suggested that a good practice consists in
proving the easy side conditions as soon as possible. Here, the first two side conditions are
indeed trivial, and, just as with the introduction patterns of the case tactic, we can use a
simplification switch // to prove them. We also combine on the same line the first three
steps, using the semicolon.2 The proof script (up to the end of the proof of the first goal)
then looks like this:
A careful comparison of the conclusions of gtnNdvd and prime_gt1 reveals that they are both
rewriting rules. While the former features an explicit “.. = false”, in the latter one the
“.. = true” part is hidden, but is there. This means both lemmas can be used as identities.
R All boolean statements can be rewritten as if they were regular identities. The result
is that the matched term is replaced with true.
Rewriting with prime_gt1 leaves open the trivial goal true (i.e., (true = true) ), and the
side condition (prime p) . Both are trivial, hence solved by prefixing the line with by.
2 From this example, one might take away the wrong impression that a semicolon is synonymous to a dot.
In general, it is not, since the tactic following it is applied to each goal resulting from the tactic preceding
it. More details can be found in [Coq, section 9.2].
62 Chapter 2. First Steps in Formal Proofs
To sum up, both apply: and rewrite are able to find the right instance of a quantified
lemma and to generate subgoals for its eventual premises. Hypotheses can be named using
move=>.
The proof script given above for example m p can be further reduced in size. One
simple improvement is to replace the chained tactic rewrite -leqNgt; move=> leq_p_m by the
equivalent rewrite -leqNgt => leq_p_m. Indeed, as we will see later (in subsection 3.2.2), the
move tactic does nothing; it is the => that is responsible for naming the hypothesis.
In section 2.4.1, we shall describe some further ways to shrink the proof script.
Here P is quantified exactly as n is, but its type is a bit more complex and deserves an
explanation. As we have seen in the first chapter, the -> denotes the type of functions; hence
s a problem with P is a function from nat to Prop. Recall that Prop is the type of propositions, i.e., something
macro when the we may want to prove. In the light of that, P is a function producing a proposition out
aracter is -, which of a natural number. For example, the property of being an odd prime can be written as
the space that follows:
s it
1 (fun n : nat => (odd n && prime n) = true)
Indeed, if we take such function as the value for P, the first premise of nat_ind becomes
Remark the similarity between the function argument to foldr that is used to describe the
general term of an iterated sum in section 1.6 and the predicate P here used to describe a
general property.
For example, here is the induction principle for sequences (although denoted by list_ind
rather than seq_ind, as seq is defined merely as a synonym for list), which has some
similarities with the one for natural numbers:
2.3 Quantifiers 63
1 About list_ind.
To sum up: reasoning by induction on a term t means finding the induction lemma
associated to the type of t and synthesizing the right predicate P. The elim: tactic has
these two functionalities, while apply: does not. Thus, while both elim: and apply: can be
used to formalize a proof by induction, the user would have to explicitly specify both t
and P in order to make use of the apply: tactic, whereas the elim: tactic does the job of
determining these parameters itself. The induction principle to be used is guessed from
the type of the argument of the tactic. Let us illustrate on an example how the value of
the parameter P is guessed by the elim: tactic and let us prove by induction on m that 0 is
neutral on the right of addn.
m : nat
1 Lemma addn0 m : m + 0 = m.
IHm : m + 0 = m
2 Proof.
=======================
3 elim: m => [ // |m IHm].
m.+1 + 0 = m.+1
The elim: tactic is used here with an introduction pattern similar to the one we used
for case:. It has two slots, because of the two constructors of type nat (corresponding
naturally to what is commonly called the “induction base” and the “induction step”), and
in the second branch we give a name not only to the argument m of the successor, but also
to the induction hypothesis. We also used the // switch to deal with the base case because
if m is 0, both sides evaluate to zero. The value of the parameter P synthesized by elim: for
us is (fun n : nat => n + 0 = n) . It has been obtained by abstracting the term m in the goal
(see section 1.1.1). This proof can be concluded by using lemma addSn to pull the .+1 out
of the sum, so that the induction hypothesis IHm can be used for rewriting.
Unfortunately proofs by induction do not always run so smooth. To our aid the elim:
tactic provides two additional services.
The first one is to let one generalize the goal. It is typically needed when the goal
mentions a recursive function that uses an accumulator: a variable whose value changes
during recursive calls; hence the induction hypothesis must be general. We show this
feature later on a concrete example (lemma foldl_rev).
Another service provided by elim: is specifying an alternative induction principle. For
example, one may reason by induction on a list starting from its end, using the following
induction principle:
3
4 Lemma foldl_rev T R f (z : R) (s : seq T) :
5 foldl f z (rev s) = foldr (fun x z => f z x) z s .
Here “elim/last_ind: s z” performs the induction using the last_ind lemma on s after
having generalized the initial value of the accumulator z. The resulting value for P hence
features a quantification on z:
which is more general than what we would have obtained if we had not generalized z
beforehand. The quantification on z is crucial since the goal in the induction step, just
before we use IHs, is the following one:
The instance of the induction hypothesis that we need is one where z takes the
value (foldr (fun y w => f w y) z [:: x]) . The generalization of z gave us the freedom to
substitute a different value for z.
Here, our use of the rewrite dvdn_addr tactic forced us to prove the side condition
p %| m‘!. Side conditions (by default) become the second, third (and potentially higher)
sub-goals in a proof script, so their proofs are usually postponed to after the first sub-goal
(the main one) is proven. This is not always desirable; therefore, it is helpful to have a
way to prove side conditions right away, on the same line where they arise. One way to do
this (which we have already seen in action) is using the simplification item // . When this
does not suffice, one can invoke another rewrite rule using the optional iterator ?. A rule
prefixed by ? is applied to all goals zero-or-more times.
The side condition p %| m‘! spawned by rewrite dvdn_addr was proven in the last
line of the script. Instead, we could have solved it right away by rewriting using
?dvdn_fact ?prime_gt0. In fact, optionally rewriting with dvdn_fact on all goals affects
only the side condition, since the main goal does not mention the factorial operator. The
same holds for prime_gt0. The resulting proof script is:
Another functionality offered by rewrite is the possibility to focus the search for the
term to be replaced by providing a context. For example, the most frequent context is RHS
(for Right Hand Side) and is used to force rewrite to operate only on the right hand side of
an equational goal.
1 Lemma silly_example n : n + 0 = (n + 0) + 0.
2 Proof. by rewrite [in RHS]addn0. Qed.
The last rewrite flag worth mentioning is the /= simplification flag. It performs
computations in the goal to obtain a “simpler” form.
The /= flag simply invokes the Coq standard simpl tactic. Whilst being handy, simpl
tends to oversimplify expressions, hence we advise using it with care. In section 4.3.3 we
propose a less risky alternative. The sequence “// /= ” can be collapsed into //= .
Another form of simplification that is often needed is the unfolding of a definition. For
example, the lemma leqE that we used in the proof of leq_mul2l back in section 2.2.3 does When reading t
not exist in the library, and there is no name associated to this equation. It is simply the I thought that l
definition of leq, and we actually do not need to state a lemma in order to relate the name exist. I think we
avoid misleading
like that.
66 Chapter 2. First Steps in Formal Proofs
of a definition, like leq, to its body fun n m => n - m == 0. Such operation can be performed
by prefixing the name of the object with / , as in rewrite /leq. Unfolding a definition is not
a deductive operation but an instance of computation, as made more precise in chapter 3.
1 Lemma leq_mul2l m n1 n2 :
2 (m * n1 <= m * n2) = m, n1, n2 : nat
3 (m == 0) || (n1 <= n2). ==========================
4 Proof. (m * n1 <= m * n2) =
5 rewrite [n1 <= _]leqE. (m == 0) || (n1 - n2 == 0)
1 Lemma leq_mul2l m n1 n2 :
2 (m * n1 <= m * n2) = m, n1, n2 : nat
3 (m == 0) || (n1 <= n2). ==========================
4 Proof. (m * n1 <= m * n2) =
5 rewrite [in RHS]leqE. (m == 0) || (n1 - n2 == 0)
More generally, one can provide context patterns like [in X in T] where X is a variable
name, bound in T. For instance pattern [in RHS] is just syntactic sugar for the context pat-
tern [in X in _ = X]. We invite the interested reader to check the reference manual [GMT15,
section 8] for more variants of patterns and for a more precise description of the different
phases in the matching algorithm used by this tactic.
As we have said, the lemma leqE does not in fact exist in the library, and instead is
just the definition of leq. However if we try to omit the first rewrite !leqE command, then
the next one, namely rewrite -mulnBr, fails:
2.4 Rewrite, a Swiss army knife 67
1 Lemma leq_mul2l m n1 n2 :
2 (m * n1 <= m * n2) = Error: The RHS of mulnBr
3 (m == 0) || (n1 <= n2). (_ * _ - _ * _)
4 Proof. does not match any subterm
5 rewrite -mulnBr. of the goal
This indicates in particular that, although the term (m * n1 <= m * n2) is equal up to
computation to the term (m * n1 - m * n2 == 0) , the matching algorithm is not able to
see it. This is due to the compromise that has been chosen, between predictability and
cleverness. Indeed the algorithm looks for a verbatim occurrence of the head symbol3 of the
pattern: in this case it hence looks for an occurrence of (_ - _) , which is not found. As a
consequence, we need an explicit step in the proof script in order to expose the subtraction
before being able to rewrite right to left with mulnBr. However if we tackle the proof in
reverse, starting from the right hand side, the first -muln_eq0 step will succeed:
1 Lemma leq_mul2l m n1 n2 :
2 (m * n1 <= m * n2) = m, n1, n2 : nat
3 (m == 0) || (n1 <= n2). ==========================
4 Proof. (m * n1 <= m * n2) =
5 rewrite -[_ || _]muln_eq0. (m * (n1 - n2) == 0)
Indeed, the [_ || _] pattern identifies term (m == 0) || (n1 <= n2) , as their head symbols
coincide. Now that we have selected a subterm, the rewrite tactic is able to identify it with
the term (m == 0) || (n1 - n2 == 0) , itself an instance of the right hand side of muln_eq0.
Indeed, while matching only sees syntactic occurrences of the head symbols of patterns, it
is able to compare the other parts of the pattern up to symbolic computation. Note that
the [_ || _] pattern is redundant here; there is no other location in the goal where the
right hand side of muln_eq0 could appear.
Patterns can not only be used in combination with a rewriting rule, but also with a
simplification step /= or an unfolding step like /leq . For example:
1 Lemma leq_mul2l m n1 n2 :
2 (m * n1 <= m * n2) = m, n1, n2 : nat
3 (m == 0) || (n1 <= n2). ==========================
4 Proof. (m * n1 - m * n2 == 0) =
5 rewrite [in LHS]/leq. (m == 0) || (n1 <= n2)
One can also re-fold a definition, but in such a case one has to specify, at least partially,
its folded form.
1 Lemma leq_mul2l_rewritten m n1 n2 :
2 (m * n1 - m * n2 == 0) = m, n1, n2 : nat
3 (m == 0) || (n1 <= n2). ==========================
4 Proof. (m * n1 <= m * n2) =
5 rewrite -/(leq _ _). (m == 0) || (n1 <= n2)
Here, we have used the -/ prefix for the rewrite tactic; it allows folding a definition, i.e.,
the reverse of unfolding.
More generally, the rewrite tactic can be used to replace a certain subterm of the goal
3 The head symbol is the root of the syntax tree of an expression.
68 Chapter 2. First Steps in Formal Proofs
1 Lemma leq_mul2l m n1 n2 :
2 (m * n1 <= m * n2) = (m == 0) || (n1 <= m, n1, n2 : nat
n2). ==========================
3 Proof. (m * (0 + n1) <= m * n2) =
4 rewrite -[n1]/(0 + n1). (m == 0) || (0 + n1 <= n2)
Last, an equation local to the proof context, like an induction hypothesis, can be
disposed of after using it by prefixing its name with {} . For example rewrite -{}IHn rewrites
with IHn right to left and drops IHn from the context.
Indeed the conclusion matches the pattern. Note that one is not forced to use wildcards; odd
alone is a perfectly valid pattern. Many more lemmas are found by leaving the conclusion
unspecified, as in “Search _ odd”.
If we require the lemma to be an equation, as in “Search eq odd”, we find the following
two lemmas (among many other things):
If we want to rule out all lemmas about coprimality we can refine the search by writing
“Search eq odd -coprime”.
2.6 Exercises
Exercise 9 Rewriting
Prove the following lemma by rewriting:
* Exercise 10 Induction
Prove the following lemma by induction:
Recall that a local equation can be disposed of (after use) by prefixing its name with {} .
(where all_words is as defined in the solution of exercise 7). This requires two inductions:
first on the length of words, then on the alphabet. In this last case, a non-trivial sub
expression has to be generalized just before starting the induction.
2.6.1 Solutions
Answer of exercise 8
1 Lemma orbA b1 b2 b3 : b1 || (b2 || b3) = b1 || b2 || b3.
2 Proof. by case: b1; case: b2; case: b3. Qed.
3 Lemma implybE a b : (a ==> b) = ~~ a || b.
4 Proof. by case: a; case: b. Qed.
5 Lemma negb_and (a b : bool) : ~~ (a && b) = ~~ a || ~~ b.
6 Proof. by case: a; case: b. Qed.
Answer of exercise 9
72 Chapter 2. First Steps in Formal Proofs
Answer of exercise 10
Answer of exercise 11
The authors made the deliberate choice to postpone the presentation of the mathematical
foundations of the Coq system and the formal definition of its language. Instead, the
previous chapters have dealt with the definition of (typed) programs and on the way these
programs can be used to describe computable functions and decidable predicates. This take
on calculations is indeed both at the core of the type theory underlying Coq and one of the
crucial ingredients to the methodology at the base of the Mathematical Components library.
The present chapter is devoted to a more in-depth presentation of these mathematical
foundations, although an exhaustive description shall remain out of the scope of the present
book. For more comprehensive presentations of type theory for formalized mathematics,
the reader shall refer to more specialized references like [NG14], or the shorter survey in
the Handbook of Automated Reasoning [BG01, Volume 2, chapter 18].
formulate the axioms of the particular theory of interest. On the contrary a type-theoretic
framework is monolithic and the same language of types is used in a uniform way to describe
mathematical objects, statements and proofs. Logical statements are identified with some
types and their proofs with terms, or programs, having this type. Thus proving a statement
consists in fact in constructing a term of the corresponding type. In set theory, the rules
which govern the construction of grammatically correct statements are rather loose, and
the goal of the game is to construct a proof for a given proposition, using first-order logic
to combine the axioms of the theory. The analogue of the meta-statement that a given
proposition has a proof is the meta-statement that a given term has a given type. Such a
meta-statement is called a typing judgment. It is written:
Γ`t :T
which means: in the context Γ, the term t has the type T . Typing judgments are justified
from typing rules, and these justifications form trees similar to the proof trees of natural
deduction. Before getting more precise about what contexts, terms and types are, let us
emphasize a couple of important differences with set theory here: first, the typing judgment
features explicit expressions for the term and the type, whereas the proof of a statement
in first-order logic is seldom mentioned. Second, the term t shall represent an arbitrary
object of the mathematical discourse, like a number or a group, and not only a proof.
contains the triple (a : T := t). We have not yet defined what a type is, because it is a
special case of term, defined using typing judgments. Actually, well-formed contexts and
typing judgments are defined inductively and simultaneously.
Typing judgments with an empty context express the axiom rules of the formalism, like
for instance the types of sorts:
From now on and as the default display mode of Coq does, we will leave the index of the
sorts Typei implicit and just write Type, as these indices do not play a significant role in
what is presented in this book. A type is a term which can be typed by a sort in a given
context:
Γ ` T : Prop or Γ ` T : Type.
Sorts are thus particular types and they are types of types. A well-formed context is either
an empty context, or the extension of an existing context with a pair (x : T) , where x is
a fresh name and T is a type. As expected, a well-formed context provides a type to the
variables it contains:
Contexts not only store global assumptions: they are also used to forge more complex
typing judgments, for more complex types. For instance, the following rule explains how
to construct non-atomic types:
The term ∀x : T,U : Type is the type of functions, as described by the rule:
and the application of a function to an argument is well-typed only if their types agree:
where U[t/x] denotes the term obtained by substituting the variable x by the term t in the
term U.
Consider the simple tautology A → A. The implication symbol → can be understood
as the logical symbol of implication but also as the symbol we used to represent the
type of functions, in the non-dependent case. The term (fun x : A => x) represents the
identity function for terms of type A and is a program of type A → A. If we consider that
A is a proposition, and that terms of type A are proofs of A, this function is the identity
function on proofs of A. More generally, the logical rules of implicative and universal
statements can be decorated with terms, so that proofs of implications can be seen as
functions transforming an arbitrary proof of the premise into a proof of the conclusion.
The introduction rules respectively for the implication and the universal quantification can
be written:
A
.. B ∀ (x fresh)
. I
B ∀x, B
→I
A→B
76 Chapter 3. Type Theory
This presentation, in the style of natural deduction, means that in order to prove A → B
one can prove B under the assumption A, and in order to prove ∀x, B one can prove B for a
fresh variable x. Let us now annotate these rules with terms whose typing rules coincide
with these proof rules:
x : A
.. b : B
. ∀I
b : B (fun x : A => b) : ∀x, B
→I
(fun x : A => b) : A→B
Actually, the term (fun .. => ..) serves as a proof for both rules and in both cases the
term b is a proof of B. The only difference is that x is allowed to occur in B only in the
second rule.
We now play the same game with the corresponding elimination rules:
A→B A →E ∀x, B
∀E (t is a term)
B B[t/x]
f : A→B t : A →E f : ∀x : A, B t : A
∀E
(f t) : B (f t) : B[t/x]
Universal quantification is not only useful to form types that play the role of propositions.
It can come handy to form data types too. In the second part of this book (section 6.8) we
shall see how the matrix data type and the type of its multiplication function benefit from
it.
This time the data type of matrices exposes the size, and matrix multiplication can be
given a type that rules out incompatible matrices and also describes
the size of the resulting matrix in terms of the size of the input ones.2
This is in fact a classic example of what is called a dependent type: a data type
depending on data, two natural numbers here.
Note that in this formalism, quantification can range on the proofs of a given statement,
just like it can range on numbers. In this way, a statement may express a property
shared by the proofs of a given statement. Such capability finds a rare, but crucial use in
Mathematical Components that we discuss in chapter 6: All the proofs of a given equality
statement between two booleans are indistinguishable.
The proofs-as-programs correspondence has a visible impact in the proofs part of the
Mathematical Components library. In particular, quantified lemmas, being programs,
can be instantiated by simply passing arguments to them. Exactly as one can pass 3
to addn and obtain (addn 3) , the function adding three, one can “pass” 3 to the lemma
2 To be precise, mulmx also needs to take in input operations to add and multiply elements of R. Such
addnC and obtain a proof of the statement (∀ y, 3 + y = y + 3) . Remark that the argument
passed to addnC shows up in the type of the resulting term (addnC 3) : The type of the addnC
program depends on the value the program is applied to. That is the difference between
the dependent function space (∀) and the standard function space (→).
R Lemma names can be used as functions, and you can pass arguments to them. For
example, (addnC 3) is a proof that (∀ y, 3 + y = y + 3) , and (prime_gt0 p_pr) is a
proof that (0 < p) whenever (p_pr : prime p) .
We refer the reader to the reference manual of Coq [Coq] for the other rules of the
system, which are variants of the ones we presented or which express subtleties of the type
system that are out of the scope of the present book, like the difference between the sorts
Prop and Type.
We conclude this section by explaining a last rule of CIC, called the conversion rule,
which describes the status of computation in this framework. Computation is modeled
by rewrite rules explaining how to apply functions to their argument. For instance, the
so-called β -reduction rule rewrites an application of the form (fun x => t)u into t[u/x]: the
formal argument x is substituted by the actual argument u in the body t of the function. A
similar computation rule models the computation of a term of the shape (let x := u in t)
into t[u/x]. Two terms t1 and t2 that are equal modulo computation rules are said to
be convertible, and these terms are indistinguishable to the type system: If T1 and T2
are two convertible types and if a term t has type T1 in the context Γ, then t also has
type T2 in the context Γ. This is the feature of the formalism that we have used in
section 2.2.1: The proofs of the statements 2 + 1 = 3 and 3 = 3 are the same, because the
terms 2 + 1 = 3 and 3 = 3 are convertible. In chapter 1 and 2 we used boolean programs to
express predicates and connectives exactly to take advantage of convertibility: Also the
compound statement (2 != 7 && prime 7) is convertible to true. Finally, as illustrated in
section 1.5, computation is not limited to terms without variables: The term (isT : true)
is a valid proof of (0 < n.+1) , as well as a proof of (0 != p.+1) .
One can also benefit from convertibility whenever one applies a lemma; otherwise said,
whenever the →E and ∀E rules apply. These rules check that the argument has the “right
type”, i.e. the type of the premise or of the bound variable respectively. At the cost of
being more verbose we could have made explicit in, say, the typing for →E that types are
compared modulo computation as follows:
f : A→B a : A0 A ≡ A0 →E
(f a) : B
introduces a new type nat : Type and two new terms (O : nat) and (S : nat -> nat) . Con-
structors are functions, possibly of zero arguments like O, and the codomain of a constructor
of the inductive type T is always T. An inductive type may occur as the type of certain
arguments of its constructors, like in the case of S. The only way to construct an inhabitant
of an inductive type is to apply a constructor to sufficiently many arguments. Constructors
are by definition injective functions. Moreover, two distinct constructors construct distinct
terms; this is why a function with an argument of an inductive type can be described
by pattern matching on this argument. For instance, in chapter 1, we have defined the
predecessor function by:
where if ... then ... else ... is a notation for the special case of pattern matching with
only two branches and one pattern. The definition of the terms of the formalism is in fact
extended with the match ... with ... end construction described in section 1.2.2. A special
reduction rule expresses that pattern matching a term which features a certain constructor
in head position reduces to the term in the corresponding branch of the case analysis.
The definition of the terms of CIC also includes so-called guarded fixpoints, which
represent functions with a recursive definition. We have used these fixpoints in chapter 1,
for instance when defining the addition of two natural numbers as:
1 Fixpoint addn n m :=
2 match n with
3 | 0 => m
4 | p.+1 => (addn p m).+1
5 end.
Note that guarded fixpoints always terminate, as a non-terminating term would allow
proofs of absurdity (see section 3.2.3).
A B ∧ A ∧ B ∧ (left)
I E
A∧B A
The first rule reads: to prove A ∧ B one needs to prove both A and B. The second states
that one proves A whenever one is able to prove the stronger statement A ∧ B.
In Coq this connective is modeled by the following inductive definition:
Remark that the “data” type and is tagged as Prop, i.e., we declare the intention to
use it as a logical connective rather than a data type. The single constructor conj takes
two arguments: a proof of A and a proof of B. Moreover and is polymorphic: A and B are
3.1 Terms, types, proofs 79
The striking similarity illustrates how programs (and data) are used in Coq to represent
proofs.
Pattern matching provides a way to express the elimination rule for conjunction as
follows:
1 Definition proj1 A B (p : A /\ B) : A :=
2 match p with conj a _ => a end.
Now recall the similarity between → and ∀, where the former is the simple, non-
dependent case of the latter. If we ask for the type of the conj constructor:
we may wonder what happens if the type of the second argument (i.e., B) becomes
dependent on the value of the first argument (of type A). What we obtain is actually the
inductive definition corresponding to the existential quantification.
As ex_intro is the only constructor of the ex inductive type, it is the only means to
prove a statement like (exists n, prime n) . In such a — constructive — proof, the first
argument would be a number n of type nat while the second argument would be a proof
p of type (prime n) . The parameter P causes the dependency of the second component of
the pair on the first component. It is a function representing an arbitrary predicate over a
term of type A. Hence (P x) is the instance of the predicate, for x. E.g., the predicate of
being an odd prime number is expressed as (fun x : nat => (odd x) && (prime x)) , and the
statement expressing the existence of such a number is
(ex nat (fun x : nat => (odd x) && (prime x))) , which (thanks to the Notation mecha-
nism of Coq) is parsed and
printed as the more familiar (exists x : nat, odd x && prime x) .
It is worth summing up the many features of type theory that intervene in the type of
ex and ex_intro:
Both ex and ex_intro are parameterized by (A : Type) : as we have seen in chapter 1, the
(∀ A : Type) quantification indicates that ex are ex_intro polymorphic constants, that can be
instantiated for any type. Both ex and ex_intro also have a parameter of type (A -> Prop) :
since it does not appear in the rest of the type of ex, this parameter is not named and
80 Chapter 3. Type Theory
the type uses the arrow syntax instead of a more verbose ∀ A : Type, ∀ P : A -> Prop, Prop.
This parameter is indicated by a so-called higher-order quantification, because the pa-
rameter has an arrow type. Constants ex and ex_intro can thus be be specialized to any
predicate P, so that the ex inductive declaration can be used on any formula. Finally, the
ex_intro constant features a last, inner-most ∀ a : A quantifier, which binds a term variable
a representing the witness of the existential statement for P.
Let us also observe the inductive definition of the disjunction or and its two constructors
or_introl and or_intror.
The detail worth noting here is that the pattern match construct has two branches,
and each branch represents a distinct sub proof. In this case, in order to prove P starting
from A \/ B, one has to deal with all cases: i.e., to prove P under the assumption A, and to
prove P under the assumption B.
Usual constants and connectives such as >, ⊥ and ¬ can be defined as follows.
Hence, in order to prove True, one just has to apply the constructor I, which requires
no arguments. So proving True is trivial, and as a consequence eliminating it provides little
help (i.e., no extra knowledge is obtained by pattern matching over I). Contrarily, it is
impossible to prove False, since it has no constructor, and pattern matching on False can
inhabit any type, since no branch has to be provided:
The only base predicate we still haven’t described is equality. The reason we left it as
the last one is that it has a tricky nature. In particular, equality, as we have seen in the
previous chapters, is an open notion in the following sense. Terms that compute to the
same syntactic expression are considered as equal, and this is true for any program the user
may write. Hence such notion of equality needs to be somewhat primitive, as match and fun
are. One also expects such notion to come with a substitutivity property: replacing equals
by equals must be licit.
The way this internal notion is exposed is via the concept of index on which an inductive
type may vary.
3.2 A script language for interactive proving 81
This is the first time we see a function type after the : symbol in an inductive type
declaration. The eq type constructor takes three arguments: a type A and two terms of
that type (the former is named x). Hence one can write (a = b) whenever a and b have the
same type. The erefl constructor takes no arguments, as I, but its type annotation says it
can be used to inhabit only the type (x = x) . Hence one is able to prove (a = b) only when
a and b are convertible (i.e., indistinguishable from a logical standpoint). Conversely, by
eliminating a term of type (a = b) one discovers that a and b are equal and b can be freely
replaced by a.
The notion of equality is one of the most intricate aspects of type theory; an in-depth
study of it is out of the scope of this book. The interested reader finds an extensive study
of this subject in [Uni13]. Later in this chapter we define and use other inductive types
to take advantage of the “automatic” substitution of the implicit equations we see here:
While px has type (P x) , it is accepted as an inhabitant of (P y) because inside the match
the term y is automatically replaced by x.
The only primitive constructor that remains without an associated proof command is
(fun .. => ..) . Operationally, what the →I and ∀I logical rule do is to introduce into the
proof context a new entry. So far we either expressed this step at the beginning of proofs
by placing such items just after the name of the lemma being proved, or just after a case:
or elim: proof command. The current section expands on this subject covering the full
management of the proof context.
========================
∀ xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1
Before accessing the assumption (prime xy.1) , one has to name the bound variable xy,
exactly as one can only access a stack from its top. The execution of => xy pr_x odd_y is
just the composition of => xy with => pr_x and finally => odd_y. Each action pulls an item
out of the stack and names it. The move proof command does nothing, so we use it as a
placeholder for the postfix => bookkeeping action:
Now, en passant, we would like to decompose xy into its first and second component.
Instead of the verbose => xy; case: xy => x y, we can use the symbolic notation [] to
perform such action.
3.2 A script language for interactive proving 83
We can place the /= switch to force the system to reduce the formulas on the stack,
before introducing them in the context, and obtain:
We can also process an assumption through a lemma; when a lemma is used in this
way, it is called a view. This feature is of general interest, but it is especially useful in the
context of boolean reflection, as described in section 4.1. For example, prime_gt1 states
(prime p -> 1 < p) for any p, and we can use it as a function to obtain a proof of (1 < x)
from a proof of (prime x) .
This time, the destruction of y generates two cases for the two branches; hence the
[ .. | .. ] syntax. In the first one, when y is 0, the // action solves the goal, by the trivial
means of the by [] terminator. In the second branch we name y the new variable (which is
legitimate, since the old y has been disposed of).
Now, the fact that y is even is not needed to conclude, so we can discard it by giving it
the _ dummy name.
The way to discard an already named assumption is to mention its name in curly braces,
as => {x_gt1}.
84 Chapter 3. Type Theory
We finally conclude with the apply: command. In the example just shown, we have
used it with two arguments: a function and its last argument. In fact, the lemma ltn_addl
looks as follows:
automatically fills in the blanks between the function ltn_addl (the lemma name)
apply:
and the argument x_gt1 provided. Since we are passing x_gt1, the variable m picks the
value 1. The conclusion of ltn_addl hence unifies with (2 < y.+1 + x) because both + and <
are defined as programs that compute: Namely, addition exposes a .+1, thus reducing to
2 < (y+x).+1; then < (or, better, the underlying <= ) eats a successor from both sides, leading
to 1 < y + x, which looks like the conclusion of the lemma we apply.
Here we have shown all possible actions one can perform in an intro pattern, squeezing
the entire proof into a single line. This has to be seen both as an opportunity and as
a danger: one can easily make a proof unreadable by performing too many actions in
the bookkeeping operator =>. At the same time, a trivial sub-proof like this one should
take no more than a line, and in that case one typically sacrifices readability in favor of
compactness: what would you learn by reading a trivial proof? Of course, finding the right
balance only comes with experience.
R The case intro pattern [..|..] obeys an exception: when it is the first item of an
intro pattern, it does not perform a case analysis, but only branch on the subgoals.
Indeed in case: n => [|m] only one case analysis is performed.
========================
∀ xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1
and we stop just after applying the view, we end up in a valid state:
One can also chain multiple views on the same stack item:
Two other operations are available on the top stack item: specialization and substitution.
Let’s take the following conjecture.
3.2 A script language for interactive proving 85
========================
(∀ n, n * 2 = n + n) -> 6 = 3 + 3
The top stack item is a quantified assumption. To specialize it to, say, 3 one can write
as follows:
The idea behind the syntax here is that when we apply a view v to the top stack item
(say, top), by writing /v , we are forming the term (v top) , whereas when we specialize the
top stack item top to an object x, by writing /(_ x) , we are forming the term (top x) . The
_ is a placeholder for the top item, and is omitted in /(v _) .
When the top stack item is an equation, one can substitute it into the rest of the goal,
using the tactics <-
and -> for right-to-left and left-to-right respectively.
In other words, the arrows are just a compact syntax for rewriting, as in the rewrite
tactic, with the top assumption.
Pushing to the stack
We have seen how to pull items from the stack to the context. Now let’s see the so called
discharging operator :, performing the converse operation. Such operator decorates proof
commands as move, case and elim with actions to be performed before the command is
actually run.
R The colon symbol in apply: is not the discharging operator. It is just a marker to
distinguish the apply: tactic of SSReflect from the apply tactic of Coq. Indeed the
two tactics, while playing similar roles, behave differently [GMT15, §5.2 and §5.3].
x, y : nat
x_gt1 : 1 < x
odd_y : odd y
========================
2 < y + x
The command case: y is equivalent to move: y; case. where move once again is a place-
holder, : y pushes the y variable onto the stack, and case operates on the top item of the
stack. Pushing items on the stack is called discharging.
Just before running case, the goal would look like this:
x : nat
x_gt1 : 1 < x
odd_y : odd y
========================
86 Chapter 3. Type Theory
∀ y, 2 < y + x
However, this is not actually a well-defined state. Indeed, the binding for y is needed
by the odd_y context item, so move: y fails. One has to push items onto the stack in a valid
order: first, all properties of a variable, then the variable itself. The correct invocation,
move: y odd_y, pushes first odd_y and only then y onto the stack, leading to the valid goal
x : nat
x_gt1 : 1 < x
========================
∀ y, odd y -> 2 < y + x
2 subgoals
x : nat
x_gt1 : 1 < x
========================
odd 0 -> 2 < 0 + x
subgoal 2 is:
∀ n : nat, odd n.+1 -> 2 < n.+1 + x
Note that listing context entry names inside curly braces purges them from the context.
For instance the tactic case: y {odd_y} clears the odd_y fact. But this would lead to a dead
end in the present proof, so let us come back to the proof of the implication ??.
One can combine : and => around a proof command, to first prepare the goal for its
execution and finally apply the necessary bookkeeping to the result. For example:
At the left of the : operator one can also put a name for an equation that links the
term at the top of the stack before and after the execution of the tactic. For example,
case E: y odd_y => [|y’] leads to the following two subgoals:
x, y : nat
x_gt1 : 1 < x
E : y = 0
============================
odd 0 -> 2 < 0 + x
x, y : nat
x_gt1 : 1 < x
y’ : nat
E : y = y’.+1
========================
3.2 A script language for interactive proving 87
Last, one can push any term onto the stack – whether or not this term appears in the
context. For example, “move: (leqnn 7)” pushes on the stack the additional assumption
(7 <= 7) (and thus “move: (leqnn 7) => A” brings this assumption into the context under the
name A). This will come handy in section 3.2.4.
1 About nat_ind.
nat_ind is a program that produces a proof of (P n) for any n, proviso a proof for the base
case (P 0) , and a proof of the inductive step (∀ n : nat, P n -> P n.+1) . Let us write such
a program by hand.
The Coq system generates this program automatically, as soon as the nat data type is
defined. Recall that recursive functions are checked for termination: Through the lenses of
the proofs-as-programs correspondence, this means that the induction principle just coded
is sound, i.e., based on a well-founded order relation.
If non-terminating functions are not ruled out, it is easy to inhabit the False type, even
if it lacks a proper constructor.
Of course Coq rejects the definition of oops. To avoid losing consistency, Coq also enforces
some restrictions on inductive data types. For example the declaration of hidden is rejected.
Note how oops calls itself, as in the previous example, even if it is not a recursive function.
Such restriction, called positivity condition, is out of scope for this book. (Roughly speaking,
it says that constructors for an inductive data type can only depend on maps to the data
type but not on maps from it.) The interested reader shall refer to [Coq].
Line 3 requires some explanations. First of all, “elim: n {-2}n (leqnn n).” is shorthand
for “move: (leqnn n). move: {-2}n. move: n. elim.” (the terms after the colon : are pushed
to the stack, from right to left; and the elim tactic is applied afterwards to the top of the
stack, which of course is the last term pushed to the stack). Let us see how these four
steps transform the goal. At the beginning, the context and the goal are
n : nat
============================
11 < n -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n
The first of our four steps (“move: (leqnn n)”) pushes the additional assumption n <= n
onto the stack (since (leqnn n) provides its proof); we are thus left with
1 subgoal
n : nat
============================
n <= n -> 11 < n -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n
The second step (“move: {-2}n”) is more interesting. Recall that move: usually “generalizes”
a variable (i.e., takes a variable appearing in the context, and binds it by the universal
quantifier, so that the goal becomes a for-all statement). The prefix {-2} means “all except
for the 2nd occurrence in the goal”; so the idea is to generalize “all except for the 2nd
occurrence of n”. Of course, this implies that n still has to remain in the context (unlike
for “move: n”), so the bound variable of the universal quantifier has to be a fresh variable,
picked automatically by Coq. For example, Coq might pick n0 for its name, and so the
state after the second step will be:
n : nat
============================
∀ n0 : nat,
n0 <= n -> 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
Notice how the n in “n0 <= n” has remained un-generalized, since it was the 2nd occur-
rence of n before the second step.
The third step (“move: n”) merely moves the n from the context to the goal. Thus, after
the three “move” steps, we are left with proving the following claim:
1 ∀ n n0 : nat,
2 n0 <= n -> 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
The elim now applies induction on the top of the stack, which is n. The corresponding
induction hypothesis IHn is:
1 IHn : ∀ n0 : nat,
2 n0 <= n ->
3 11 < n0 -> exists s4 s5 : nat, s4 * 4 + s5 * 5 = n0
(Of course, the n here is not the original n, but the new n introduced in the =>[|n IHn]
pattern.)
Lines 4, 9 and 10 deserve a few comments.
• Line 4 repeats a tactic 12 times using the do 12! tactical. This deals with the 12 cases
where n0 is not greater than 11.
• Line 9 uses the set proof command, which is used to define a new constant in the
context. For example, “set a := 24 * 11.” would create a new “a := 24 * 11 : nat”
item in the context. The command also tries to substitute the newly-defined constant
for its appearances in the goal; for example, “set a := 11.” would not only create
a new “a := 11 : nat” in the context, but also replace the “11 < m’.+4.+4.+4.+4” in
the goal4 by an “a < m’.+4.+4.+4.+4”. In our example above (“set m := _.+1”), we are
using the set command with a wildcard; this captures the first term of the form _.+1
appearing in the goal and denotes it by m, replacing it by m on the goal. In our case,
this first term is m’.+4.+4.+4.+4 (which is just syntactic sugar for m’.+1.+1..... with
16 appearances of .+1)5 , and so the name m is given to this term. We could have
achieved the same goal using “set m := m’.+4.+4.+4.+4”.
4 Don’tbe surprised by the fact that an addition of 16 is circumscribed by four additions of 4. By default,
Mathematical Components has the notations .+1, .+2, .+3 and .+4 pre-defined, but not .+5 and higher.
5 This is slightly counterintuitive, as you might instead believe it to be m’.+3.+4.+4.+4. But keep in
mind that m’.+3.+4.+4.+4 < n.+1 is just syntactic sugar for m’.+4.+4.+4.+4 <= n.+1.
90 Chapter 3. Type Theory
Further details about the set tactic can be found in [GMT15, §4.2]; let us only
mention the (by now) habitual variant set a := {k}(pattern), which defines a new
constant a to equal the first subterm of the goal that matches the pattern pattern,
but then replaces only the k-th appearance of this subterm in the goal by a. As usual,
if the pattern-matching algorithm keeps finding the wrong subterms, it is always
possible to completely specify the subterm, leaving no wildcards.
• Line 10 instantiates the induction hypothesis with the value (m-4) , with a placeholder
for a missing proof of (m-4 < n) , and with a proof that (11 < m-4) . The proof given
for (11 < m-4) is just a simple application of isT; this is accepted because the term
(11 < m-4) computes to true (thanks to the computational definitions of < and of
subtraction, and thanks to m := m’.+4.+4.+4.+4). The missing proof of (m-4 < n) is
not automatically inferred; it becomes the first subgoal. The induction hypothesis
yields exists s4 s5 : nat, s4 * 4 + s5 * 5 = m-4. The introduction pattern in line 10
gives names to the values of s4 and s5 whose existence is thus guaranteed, and to the
statement that s4 * 4 + s5 * 5 = m-4. In other words, it gives names s4 and s5 to the
quantities of 4-cent and 5-cent stamps needed to cover the amount of postage (m-4) ,
as well as to the fact that they do cover this exact amount of postage.
The classically box can only be opened when the statement to be proved in the current
goal is a boolean, hence an instance of a decidable predicate. Inside such a box the excluded
middle is made available by combining classic_EM and classic_bind. Nevertheless, when
proving a statement that is not a boolean, like exists n, ..., one cannot access assumptions
in the classically box.
3.3 On the status of Axioms 91
At this stage, we are in the presence of one of the main issues in the representation of
mathematics in a formal language: Very often, several data structures can be used to
represent one and the same mathematical definition or statement. The choice between
them may have a significant impact on the upcoming layers of formalized theories. So
far, we have seen two ways of expressing logical statements: using boolean predicates and
truth values on one hand, and using logical connectives and the Prop sort on the other. For
instance, in order to define the predicate “the sequence s has at least one element satisfying
the (boolean) predicate a”, we can either use a boolean predicate:
(where we are assuming that x0 is a given element of T; otherwise, we can, e.g., quantify
the whole statement by exists (x0 : T)).
Term (has a s) is a boolean value. It is hence easy to use it in a proof to perform a case
analysis on the fact that sequence s has an element such that a holds, using the case tactic:
As we already noted, computation provides some automation for free. For example in order
to establish that (has odd [:: 3; 2; 7]) = true , we only need to observe that the left hand
side computes to true.
It is not possible to perform a similar case analysis in a proof using the alternative
version (s_has_aP : has_prop a x0 s) , since, as sketched in section 3.3, excluded middle holds
94 Chapter 4. Boolean Reflection
in Coq only for boolean tests. On the other hand, this phrasing of the hypothesis easily
gives access to the value of the index at which the witness is to be found:
introduces in the context of the goal a natural number n : nat and the fact (asn : a (nth x0 s n)) .
In order to establish that (has_prop a x0 s) , we cannot resort to computation. Instead, we
can prove it by providing the index at which a witness is to be found — plus a proof of
this fact — which may be better suited for instance to an abstract sequence s.
In summary, boolean statements are especially convenient for excluded middle arguments
and its variants (reductio ad absurdum, . . . ). They furthermore provide a form of small-
step automation by computation.1 Specifications in the Prop sort are structured logical
statements, that can be “destructed” to provide witnesses (of existential statements),
instances (of universal statements), subformulae (of conjunctions), etc.. They are proved
by deduction, building proof trees made with the rules of the logic. Formalizing a predicate
by means of a boolean specification requires implementing a form of decision procedure
and possibly proving a specification lemma if the code of the procedure is not a self-
explanatory description of the mathematical notion. For instance a boolean definition
(prime : nat -> bool) implements a complete primality test, which requires a companion
lemma proving that it is equivalent to the usual definition in terms of proper divisors.
Postulating the existence of such a decision procedure for a given specification is akin to
assuming that the excluded middle principle holds on the corresponding predicate.
The boolean reflection methodology proposes to avoid committing to one or the other
of these options, and provides enough infrastructure to ease the bureaucracy of navigating
between the two. The is_true coercion, which was being used silently in the background
since the early pages of chapter 2, is in fact one piece of this infrastructure.
The is_true function is automatically inserted by Coq to turn a boolean value into a
Prop, i.e. into a regular statement of a theorem. More on this mechanism will be told in
section 4.4.
analysis on the fact that P holds or not, or to use its companion version (b = false <-> ~ P) .
The following proof script illustrates the kind of undesirable bureaucracy entailed by this
wording:
The last goal, just before line 5 is executed, is the following one:
1 subgoal
P : Prop
hlr : false = true -> P
hrl : P -> false = true
========================
P \/ ~ P
We could try alternative formulations based on the connectives seen in section 3, like
for instance (b = true /\ P) \/ (b = false /\ ~ P) , but again the bureaucracy would be
non-negligible.
A better solution is to use an ad hoc inductive definition that resembles a disjunction of
conjunctions: we inline the two constructors of a disjunction and each of these constructors
has the two arguments of the conjunction’s single constructor:
We can prove that the statement reflect P b is actually equivalent to the double
implication bool_Prop_equiv; see exercise 12.
Let us illustrate the benefits of this alternate specialized double implication:
A simple case analysis on the hypothesis (reflect P b) exposes in each branch both
versions of the statement. Note that the actual reflect predicate defined in the ssrbool
library is slightly different from the one we give here: this version misses an ultimate
refinement that will be presented in section 4.2.1.
We start our collection of links between boolean and Prop statements with the lemmas
relating boolean connectives with their Prop versions:
96 Chapter 4. Boolean Reflection
1 Lemma andP (b1 b2 : bool) : reflect (b1 /\ b2) (b1 && b2).
2 Proof. by case: b1; case: b2; [ left | right => //= [[l r]] ..]. Qed.
3
4 Lemma orP (b1 b2 : bool) : reflect (b1 \/ b2) (b1 || b2).
5 Proof.
6 case: b1; case: b2; [ left; by [ move | left | right ] .. |].
7 by right=> // [[l|r]].
8 Qed.
9
10 Lemma implyP (b1 b2 : bool) : reflect (b1 -> b2) (b1 ==> b2).
11 Proof.
12 by case: b1; case: b2; [ left | right | left ..] => //= /(_ isT).
13 Qed.
In each case, the lemma is proved using a simple inspection by case analysis of the truth
table of the boolean formula. The case analysis generates several branches and we use a
special syntax to describe the tactics which should be applied to some specific branches,
and the tactic which should be applied in the general case. The “;[ t1 | t2 .. | tn ]”
syntax indeed corresponds to the application of the tactic t1 to the first subgoal generated
by what comes before ;, and the application of the tactic tn to the last subgoal, and the
application of the tactic t2 to all the branches in between. See [Coq, section 9.2]) for a
complete description of this feature.
More generally, a theorem stating an equivalence between a boolean expression and a
Prop statement is called a reflection view, since it is used to view an assumption from a
different perspective.
The next section is devoted to the proof and usage of more involved views.
Each implication can be proved by a simple induction on one of the natural numbers,
but we still need to generate the two subgoals corresponding to these implications, as the
split tactic is of no help here.
In order to trigger this branching in the proof tree, we resort to the bridge between the
reflect predicate and a double implication. The ssrbool library provides a general version
of this bridge:
Lemma iffP relates two equivalences (reflect P b) and (reflect Q b) involving one and
the same boolean b but different Prop statements P and Q, as soon as one provides a proof
4.1 Reflection views 97
We can now come back to the proof of lemma eqnP, and start its proof script by applying
iffP.
The equality decision procedure just consists in pre-applying the injection f to the
decision procedure eqn available on type nat. Since we already know that eqn is a decision
procedure for equality, we just need to prove that (x = y) if and only if (f x = f y) , which
follows directly from the injectivity of f. Using iffP, a single proof command splits the
goal into two implications, replacing on the fly the evaluation (eqn (f x) (f y)) by the Prop
equality (f x = f y) :
Note that eqn, being completely specified by eqnP, is not anymore part of the picture.
Finishing the proof is left as exercise 14.
The latter example illustrates the convenience of combining an action on a goal, here
breaking an equivalence into one subgoal per implication, with a change of viewpoint, here
by the means of the eqnP view. This combination of atomic proof steps is pervasive in a
library designed using the boolean reflection methodology: the SSReflect tactic language
lets one use view lemmas freely in the middle of intro-patterns.
patterns are named after reflection views because this feature of the tactic language was
originally designed for what is now the special case of reflection views. For instance, suppose
that one wants to access the components of a conjunctive hypothesis, stated as a boolean
conjunction. We can use lemma andP in a view intro-pattern in this way:
The view intro-pattern /andP has applied the reflection view andP to the top entry of the
stack (n <= m) && (m <= k) and transformed it into its equivalent form (n <= m) /\ (m <= k) .
Note that strictly speaking, lemma andP does not have the shape of an implication, which
can be fed with a proof of its premise: it is (isomorphic to) the conjunction of two such
implications. The view mechanism implemented in the tactic language has automatically
guessed and inserted a term, called hint view, which plays the role of an adapter.
More precisely the /andP intro pattern has wrapped the top stack item, called top here, of
type ((n <= m) && (m <= k)) into (elimTF andP top) obtaining a term of type ((n <= m) /\ (m <= k)) .
which reduces to ((n <= m) /\ (m <= k)) since c is true (recall the hidden “.. = true” in the
type of the top stack entry).
Going back to our example: we can then chain this view with a case intro-pattern to
break the conjunction and introduce its components:
R Combining wisely the structured reasoning of inductive predicates in Prop with the
ease to reason by equivalence via rewriting of boolean identities leads to concise
proofs.
Let us now move to a non-artificial example to see how the SSReflect tactic language
supports the combination of views with the apply, case and rewrite tactics.
The first step of the proof is to view this disjunction as an implication, using the
classical equivalence and a negated premise:
This is now an instance of the weakening property of the comparison, except that
it is expressed with a boolean implication. But the view mechanism not only exists in
intro-patterns: it can also be used in combination with the apply tactic, to apply a view to
a given goal with a minimal amount of bureaucracy:
The case tactic also combines well with the view mechanism, which eases reasoning by
cases along a disjunction expressed with a boolean statement, like the just proved leq_total.
For example we may want to start the proof of the following lemma by distinguishing two
cases: n1 <= n2 and n2 <= n1.
100 Chapter 4. Boolean Reflection
1 Lemma leq_max m n1 n2 :
2 (m <= maxn n1 n2) = (m <= n1) || (m <= n2).
3 Proof.
4 case/orP: (leq_total n2 n1) => [le_n21 | le_n12].
m, n1, n2 : nat
le_n21 : n2 <= n1
============================
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
Even if it is not displayed here, subgoal two has (n1 <= n2) in its context.
Finally, the rewrite tactic also handles views that relate an equation in Prop with a
boolean formula.
The tactic sees (maxn_idPl le_n21) as the equation corresponding to the boolean formula
le_n21, namely (maxn n1 n2 = n1) , and rewrites with it obtaining:
m : nat
n1 : nat
n2 : nat
le_n21 : n2 <= n1
============================
(m <= n1) = (m <= n1) || (m <= n2)
subgoal 2 is:
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
The full proof of leq_max is quite interesting and will be detailed in section 4.3.2
Spec predicates are inductive families with indexes, exactly as the eq predicate seen in
section 3.1.3. In particular their elimination rule encapsulates the notion of substitution,
and that operation is performed automatically by the logic.
If we look at reflect, and its use, one is very likely to substitute b for its value in each
branch of the case.
This alternative formulation makes the equation implicitly stated and also automatically
substituted during case analysis.
Here the second argument of reflect is said to be an index and it is allowed to vary
depending on the constructor: ReflectT always builds a term of type (reflect P true) while
ReflectF builds a term of type (reflect P false) . When one reasons by cases on a term
of type (reflect P b) he obtains two proof branches, in the first one b is replaced by true,
since it corresponds to the ReflectT constructor. Conversely, b is replaced by false in the
second branch.
Let’s take an example where we reason by cases on the andP lemma, that states
(∀ a b, reflect (a /\ b) (a && b)) .
a, b : bool
1 Lemma example a b :
ab : a /\ b
2 a && b ==> (a == b).
========================
3 Proof.
true ==> (a == b)
4 case: andP => [ab|nab].
5
subgoal 2 is:
6
false ==> (a == b)
Remark how the automatic substitution trivializes the second goal. The first one can
be solved by replacing both a and b by their truth values, once ab is destructed. Hence the
full proof script is:
Note that we have not specified a value for the variables quantified in the statement of
andP. Such a view is in fact accompanied by an implicit argument declaration as follows:
We recall that this makes a and b implicit, hence writing andP is equivalent to (@andP _ _)
whose type is (reflect (_ /\ _) (_ && _)) . The value of the index of the inductive family
to be replaced by true or false is here a pattern (_ && _) and the goal is searched for an
instance of such pattern by the same matching algorithm the rewrite tactic uses for rewrite
102 Chapter 4. Boolean Reflection
rules. The tuning of implicit arguments is key to obtaining lemmas easy to use, even more
so in the case of the “spec” ones.
If one needs to override the pattern inferred for the index of andP, he can provide one
by hand as follows:
A more detailed explanation of this syntax can be found in [GMT15, section 5.6].
The Mathematical Components library provides many spec lemmas to be used this way.
A paradigmatic one is ifP.
1 Section If.
2 Variables (A : Type) (vT vF : A) (b : bool).
3
4 Inductive if_spec : bool -> A -> Type :=
5 | IfSpecTrue (p : b) : if_spec true vT
6 | IfSpecFalse (p : b = false) : if_spec false vF.
7
8 Lemma ifP : if_spec b (if b then vT else vF).
Reasoning by cases on ifP has the following effects: 1) the goal is searched for an
expression like (if _ then _ else _) ; 2) two goals are generated, one in which the condition
of the if statement is replaced by true and the if-then-else expression by the value of the
then branch, another one where the condition is replaced by false and the if-then-else by
the value of the else branch; 3) the first goal gets an extra assumption (b = true) , while
the second goal gets (b = false) . Note that “case: ifP” is very compact, much shorter than
any if-then-else expression.
It is worth mentioning the convenience lemma boolP that takes a boolean formula and
reasons by excluded middle providing some extra comfort like an additional hypothesis in
each sub goal.
Another reflection view worth mentioning is leqP that replaces, in one shot, both
(_ <= _) and the converse (_ < _) by opposite truth values. Sometime a proof works best
by splitting into three branches, i.e., separating the equality case. The ltngtP lemma is
designed for that.
In practice lines of reasoning consisting in a specific branching of a proof can often be
modelled by an appropriate spec lemma.
R The structure of the proof shall not be driven by the syntax of the definition/predicate
under study but by the view/spec used to reason about it
4.3 Real proofs, finally! 103
After the first line the proof state is the following one:
m, n : nat
IHn : m < n -> m.+1 %| n‘!
========================
(m == n) || (m < n) -> m.+1 %| (n.+1)‘!
The case analysis rules out (m = 0) , and simplifies the hypothesis to (m <= n) . Recall
that (x <= y <= z) is a notation for ((x <= y) && (y <= z)) ; hence when the first inequality
evaluates to true (e.g. when x is 0) the conjunction simplifies to the second conjunct. The
leq_eqVlt rewrite rule rephrases <= as a disjunction (the capital V letter is reminiscent of ∨).
When we reason by cases on the top assumption, line 4, we face two goals, both easy
to solve if we look at the development of the factorial of n.+1, i.e., (n.+1 * n‘!) . The
former amounts to showing that (n.+1 %| n.+1 * n‘!) , while the latter to showing that
(m.+1 %| n.+1 * n‘!) under the (inductive) hypothesis that (m.+1 %| n‘!) .
What is paradigmatic in this little proof is the use of the goal stack as a work space. In
other words the proof script would be much more involved if we started by introducing in
the proof context all assumptions.
We can now move to the proof of the main result. We state it using a “synonym” of
the exists quantifier that is specialized to carry two properties. This way the statement
is simpler to destruct: with just one case analysis we obtain the witness and the two
properties. We also resort to the following lemmas.
104 Chapter 4. Boolean Reflection
The first step is to prove that m! + 1 is greater than 1, a triviality. Still it gives us the
occasion to explain the have tactic, which lets us augment the proof context with a new
fact, typically an intermediate step of our proof.
Its syntax is similar to the one of the Lemma command: it takes a name, a statement
and starts a (sub) proof. Since the proof is so short, we will put it on the same line, and
remove the full stop.
The next step is to use the pdivP lemma to gather a prime divisor of m‘!.+1. We end up
with the following, rather unsatisfactory, script.
It is unsatisfactory because in our paper proof what plays an interesting role is the p
that we obtain in the second line, and not the m1_gt1 fact we proved as an intermediate
fact.
We can resort to the flexibility of have to obtain a more pertinent script: the first
argument to have, here a name, can actually be any introduction pattern, i.e. what follows
the => operator, for example a view application. In the light of that, the script can be
rearranged as follows.
Here the first line obtains a prime p as desired, the second one begins to show it fits by
contrapositive reasoning, and the third one, already commented in section 2.3.3, concludes.
As a general principle, in the proof script style we propose, a full line should represent
a meaningful reasoning step (for a human being).
The proof uses the following lemmas. Pay attention to the premise of orb_idr, which is
an implication.
Our first attempt takes no advantage of the symmetry argument: we reason by cases
on the order relation, we name the resulting fact on the same line (it eases tracking where
things come from) and we solve the two goals independently.
1 Proof.
2 case/orP: (leq_total n2 n1) => [le_n21|le_n12].
3 rewrite (maxn_idPl le_n21) orb_idr // => le_mn2.
4 by apply: leq_trans le_mn2 le_n21.
5 rewrite maxnC orbC.
6 rewrite (maxn_idPl le_n12) orb_idr // => le_mn1.
7 by apply: leq_trans le_mn1 le_n12.
8 Qed.
2 subgoals
m, n1, n2 : nat
le_n21 : n2 <= n1
========================
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
subgoal 2 is:
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
The first goal is simplified by rewriting with maxn_idPl (as we did in section 4.1.4). Then
trivializes the main goal and generates a side condition with an extra hypothesis
orb_idr
we name le_mn2.
2 subgoals
m, n1, n2 : nat
le_n21 : n2 <= n1
========================
(m <= n1) = (m <= n1) || (m <= n2)
2 subgoals
m, n1, n2 : nat
le_n21 : n2 <= n1
le_mn2 : m <= n2
========================
m <= n1
Line 4 combines by transitivity the two hypotheses to conclude. Since it closes the
proof branch we use the prefix by to asserts the goal is solved and visually signal the end
of the paragraph. Line 5 commutes max and ||. We can then conclude by copy-paste.
To avoid copy-pasting, shrink the proof script and finally make the symmetry step
visible we can resort to the have tactic. In this case the statement is a variation of what we
need to prove. Remark that as for Lemma, we can place parameters, x and y here, before the
: symbol.
The proof for the th_sym sub proof is the text we copy-paste in the previous script, while
here it is factored out. Once we have such extra fact in our context we reason by cases on
the order relation and we conclude. Remark that the last line instantiates th_sym in each
branch using the corresponding hypothesis on n1 and n2 generated by the case analysis. As
expected the two instances are symmetric.
2 subgoals
m, n1, n2 : nat
th_sym : ∀ x y : nat,
y <= x -> (m <= maxn x y) = (m <= x) || (m <= y)
========================
(m <= maxn n1 n2) = (m <= n1) || (m <= n2) ->
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
subgoal 2 is:
(m <= maxn n2 n1) = (m <= n2) || (m <= n1) ->
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
This is exactly what is needed in the first branch of the case analysis. The last subgoal
just requires commuting max and ||.
We can further improve the script. For example we could rephrase the proof putting
in front the justification of the symmetry, and then prove one case when we pick x to be
smaller than y.
4.3 Real proofs, finally! 107
The suff tactic (or suffices) is like have but swaps the two goals.
Note that here the sub proof is now the shortest paragraph. This is another recurrent
characteristic of the proof script style we adopt in the Mathematical Components library.
There is still a good amount of repetition in the current script. In particular the
main conjecture has been almost copy-pasted in order to invoke have or suff. When this
repetition is a severe problem, i.e. the statement to copy is large, one can resort to the
wlog tactic (or without loss).
Remark how wlog only needs the statement of the extra assumption, and which portion
of the context needs to be abstracted, here n1 and n2. The sub goal to be proved is the
following one.
2 subgoals
m, n1, n2 : nat
th_sym : ∀ n1 n2 : nat, n2 <= n1 ->
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
========================
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
subgoal 2 is:
(m <= maxn n1 n2) = (m <= n1) || (m <= n2)
To keep the script similar to the previous one, we named explicitly th_sym, to better
link the final script to the previous attempts. This is rarely the case in proof scripts of the
library, since one typically uses the /(_ ...) intro pattern to specialize the top of the stack.
Shrinking proof scripts is a never ending game. The impatient reader can jump to the
next section to see how intro patterns can be used to squeeze the last two lines into a
single one. In the end, this proof script consists of three steps: the remark that we can
assume (n2 <= n1) without losing generality; its justification in terms of totality of the order
relation and commutativity of max and ||; and the final proof, by transitivity, in the case
when the max is n1 due to the extra assumption.
Partially applied views
A less important, but very widespread, feature of the SSReflect proof language can be used
to shrink the proof even further. In this proof script, we have named the fact le_mn2 only
for the purpose of referring to this fact in the transitivity step.
108 Chapter 4. Boolean Reflection
Remember that the statement of leq_trans is (∀ c a b, a <= c -> c <= b -> a <= b) and
we have used it to transform the top assumption (m <= n2) . Note that the leq_trans expects
a second proof argument, and that its type would fix b, that is otherwise unspecified. If one
puts a full stop just before the terminating -> , to see the output of the view application,
one sees the following stack:
Rewriting the top assumption fixes n to n1, trivializes the goal (m <= n1) to true and
opens a trivial side condition (n2 <= n1) .
The very compact idiom /leq_trans-> is quite frequent in the Mathematical Components
library.
1 Definition edivn_rec d :=
2 fix loop m q := if m - d is m’.+1 then loop m’ q.+1 else (q, m).
3
4 Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
The fix keyword lets one write a recursive function locally, without providing a global
name as Fixpoint does. This also means that d is a parameter of edivn_rec that does not
change during recursion. The edivn program handles the case of a null divisor, producing
the dummy pair (0,m) for the quotient and the reminder respectively.
We start by showing the following equation.
1 Lemma edivn_recE d m q :
2 edivn_rec d m q = if m - d is m’.+1 then edivn_rec d m’ q.+1 else (q,m).
3 Proof. by case: m. Qed.
It is often useful to state and prove unfolding equations like this one. When the simplification
tactic /= unfolds too aggressively, rewriting with such equations gives better control on
how many unfold steps one performs.
The statement of our theorem uses a let-in construct (remark the := sign) to name an
expression used multiple times, in this case the result of the division of m by d.
As one expects, edivn being a recursive program, its specification needs to be proved
by induction. Given that the recursive call is on the subtraction of the input, we need to
perform a strong induction, as we did for the postage example in section 3.2.4.
But let’s start by dealing with the trivial case of a null divisor.
4.4 Notational aspects of specifications 109
Line 1 handles the case of d being zero. The “in E...” suffix can be appended to any tactic
in order to push on the stack the specified hypotheses before running the tactic and pulling
them back afterwards (see [GMT15, section 6.5]). The * means that the goal is also affected
by the tactic, and not just the hypotheses explicitly selected.
Lines 2 and 3 prepare the induction by unfolding the definition of edivn (to expose the
initial value of the accumulators of edivn_rec) and makes the invariant of the division loop
explicit replacing m by (0 * d.+1 + m) . Recall the case d being 0 has already been handled.
Line 4 performs a strong induction, also generalizing the initial value of the accumulator
0, leading to the following goal:
d, n : nat
IHn : ∀ m n0 : nat, m <= n ->
let ed := edivn_rec d m n0 in
(ed.2 < d.+1) && (n0 * d.+1 + m == ed.1 * d.+1 + ed.2)
m, q : nat
le_mn : m < n.+1
========================
let ed := edivn_rec d m.+1 q in
(ed.2 < d.+1) && (q * d.+1 + m.+1 == ed.1 * d.+1 + ed.2)
Note that the induction touches variables used in ed that is hence pushed on the goal stack.
The @ modifier tells SSReflect to keep the body of the let-in.
Line 5 unfolds the recursive function and uses the following lemma to push the subtrac-
tion into the branches of the if statement. Then it reasons by cases on the guard of the
if-then-else statement.
1 Lemma subn_if_gt T m n F (E : T) :
2 (if m.+1 - n is m’.+1 then F m’ else E) =
3 (if n <= m then F (m - n) else E).
The else branch corresponds to the non-recursive case of the division algorithm and is
trivially solved in line 6. The recursive call is done on (m-d) , hence the need for a strong
induction. In order to satisfy the premise of the induction hypothesis, line 7 shows that
(m - d <= n) . Line 8 concludes.
When the statement of the example is processed by Coq and it is enforced to be a type,
but (prime 17) is actually a term of type bool. Early in the library the function is_true is
declared as a coercion from bool to Prop and hence it is inserted by Coq automatically.
Another coercion that is widely used injects booleans into naturals. Two examples
follow:
where pred T is a notation for the type T -> bool of boolean predicates.
At line number 2 the term (a x) is a boolean. The nat_of_bool function is automatically
inserted to turn true into 1 and false into 0. This notational trick is reminiscent of
Kronecker’s δ notation. Similarly, in the last line the membership test is turned into a
number, that is shown to be equivalent to the count of any element in a list that is duplicate
free.
Coercions are composed transitively: in the following example, true is used as the tail
of a seq. Even though there is no direct coercion from bool to seq, Coq can go from one to
the other via nat. Thus true is first coerced to 1 of type nat by nat_of_bool, which is then
turned into a seq (of length 1 containing 0s) by zerolist.
For the convenience of the reader we list here the most widely used coercions. There
are also a bunch on Funclass not listed and elimT surely deserves some explanation.
Coercions
coercion source target
Posz nat int
nat_of_bool bool nat
elimT reflect Funclass
isSome option bool
is_true bool Sortclass
The reader already familiar with the concept of coercion may find the presentation of
this chapter nonstandard. Coercions are usually presented as a device to model subtyping
in a theory that, like the Calculus of Inductive Constructions, does not feature subtyping.
4.5 Exercises 111
As we will see in chapter 7 the role played by coercions in the modelling of the hierarchy of
algebraic structures is minor. The job of coercions in that context is limited to forgeting
some fields of a structure to obtain a simpler one, and that is easy. What is hard is to
reconstruct the missing fields of a structure or compare two structures finding the minimum
super structure. These tasks are mainly implemented with programming type inference.
4.5 Exercises
Exercise 12 reflect
Prove the following lemmas. In particular prove the first one with and without using iffP.
Exercise 13 eqnP
Finish this proof.
4.5.1 Solutions
Answer of exercise 12
1 Lemma iffP_lr (P : Prop) (b : bool) :
2 (P -> b) -> (b -> P) -> reflect P b.
3 Proof.
4 by case: b => [_ H|H _]; [left; apply H | right=> p; move: (H p)].
5 (* with iffP: by move=> *; apply: (iffP idP). *)
6 Qed.
7
8 Lemma iffP_rl (P : Prop) (b : bool) :
9 reflect P b -> ((P -> b) /\ (b -> P)).
10 Proof. by case: b; case=> p; split. Qed.
112 Chapter 4. Boolean Reflection
Answer of exercise 13
Answer of exercise 14
Answer of exercise 15
6 Sub-Types . . . . . . . . . . . . . . . . . . . . . . . . . . 137
6.1 n-tuples, lists with an invariant on the length
6.2 n-tuples, a sub-type of sequences
6.3 Finite types and their theory
6.4 The ordinal subtype
6.5 Finite functions
6.6 Finite sets
6.7 Permutations
6.8 Matrix
The rules of the Calculus of Inductive Constructions, as the ones sketched in 3, are
expressed on the syntax of terms and are implemented by the kernel of Coq. Such software
component performs type checking: given a term and type, it checks if such term has the
given type. To keep type checking simple and decidable the syntax of terms makes all
information explicit. As a consequence the terms written in such verbose syntax are pretty
large.
Luckily the user very rarely interacts directly with the kernel. Instead she almost always
interacts with the refiner, a software component that is able to accept open terms. Open
terms are in general way smaller than regular terms because some information can be left
implicit [Pol92]. In particular one can omit any subterm by writing “_” in place of it. Each
missing piece of information is either reconstructed automatically by the type inference
algorithm, or provided interactively by means of proof commands. In this chapter we focus
on type inference.
Type inference is ubiquitous: whenever the user inputs a term (or a type) the system
tries to infer a type for it. One can think of the work of the type inference algorithm as
trying to give a meaning to the input of the user possibly completing and constraining it
by inferring some information. If the algorithm succeeds, the term is accepted; otherwise
an error is given.
What is crucial to the Mathematical Components library is that the type inference
algorithm is programmable: one can extend the basic algorithm with small declarative
programs1 that have access to the library of already formalized facts. In this way one can
make the type inference algorithm aware of the contents of the library and make Coq
behave as a trained reader who is able to guess the intended meaning of a mathematical
expressions from the context thanks to her background knowledge.
This chapter also introduces the key concepts of interface and instance. An interface is
1A program is said to be declarative when it explains what it computes rather than how. The programs
in question are strictly linked with the Prolog programming language, a technology that found applications
in artificial intelligence and computational linguistic.
116 Chapter 5. Implicit Parameters
placeholder “_”, they are all considered as potentially different by the system, and hence
hold (internally) unique names. For the sake of clarity we take the freedom to use the
alternative syntax ?x for implicit arguments (where x is a unique name).
1 Definition id A (a : A) : A := a.
2 Check (id nat 3). id nat 3 : nat
3 Check (id _ 3). id nat 3 : nat
In the expression (id nat 3) no subterm was omitted, therefore Coq accepted the term
and printed its type. In the third line, even if the subterm nat was omitted, Coq accepted
the term. Type inference found a value for the placeholder for us by proceeding in the
following way: it traversed the term recursively from left to right, ensuring that the type of
each argument of the application had the type expected by the function. In particular id
takes two arguments. The former argument is expected to have type Type and the user left
such argument implicit (we name it ?A ). Type inference imposes that ?A has type Type, and
this constraint is satisfiable. The algorithm continues checking the remaining argument.
According to the definition of id the type of the second argument must be the value of the
first argument. Hence type inference runs recursively on the argument 3 discovering it has
type nat and imposes that it unifies with the value of the first argument (that is ?A ). For
this to be true ?A has to be assigned the value nat. As a result the system prints the input
term, where the placeholder has been replaced by the value type inference assigned to it.
In the light of that, we observe that every time we apply the identity function to a
term we can omit to specify its first argument, since Coq is able to infer it and complete
the input term for us. This phenomenon is so frequent that one can ask the system to
insert the right number of _ for him. For more details refer to [Coq, section 2.7]. Here we
only provide a simple example.
1 Arguments id {A} a.
2 Check (id 3). id 3 : nat
3 Check (@id nat 3). id 3 : nat
The Arguments directive “documents” the constant id. In this case it just marks the
argument that has to be considered as implicit by surrounding it with curly braces. The
declaration of implicit arguments can be locally disabled by prefixing the name of the
constant with the @ symbol.
Another piece of information that is often left implicit is the type of abstracted or
quantified variables.
1 Check (fun x => @id nat x). fun x : nat => id x : nat -> nat
2
3 Lemma prime_gt1 p : p : nat
4 prime p -> 1 < p. ============================
5 prime p -> 1 < p
118 Chapter 5. Implicit Parameters
In the first line the syntax (fun x => ...) is sugar for (fun x : _ => ...) where we leave
the type of x implicit. Type inference fixes it to nat when it reaches the last argument of
the identity function. It unifies the type of x with the value of the first argument given to
id that in this case is nat. This last example is emblematic: most of the time the type of
abstracted variables can be inferred by looking at how they are used. This is very common
in lemma statements. For example, the third line states a theorem on p without explicitly
giving its type. Since the statement uses p as the argument of the prime predicate, it is
automatically constrained to be of type nat.
The kind of information filled in by type inference can also be of another, more
interesting, nature. So far all placeholders were standing for types, but the user is also
allowed to put _ in place of a term.
q : nat
1 Lemma example q : prime q -> 0 < q.
pr_q : prime q
2 Proof.
========================
3 move=> pr_q.
0 < q
The proof begins by giving the name pr_q to the assumption (prime q). Then it builds
a proof term by hand using the lemma stated in the previous example and names it q_gt1.
In the expression (prime_gt1 _ pr_q), the placeholder, that we name ? p , stands for a
natural number. When type inference reaches ? p , it fixes its type to nat. What is more
interesting is what happens when type inference reaches the pr_q term. Such term has its
type fixed by the context: (prime q). The type of the second argument expected by prime_gt1
is (prime ? p ) (i.e., the type of prime_gt1 where we substitute ? p for p. Unifying (prime ? p )
with (prime q) is possible by assigning q to ? p . Hence the proof term just constructed is
well typed, its type is (1 < q) and the placeholder has been set to be q. As we did for the
identity function, we can declare the p argument of prime_gt1 as implicit. Choosing a good
declaration of implicit arguments for lemmas is tricky and requires one to think ahead how
the lemma is used.
So far we have been using only the simplest form of type inference in our interaction
with the system. The unification problems we have encountered would have been solved by
a first order unification algorithm and we did not need to compute or synthesize functions.
In the next section we illustrate how the unification algorithm used in type inference can
be extended in order to deal with higher-order problem. This extension is based on the use
of declarative programs, and we present the encoding of the relations which describe these
programs. As of today however there is no precise, published, documentation of the type
inference and unification algorithms implemented in Coq. For a technical presentation
of a type inference algorithm close enough to the one of Coq we suggest the interested
reader to consult [Asp+12]. The reader interested in a technical presentation of a simplified
version of the unification algorithm implemented in Coq can read [Gon+13b; SZ14].
Constructions as inductive data types with just one constructor, recall section 1.3.4. The
peculiarity of the records we are going to use is that they are dependently typed : the type
of each field is allowed to depend on the values of the fields that precede it.
Coq provides syntactic sugar for declaring record types.
The sentence above declares a new inductive type called eqType with one constructor
named Pack with two arguments. The first one is named sort and holds a type; the second
and last one is called eq_op and holds a comparison function on terms of type sort. We
recall that what this special syntax does is declaring at once the following inductive type
plus a named projection for each record field:
Note that the type dependency between the two fields requires the first projection to
be used in order to define the type of the second projection.
We think of the eqType record type as a relation linking a data type with a comparison
function on that data type. Before putting the eqType relation to good use we declare an
inhabitant of such type, that we call an instance, and we examine a crucial property of the
two projections just defined.
We relate the eqn comparison function with the nat data type.
Projections, when applied to a record instance like nat_eqType compute and extract the
desired component.
= nat : Type
1 Eval simpl in sort nat_eqType.
= eqn : sort nat_eqType ->
2 Eval simpl in @eq_op nat_eqType.
sort nat_eqType -> bool
Given that (sort nat_eqType) and nat are convertible, equal up to computation, we can
use the two terms interchangeably. The same holds for (eq_op nat_eqType) and eqn. Thanks
to this fact Coq can type check the following term:
This term is well typed, but checking it is not as simple as one may expect. The
eq_op function is applied to three arguments. The first one is nat_eqType and its type,
eqType, is trivially equal to the one expected by eq_op. The following two arguments are
hence expected of to be of type (sort nat_eqType) but 3 and 4 are of type nat. Recall that
120 Chapter 5. Implicit Parameters
unification takes computation into account exactly as the convertibility relation. In this
case the unification algorithm unfolds the definition of nat_eqType obtaining (Pack nat eqn)
and reduces the projection extracting nat. The obtained term literally matches the type of
the last two arguments given to eq_op.
Now, why this complication? Why should one prefer (eq_op nat_eqType 3 4) to (eqn 3
4)? The answer is overloading. It is recurrent in mathematics and computer science to
reuse a symbol, a notation, in two different contexts. A typical example coming from the
mathematical practice is to use the same infix symbol ∗ to denote any ring multiplication.
A typical computer science example is the use of the same infix == symbol to denote the
comparison over any data type. Of course the underlying operation one intends to use
depends on the values it is applied to, or better their type 2 . Using records lets us model
these practices. Note that, thanks to its higher-order nature, the term eq_op can always
be the head symbol denoting a comparison. This makes it possible to recognize, hence
print, comparisons in a uniform way as well as to input them. On the contrary, in the
simpler expression (eqn 3 4), the name of the head symbol is very specific to the type of
the objects we are comparing.
In the rest of this chapter, we focus on the overloading of the == symbol and we start
by defining another comparison function, this time for the bool data type.
Now the idea is to define a notation that applies to any occurrence of the eq_op head
constant and use such notation for both printing and parsing.
As a printing rule, the placeholder stands for a wild card: the notation is used no
matter the value of the first argument of eq_op. As a result both occurrences of eq_op, line 2
and 3, are printed using the infix == syntax. Of course the two operations are different; they
are specific to the type of the arguments and the typing discipline ensures the arguments
match the type of the comparison function packaged in the record.
When the notation is used as a parsing rule, the placeholder is interpreted as an implicit
argument: type inference is expected to find a value for it. Unfortunately such notation
does not work as a parsing rule yet.
1 Check (3 == 4). Error: The term "3" has type "nat" while
2 it is expected to have type "sort ?e".
If we unravel the notation, the input term is really (eq_op _ 3 4). We name the
placeholder ?e . If we replay the type inference steps seen before, the unification step is now
failing. Instead of (sort nat_eqType) versus nat, now unification has to solve the problem
(sort ?e ) versus nat. This problem falls in one of the problematic classes we presented in
2 The meaning of a symbol in mathematics is even deeper: by writing a ∗ b one may expect the reader to
figure out which ring she talks about, recall its theory, and use this knowledge to justify some steps in a
proof. By programming type inference appropriately, we model this practice in section 5.4.
5.3 Records as relations 121
section 5.1: the system has to synthesize a comparison function (or better a record instance
containing a comparison function).
Coq gives up, leaving to the user the task of extending the unification algorithm
with a declarative program that is able to solve unification problems of the form (sort ?e )
versus T for any T. Given the current context, it seems reasonable to write an extension
that picks nat_eqType when T is nat and bool_eqType when T is bool. In the language of
Canonical Structures, such a program is expressed as follows.
1 Canonical nat_eqType.
2 Canonical bool_eqType.
The keyword Canonical was chosen to stress that the program is deterministic: each
type T is related to (at most) one canonical comparison function.
The mechanics of the small program we wrote using the Canonical keyword can be
explained using the global table of canonical solutions. Whenever a record instance is
declared as canonical Coq adds to such table an entry for each field of the record type.
canonical structures Index
projection value solution
sort nat nat_eqType
sort bool bool_eqType
Whenever a unification problem with the following shape is encountered, the table of
canonical solution is consulted.
The table is looked up using as keys the projection name and the value. The corresponding
solution is assigned to the implicit argument ?S .
In the table we reported only the relevant entries. Entries corresponding to the eq_op
projection play no role in the Mathematical Components library. The name of such
projections is usually omitted to signal that fact.
What makes this approach interesting for a large library is that record types can play
the role of interfaces. Once a record type has been defined and some functionality associated
to it, like a notation, one can easily hook a new concept up by defining a corresponding
record instance and declaring it canonical. One gets immediately all the functionalities tied
to such interface to work on the new concept. For example a user defining new data type
with a comparison function can immediately take advantage of the overloaded == notation
by packing the type and the comparison function in an eqType instance.
This pattern is so widespread and important that the Mathematical Components library
consistently uses the synonym keyword Structure in place of Record in order to make record
types playing the role of interfaces easily recognizable.
The computer-science inclined reader shall see records as first-class values in the Calculus
of Inductive Constructions programming language. Otherwise said, the projections of a
record are just ordinary functions, defined by pattern-matching on an inductive type, and
which access the fields of the record. Exercise 1 proposed to implement the projections of a
122 Chapter 5. Implicit Parameters
triple onto its components, and these functions are the exact analogues of the projections
of a record with three fields. In particular, the fields of two given instances of records can
be combined and used to build a new instance of another record. Canonical structures
provide a language to describe how new instances of records, also called structures in this
case, can be built from existing ones, via a set of combinators defined by the user.
So far we have used the == symbol for terms whose type is atomic, like nat or bool. If
we try for example to use it on terms whose type was built using a type constructor like
the one of pairs we encounter an error.
1 Check (3, true) == (4, false). Error: The term "(3, true)" has type
2 "(nat * bool)%type" while it is expected
3 to have type "sort ?e".
The term (3,true) has type (nat * bool) and, so far, we only taught Coq how to
compare booleans and natural numbers, not how to compare pairs. Intuitively the way to
compare pairs is to compare their components using the appropriate comparison function.
Let’s write a comparison function for pairs.
What is interesting about this comparison function is that the pairs x and y are not
allowed to have an arbitrary, product, type here. The typing constraints imposed by the
two eq_op occurrences force the type of x and y to be (sort eqA * sort eqB). This means
that the records eqA and eqB hold a sensible comparison function for, respectively, terms of
type (sort eqA) and (sort eqB).
It is now sufficient to pack together the pair data type constructor and this comparison
function in an eqType instance to extend the canonical structures inference machinery with
a new combinator.
1 Check (3, true) == (4, false). (3, true) == (4, false) : bool
1 Module Equality.
2
3 Structure type : Type := Pack {
4 sort : Type;
5 op : sort -> sort -> bool;
6 axiom : ∀ x y, reflect (x = y) (op x y)
7 }.
8
9 End Equality.
The extra property turns the eqType relation into a proper interface, which fully specifies
what op is.
The axiom says that the boolean comparison function is compatible with equality: two
ground terms compare as equal if and only if they are syntactically equal. Note that this
means that the comparison function is not allowed to quotient the type by identifying two
syntactically different terms.
R The infix notation == stands for a comparison function compatible with Leibniz
equality (substitution in any context).
The Equality module enclosing the record acts as a name space: type, sort, eq and
axiom, three very generic words, are here made local to the Equality name space becoming,
respectively, Equality.type, Equality.sort, Equality.op and Equality.axiom.
As in section 5.3, the record plays the role of a relation and its sort component is again
the only field that drives canonical structure inference. Following a terminology typical
of object-oriented programming languages, the set of operations (and properties) that
define an interface is called a class. In the next chapter, we are going to re-use already
defined classes in order to build new ones by mixing-in additional properties (typically
called axioms). Hence the definition of eqType in the Mathematical Components library is
closer to the following one:
1 Module Equality.
2
3 Definition axiom T (e : rel T) := ∀ x y, reflect (x = y) (e x y).
124 Chapter 5. Implicit Parameters
4
5 Record mixin_of T := Mixin {op : rel T; _ : axiom op}.
6 Notation class_of := mixin_of.
7
8 Structure type : Type := Pack {sort :> Type; class : class_of sort; }.
9
10 End Equality.
11
12 Notation eqType := Equality.type.
13 Definition eq_op T := Equality.op (Equality.class T).
14 Notation "x == y" := (@eq_op _ x y).
In this simple case, there is only one property, named Equality.axiom, and the class is
exactly the mixin.
That being said, nothing really changes: the eqType structure relates a type with a
signature.
Remark the use of :> instead of : to type the field called sort. This tells Coq
to declare the Equality.sort projection as a coercion. This makes it possible to write
(∀ T : eqType, ∀ x y : T, P) even if T is not a type and only (sort T) is.
Given the new definition of eqType, when we write (a == b), type inference does not
only infer a function to compare a with b, but also a proof that such a function is correct.
Declaring the eqType instance for nat now requires some extra work, namely proving the
correctness of the eqn function.
Note that the Canonical declaration is expanded (showing the otherwise implicit first
argument of Pack) to document that we are relating the type nat with its comparison
operation.
The proof is just unpacking the input T. We can use it on a concrete example of eqType
like nat
In short, eqP can be used to change view: turn any == into = and vice versa.
The eqP lemma also applies to abstract instances of eqType. When we rework the instance
of the type (T1 * T2) we see that the proof, by means of the eqP lemma, uses the axiom of
T1 and T2:
1 Section ProdEqType.
2 Variable T1 T2 : eqType.
3
4 Definition pair_eq := [rel u v : T1 * T2 | (u.1 == v.1) && (u.2 == v.2)].
5
6 Lemma pair_eqP : Equality.axiom pair_eq.
7 Proof.
8 move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=.
9 by move/eqP->; move/eqP->.
10 Qed.
11
12 Definition prod_eqMixin := Equality.Mixin pair_eqP.
13 Canonical prod_eqType := @Equality.Pack (T1 * T2) prod_eqMixin.
14 End ProdEqType.
where notation [rel x y : T | E] defines a binary boolean relation on type T. Note that
a similar notation [pred x : T | E] exists for unary boolean predicates.
The generic lemma eqP applies to any eqType instance, like (bool * nat)
The (a,x) == (b,y) assumption is reflected to (a,x) = (b,y) by using the eqP view specified
by the user. Here we write == to have all the benefits of a computable function (simplification,
reasoning by cases), but when we need the underlying logical property of substitutivity we
access it via the view eqP.
This statement is true (or better, the hypothesis is false) by computation. In this last
example the use of == give us immediate access to reasoning by cases.
R Whenever we want to state equality between two expressions, if they live in an eqType,
always use ==.
126 Chapter 5. Implicit Parameters
1 Section SeqTheory.
2 Variable T : eqType.
3 Implicit Type s : seq T.
4
5 Fixpoint mem_seq s x :=
6 if s is y :: s’ then (y == x) || mem_seq s’ x else false.
Like we did for the overloaded == notation, we can define the \in (and \notin ) infix
notation. We can then easily define what a duplicate-free sequence is, and how to enforce
such property.
1 Fixpoint uniq s :=
2 if s is x :: s’ then (x \notin s’) && uniq s’ else true.
3 Fixpoint undup s :=
4 if s is x :: s’ then
5 if x \in s’ then undup s’ else x :: undup s’
6 else [::].
Proofs about such concepts can be made pretty much as if the type T was nat or bool,
i.e. our predicates do compute.
The proof of undup_uniq requires no new ingredients and completes the specification of
undup.
The last, very important step in the theory of sequences is to show that the container
preserves the eqType interface: whenever we can compare the elements of a sequence, we
can also compare sequences.
In this script, (x1 =P x2) is a notation for (@eqP T x1 x2) , a proof of the reflect inductive spec;
a case analysis on the term (x1 =P x2) has thus two branches. Since the constructors ReflectT
and ReflectF carry a proof, each branch of this analysis features an extra assumption; the
branch corresponding to ReflectT has the hypothesis x1 = x2 and the branch corrsponding
to ReflectF has its negation x1 != x2.
As an example we build a sequence of sequences, and we assert that we can use the ==
and \in notation on it, as well as apply the list operations and theorems on objects of type
(seq (seq T)) when T is an eqType.
1 Let s1 := [:: 1; 2 ].
2 Let s2 := [:: 3; 5; 7].
3 Let ss : seq (seq nat) := [:: s1 ; s2 ].
4 Check (ss != [::]) && s1 \in ss.
5 Check undup_uniq ss.
n [
∑ f (i) = f (1) + f (2) + . . . + f (n) g(a) = g(a1 ) ∪ g(a2 ) ∪ . . . ∪ g(a|A| )
i=1 a∈A
The only component of typical notations for iterated operations we have not discussed
yet is the filter, used to iterate the operation only on a subset of the domain. For example,
to state that the sum of the first n odd numbers is n2 , one could write:
∑ i = n2
i<2n, 2-i
An alternative writing for the same summation exploits the general terms to rule out even
numbers:
∑ (i ∗ 2 + 1) = n2
i<n
While this latter writing is elegant, it is harder to support generically, since the filtering
condition is not explicit. For example the following equation clearly holds for any filter,
range and general term. It would be hard to express such a statement if the filter were
mixed with the general term, and hence its negation were not obvious to formulate.
∑ i+ ∑ i= ∑i
i<2n, 2|i i<2n, 2-i i<2n
Last, not all filtering conditions can be naturally expressed in the general term. An
example is not being a prime number.
In the light of that, our formal statement concerning the sum of odd numbers is the
following:
where .*2 is a postfix notation, similar to .+1, standing for doubling. Under the hood we
expect to find the following expression:
5.7 The generic theory of “big” operators 129
1 Lemma sum_odd n :
2 foldr (fun acc i => if odd i then i + acc else acc)
3 0 (index_iota 0 n.*2)
4 = n^2
The following section details how the generic notation for iterated operation is built
and specialized to frequent operations like Σ. Section 5.7.2 focuses on the generic theory of
iterated operations.
1 Lemma sum_odd n :
2 bigop 0 addn (index_iota 0 n.*2) odd (fun i => i) = n^2.
Note that odd is already a predicate on nat, the general term is the identity function,
the range r is (index_iota 0 n.*2) , the iterated operation addn and the initial value is 0.
A generic notation can now be attached to bigop.
Here op is the iterated operation, idx the neutral element, r, the range, P the filter
(hence the boolean scope) and F the general term. Using such notation the running example
can be stated as follows.
To obtain a notation closer to the mathematical one, we can specialize at once the
iterated operation and the neutral element as follows.
We can now comfortably state the theorem about the sum of odd numbers inside
nat_scope. The proof of this lemma is left as an exercise; we now focus on a simpler instance,
for n equal to 3, to introduce the library that equips iterated operations.
The bigop constant is “locked” to make the notation steady. To unravel its computational
behavior one has to rewrite with the unlock lemma.
============================
1 + (3 + (5 + 0)) = 3^2
The computation behavior of bigop is generic; it does not depend on the iterated
operation. By contrast, some results on iterated operations may depend on a particular
property of the operation. For example, to pull out the last item from the summation, i.e.,
using the following lemma
if a ≤ b then ∑ Fi = ∑ Fi + Fb
a≤i<b+1 a≤i<b
to obtain
============================
1 + (3 + 0) + 5 = 3^2
one really needs the iterated operation, addition here, to be associative. Also note that,
given the filter, what one really pulls out is (if odd 5 then 5 else 0) , so for the theorem to
be true for any range, 0 must also be neutral.
The lemma to pull out the last item of an iterated operation is provided as the
combination of two simpler lemmas called respectively big_nat_recr and big_mkcond.
The former states that one can pull out of an iterated operation on a numerical range
the last element, proviso the range is non-empty.
Such lemma applies to any operation *%M and any neutral element 1 and any generic
term F, while the filter P is fixed to true (i.e., no filter). The big_mkcond lemmas moves the
filter into the generic term.
If we chain the two lemmas we can pull out the last item.
5.7 The generic theory of “big” operators 131
1 Lemma sum_odd_3 :
============================
2 \sum_(0 <= i < 3.*2 | odd i) i = 3^2.
\sum_(0 <= i < 5) (if odd i then i else 0)
3 Proof.
+ 5 =
4 rewrite big_mkcond big_nat_recr //=.
3^2
5 rewrite unlock /=.
When the last item is pulled out, we can unlock the computation and obtain the
following goal:
============================
0 + (1 + (0 + (3 + (0 + 0)))) + 5 = 3^2
It is clear that for the two lemmas to be provable, one needs the associativity property
of addn and also that 0 is neutral. In other words, the lemmas we used require the operation
*%M to form a monoid together with the unit 1.
We detail how this requirement is stated, and automatically satisfied by Coq in the
case of addn, in the next section. We conclude this section by showing that the same lemmas
also apply to an iterated product.
This is the reason why we can say that the bigop library is generic: it works uniformly
on any iterated operator, and, provided the operator has certain properties, it gives uniform
access to a palette of lemmas.
1 Module Monoid.
2 Section Definitions.
3 Variables (T : Type) (idm : T).
4
5 Structure law := Law {
6 operator : T -> T -> T;
7 _ : associative operator;
8 _ : left_id idm operator;
9 _ : right_id idm operator
10 }.
The Monoid.law structure relates the operator (the key used by canonical structures) to
the three properties of monoids.
We can then use this interface as a parameter for a bunch of lemmas, describing the
theory shared by its instances. The (Monoid.law idx) type annotation may seem puzzling at
132 Chapter 5. Implicit Parameters
first. It combines various mechanisms we have seen earlier in the book: once the section
Definitions is closed, the Variables (T : Type) and (idm : T) are abstracted in the definition
of law (and the operator projection). Moreover T becomes an implicit argument: applying
Monoid.law to idx thus builds a type.
The lemma we used in the previous section, big_nat_recr, is stated as follows. Note
that op is a record, and not a function, but since the operator projection is declared as a
coercion we can use op as such. In particular under the hood of the expression \big[*%M/1]
we find \big[ operator op / idx ] .
If we print such statement once the Section MonoidProperties is closed, we see the
requirement affecting the operation op explicitly.
big_nat_recr :
∀ (R : Type) (idx : R) (op : Monoid.law idx) (n m : nat) (F : nat -> R),
m <= n ->
\big[op/idx]_(m <= i < n.+1) F i =
op (\big[op/idx]_(m <= i < n) F i) (F n)
Note that wherever the operation op occurs, we also find the Monoid.operator projection.
To make this lemma available on the addition on natural numbers, we need to declare
the canonical monoid structure on addn.
This command adds the following rule to the canonical structures index:
canonical structures Index
projection value solution
Monoid.operator addn addn_monoid
the following unification problem has to be solved: addn versus (operator ?m) . Inferring
a value for ?m mean inferring a proof that addn forms a monoid with 0; this is a prerequisite
for the big_nat_recr lemma we don’t have to provide by hand.
5.8 Stable notations for big operators ?? 133
A lemma stating that an empty sum is zero is not part of the library. What is part of
the library is a lemma that says that, if the list being folded is nil, then the result is the
initial value. Such a lemma, called big_nil, thus mentions only [::] in its statement, and
not the (logically) equivalent (index_iota 0 0) . Still the goal (\sum_(0 <= i < 0) i = 0) can
be solved by big_nil. Finally, the pattern we provide specifies a trivial filter, while the
lemma is true for any filtering predicate. Of course one can craft a pattern that finds such
lemma, but it is very verbose and hence inconvenient.
The recommended way to search the library is by name, using the word “big”. For exam-
ple to find all lemmas allowing one to prove the equality of two iterated operators one can
Search "eq" "big". Similarly, induction lemmas can be found with Search "ind" "big"; index
exchange lemmas with Search "exchange" "big"; lemmas pulling out elements from the itera-
tion with Search "rec" "big"; lemmas working on the filter condition with Search "cond" "big",
etc. . .
Finally the Mathematical Components user is advised to read the contents of the bigop
file in order to get acquainted with the naming policy used in that library.
1 Lemma sum_odd n :
2 bigop 0 addn (index_iota 0 n.*2) (fun j => odd j) (fun i => i) = n^2
1 Lemma sum_0 n :
2 bigop 0 addn (index_iota 0 n) (fun _ => true) (fun _ => 0) = 0
To solve these problems we craft a box, BigBody, with separate compartments for each
sub component. Such box will be used under a single binder and will hold an occurrence of
the bound variable even if it is unused in the predicate and in the general term.
The arguments of BigBody are respectively the index, the iterated operation, the filter
and the generic expression. For our running example the bigbody component would be:
134 Chapter 5. Implicit Parameters
It is then easy to turn such compound term into the function expected by foldr:
While the two terms are logically equivalent (i.e., the logic cannot distinguish them),
the pretty printer can. The overloaded == notation is attached to the eq_op constant, and
if such constant fades away the notation follows it. Coq lets one declare constants that
should not be automatically simplified away, unless they occur in a context that demands
it.
The first call to simpl does not reduce away eq_op leaving the expression untouched. In
the second example, it does reduce to false the test (true == false) in order to simplify
the || connective.
The converse technological issue may arise when canonical structure inference “promotes”
the operator name to a projection of the corresponding canonical monoid structure.
5.10 Querying canonical structures ? 135
The Phantom constructor expects two arguments. If we apply it to nat, as in (Phantom Type nat) ,
we obtain a term of type (phantom Type nat) . If we apply it to addn as in (Phantom (nat -> nat -> nat) addn)
we obtain a term of type (phantom (nat -> nat -> nat) addn) . In both cases the input term
(nat and addn respectively) is now part of a type.
The following example defines a notation {set T} that fails if T is not an eqType: it is an
alias of the type (seq T) that imposes extra requirements on the type argument.
When type inference runs on {set nat} the underlying term being typed is (set_of ?T (Phantom Type nat)) .
The unification problem arising for the last argument of set_of is (phantom Type (Equality.sort ?T))
136 Chapter 5. Implicit Parameters
versus (phantom Type nat) , that in turn contains the sub problem we are interested in:
(Equality.sort ?T) versus nat.
5.11 Exercises
5.11.1 Solutions
Answer of exercise 16
1 Lemma sum_odd n : \sum_(0 <= i < n.*2 | odd i) i = n^2.
2 Proof.
3 elim: n => [|n IHn]; first by rewrite unlock.
4 rewrite doubleS big_mkcond 2?big_nat_recr // -big_mkcond /=.
5 by rewrite {}IHn odd_double /= addn0 -addnn -!mulnn; ring.
6 Qed.
6. Sub-Types
Inductive data types have been used to both code data, like lists, and logical connectives,
like the existential quantifier. Properties were always expressed with boolean programs.
The questions addressed in this chapter are the following ones. What status do we want
to give to, say, lists of size 5, or integers smaller than 7? Which relation to put between
integers and integers smaller than 7? How to benefit from extra properties integers smaller
than 7 have, like being a finite collection?
In standard mathematics one would simply say that the integers are an infinite set
(called nat), and that the integers smaller that 7 form a finite subset of the integers (called
’I_7 ). Integers and integers smaller than 7 are interchangeable data: if (n : nat) and
(i : ’I_7) one can clearly add n to i, and possibly show that the sum is still smaller than
7. Also, an informed reader knows which operations are compatible with a subset. E.g.
(i-1) stays in ’I_7 , as well as (i+n %| 7) . So in a sense, subsets also provide a linguistic
construct to ask the reader to track an easy invariant and relieving the proof text from
boring details.
The closest notion provided by the Calculus of Inductive Constructions is the one of
Σ−types, that we have already seen in the previous chapter in their general form of records.
For example, one can define the type ’I_7 as Σ(n:nat) n < 7. Since proofs are terms, one can
pack together objects and proofs of some properties to represent the objects that have
those properties. For example 3, when seen as an inhabitant of ’I_7 , is represented by a
dependent pair (3, p) where (p : 3 < 7) . Note that, by forgetting the proof p, one recovers
a nat that can be passed to, say, the program computing the addition of natural numbers,
or to theorems quantified on any nat. Also, an inhabitant of ’I_7 can always be proved
smaller than 7, since such evidence is part of the object itself. We call this construction a
sub-type.
Such representation can be expensive in the sense that it imposes extra work (proofs!)
to create a sub-type object, so it must be used with care. The Mathematical Components
library provides several facilities that support the creation of record-based sub-types, and
of their inhabitants. We shall in particular see how both type inference and dynamic tests
138 Chapter 6. Sub-Types
can be used to supply the property proofs, modelling once again the eye of a trained reader.
Finally, let us point out that we have already encountered proof-carrying records in the
previous chapter, with eqType. The eqType record played the role of an interface, expressing
a relation between a type and a function (the comparison operation), and giving access to
a whole theory of results through type inference. Many such interfaces can be extended to
sub-types, and we shall see that the Mathematical Components library provides facilities
to automate this.
The key property of this type is that it tells us the length of its elements when seen as
sequences:
In other words each inhabitant of the tuple type carries, in the form of an equality
proof, its length. As test bench we pick this simple example: a tuple is processed using
functions defined on sequences, namely rev and map. These operations do preserve the
invariant of tuples, i.e., they don’t alter the length of the subjacent list.
There are two ways to prove that lemma. The first one is to ignore the fact that t is a
tuple; consider it as a regular sequence, and use only the theory of sequences.
Mapping a function over the reverse of a list is equivalent to first mapping the function
over the list and then reversing the result (map_rev). Then, reversing twice a list is a no-op,
since rev is an involution (revK). Finally, mapping a function over a list does not change
its size (size_map). The sequence of rewritings makes the left hand side of the conjecture
identical to the right hand side, and we can conclude.
This simple example shows that the theory of sequences is usable on terms of type
tuple. Still we didn’t take any advantage from the fact that t is a tuple.
The second way to prove this theorem is to rely on the rich type of t to actually compute
the length of the underlying sequence.
6.1 n-tuples, lists with an invariant on the length 139
1 subgoal
n : nat
t : n .-tuple nat
============================
size (rev [seq 2 * x | x <- rev t]) = n
The rewriting replaces the right hand side with n as expected, but we can’t go any
further: the lemma does not apply (yet) to the left hand side, even if we are working with
a tuple t. Why is that? In the left hand side t is processed using functions on sequences.
The type of rev for example is (∀ T, seq T -> seq T). The coercion tval from tuple_of to
seq makes the expression (rev (tval t)) well typed, but the output is of type (seq nat). We
would like the functions on sequences to return data as rich as the one taken in input, i.e.,
preserve the invariant expressed by the tuple type. Or, in alternative, we would like the
system to recover such information.
Let us examine what happens if we try to unify the left hand side of the size_tuple
equation with the redex (size (rev t)), using the following toolkit:
Error:
In environment
T : Type
n : nat
t : n .-tuple T
LHS := size (tval ?94 ?92 ?96) (*...*) : nat
RDX := size (rev (tval n T t)) : nat
The term "erefl ?95" has type "?95 = ?95" while
it is expected to have type "LHS = RDX".
Unifying (size (tval ?n ?T ?t )) with (size (rev (tval n T t))) is hard. Both term’s
head symbol is size, but then the projection tval applied to unification variables has to be
unified with (rev ...), and both terms are in normal form.
140 Chapter 6. Sub-Types
Such problem is nontrivial because to solve it one has to infer a record for ?t that
contains a proof: a tuple whose tval field is rev t (and whose other field contains a proof
that such sequence has length ?n ).
We have seen in the previous chapter that this is exactly the class of problems that
is addressed by canonical structure instances. We can thus use Canonical declarations to
teach Coq the effect of list operations on the length of their input.
1 Section CanonicalTuples.
2 Variables (n : nat) (A B : Type).
3
4 Lemma rev_tupleP (t : n.-tuple A) : size (rev t) == n.
5 Proof. by rewrite size_rev size_tuple. Qed.
6 Canonical rev_tuple (t : n.-tuple A) := Tuple (rev_tupleP t).
7
8 Lemma map_tupleP (f: A -> B) (t: n.-tuple A) : size (map f t) == n.
9 Proof. by rewrite size_map size_tuple. Qed.
10 Canonical map_tuple (f: A -> B) (t: n.-tuple A) := Tuple (map_tupleP f t).
Even if it is not needed for the lemma we took as our test bench, we add another
example where the length is not preserved, but rather modified in a statically known way.
Thanks to the now extended capability of type inference, we can prove our lemma by
just reasoning about tuples.
The iterated rewriting acts now twice replacing both the left hand and the right hand
side with n. It is worth observing that the size of this proof (two rewrite steps) does not
depend on the complexity of the formula involved, while the one using only the theory of
lists requires roughly one step per list-manipulating function. What depends on the size of
the formula is the number of canonical structure resolution steps type inference performs.
Another advantage of this last approach is that one is not required to know the names of
the lemmas: it is the new concept of tuple that takes care of the size related reasoning
steps.
declaration of sub-types.
The first step is to define a comparison function for tuples.
Here we simply reuse the one on sequences, and we ignore the proof part of tuples.
What we need now to prove
The first direction is trivial by rewriting. The converse direction makes an essential use
of the eq_irrelevance lemma, which is briefly discussed in section 6.2.2.
2 subgoals
n : nat
T : eqType
x, y : n .-tuple T
============================
x = y -> tval x = tval y
subgoal 2 is:
tval x = tval y -> x = y
1 subgoal
n : nat
T : eqType
s1 : seq T
p1 : size s1 = n
s2 : seq T
p2 : size s2 = n
E : s2 = s1
============================
Tuple p2 = Tuple p1
As a simple test we check that the notations and the theory that equips eqType is
available on tuples.
142 Chapter 6. Sub-Types
Although all these proofs and definitions are specific to tuple, we are following a
general schema here, involving three parameters: the original type (seq T) , the sub-type
(n.-tuple T) and the projection tval. The Mathematical Components library provides a
sub-type kit to let one write just the following text:
Line 1 registers tval as a canonical projection to obtain a known type out of the
newly defined type of tuples. Once the projection is registered the equality axiom can be
proved automatically by [eqMixin of n.-tuple T by <:], where <: is just a symbol that is
reminiscent of sub-typing in functional languages like OCaml. The following section details
the implementation of the sub-type kit.
As we will see in the next section, the subType structure provides a generic notation val
for the projector of a sub-type (i.e., tval for tuple), with an overloaded injectivity lemma
val_inj saying that two objects equal in ST are also equal in T.
In addition to the generic projection, we get a generic static constructor Sub, which
takes a value in the type T and a proof.
More interestingly, the sub-type kit provides the dynamic constructors insub and insubd
that do not need a proof as they dynamically test the property, and offer an attractive
encapsulation of the difficult convoy pattern [Chl14, section 8.4]. The insubd constructor
takes a default sub-type value which it returns if the tests fails, while insub takes only a
base type value and returns an option; both are locked and will not evaluate the test, even
for a ground base type value.1
Both Sub and insub expect the typing context to specify the sub-type.
Here is a few example uses, using tuple:
We put insub to good use in section 6.4 when an enumeration for sub-types is to be
defined.
1 The equations describing the computation of insub are called insubT and insubF.
6.2 n-tuples, a sub-type of sequences 143
The subType structure describes a boolean sigma-type (a dependent pair whose second
component is the proof of a boolean formula) in terms of its projector, constructor, and
elimination rule:
1 Section SubTypeKit.
2 Variables (T : Type) (P : pred T).
3
4 Structure subType : Type := SubType {
5 sub_sort :> Type;
6 val : sub_sort -> T;
7 Sub : ∀ x, P x -> sub_sort;
8 (* elimination rule for sub_sort *)
9 _ : ∀ K (_ : ∀ x Px, K (@Sub x Px)) u, K u;
10 _ : ∀ x Px, val (@Sub x Px) = x
11 }.
Instances can provide unification hints for any of the three named fields, not just for
sub_sort. Hence, val ?u unifies with tval t, and Sub ?x ?xP unifies with Tuple s sP, including
in rewrite patterns.
The subType constructor notation assumes the sub-type is isomorphic to a sigma-type,
so that its elimination rule can be derived using Coq’s generic destructing let, and the
projector-constructor identity can be proved by reflexivity.
Note how the value of Sub is determined by unifying the type of the first function with
the type expected by SubType, with the help of the “as u return K u” annotation, see [Coq,
section 1.2.13].
A useful variant of [subType for tval] is [newType for Sval]. Such specialized construc-
tors force the predicate defining the sub-type to be the trivial one: the sub-type ST adds
no property to the type T, but the resulting type ST is different from T and inhabitants of
ST cannot be mistaken for inhabitants of T. Of course all the theory that equips T is also
available on ST. Aliasing a type is useful to attach to it different notations or coercions.
If we pick the concrete example of bool, then all proofs that (b = true) for a fixed b are
identical.
Here we can see another crucial advantage of boolean reflection. Forming sub-types
poses no complication from a logic perspective since proofs of boolean identities are very
simple, canonical, objects.
144 Chapter 6. Sub-Types
In the Mathematical Components library, where all predicates that can be expressed as
a boolean function are expressed as a boolean function, forming sub-types is extremely easy.
R It is convenient to define new types as sub-types of existing ones, since they inherit
all the theory.
The axiom asserts that any inhabitant of T occurs exactly once in the enumeration e.
We omit here the full definition of the interface, as it will be discussed in detail in the next
chapter. What is relevant for the current section is that finType is the structure of types
equipped with such enumeration, that any finType is also an eqType (see the parameter of
the mixin), and that, to declare a finType instance, one can write:
Given that the most recurrent way of showing that an enumeration validates Finite.axiom
is by proving that it is both duplicate free and exhaustive, a convenience mixin constructor
is provided.
The interface of finType comes equipped with a theory that, among other things, provides
a cardinality operator #|T| and bounded boolean quantifications like [∀ x, P].
The constructor Ordinal has two arguments: a natural number m and a proof that this number
is smaller than the parameter n. We use the of notation for arguments of constructors that
do not need to be named; thus Ordinal m of m < n stands for Ordinal m (_ : m < n)
We start by making ordinals a subtype of natural numbers, and hence inherit the theory
of eqType. To show they form a finType, we need to provide a good enumeration.
The iota function produces the sequence [:: 0; 1; ...; n.-1]. Such a sequence is
mapped via insub that tests if an element x is smaller than n. If it is the case it produces
(Some x) , where x is an ordinal, else None. pmap drops all None items, and removes the Some
constructor from the others.
What ord_enum produces is hence a sequence of ordinals, i.e., a sequence of terms
like (@Ordinal m p) where m is a natural number (as produced by iota) and p is a proof
that (m <= n) . What we are left to show is that such an enumeration is complete and
non-redundant.
It is worth pointing out how the val_ord_enum lemma shows that the ordinals in ord_enum
are exactly the natural numbers generated by (iota 0 n) . In particular, the insub construc-
tion completely removes the need for complex dependent case analysis.
146 Chapter 6. Sub-Types
2 subgoals
n : nat
============================
[seq x <- iota 0 n | isSome (insub x)] = iota 0 n
subgoal 2 is:
ocancel insub val
The view all_filterP shows that reflect ([seq x <- s | a x] = s) (all a s) for any se-
quence s and predicate a. After applying that view, one has to prove that if (i \in iota 0 n)
then (i < n) , that is trivialized by mem_iota.
We can now declare the type of ordinals as a instance of finType.
1 Definition ordinal_finMixin n :=
2 Eval hnf in UniqFinMixin (ord_enum_uniq n) (mem_ord_enum n).
3 Canonical ordinal_finType n :=
4 Eval hnf in FinType (ordinal n) (ordinal_finMixin n).
An example of ordinals at work is the tnth function. It extracts the n-th element of a
tuple exactly as nth for a sequence but without requiring a default element. As a matter of
fact, one can use ordinals to type the index, making Coq statically checks that the index
is smaller than the size of the tuple.
1 Section FinFunDef.
2 Variables (aT : finType) (rT : Type).
3
6.5 Finite functions 147
As a result, the final notation provides a way to describe an instance of the type of finite
function by giving the mere type of the domain and co-domain, without mentioning the name
of the instance of finType for the domain. One can thus write the term {ffun ’I_7 -> nat} but
the term {ffun nat -> nat} would raise an error message, and their cannot be a registered
instance of finite type for nat.
Other utilities let one apply a finite function as a regular function or build a finite
function from a regular function.
What codom_tuple builds is a list of values f takes when applied to the values in the
enumeration of its domain.
Finite functions inherit from tuples the eqType structure whenever the codomain is an
eqType.
When the codomain is finite, the type of finite functions is itself finite. This property is
again inherited from tuples. Recall the all_words function, solution of exercise 7.
A relevant property of the finType of finite functions is its cardinality, being equal to
#|rT| ^ #|aT|.
148 Chapter 6. Sub-Types
Such lemma, rephrased in mathematical notation down below, states that the indices i
and j are independently chosen.
∏ ∑ Fi j = ∑ ∏ Fi( f i)
i∈I j∈J f ∈I→J i∈I
Remark how the finite type of functions from I to J is systematically formed in order
to provide its enumeration as the range of the summation.
1 Section finSetDef.
2 Variable T : finType.
3 Inductive set_type : Type := FinSet of {ffun pred T}.
4 Definition finfun_of_set A := let: FinSet f := A in f.
We omit again the trick to statically enforce that T is a finite type whenever we write
{set T} , exactly as we did for finite functions. Finite sets do validate extensionality and
are equipped with subset-wise and point-wise operations:
It is worth noticing that many “set” operations are actually defined on simpler structures
we did not detail for conciseness. In particular membership and subset are also applicable
to predicates, i.e. terms that can be seen as functions from a type to bool.
Since T is finite, values of type {set T} admit a complement and {set T} is closed under
power-set construction.
We have seen how tuples can be used to carry an invariant over sequences. In particular
type inference was programmed to automatically infer the effect of sequence operations
over the size of the input tuple. In a similar way finite groups can naturally be seen as sets
and some set-wise operations, like intersection, do preserve the group structure and type
inference can be programmed to infer so automatically.
6.7 Permutations
Another application of finite functions is the definition of the type of permutations.
This time we add the property of being injective, that in conjunction with finiteness
characterizes permutations as bijections.
Similarly to finite functions we can declare a coercion to let one write (s x) for
(s : {perm T}) to denote the result of applying the permutation s to x.
Thanks to the sub-type kit it is easy to transport to the type {perm T} the eqType and
finType structures of ffun T -> T.
6.8 Matrix
We finally have all the bricks to define the type of matrices and provide compact formulations
for their most common operations.
As for permutations and finite functions we declare a coercion to let one denote (A i j)
the coefficient in column j of row i. Note that type inference will play an important role
here. If A has type ’M[R]_(m,n) , then Coq will infer that (i : ’I_m) and (j : ’I_n) from the
expression (A i j) . In combination with the notations for iterated operations, this lets one
define, for example, the trace of a square matrix as follows.
Note that, for the \sum notation to work, R needs to be a type equipped with an addition,
for example a ringType. We will describe such type only in the next chapter. From now on
the reader shall interpret the + and * symbols on the matrix coefficients as (overloaded)
ring operations, exactly as == is the overloaded comparison operation of eqType.
Via the sub-type kit we can transport eqType and finType from {ffun ’I_m * ’I_n -> R}
to ’M[R]_(m,n) . We omit the Coq code for brevity.
A useful accessory is the notation to define matrices in their extension. We provide a
variant in which the matrix size is given and one in which it has to be inferred from the
context.
1 Definition matrix_of_fun R m n F :=
2 Matrix [ffun ij : ’I_m * ’I_n => F ij.1 ij.2].
3 Notation "\matrix_ ( i < m , j < n ) E" :=
4 (matrix_of_fun (fun (i : ’I_m) (j : ’I_n) => E))
5 Notation "\matrix_ ( i , j ) E" := (matrix_of_fun (fun i j => E)).
6
7 Example diagonal := \matrix_(i < 3, j < 7) if i == j then 1 else 0.
First, the type of the inputs makes such operation total, i.e., Coq rejects terms which
would represent the product of two matrices whose sizes are incompatible.
This has to be compared with what was done for integer division, that was made total
by returning a default value, namely 0, outside its domain. In the case of matrices a size
annotation is enough to make the operation total, while for division a proof would be
necessary. Working with rich types is not always easy, for example the type checker does
not understand automatically that a square matrix of size (m + n) can be multiplied with
a matrix of size (n + m) . In such case the user has to introduce explicit size casts, see
section 6.8.3. At the same time type inference lets one omit size information most of the
time, playing once again the role of a trained reader.
The idea of the proof is to lift the commutativity property of the multiplication in
the coefficient’s ring. The first step is to prove an equation that expands the trace of
matrix product. The plan is to expand it on both sides, then exchange the summations
and compare the coefficients pairwise.
1 subgoal
R : comRingType
m, n : nat
A : ’M_(m, n)
B : ’M_(n, m)
============================
\sum_i \sum_j A i j * B j i = \tr (B *m A)
152 Chapter 6. Sub-Types
It is worth noticing that the equation we used to expand the left hand side and the one
we need to expand the right hand side are very similar. Actually the sub proof following
have can be generalized to any pair of matrices A and B. The Small Scale Reflection proof
language provides the gen modifier in order to tell have to abstract the given formula over a
list of context entries, here m n A B.
The gen have step now generates two equations, a general one called trE, and its instance
to A and B called trAB.
1 subgoal
R : comRingType
m, n : nat
A : ’M_(m, n)
B : ’M_(n, m)
trE : ∀ m n (A : ’M_(m, n)) B, \tr (A *m B) = \sum_i \sum_j A i j * B j i
trAB : \tr (A *m B) = \sum_i \sum_j A i j * B j i
============================
\sum_i \sum_j A i j * B j i = \sum_i \sum_j B i j * A j i
The proof is then concluded by exchanging the summations, i.e., summing on both
sides first on i then on j, and then proving their equality by showing the identity on the
summands.
Note that the final identity is true only if the multiplication of the matrix coefficients is
commutative. Here R was assumed to be a comRingType, the structure of commutative rings
and mulrC is the name of the commutative property (C) of ring (r) multiplication (mul). A
more detailed description of the hierarchy of structures is the subject of the next chapter.
Conversely blocks can be glued together. This time, it is the size of the resulting matrix
that shows a trace of the way it was built.
6.8 Matrix 153
1 Definition row_mx (A1 : ’M_(m, n1)) (A2 : ’M_(m, n2)) : ’M_(m, n1 + n2)
2 Definition col_mx (A1 : ’M_(m1, n)) (A2 : ’M_(m2, n)) : ’M_(m1 + m2, n)
3 Definition block_mx Aul Aur Adl Adr : ’M_(m1 + m2, n1 + n2)
The interested reader can find in [Gar+09] a description of Cormen’s LUP decomposition,
an algorithm making use of these constructions. In particular, recursion on the size of a
square matrix of size n naturally identifies an upper left square block of size 1, a row and a
column of length n − 1, and a square block of size n − 1.
1 Section SizeCast.
2 Variables (n n1 n2 n3 m m1 m2 m3 : nat).
3
4 Lemma row_mxA (A1 : ’M_(m, n1)) (A2 : ’M_(m, n2)) (A3 : ’M_(m, n3)) :
5 row_mx A1 (row_mx A2 A3) = row_mx (row_mx A1 A2) A3.
Observe that the left hand side has type ’M_(m, n1 + (n2 + n3)) while the right hand
side has type ’M_(m, (n1 + n2) + n3) . The castmx operator, and all its companion lemmas,
let one deal with this inconvenience.
1 Lemma row_mxA (A1 : ’M_(m, n1)) (A2 : ’M_(m, n2)) (A3 : ’M_(m, n3)) :
2 let cast := (erefl m, esym (addnA n1 n2 n3)) in
3 row_mx A1 (row_mx A2 A3) = castmx cast (row_mx (row_mx A1 A2) A3).
The cast object provides the proof evidence that (m = m) , not strictly needed, and that
(n1 + (n2 + n3) = (n1 + n2) + n3) .
Lemmas like the following two let one insert or remove additional casts.
Remark that erefl_mn must have type ((m = m) * (n = n)) , i.e., it is a useless cast.
Another useful tool is conform_mx that takes a default matrix of the right dimension and
a second one that is returned only if its dimensions match.
Remember that the notation (m =P m1) stands for (@eqP nat_eqType m m1) , a proof of the
reflect inductive spec. Remember also that the ReflectT constructor carries a proof of the
equality.
The following helper lemmas describe the behavior of conform_mx and how it interacts
with casts.
154 Chapter 6. Sub-Types
We have seen in the last two chapters how inferred dependent records — structures — are
an efficient means of endowing mathematical objects with their expected operations and
properties. So far we have only seen single-purpose structures: eqType provides decidable
equality, subType an embedding into a representation type, etc.
However, the more interesting mathematical objects have many operations and prop-
erties, most of which they share with other kinds of objects: for example, elements of
a field have all the properties of those of a ring (and more), which themselves have all
the properties of an additive group. By organizing the corresponding Calculus of Induc-
tive Constructions structures in a hierarchy, we can materialize these inclusions in the
Mathematical Components library, and share operations and properties between related
structures. For example, we can use the same generic ring multiplication for rings, integral
domains, fields, algebras, and so on.
Organizing structures in a hierarchy does not require any new logical feature beyond
those we have already seen: type inference with dependent types, coercions and canonical
instances of structures. It is only a “simple matter of programming”, albeit one that involves
some new formalisation idioms. This chapter describes the most important: telescopes,
packed classes, and phantom parameters.
While some of these formalisation patterns are quite technical, casual users do not
need to master them all: indeed the documented interface of structures suffices to use and
declare instances of structures. We describe these interfaces first, so only those who wish
to extend old or create new hierarchies need to read on.
structure.
The intrinsic interface of a structure is much smaller, and consists mostly of functions
for creating instances to be typically declared Canonical. For structures like eqType that are
packaged in a submodule (Equality for eqType), the interface coincides with the contents of
the Exports submodule. For eqType the interface comprises:
• eqType: a short name for the structure type (here, Equality.type)
• EqMixin, PcanEqMixin, [eqMixin of T by <:]: mixin constructors that bundle the new
operations and properties the structure provides.
• EqType: an instance constructor that creates an instance of the structure from a mixin.
• [eqType of T], [eqType of T for S]: cloning constructors that specialize a canonical or
given instance of the structure (to T here).
• canonical instances and coercions that link the structures to lower ones in the hierarchy
or to its elements, e.g., Equality.sort.
Canonical instances and coercions are not mentioned directly in the documentation because
they are only used indirectly, through type inference; a casual user of a structure only
needs to be aware of which other structure it extends, in the hierarchy.
Let us see how the creation operations are used in practice, drawing examples from the
zmodp library that puts a “mod p” algebraic structure on the type ordinal p of integers
less than p. The ordinal type is defined in library fintype as follows:
Algebra only makes sense on non-empty types, so zmodp only defines arithmetic on ’I_p
when p is an explicit successor. This makes it easy to define inZp, a “mod p” right inverse
to the ordinal >-> nat coercion, and a 0 value. With these the definition of arithmetic
operations and the proof of the basic algebraic identities is straightforward.
1 Variable p’ : nat.
2 Local Notation p := p’.+1.
3 Implicit Types x y : ’I_p.
4 Definition inZp i := Ordinal (ltn_pmod i (ltn0Sn p’)).
The inZp construction injects any natural number i into ’I_p by applying the modulus.
Indeed the type of ltn_pmod is (∀ m d : nat,0 < d -> m %% d < d) , and (ltn0Sn p’) is a proof
that (0 < p) .
We can now build the Z-module operations and properties:
Creating an instance of the lowest ssralg structure, the Z-module (i.e., additive group),
requires two lines:
7.1 Structure interface 157
Line 1 bundles the additive operations (0, +, −) and their properties in a mixin, which
is then used in line 2 to create a canonical instance. After line 2 all the additive algebra
provided in ssralg becomes applicable to ’I_p; for example 0 denotes the zero element, and
i + 1 denotes the successor of i mod p.
The ZmodMixin constructor infers the operations Zp_add, etc., from the identities Zp_add0z,
etc.. Providing an explicit definition for the mixin, rather than inlining it in line 2, is
important as it speeds up type checking, which never need to open the mixin bundle.
The first argument to the instance constructor ZmodType is somewhat redundant, but
documents precisely the type for which this instance will be used. This can be important as
the value inferred by Coq could be “different”. Indeed line 2 does perform some nontrivial
inference, because, although zmodType is the first ssralg structure, it is not at the bottom
of the hierarchy: in particular zmodType derives from eqType, so the == test can be used on
all zmodType elements. The ZmodType constructor infers a parent structure instance from its
first argument, then combines it with the mixin to create a full zmodType instance. This
inference can have the side effect of unfolding constants occurring in the description of the
type (though not in this case), that is the value on which the canonical solution is indexed.
For this reason the type description, ’I_p here, has to be provided explicitly. Section 7.4
gives the technical details of instance constructors.
Rings are the next step in the algebraic hierarchy. In order to simplify the formalization
of the theory of polynomials, ssralg only provides structures for nontrivial rings, so we now
need to restrict to p of the form p’.+2:
1 Variable p’ : nat.
2 Local Notation p := p’.+2.
3 Lemma Zp_nontrivial : Zp1 != 0 :> ’I_p. Proof. by []. Qed.
4 Definition Zp_ringMixin :=
5 ComRingMixin (@Zp_mulA _) (@Zp_mulC _) (@Zp_mul1z _) (@Zp_mul_addl _)
Zp_nontrivial.
6 Canonical Zp_ringType := RingType ’I_p Zp_ringMixin.
7 Canonical Zp_comRingType := ComRingType ’I_p (@Zp_mulC _).
Line 6 endows ’I_p with a ringType structure, making it possible to multiply in ’I_p or
have polynomials over ’I_p. Line 7 adds a comRingType commutative ring structure, which
makes it possible to reorder products, or distribute evaluation over products of polynomials.
Note that no mixin definition is needed for line 8 as only a single property is added.
Constraining the shape of the modulus p is a simple and robust way to enforce p > 1:
it standardizes the proofs of p > 0 and p > 1, which avoid the unpleasantness of multiple
interpretations of 0 stemming from different proofs of p > 0 — the latter tends to happen
with ad hoc inference of such proofs using canonical structures or tactics. The shape
constraint can however be inconvenient when the modulus is an abstract constant (say,
Variable p), and zmodp provides some syntax to handle that case:
Although it is provably equal to ’I_p when p > 1, ’Z_p is the preferred way of referring
to that type when using its ring structure. Note that the two types are identical when p is
a nat literal such as 3 or 5.
158 Chapter 7. Organizing Theories
Cloning constructors are mainly used to quickly create instances for defined types, such
as
While ssralg and zmodp provide the instances type inference needs to synthesize a ring
structure for Zmn, Coq has to expand the definition of Zmn to do so. Declaring Zmn-specific
instances will avoid such spurious expansions, and is easy thanks to cloning constructors:
Cloning constructors are also useful to create on-the-fly instances that must be passed
explicitly, e.g., when specializing lemmas:
Finally, instances of join structures that are just the union of two smaller ones are always
created with cloning constructors. For example, ’I_p is also a finite (explicitly enumerable)
type, and the fintype library declares a corresponding finType structure instance. This
means that ’I_p should also have an instance of the finRingType join structure (for p of the
right shape). This is not automatic, but thanks to the cloning constructor requires only
one line in zmodp.
7.2 Telescopes
While using and populating a structure hierarchy is fairly straightforward, creating a robust
and efficient hierarchy can be more difficult. In this section we explain telescopes, one of
the simpler ways of implementing a structure hierarchy. Telescopes suffice for most simple
— tree-like and shallow — hierarchies, so new users do not necessarily need expertise with
the more sophisticated packed class organization covered in the next section.
Because of their limitations (covered at the end of this section), telescopes were not
suitable for the main type structure hierarchy of the Mathematical Components library,
including eqtype, choice, fintype and ssralg. However, as we have seen in section 5.7.2,
structures can be used to associate properties to any logical object, not just types, and the
Monoid.law structure introduced in section 5.7.2 is part of a telescope hierarchy. Recall that
Monoid.law associates an identity element and Monoid axioms to a binary operator:
1 Module Monoid.
2 Variables (T : Type) (idm : T).
3 Structure law := Law {
4 operator : T -> T -> T;
5 _ : associative operator;
6 _ : left_id idm operator;
7 _ : right_id idm operator
8 }.
9 Coercion operator : law >-> Funclass.
7.2 Telescopes 159
The Coercion declaration facilitates writing generic bigop simplification rules such as
Because the Monoid hierarchy is small, there is no need to bundle the Monoid.law properties
in a mixin. It thus takes only one line to declare an instance for the boolean “and” operator
andb
This declaration makes it it possible to use big1_eq to simplify the “big and” expression
1 \big[and/true]_(i in A) true
to just true,1 as it informs type inference how to solve the unification problem (operator
?L ) versus andb, by setting ?L to andb_monoid.
Now many of the more interesting bigop properties permute the operands of the iterated
operator; for example
Such properties only hold for commutative monoids, so, in order to state pair_bigA as
above, we need a structure encapsulating commutative monoids — and one that builds on
Monoid.law at that, to avoid mindless duplication of theories. The most naı̈ve way of doing
this, merely combining a law with a commutativity axiom, works remarkably well. After
1 \big[andb/true]_i \big[andb/true]_j M i j.
However, things are not so simple on closer examination: the idiom only works because
of the invisible coercions inserted during type inference.
The definition of andb_comoid infers the implicit com_operator argument ?L of ComLaw by
unifying the expected statement commutative (operator ?L ) of the commutativity property,
with the actual statement of andbC : commutative andb. This finds ?L to be andb_monoid as
above.
1 There is no spurious add_monoid because the identity element is a manifest field stored in the structure
type.
160 Chapter 7. Organizing Theories
More importantly, the op in the statement of big_pairA really stands for operator
(com_operator op). Thus applying big_pairA to the term above leads to the unification
of operator (com_operator ?C ) with andb. This first resolves the outer operator, as above,
reducing the problem to unifying com_operator ?C with andb_monoid, which is finally solved
using andb_comoid. Hence, andb_comoid associates commutativity with the law andb_monoid
rather than the operator andb, and the invisible chain of coercions guides the instance
resolution.
The telescope idiom works recursively for arbitrarily deep hierarchies, though the Monoid
one only has one more level for a distributivity property
then associates distributivity to the andb_comoid structure which is inferred by the two-stage
resolution process above, and applying the iterated distributivity
1 bigA_distr_bigA :
2 \big[times/one]_(i : I) \big[plus/zero]_(j : J) F i j
3 = \big[plus/zero]_(f : {ffun I -> J}) \big[times/one]_i F i (f i).
1 Module Equality.
2
3 Definition axiom T (e : rel T) := ∀ x y, reflect (x = y) (e x y).
4
5 Record mixin_of T := Mixin {op : rel T; _ : axiom op}.
6 Notation class_of := mixin_of.
7
8 Structure type := Pack {sort :> Type; class : class_of sort}.
9 ...
10 Module Exports.
11 Coercion sort : type >-> SortClass.
12 Notation eqType := type.
13 ...
14 End Equality.
15 Export Equality.Exports.
The Exports submodule, which we had omitted in section 5.4, regroups all the dec-
larations in Equality that should have global scope, such as the Coercion declaration for
Equality.sort.
The roles of mixin and class are conflated for eqType because it sits at the bottom of
the type structure hierarchy. To clarify the picture, we need to move one level up, to the
choiceType structure that provides effective choice for decidable predicates:
1 Module Choice.
2
3 Record mixin_of T := Mixin {
4 find : pred T -> nat -> option T;
5 _ : ∀ P n x, find P n = Some x -> P x;
6 _ : ∀ P : pred T, (exists x, P x) -> exists n, find P n;
7 _ : ∀ P Q : pred T, P =1 Q -> find P =1 find Q
8 }.
9
10 Record class_of T :=
11 Class {base : Equality.class_of T; mixin : mixin_of T}.
12
13 Structure type := Pack {sort; _ : class_of sort}.
The main operation provided by the choiceType structure T is a choice function for
decidable predicates (choose : pred T -> T -> T) satisfying:
The mixin actually specifies a specific, depth-based, strategy for searching and electing
a witness: choose can be defined using find and the axiom of countable choice, which is
derivable in Calculus of Inductive Constructions.
An important difference to telescopes is that the definition of Choice.type does not link
it directly to eqType: a choiceType structure contains an Equality.class_of record, rather
than an eqType structure. That link needs to be constructed explicitly in the code that
follows the definition of Choice.type:
Here class is just the explicit definition of the second component of the Section variable
cT : type.
Thanks to the Coercion declarations, the eqType definition is indeed the eqType structure
associated to cT, with sort equal to cT ≡ sort cT and class equal to base class. The actual
link between choiceType and eqType is established by the following two lines in Choice.Exports:
Line 1 merely lets us explicitly use a choiceType where an eqType is expected, which
is rare as structures are almost alway implicit and inferred. It is line 2 that really lets
choiceType extend eqType, because it makes it possible to use any element (T : choiceType)
as an element of an eqType, namely Choice.eqType T: it tells type inference that Choice.sort T
can be unified with Equality.sort ?E by taking ?E = Choice.eqType T.
The bottom structure in the Mathematical Components algebraic hierarchy introduced
by the ssralg library is zmodType (GRing.Zmodule.type); it encapsulates additive groups, and
directly extends the choiceType structure.
1 Module GRing.
2
3 Module Zmodule.
4
5 Record mixin_of (V : Type) : Type := Mixin {
6 zero : V; opp : V -> V; add : V -> V -> V;
7 _ : associative add;
8 ...}.
9
10 Record class_of T := Class { base: Choice.class_of T; mixin: mixin_of T }.
11 Structure type := Pack {sort; _ : class_of sort}.
Strictly speaking, the Mathematical Components algebraic structures don’t really have
to extend choiceType, but it is very convenient that they do. We can use eqType and
choiceType operations to test for 0 in fields, or choose a basis of a subspace, for example.
Furthermore, this is essentially a free assumption, because the Mathematical Components
algebra mixins specify strict identities, such as associative add on line 7 above. In the pure
Calculus of Inductive Constructions, these can only be realized for concrete data types
with a binary representation, which are both discrete and countable, hence are choiceTypes.
On the other hand, the “classical Calculus of Inductive Constructions” axioms needed to
construct, e.g., real numbers, imply that all types are choiceTypes.
Similarly to the definition of eq_op in eqtype, the operations afforded by zmodType are
defined just after the Zmodule module.
7.3 Packed classes ? 163
These are defined inside the GRing module that encloses most of ssralg, and also given
the usual arithmetic syntax (0, - x , x + y) in the %R scope. Only the notations are exported
from GRing, as these definitions are intended to remain private.
The next structure in the hierarchy encapsulates nontrivial rings. Imposing the non-
triviality condition 1 6= 0 is a compromise: it greatly simplifies the theory of polynomials
(ensuring for instance that X has degree 1), at the cost of ruling out possibly trivial matrix
rings.
1 Module Ring.
2
3 Record mixin_of (R : zmodType) : Type := Mixin {
4 one : R;
5 mul : R -> R -> R;
6 _ : associative mul;
7 _ : left_id one mul;
8 _ : right_id one mul;
9 _ : left_distributive mul +%R;
10 _ : right_distributive mul +%R;
11 _ : one != 0
12 }.
13
14 Record class_of (R : Type) : Type := Class {
15 base : Zmodule.class_of R;
16 mixin : mixin_of (Zmodule.Pack base)
17 }.
18
19 Structure type := Pack {sort; _ : class_of sort}.
Unlike choiceType and zmodType, the definition of the ringType mixin depends on the
zmodType structure it extends. Observe how the class definition instantiates the mixin’s
zmodType parameter with a record created on the fly by packing the representation type
with the base class.
This additional complication does not affect the hierarchy declarations. These follow
exactly the pattern we saw for choiceType, except that we have three definitions, one for
each of the three structures ringType extends. They all look identical, thanks to the hidden
XXX.base coercions.
are reasonable instances of each: 2 × 2 matrices over Q have computable inverses but do
not commute, while polynomials over Z p commute but do not have easily computable
inverses. The definition of comRingType and unitRingType follow exactly the pattern we have
seen, except there is no need for a ComRing.mixin_of record.
Since there are also rings such as Z p that commute and have computable inverses,
and properties such as (x/y)n = xn /yn that hold only for such rings, ssralg provides a
comUnitRingType structure for them. Although this structure simultaneously extends two
unrelated structures, it is easy to define using the packed class pattern: we just reuse the
UnitRing mixin.
1 Module ComUnitRing.
2
3 Record class_of (R : Type) : Type := Class {
4 base : ComRing.class_of R;
5 mixin : UnitRing.mixin_of (Ring.Pack base)
6 }.
7
8 Structure type := Pack {sort; _ : class_of sort}.
Since we construct explicitly the links between structures with the packed class pattern,
the fact that the hierarchy is no longer a tree is not an issue.
In the above code, lines 1–6 relate the new structure to each of the six structures
it extends, just as before. Line 7 is needed because comUnitRingType has several direct
ancestors in the hierarchy. Making ComUnitRing.com_unitRingType a canonical unitRingType
instance tells type inference that it can unify UnitRing.sort ?U with ComRing.sort ?C , by
unifying ?U with ComUnitRing.com_unitRingType ?R and ?C with ComUnitRing.comRingType ?R ,
where ?R : comUnitRingType is a fresh unification variable. In other words, the ComUnitRing.
com_unitRingType instance says that comUnitRingType is the join of comRingType and unitRingType
in the structure hierarchy (see also [MT13, section 5]).
If a new structure S extends structures that are further apart in the hierarchy more than
one such additional link may be needed: precisely one for each pair of structures whose join
is S. For example, unitRingAlgebraType requires three such links, while finFieldType in library
finalg requires 11. It is highly advisable to map out the hierarchy when simultaneously
extending multiple structures.
Finally, the telescope and packed class design patterns are not at all incompatible: it
is possible to extend a packed class hierarchy with telescopes (library fingroup does this),
or to add explicit “join” links to a telescope hierarchy (ssralg does this for its algebraic
predicate hierarchy).
int * rat is
In the definition of the structure type for left modules, which depends on ringType
parameter R, we add a dummy phant R parameter phR.
1 Module Lmodule.
2
3 Variable R : ringType.
4
5 Record mixin_of (R : ringType) (V : zmodType) := Mixin {
6 scale : R -> V -> V;
7 ...}.
8
9 Record class_of V := Class {
10 base : Zmodule.class_of V;
11 mixin : mixin_of R (Zmodule.Pack base)
12 }.
13
14 Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Then the Phant constructor readily yields a value for phR, from just the sort of R. Hiding
the call to Phant in a Notation
allows us to write V : lmodType (int * rat) and let type inference fill in the unsightly
expression pair_ringType int_ringType rat_ringType for R.
Inference for constructors is more involved, because it has to produce bespoke classes
and mixins subject to dependent typing constraints. While it is in principle possible to
program this using dependent matching and transport, the complexity of doing so can be
daunting.
Instead, we propose a simpler, static solution using a combination of phantom and
function types:
166 Chapter 7. Organizing Theories
For example, each packed class contains exactly the same definition of the clone
constructor, following the introduction of section variables T and cT, and the definition of
class:
Recall that with SSReflect loaded, & T introduces an anonymous parameter of type T.
As for lmodType above we use Notation to supply the identity function for this dummy
functional parameter
1 Definition pack T m :=
2 fun bT b & phant_id (Equality.class bT) b => Pack (@Class T b m).
3 Notation ChoiceType T m := (@pack T m _ _ id).
For ringType we use a second phant_id id parameter to check the dependent type
constraint on the mixin.
Type-checking the second id will set m to m0 after checking that the inferred base class
b ≡ Zmodule.class bT coincides with the actual base class b0 in the structure parameter of
the type of m0. Forcing the sort of that parameter to be equal to T allows Coq to infer T
from m.
The instance constructor for the join structure comUnitRingType uses a similar projection-
by-unification idiom to extract a mixin of the appropriate type from the inferred unitRingType
of a given type T. This is the only constructor for comUnitRingType.
1 Definition pack T :=
2 fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) =>
3 fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) =>
4 Pack (@Class T b m).
7.5 Linking a custom data type to the library 167
Finally, the instance constructor for the left algebra structure lalgType, a join structure
with an additional axiom and a ringType parameter, uses all the patterns discussed in this
section, using a phant and three phant_id arguments.
The interested reader can also refer to [MT13, section 7] for a description of this technique.
1 Inductive windrose := N | S | E | W.
The most naive way to show that windrose is a finType is to provide a comparison function,
then a choice function, . . . finally an enumeration. Instead, it is much simpler to show one
can punt windrose in bijection with a pre-existing finite type, like ’I_4 . Let us start by
defining the obvious injections.
Remark how the inord constructor lets us postpone the (trivial by computation) proofs
that 0, 1, 2, 3 are smaller than 4.
The type of ordinals is larger; hence we provide only a partial function.
Now, thanks to the PcanXXXMixin family of lemmas, one can inherit on windrose the structures
of ordinals.
168 Chapter 7. Organizing Theories
Only one tiny detail is left on the side. To use windrose in conjunction with \in and #|...|,
the type declaration has to be tagged as a predArgType as follows.
After that, our new data type can be used exactly as the ordinal one can.
More in general a data type can be equipped with a eqType, choiceType, and countType
structure by providing a correspondence with the generic tree data type (GenTree.tree T) :
an n-ary tree with nodes labelled with natural numbers and leafs carrying a value in T.
III
Synopsis
8.1 Definition
8.1.1 Data structure
1 Inductive nat : Type := O | S (n : nat)
opens two subgoals: in the first one n is substituted by O, in the second one it is substituted
by m.+1.
Recurrence
On a natural number n : nat present in the context, the tactic:
opens two subgoals: in the first one n is substituted by O, in the second one it is substituted
by m.+1. The second subgoal features an induction hypothesis, for m, named ihm.
See also
Section 8.7.
8.2 Comparisons
See also
Section 8.6.
T he bar ===============
P : nat -> Prop P : nat -> Prop
Goal ∀ y, y == x -> y \in S x : nat x : nat
cmd=> /andP[pa pb]
| {z } | {z } ====================== → h : P x
(∀ n, P n) -> G =================
Assumptions Conclusion Run cmd, then apply the view andP to Top, then destruct G
the conjunction and introduce in the context the two parts
Top is the first assumption, y here naming the pa and pb
Stack alternative name for the list of Assumptions
========= pa : A Pushing to the stack
Popping from the stack A && B -> C -> D pb : B
→ Note: in the following cmd is not apply or exact. Moreover
=========
Note: in the following we assume cmd does nothing, exactly C -> D we display the goal just before cmd is run.
like move.
cmd: (x) y
cmd=> x px
cmd=> /= {px}
Run cmd, then pop Top, put it in the context naming it x Run cmd then simplify the goal then discard px from then Push y then push x on the stack. y is also cleared
then pop the new Top and names it px in the context context
x, y : nat x : nat
========= x : T x : nat x : nat px : P x px : P x
px : P x =========
→
∀ x, px : P x ========= =========
→ →
P x -> Q x -> G ========= ========= Q x -> R x Q x y ∀ x0 y, Q x0 y
Q x -> G true && Q x -> R x
Unfold the definition of && Reason by cases using the leqP spec lemma
Clear px and generalize the goal with respect to the first a, b : nat a, b : nat
a : bool a : bool
match of the pattern _.+1 ========= ========= ========= → =========
→ a <= b && b > a true && false
a && a = a if a then a
else false = a
x : nat x : nat
px : P x ========= a, b : nat
→
========= ∀ x0, x < x0 =========
x < x.+1 rewrite /= -[a]/(0+a) -/c. false && true
Simplify the goal, then change a into 0+a, finally fold back
Proof commands the local definition c elim: s.
ab : A /\ B =========
Eab : a = b Eab : a = b ========= A -> B -> G =========
→
Eac : a = c ========= G ∀ s x,
→
========= P c P s ->
P b P (rcons s x)
have pa : P a. apply: (iffP V) Eab : a == b Eab : a == b
============= → =========
P a P b
Open a new goal for P a. Once resolved introduce a new Proves a reflection goal, applying the view lemma V to
entry in the context for it named pa the propositional part of reflect. E.g. apply: (iffP idP)
Idioms
a : T a : T case: b => [h1| h2 h3]
P : Prop P : Prop
========= → =========
b : bool b : bool
G P a →
============= =========
reflect P b b -> P
Push b, reason by cases, then pop h1 in the first branch
and h2 and h3 in the second
a : T
pa : P a have /andP[x /eqP->] : P a && b == c
========= P : Prop
G b : bool
========= Open a subgoal for P a && b == c. When proved apply
P -> b to it the andP view, destruct the conjunction, introduce x,
apply the view eqP to turn b == c into b = c, then rewrite
by []. with it and discard the equation
apply/V1/V2
elim: n.+1 {-2}n (ltnSn n) => {n}// n
Prove the goal by trivial means, or fail
Prove boolean equalities by considering them as logical General induction over n, note that the first goal has a
=========
→ double implications. The term V1 (resp. V2) is the view false assumption ∀ n, n < 0 -> ... and is thus solved by
0 <= n
lemma applied to the left (resp. right) hand side. E.g. //
apply/idP/negP
n : nat
n : nat
exact: H. =========
b1 : bool b1 : bool ========= →
(∀ m, m < n -> P m) ->
b2 : bool b2 : bool P n
→ ∀ m, m < n.+1 -> P m
========= =========
Apply H to the current goal and then assert all remaining b1 = ~~ b2 b1 -> ~ b2
goals, if any, are trivial. Equivalent to by apply: H.
rewrite lem1 ?lem2 //
H : B b1 : bool
========= → b2 : bool
B ========= Use the equation with premises lem1, then get rid of the
~ b2 -> b1 side conditions with lem2
Searching
Reflect and views
rewrite: (eqP Eab) Search _ addn (_ * _) "C" in ssrnat
reflect P b
set n := {2 4}(_ + b)
rewrite [e in X in pat1]lem1
Like before, but override the pattern inferred from lem1 Put in the context a local definition named n for the second
with e and fourth occurrences of the sub terms selected by the
pattern (_ + b)
rewrite [e as X in pat1]lem1
n := a + b
=========
Like rewrite [X in pat1]lem1 but match pat1[X := e] in- =========
(a + b) + (a + b) = →
stead of just pat1 (a + b) + n =
(a + b) + (0 + a + b)
(a + b) + n
Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . 191
Concepts
abbreviation, 37 identity, 45
Abstracting variables, 34 implicit argument, 29
abstraction, 14 improving by [], 58
induction, 62
binder, 14, 19 curse of values, 88
generalizing, 64
case analysis, 48
strong, 88
naming, 50
inductive type, 20
coercion, 110
constructor, 20
computation, 16, 24, 47
symbolic, 34 keyed matching, 67
consistency, 87
convertibility, 77 list comprehension, 31
currying of functions, 16
machine checked proof, 48
dependent function space, 77 matching algorithm, 66
dependent type, 74, 76
natural number, 21
equality, 43, 81 notation, 37
formal proof, 47 notation scope, 32
forward reasoning, 103, 104
partial application, 17
function application, 14
pattern, 53
functional extensionality, 146
pattern matching, 23
general term, see also higher-order, 62 exhaustiveness, 23
goal stack model, 82 irrefutable, 33
ground equality, 43 polymorphism, 28
positivity, 88
higher-order, 17, 62 proof irrelevance, 141, 143
proposition, 43 section, 33
provide choiceType structure, 167 simplifying equation, 108
provide eqType structure, 167 symmetric argument, 104
provide finType structure, 167
terminating tactic, 48
record, 32 termination, 25, 87
recursion, 24, 30 type, 15
termination, 25 type error, 16
reflection view, 94 typing an application, 17
reordering goals, 51
unfolding equation, 108
rewrite rule, 54
rewriting, 53 view, 83
[Asp+12] Andrea Asperti et al. “A Bi-Directional Refinement Algorithm for the Calculus
of (Co)Inductive Constructions”. In: Logical Methods in Computer Science
8.1 (2012). doi: 10.2168/LMCS-8(1:18)2012. url: http://dx.doi.org/10.
2168/LMCS-8(1:18)2012 (cited on page 118).
[BG01] Henk Barendregt and Herman Geuvers. “Proof Assistants using Dependent
Type Systems”. In: Handbook of Automated Reasoning. Edited by A. Robinson
and A. Voronkov. Volume 2. Elsevier, 2001. Chapter 18, pages 1149–1238
(cited on page 73).
[BC04] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program
Development. Coq’Art: The Calculus of Inductive Constructions. Springer,
2004 (cited on pages 3, 25).
[Bou04] Nicolas Bourbaki. Theory of sets. Elements of Mathematics (Berlin). Reprint
of the 1968 English translation [Hermann, Paris; MR0237342]. Springer-Verlag,
Berlin, 2004, pages viii+414. isbn: 3-540-22525-0. doi: 10.1007/978-3-642-
59309-3. url: http://dx.doi.org/10.1007/978-3-642-59309-3 (cited
on page 73).
[Chl14] Adam Chlipala. Certified Programming with Dependent Types. The MIT Press,
2014. isbn: 9780262026659 (cited on pages 3, 142).
[Coh12] Cyril Cohen. “Construction of Real Algebraic Numbers in Coq”. In: Interactive
Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ,
USA, August 13-15, 2012. Proceedings. 2012, pages 67–82. doi: 10.1007/978-
3-642-32347-8_6. url: http://dx.doi.org/10.1007/978-3-642-32347-
8_6 (cited on page 91).
[Coh+15] Cyril Cohen et al. Cubical Type Theory: a constructive interpretation of the
univalence axiom. Preprint. 2015 (cited on page 146).
[Coq] Coqdev - The Coq development team. The Coq proof assistant reference
manual. Inria. url: http://coq.inria.fr (cited on pages 3, 16, 25, 32, 34,
35, 37, 61, 73, 77, 88, 96, 117, 143).
[CH88] Thierry Coquand and Gérard Huet. “The calculus of constructions”. In: Infor-
mation and Computation 76.2-3 (1988), pages 95–120. issn: 0890-5401 (cited
on page 73).
[CP90] Thierry Coquand and Christine Paulin-Mohring. “Inductively defined types”.
In: Colog’88. Volume 417. LNCS. Springer-Verlag, 1990 (cited on pages 73,
77).
[Gar+09] François Garillot et al. “Packaging Mathematical Structures”. In: Theorem
Proving in Higher Order Logics. Edited by Tobias Nipkow and Christian
Urban. Volume 5674. Lecture Notes in Computer Science. Munich, Germany:
Springer, 2009. url: https://hal.inria.fr/inria- 00368403 (cited on
page 153).
[Gon08] Georges Gonthier. “Formal Proof – The Four-Color Theorem”. In: Notices
of the American Mathematical Society 55.11 (Dec. 2008), pages 1382–1393.
url: http://www.ams.org/notices/200811/tx081101382p.pdf (cited on
page 3).
[GMT15] Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection
Extension for the Coq system. Research Report RR-6455. Inria Saclay Ile
de France, 2015. url: https://hal.inria.fr/inria-00258384 (cited on
pages 3, 52, 55, 64, 66, 85, 90, 102, 109).
[Gon+13a] Georges Gonthier et al. “A Machine-Checked Proof of the Odd Order Theorem”.
In: ITP 2013, 4th Conference on Interactive Theorem Proving. Edited by
Sandrine Blazy, Christine Paulin, and David Pichardie. Volume 7998. LNCS.
Rennes, France: Springer, July 2013, pages 163–179. doi: 10.1007/978-3-
642-39634-2\_14. url: https://hal.inria.fr/hal-00816699 (cited on
page 3).
[Gon+13b] Georges Gonthier et al. “How to make ad hoc proof automation less ad
hoc”. In: J. Funct. Program. 23.4 (2013), pages 357–401. doi: 10 . 1017 /
S0956796813000051. url: http://dx.doi.org/10.1017/S0956796813000051
(cited on page 118).
[Hed98] Michael Hedberg. “A Coherence Theorem for Martin-Löf’s Type Theory”.
In: J. Funct. Program. 8.4 (July 1998), pages 413–436. issn: 0956-7968.
doi: 10.1017/S0956796898003153. url: http://dx.doi.org/10.1017/
S0956796898003153 (cited on page 143).
[MT13] Assia Mahboubi and Enrico Tassi. “Canonical Structures for the working Coq
user”. In: ITP 2013, 4th Conference on Interactive Theorem Proving. Edited
by Sandrine Blazy, Christine Paulin, and David Pichardie. Volume 7998.
LNCS. Rennes, France: Springer, July 2013, pages 19–34. doi: 10.1007/978-
3-642-39634-2\_5. url: https://hal.inria.fr/hal-00816703 (cited on
pages 164, 167).
[NG14] Rob Nederpelt and Herman Geuvers. Type theory and formal proof. An intro-
duction, With a foreword by Henk Barendregt. Cambridge University Press,
Cambridge, 2014, pages xxv+436. isbn: 978-1-107-03650-5. doi: 10.1017/
CBO9781139567725. url: http://dx.doi.org/10.1017/CBO9781139567725
(cited on page 73).
[NGV94] Rob Nederpelt, Herman Geuvers, and Roel de Vrijer, editors. Selected Pa-
pers on Automath. Volume 133. Studies in Logic and the Foundations of
Mathematics. North-Holland, 1994 (cited on page 81).
[Pau93] Christine Paulin-Mohring. “Inductive Definitions in the System Coq - Rules
and Properties”. In: Proceedings of the conference Typed Lambda Calculi
and Applications. Edited by M. Bezem and J.-F. Groote. Lecture Notes in
Computer Science 664. LIP research report 92-49. 1993 (cited on page 77).
[Pau15] Christine Paulin-Mohring. “Introduction to the Calculus of Inductive Construc-
tions”. In: All about Proofs, Proofs for All. Edited by Bruno Woltzenlogel Paleo
and David Delahaye. Volume 55. Studies in Logic (Mathematical logic and foun-
dations). College Publications, Jan. 2015. url: https://hal.inria.fr/hal-
01094195 (cited on page 3).
[Pie+15] Benjamin C. Pierce et al. Software Foundations. Electronic textbook, 2015
(cited on page 3).
[Pol92] Robert Pollack. “Implicit Syntax”. In: Informal Proceedings of First Workshop
on Logical Frameworks. 1992, pages (cited on page 115).
[SZ14] Matthieu Sozeau and Beta Ziliani. “Towards A Better Behaved Unification
Algorithm for Coq”. In: Proceedings of The 28th International Workshop on
Unification. 2014. url: http://www.pps.univ-paris-diderot.fr/~sozeau/
research / publications / Towards _ A _ Better _ Behaved _ Unification _
Algorithm_for_Coq-UNIF14-130714.pdf (cited on page 118).
[Uni13] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foun-
dations of Mathematics. Institute for Advanced Study: https://homotopytypetheory.
org/book, 2013 (cited on pages 3, 73, 81).