Programs and Proofs: Ilya Sergey
Programs and Proofs: Ilya Sergey
Programs and Proofs: Ilya Sergey
Lecture Notes
Ilya Sergey
1 Introduction 5
1.1 Why yet another course on Coq? . . . . . . . . . . . . . . . . . . . . . . 5
1.1.1 What this course is about . . . . . . . . . . . . . . . . . . . . . . 7
1.1.2 What this course is not about . . . . . . . . . . . . . . . . . . . . 7
1.1.3 Why Ssreflect? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2 Prerequisites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.3 Setup . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.3.1 Installing Coq, Ssreflect and Mathematical Components . . . . . . 9
1.3.2 Emacs set-up . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.3.3 Getting the lecture files and solutions . . . . . . . . . . . . . . . . 10
1.4 Naming conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.5 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3 Propositional Logic 29
3.1 Propositions and the Prop sort . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 The truth and the falsehood in Coq . . . . . . . . . . . . . . . . . . . . . 30
3.3 Implication and universal quantification . . . . . . . . . . . . . . . . . . . 35
3.3.1 On forward and backward reasoning . . . . . . . . . . . . . . . . 37
3.3.2 Refining and bookkeeping assumptions . . . . . . . . . . . . . . . 38
3.4 Conjunction and disjunction . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.5 Proofs with negation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.6 Existential quantification . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.6.1 A conjunction and disjunction analogy . . . . . . . . . . . . . . . 45
3.7 Missing axioms from classical logic . . . . . . . . . . . . . . . . . . . . . 46
3.8 Universes and Prop impredicativity . . . . . . . . . . . . . . . . . . . . . 47
3.8.1 Exploring and debugging the universe hierarchy . . . . . . . . . . 48
2 Contents
9 Conclusion 143
Bibliography 145
Index 151
1 Introduction
These lecture notes are the result of the author’s personal experience of learning how to
structure formal reasoning using the Coq proof assistant and employ Coq in large-scale
research projects. The present manuscript offers a brief and practically-oriented intro-
duction to the basic concepts of mechanized reasoning and interactive theorem proving.
The primary audience of this text are the readers with expertise in software develop-
ment and programming and knowledge of discrete mathematic disciplines on the level
of an undergraduate university program. The high-level goal of the course is, therefore,
to demonstrate how much the rigorous mathematical reasoning and development of ro-
bust and intellectually manageable programs have in common, and how understanding of
common programming language concepts provides a solid background for building math-
ematical abstractions and proving theorems formally. The low-level goal of this course
is to provide an overview of the Coq proof assistant, taken in its both incarnations: as
an expressive functional programming language with dependent types and as a proof
assistant providing support for mechanized interactive theorem proving.
By aiming for these two goals, this manuscript is, thus, intended to provide a demon-
stration how the concepts familiar from the mainstream programming languages and
serving as parts of good programming practices can provide illuminating insights about
the nature of reasoning in Coq’s logical foundations and make it possible to reduce the
burden of mechanical theorem proving. These insights will eventually give the reader
a freedom to focus solely on the essential part of her formal development instead of
fighting with a proof assistant in futile attempts to encode the “obvious” mathematical
intuition—a reason that made many of the new-comers abandon their attempts to apply
the machine-assisted approach for formal reasoning as an everyday practice.
• The classical book Interactive Theorem Proving and Program Development. Coq’Art:
The Calculus of Inductive Constructions by Yves Bertot and Pierre Castéran [3] is
a great and exhaustive overview of Coq as a formal system and a tool, covering
both logical foundations, reasoning methodologies, automation tools and offering
large number of examples and exercises (from which this course borrows some).
6 1 Introduction
• Benjamin Pierce et al.’s Software Foundations electronic book [53] introduces Coq
development from an angle of the basic research in programming languages, focusing
primarily on formalization of program language semantics and type systems, which
serve both as main motivating examples of Coq usage and a source of intuition for
explaining Coq’s logical foundations.
• The most recently published book, Certified Programming with Dependent Types
by Adam Chlipala [7] provides a gentle introduction to Coq from the perspective of
writing programs that manipulate certificates, i.e., first-class proofs of the program’s
correctness. The idea of certified programming is a natural fit for a programming
language with dependent types, which Coq offers, and the book is structured as
a series of examples that make the dependently-typed aspect of Coq shine, along
with the intuition behind these examples and a detailed overview of state-of-the-art
proof automation techniques.
Although all the three books have been used in numerous introductory courses for Coq
with a large success, it is the author’s opinion that there are still some topics essential
for grasping the intuition behind rigorous and boilerplate-free mathematical reasoning
via a proof assistant that are left underrepresented. This course is targeted to fill these
gaps, while giving the reader enough background to proceed as a Coq hacker on her own.
In particular, this manuscript describes in detail the following aspects of proof engineer-
ing, most of which are enabled or empowered by Gonthier et al.’s small-scale reflection
extension (Ssreflect) to Coq [23] and its accompanying library called Mathematical Com-
ponents:
• Special treatment is given to the computational nature of inductive reasoning about
decidable propositions, which makes it possible to compute a result of the vast
majority of them (as opposed to prove them constructively) as a boolean value,
given that they are formulated as computable recursive Coq functions, rather than
inductive predicates (which is more in the spirit of the traditional Coq school).
• Instead of supplying the reader with a large vocabulary of tactics necessary for
everyday Coq hacking, this course focuses on a very small but expressive set of
proof constructing primitives (of about a seven in total), offered by Ssreflect or
inherited from the vanilla Coq with notable enhancements.
• This course advocates inductive types’ parameters as an alternative to indices as a
way of reasoning about explicit equalities in datatypes with constraints.
• The reasoning by rewriting is first presented from the perspective of Coq’s definition
of propositional equality and followed by elaboration on the idea of using datatype
indices as a tool to define client-specific conditional rewriting rules.
• This manuscript explains the essentials of Ssreflect’s boolean reflection between the
sort Prop and the datatype bool as a particular case of conditional rewriting, follow-
ing the spirit of the computational approach to the proofs of decidable propositions.
• Formal encoding of familiar mathematical structures (e.g., monoids and lattices)
is presented by means of Coq’s dependent records and overloading mathematical
operations using the mechanism of canonical instances.
1.1 Why yet another course on Coq? 7
• Reasoning about infinite objects in Coq via co-induction (see Chapters 5 and 7 of
the book [7] as well as the research papers [32, 34]).
• Proof automation by means of tactic engineering (see [7, Chapters 13–15] and the
papers [61, 62, 70]) or lemma overloading [25].
• Using a proof assistant in the verification of program calculi [2, 53] and optimizing
compilers [1] as well as employing Coq to specify and verify low-level and concurrent
programs [5, 8, 17, 44].
developments, in particular, the fully formal machine-checked proofs of the four color
theorem [22] and Feit-Thompson (odd order) theorem [24].
Ssreflect includes a small set of powerful novel primitives for interactive proof con-
struction (tactics), different from the traditional set provided by Coq. It also comes with
a large library of various algebraic structures, ranging from natural numbers to graphs,
finite sets and algebras, formalized and shipped with exhaustive toolkits of lemmas and
facts about them. Finally, Ssreflect introduces some mild modifications to Coq’s native
syntax and the semantics of the proof script interpreter, which makes the produced proofs
significantly more concise.
Using Ssreflect for the current development is not the goal by itself: a large part of
the manuscript could be presented using traditional Coq without any loss in the insights
but, perhaps, some loss in brevity. However, what is more important, using Ssreflect’s
libraries and tactics makes it much easier to stress the main points of this course, namely,
that (a) the proof construction process should rely on Coq’s native computational ma-
chinery as much as possible and (b) rewriting (in particular, by equality) is one of the
most important proof techniques, which should be mastered and leveraged in the proofs.
Luckily, the way most of the lemmas in Ssreflect and Mathematical Components libraries
are implemented makes them immediately suitable to use for rewritings, which directly
follows the natural mathematical intuition. The enhancements Ssreflect brings over the
standard Coq rewriting machinery also come in handy.
Last, but not least, Ssreflect comes with a much improved Search tool (comparing to
the standard one of Coq). Given that a fair part of time spent for development (either
programs and proofs) is typically dedicated to reading and understanding the code (or,
at least, specifications) written by other implementors, the Search tool turns out to be
invaluable when it comes to looking for necessary third-party facts to employ in one’s
own implementation.
In the further chapters of this course, we will not be making distinction between native
Coq and Ssreflect-introduced commands, tactics and tacticals, and will keep the combined
lists of them in the Index section at the end of the manuscript.
1.2 Prerequisites
The reader is expected to have some experience with mainstream object-oriented and
functional programming languages, such as Scala [46], Haskell [31], OCaml [35] or Stan-
dard ML [39]. While strong knowledge of any of the mentioned languages is not manda-
tory, it might be useful, as many of the Coq’s concepts making appearance in the course
are explained using the analogies with constructs adopted in practical programming, such
as algebraic datatypes, higher-order functions, records and monads.
While this manuscript is aiming to be self-contained in its presentation of a subset
of Coq, it would be naïve to expect it to be the only Coq reference used for setting-up
a formal development. That said, we encourage the reader to use the standard Coq
manual [10] as well as Ssreflect documentation [23] whenever an unknown tactic, piece
of syntax or obscure notation is encountered. Coq’s Search, Locate and Print tools,
explained in Chapter 2 are usually of great help when it comes to investigating what
someone’s Coq code does, so don’t hesitate to use them.
1.3 Setup 9
Finally, we assume that the Emacs text editor with a Proof General mode installed
(as explained further in this chapter) will be used as the environment for writing code
scripts, and the GNU make machinery is available on the reader’s machine in order to
build the necessary libraries and tools.
1.3 Setup
In order to be able to follow the manuscript and execute the examples provided, the
reader is expected to have Coq with Ssreflect installed on her machine. This section
contains some general instructions on the installation and set-up. Most of the mentioned
below sources can be downloaded from the following URL, accompanying these notes:
http://ilyasergey.net/pnp
Alternatively, you can clone the sources of these lecture notes, along with the exercises
and the solution from the following public GitHub repository:
https://github.com/ilyasergey/pnp
(cua-mode t)
(setq cua-auto-tabify-rectangles nil)
(transient-mark-mode 1)
(setq cua-keep-region-after-copy t)
Every Coq file has the extension .v. Opening any .v file will automatically trigger the
Proof General mode.
Finally, the optional Company-Coq5 collection of extensions to Proof General adds
many modern IDE features such as auto-completion of tactics and names, refactoring,
and inline help.
1.5 Acknowledgements
This course was inspired by the fantastic experience of working with Aleks Nanevski on
verification of imperative and concurrent programs during the author’s stay at IMDEA
Software Institute. Aleks’ inimitable sense of beauty when it comes to formal proofs has
been one of the main principles guiding the design of these lecture notes.
I’m grateful to Michael D. Adams, Amal Ahmed, Jim Apple, Daniil Berezun, Gio-
vanni Bernardi, Dmitri Boulytchev, William J. Bowman, Kirill Bryantsev, Santiago Cuel-
lar, Andrea Cerone, Olivier Danvy, Rémy Haemmerle, Wojciech Karpiel, José Francisco
Morales, Phillip Mates, Gleb Mazovetskiy, Anton V. Nikishaev, Karl Palmskog, Daniel
Patterson, Anton Podkopaev, Leonid Shalupov, Kartik Singhal, Jan Stolarek, Anton
Trunov and James R. Wilcox who provided a lot of valuable feedback and found count-
less typos in earlier versions of the notes.
The mascot picture Le Coq Mécanisé on the front page is created by Lilia Anisimova.
2 Functional Programming in Coq
Our journey to the land of mechanized reasoning and interactive theorem proving starts
from observing the capabilities of Coq as a programming language.
Coq’s programming component is often described as a functional programming lan-
guage, since its programs are always pure (i.e., not producing any sort of side effects),
possibly higher-order functions, which means that they might take other functions as
parameters and return functions as results. Similarly to other functional programming
languages, such as Haskell, OCaml or Scala, Coq makes heavy use of algebraic datatypes,
represented by a number of possibly recursive constructors. Very soon, we will see how
programming with inductive algebraic datatypes incorporates reasoning about them, but
for now let us take a short tour of Coq’s syntax and define a number of simple programs.
tt
: unit
Moreover, we can make sure that the unit datatype itself defines a set:
Check unit.
unit
: Set
In fact, since Coq makes the analogy between sets and types so transparent, it is not
difficult to define a type describing the empty set:
1
Use the Ctrl-C Ctrl-Enter keyboard shortcut to initiate the interactive programming/proof mode
in Proof General and gradually compile the file.
14 2 Functional Programming in Coq
That is, the empty set is precisely described by the type, values of which we simply
cannot construct, as the type itself does not provide any constructors! In fact, this
observation about inhabitance of types/sets and the definition of an empty type will
come in quite handy very soon when we will be talking about the truth and falsehood
in the setting of the Curry-Howard correspondence in Chapter 3. Unfortunately, at this
moment there is not so much we can do with such simple types as unit or empty, so we
proceed by defining some more interesting datatypes.
The type bool is familiar to every programmer. In Coq, it is unsurprisingly defined
by providing exactly two constructors: true and false. Since bool is already provided by
the standard Coq library, we do not need to define it ourselves. Instead, we include the
following modules into our file using the From ... Require Import command:2
From mathcomp
Require Import ssreflect ssrbool.
Now, we can inspect the definition of the bool type by simply printing it:
Print bool.
Let us now try to define some functions that operate with the bool datatype ignoring
for a moment the fact that most of them, if not all, are already defined in the standard
Coq/Ssreflect library. Our first function will simply negate the boolean value and return
its opposite:
Definition negate b :=
match b with
| true ⇒ false
| false ⇒ true
end.
The syntax of Coq as programming language is very similar to Standard ML. The
keyword Definition is used to define non-recursive values, including functions. In the
example above, we defined a function with one argument b, which is being scrutinized
against two possible value patterns (true and false), respectively, and the corresponding
results are returned. Notice that, thanks to its very powerful type inference algorithm,
Coq didn’t require us to annotate neither the argument b with its type, nor the function
itself with its result type: these types were soundly inferred, which might be confirmed
by checking the overall type of negate, stating that it is a function from bool to bool:
Check negate.
negate : bool → bool
2
The From ... premise is optional, and in this particular case it allows to include libraries from mathcomp
without additional qualifiers.
2.2 Simple recursive datatypes and programs 15
3
It is important to bear in mind that .+1 is not just a function for incrementation, but also is a datatype
constructor, allowing one to obtain the Peano successor of a number n by taking n.+1.
16 2 Functional Programming in Coq
The type of nat rec requires a bit of explanation. It is polymorphic in the sense of
Haskell and OCaml (i.e., it is parametrized over another type). More precisely, its first
parameter, bound by the ∀ quantifier is a function, which maps natural numbers to types
(hence the type of this parameter is nat → Set). The second parameter is a result of
type described by application of the function P to zero. The third parameter is a family
of functions, indexed by a natural number n. Each function from such a family takes
an argument of type P n and returns a result of type P n.+1. The default recursion
principle for natural numbers is therefore a higher-order function (i.e., a combinator).
If the three discussed arguments are provided, the result of nat rec will be a function,
mapping a natural number n to a value of type P n.
To see how nat rec is implemented, let us explore its generalized version, nat rect:
Print nat rect.
nat rect =
fun (P : nat → Type) (f : P 0) (f0 : ∀ n : nat, P n → P n.+1) ⇒
fix F (n : nat) : P n :=
match n as n0 return (P n0 ) with
|0⇒f
| n0.+1 ⇒ f0 n0 (F n0 )
end
: ∀ P : nat → Type,
P 0 → (∀ n : nat, P n → P n.+1) → ∀ n : nat, P n
Abstracting away from the details, we can see that nat rect is indeed a function with
three parameters (the keyword fun is similar to the lambda notation and is common in
the family of ML-like languages). The body of nat rect is implemented as a recursive
function (defined via the keyword fix) taking an argument n of type nat. Internally, it
proceeds similarly to our implementation of my plus: if the argument n is zero, then the
“default” value f of type P 0 is returned. Otherwise, the function proceeds recursively
with a smaller argument n0 by applying the “step” function f0 to the n0 and the result
of recursive call F n0.
Therefore, the summing function can be implemented via the nat’s recursion combi-
nator as follows:
Definition my plus’’ n m := nat rec (fun ⇒ nat) m (fun n’ m’ ⇒ m’.+1) n.
Eval compute in my plus’’ 16 12.
= 28 : (fun : nat ⇒ nat) 16
The result of invoking my plus’’ is expectable. Notice, however, that when defining it
we didn’t have to use the keyword Fixpoint (or, equivalently, fix), since all recursion
has been “sealed” within the definition of the combinator nat rect.
= 15
: (fun n : nat ⇒ match n with
| 0 ⇒ unit
| .+1 ⇒ nat
end) 5
The toy function sum no zero maps every natural number n to a sum of numbers 1
... n, except for 0, which is being mapped into the value tt of type unit. We define it
via the nat rec combinator by providing it a function P, which defines the type contract
described just above. Importantly, as the first parameter to nat rec, we pass a type-
level function P, which maps 0 to the unit type and all other values to the type nat.
The “step” function, which is a third parameter, of this nat rec call, makes use of the
dependent pattern matching, which now explicitly refines the return type P n’ → of
the whole match e with ps end expression. This small addition allows the Coq type
checker to relate the expected type of my plus’ first argument in the second branch to
the type of the pattern matching scrutinee n’. Without the explicit return in the pattern
matching, in some cases when its result type depends on the value of the scrutinee, the
Coq type checking engine will fail to unify the type of the branch and the overall type. In
particular, had we omitted the return clauses in the pattern matching, we would get the
following type-checking error, indicating that Coq cannot infer that the type of my plus’
argument is always nat, so it complains:
Error:
In environment
20 2 Functional Programming in Coq
n : ?37
P := fun n : nat ⇒ match n with
| 0 ⇒ unit
| .+1 ⇒ nat
end : nat → Set
n’ : nat
m : P n’
The term "m" has type "P n’" while it is expected to have type "nat".
In general, dependent pattern matching is a quite powerful tool, which, however, should
be used with a great caution, as it makes assisting the Coq type checker a rather non-
trivial task. In the vast majority of the cases dependent pattern matching can be avoided.
We address the curious reader to the Chapter 8 of the book [7] for more examples on the
subject.
Dependent function types, akin to those of nat rec and our sum no zero, which allow
the type of the result to vary depending on the value of a function’s argument, are
a powerful way to specify the behaviour of functions, and therefore, are often used to
“enforce” the dependently-typed programs to work in a particular expected way. In
Coq, dependent function types are omnipresent, and are syntactically specified using
the ∀-binder, similarly to the way parametric types are specified in Haskell or typed
calculi like polymorphic lambda calculus (also known as System F [21, 56]).9 The crucial
difference between Coq’s core calculus and System F is that in Coq the types can be
parametrised not just by types but also by values. While the utility of this language
“feature” can be already demonstrated for constructing and type-checking programs (for
example, sum no zero), its true strength is best demonstrated when using Coq as a
system to construct proofs, which is the topic of the subsequent chapters.
empty rect
: ∀ (P : empty → Type) (e : empty), P e
Very curiously, the type signature of empty rect postulates that it is sufficient to provide
a function from empty to any type (which can very well be just a constant type, e.g.,
nat), and an argument e of type empty, so the result of the call to empty rect will be of
type P e. More concisely, empty rect allows us to produce a result of any type, given that
9
Although, generally speaking, Coq abuses the ∀-notation using it for what is denoted in other typed
calculi by means of quantifiers Λ (terms parametrized by types), ∀ (types parametrized by types) and
Π (types parametrized by terms) [52].
2.3 More datatypes 21
we can provide an argument of type empty. While it might sound very surprising at the
first moment, upon some reflection it seems like a perfectly valid principle, since we will
never be able to construct the required value of type empty in the first place. In more
fancy words, such recursion principle can be reformulated as the following postulate:
This is a very important insight, which will become illuminating when we will be
discussing the reasoning with negation in the next chapter.
To conclude this section, we only mention that defining a datatype with no constructors
is not the only way to get a type, which is not inhabited. For example, the following
type strange [3] has a constructor, which, however, can never be invoked, as it requires
a value of it type itself in order to return a value:
Inductive strange : Set := cs : strange → strange.
Therefore, an attempt to create a value of type strange by invoking its single con-
structor will inevitably lead to an infinite, non-terminating, series of constructor calls,
and such programs cannot be encoded in Coq. It is interesting to take a look at the
recursion principle of strange:
Check strange rect.
strange rect
: ∀ P : strange → Type,
(∀ s : strange, P s → P (cs s)) → ∀ s : strange, P s
That is, if we pose the argument P to be a constant type function fun ⇒ empty,
and the second argument to be just an identity function (fun x ⇒ x) that maps its
second argument to itself, we will get a function that, upon receiving argument of type
strange will construct an argument of type empty! More precisely, the existence of a
value of type strange would allow us to create a value of type empty and, therefore
a value of any type, as was previously demonstrated. The following definition of the
function strange to empty substantiates this observation:
Definition strange to empty (s: strange): empty :=
strange rect (fun ⇒ empty) (fun e ⇒ e) s.
To summarize, designing a datatype, which is not inhabited, while not trivial, is not
impossible, and it is a task of a designer of a particular type to make sure that its values
in fact can be constructed.
OCaml, prod can also be seen as a type-level constructor with two parameters that can
be possibly curried:
Check prod.
fst : ∀ A B : Type, A × B → A
Check snd.
2.3 More datatypes 23
snd : ∀ A B : Type, A × B → B
Curiously, the notation “ × ” is not hard-coded into Coq, but rather is defined as
a lightweight syntactic sugar on top of standard Coq syntax. Very soon we will see how
one can easily extend Coq’s syntax by defining their own notations. We will also see how
is it possible to find what a particular notation means.
The arsenal of a functional programmer in Coq would be incomplete without proper
sum and list datatypes:10
Print sum.
= [:: 1; 4; 2; 5; 3; 6]
: seq nat
Eval compute in alternate [:: 1] [:: 4;5;6].
= [:: 1; 4; 5; 6]
: seq nat
Eval compute in alternate [:: 1;2;3] [:: 4].
= [:: 1; 4; 2; 3]
: seq nat
Hint: The reason why the “obvious” elegant solution might fail is that the argument is
not strictly decreasing.
10
In Ssreflect’s enhanced library lists are paraphrased as the seq datatype, which is imported from the
module seq.
24 2 Functional Programming in Coq
by defining completely intractable abbreviations, which might say a lot to the library
developer, but not to its client. Coq provides the Locate command to help in demystifying
notations as well as locating the position of particular definitions. For example, the
following query will show all the definitions of the notation “ + ” as well as the scopes
they defined in.
Locate " + ".
Notation Scope
"x + y" := sum x y : type scope
Constant Coq.Lists.List.map
(shorter name to refer to it in current context is List.map)
Constant Ssreflect.ssrfun.Option.map
(shorter name to refer to it in current context is ssrfun.Option.map)
...
Error: The term "1" has type "nat" while it is expected to have type "Type".
11
The module system of Coq is similar to OCaml and will be discussed further in this chapter.
26 2 Functional Programming in Coq
The error message is caused by the fact that the constructor has expected the type
parameters to be provided explicitly first, so the value above should in fact have been
created by calling my pair nat unit 1 tt. Since mentioning types every time is tedious, we
can now take advantage of Coq’s elaboration algorithm, which is capable to infer them
from the values of actual arguments (e.g., 1 and tt), and declare my pair’s type arguments
as implicit:
Arguments my pair [A B].
We have already witnessed standard Coq’s datatypes making use of specific user-defined
notations. Let us define such notation for the type my prod and its my pair constructor.
Notation "X ** Y" := (my prod X Y ) (at level 2).
Notation "( X „ Y )" := (my pair X Y ).
The level part in the first notation definition is mandatory for potentially left-recursive
notations, which is the case here, in order to set up parsing priorities with respect to other
notations.
With these freshly defined notations we are now free to write the following expressions:
Check (1 „ 3).
(1„ 3)
: nat ** nat
Check nat ** unit ** nat.
my mult =
fun n : nat ⇒
fix my mult (m : nat) : nat :=
let (n0, y) := (n, m) in
match n0 with
|0⇒0
| .+1 ⇒ match y with
|0⇒0
| m’.+1 ⇒ my plus (my mult m’) n
end
end
: nat → nat → nat
We can see now that the variable n became an actual parameter of my mult, so the
function now takes two parameters, just as expected.
An alternative to sections in Coq, which provides better encapsulation, are modules.
A module, similarly to a section, can contain locally-declared variables, sections and
modules (but not modules within sections!). However, the internals of a module are not
implicitly exposed to the outside, instead they should be either referred to by qualified
names or exported explicitly by means of putting them into a submodule and via the
command Export, just as demonstrated below:
Module NatUtilModule.
Fixpoint my fact n :=
if n is n’.+1 then my mult n (my fact n’) else 1.
Module Exports.
Definition fact := my fact.
End Exports.
28 2 Functional Programming in Coq
End NatUtilModule.
The submodule Exports creates a synonym fact for the function my fact, defined out-
side of it. The following command explicitly exports all internals of the module NatU-
tilModule.Exports, therefore making fact visible outside of NatUtilModule.
Export NatUtilModule.Exports.
Check my fact.
Error: The reference my fact was not found in the current environment.
Check fact.
fact
: nat → nat
3 Propositional Logic
In the previous chapter we had an opportunity to explore Coq as a functional program-
ming language and learn how to define inductive datatypes and programs that operate
with them, implementing the latter ones directly or using the automatically-generated
recursion combinators. Importantly, most of the values that we met until this moment,
inhabited the types, which were defined as elements of the sort Set. The types unit,
empty, nat, nat × unit etc. are good examples of first-order types inhabiting the sort
Set and, therefore, contributing to the analogy between sets and first-order types, which
we explored previously. In this chapter, we will be working with a new kind of entities,
incorporated by Coq: propositions.
Only those propositions are considered to be true, which are provable constructively,
i.e., by providing an explicit proof term, that inhabits them.
by checking the corresponding truth tables), it does not quite scale when it comes to
the higher-order propositions (i.e., quantifying over predicates) as well as of propositions
quantifying over elements of arbitrary domains. For instance, the following proposition,
in which the reader can recognize the induction principle over natural numbers, can-
not be formulated in the zeroth- or first-order propositional logic (and, in fact, in any
propositional logic):
For any predicate P , if P (0) holds, and for any m, P (m) implies P (m + 1),
then for any n, P (n) holds.
mere truth or falsehood are implemented. From now on, we will be always including to
the development the standard Ssreflect’s module ssreflect, which imports some necessary
machinery for dealing with propositions and proofs.
From mathcomp Require Import ssreflect.
The truth is represented in Coq as a datatype of sort Prop with just one constructor,
taking no arguments:
Print True.
============================
True
The command Theorem serves two purposes. First, similarly to the command Definition,
it defines a named entity, which is not necessarily a proposition. In this case the name is
true is true. Next, similarly to Definition, there might follow a list of parameters, which
is empty in this example. Finally, after the colon : there is a type of the defined value,
which in this case it True. With this respect there is no difference between Theorem and
Definition. However, unlike Definition, Theorem doesn’t require one to provide the
expression of the corresponding type right away. Instead, the interactive proof mode is
activated, so the proof term could be constructed incrementally. The process of the grad-
ual proof construction is what makes Coq to be a interactive proof assistant, in addition
to being already a programming language with dependent types.
Although not necessary, it is considered a good programming practice in Coq to start
any interactive proof with the Coq’s command Proof, which makes the final scripts easier
to read and improves the general proof layout.
Proof.
In the interactive proof mode, the goals display shows a goal of the proof—the type
of the value to be constructed (True in this case), which is located below the double
line. Above the line one can usually see the context of assumptions, which can be used
in the process of constructing the proof. Currently, the assumption context is empty, as
the theorem we stated does not make any and ventures to prove True out of thin air.
Fortunately, this is quite easy to do, as from the formulation of the True type we already
know that it is inhabited by its only constructor I. The next line proved the exact value
of the type of the goal.
3
In the context of propositional logic, we will be using the words “type” and “proposition” interchange-
ably without additional specification when it’s clear from the context.
32 3 Propositional Logic
exact: I.
This completes the proof, as indicated by the Proof General’s *response* display:
No more subgoals.
(dependent evars:)
The only thing left to complete the proof is to inform Coq that now the theorem
true is true is proved, which is achieved by typing the command Qed.
Qed.
In fact, typing Qed invokes a series of additional checks, which ensure the well-formedness
of the constructed proof term. Although the proof of true is true is obviously valid, in
general, there is a number of proof term properties to be checked a posteriori and par-
ticularly essential in the case of proofs about infinite objects, which we do not cover in
these course (see Chapter 13 of [3] for a detailed discussion on such proofs).
So, our first theorem is proved. As it was hinted previously, it could have been stated
even more concisely, formulated as a mere definition, and proved by means of providing
a corresponding value, without the need to enter the proof mode:
Definition true is true’: True := I.
Although this is a valid way to prove statements in Coq, it is not as convenient as
the interactive proof mode, when it comes to construction of large proofs, arising from
complicated statements. This is why, when it comes to proving propositions, we will
prefer the interactive proof mode to the “vanilla” program definition. It is worth noticing,
though, that even though the process of proof construction in Coq usually looks more
like writing a script, consisting from a number of commands (which are called tactics in
Coq jargon), the result of such script, given that it eliminates all of the goals, is a valid
well-typed Coq program. In comparison, in some other dependently-typed frameworks
(e.g., in Agda), the construction of proof terms does not obscure the fact that what is
being constructed is a program, so the resulting interactive proof process is formulated as
“filling the holes” in a program (i.e., a proof-term), which is being gradually refined. We
step away from the discussion on which of these two views to the proof term construction
is more appropriate.
There is one more important difference between values defined as Definitions and
Theorems. While both define what in fact is a proof terms for the declared type, the
value bound by Definition is transparent: it can be executed by means of unfolding and
subsequent evaluation of its body. In contrast, a proof term bound by means of Theorem
is opaque, which means that its body cannot be evaluated and serves only one purpose:
establish the fact that the corresponding type (the theorem’s statement) is inhabited,
and, therefore is true. This distinction between definitions and theorems arises from the
notion of proof irrelevance, which, informally, states that (ideally) one shouldn’t be able
to distinguish between two proofs of the same statement as long as they both are valid.4
Conversely, the programs (that is, what is created using the Definition command) are
typically of interest by themselves, not only because of the type they return.
The difference between the two definitions of the truth’s validity, which we have just
constructed, can be demonstrated by means of the Eval command.
4
Although, in fact, proof terms in Coq can be very well distinguished.
3.2 The truth and the falsehood in Coq 33
False ind
: ∀ P : Prop, False → P
That is, any proposition can be derived from the falsehood by means of implication.6
For instance, we can prove now that False implies the equality 1 = 2.7
5
While we consider this to be a valid analogy to the mathematical community functions, it is only true
in spirit. In the real life, the statements proved once, are usually re-proved by students for didactical
reasons, in order to understand the proof principles and be able to produce other proofs. Furthermore,
the history of mathematics witnessed a number of proofs that have been later invalidated. Luckily,
the mechanically-checked proofs are usually not a subject of this problem.
6
In light of the Curry-Howard analogy, at this moment it shouldn’t come as a surprise that Coq uses
the arrow notation -> both for function types and for propositional implication: after all, they both
are just particular cases of functional abstraction, in sorts Set or Prop, correspondingly.
7
We postpone the definition of the equality till the next chapter, and for now let us consider it to be
just an arbitrary proposition.
34 3 Propositional Logic
Qed.
∀ P Q R: Prop, (P → Q) → (Q → R) → P → R
8
As it has been noticed in Chapter 2 the ∀-quantifier is Coq’s syntactic notation for dependent function
types, sometimes also referred to a Π-types or dependent product types.
9
Recall that the arrows have right associativity, just like function types in Haskell and OCaml, which
allows one to apply functions partially, specifying their arguments one by one
36 3 Propositional Logic
A : Prop
B : Prop
C : Prop
============================
(A → B) → (B → C ) → A → C
We can now move the three other arguments to the top using the same command: the
move⇒ combination works uniformly for ∀-bound variables as well as for the propositions
on the left of the arrow.
move⇒ H1 H2 a.
H1 : A → B
H2 : B → C
a: A
============================
C
Again, there are multiple ways to proceed now. For example, we can recall the func-
tional programming and get the result of type C just by two subsequent applications of
H1 and H2 to the value a of type A:
exact: (H2 (H1 a)).
Alternatively, we can replace the direct application of the hypotheses H1 and H2 by
the reversed sequence of calls to the apply: tactics.
Undo.
The first use of apply: will replace the goal C by the goal B, since this is what it takes
to get C by using H2 :
apply: H2.
H1 : A → B
a: A
============================
B
The second use of apply: reduces the proof of B to the proof of A, demanding an
appropriate argument for H1.
apply: H1.
a: A
============================
A
Notice that both calls to apply: removed the appropriate hypotheses, H1 and H2
from the assumption context. If one needs a hypothesis to stay in the context (to use
it twice, for example), then the occurrence of the tactic argument hypothesis should be
parenthesised: apply: (H1 ).
3.3 Implication and universal quantification 37
Finally, we can see that the only goal left to prove is to provide a proof term of type A.
Luckily, this is exactly what we have in the assumption by the name a, so the following
demonstration of the exact a finishes the proof:
exact: a.
Qed.
In the future, we will replace the use of trivial tactics, such as exact: by Ssreflect’s
much more powerful tactics done, which combines a number of standard Coq’s tactics in
an attempt to finish the proof of the current goal and reports an error if it fails to do so.
Exercise 3.1 (∀-distributivity). Formulate and prove the following theorem in Coq,
which states the distributivity of universal quantification with respect to implication:
Hint: Be careful with the scoping of universally-quantified variables and use parentheses
to resolve ambiguities!
imp trans =
fun (A B C : Prop) (H1 : A → B) (H2 : B → C ) (a : A) ⇒
(fun evar 0 : B ⇒ H2 evar 0 ) ((fun evar 0 : A ⇒ H1 evar 0 ) a)
: ∀ P Q R : Prop, (P → Q) → (Q → R) → P → R
• The backward proof style assumes that the goal is being gradually transformed by
means of applying some tactics, until its proof becomes trivial and can be completed
by means of basic tactics, like exact: or done.
• The forward proof style assumes that the human prover has some “foresight” with
respect to the goal she is going to prove, so she can define some “helper” entities as
38 3 Propositional Logic
well as to adapt the available assumptions, which will then be used to solve the goal.
Typical example of the forward proofs are the proofs from the classical mathematic
textbooks: first a number of “supporting” lemmas is formulated, proving some
partial results, and finally all these lemmas are applied in concert in order to prove
an important theorem.
While the standard Coq is very well supplied with a large number of tactics that support
reasoning in the backward style, it is less convenient for the forward-style reasoning.
This aspect of the tool is significantly enhanced by Ssreflect, which introduces a small
number of helping tactics, drastically simplifying the forward proofs, as we will see in the
subsequent chapters.
H1 : Q → R
H2 : P → Q
H : (P → Q) → (Q → R) → P → R
============================
P →R
What has happened now is a good example of the forward reasoning: the specialized
version of (imp trans P Q R), namely, (P → Q) → (Q → R) → P → R, has been moved
to the goal, so it became ((P → Q) → (Q → R) → P → R) → P → R. Immediately
after that, the top assumption (that is, what has been just “pushed” to the goal stack)
was moved to the top and given the name H. Now we have the assumption H that can
be applied in order to reduce the goal.
apply: H.
H1 : Q → R
3.4 Conjunction and disjunction 39
H2 : P → Q
============================
P →Q
Variables P Q R: Prop.
The propositional conjunction of P and Q, denoted by P ∧ Q, is a straightforward
Curry-Howard counterpart of the pair datatype that we have already seen in Chapter 2,
and is defined by means of the predicate and.
Locate " /\ ".
"A ∧ B" := and A B : type scope
Print and.
P : Prop
Q : Prop
R : Prop
x : P
42 3 Propositional Logic
============================
Q∨P
by right.
P : Prop
Q : Prop
R : Prop
x : Q
============================
Q∨P
In the second branch the type of x is Q, as it accounts for the case of the or intror
constructor.
by left.
Qed.
It is worth noticing that the definition of disjunction in Coq is constructive, whereas
the disjunction in classical propositional logic is not. More precisely, in classical logic
the proof of the proposition P ∨ ~P is true by the axiom of excluded middle (see Sec-
tion 3.7 for a more detailed discussion), whereas in Coq, proving P ∨ ~P would amount
to constructing the proof of either P or ~P. Let us illustrate it with a specific example.
If P is a proposition stating that P = NP, then in classical logic tautology P ∨ ~P holds,
although it does not contribute to the proof of either of the disjuncts. In constructive
logic, which Coq is an implementation of, in the trivial assumptions given the proof of P
∨ ~P, we would be able to extract the proof of either P or ~P.12
of Constructions lacks the double negation elimination axiom, which means that the proof
of ~~A will not deliver the proof of A, as such derivation would be non-constructive, as
one cannot get a value of type A out of a function of type (A → B) → B, where B is
taken to be False.
However, reasoning out of negation helps to derive the familiar proofs by contradiction,
given that we managed to construct P and ~P, as demonstrated by the following theorem,
which states that from any Q can be derived from P and ~P.
Theorem absurd: P → ~P → Q.
Proof. by move⇒p H ; move : (H p). Qed.
One extremely useful theorem from propositional logic involving negation is contrapo-
sition. It states that in an implication, the assumption and the goal can be flipped if
inverted.
Theorem contraP: (P → Q) → ~Q → ~P.
Let us see how it can be proved in Coq
Proof.
move⇒ H Hq.
move /H.
H :P →Q
Hq : ~Q
============================
Q → False
The syntax move / H (spaces in between are optional) stands for one of the most
powerful features of Ssreflect, called views (see Section 9 of [23]), which allows one to
weaken the assumption in the goal part of the proof on the fly by applying a hypothesis
H to the top assumption in the goal. In the script above the first command move⇒ H
Hq simply popped two assumptions from the goal to the context. What is left is ~P,
or, equivalently P → False. The view mechanism then “interpreted” P in the goal via
H and changing it to Q, since H was of type P → Q, which results in the modified goal
Q → False. Next, we apply the view Hq to the goal, which switches Q to False, which
makes the rest of the proof trivial.
move /Hq.
done.
Qed.
: type scope
Print ex.
A : Type
S : A → Prop
T : A → Prop
a: A
13
In the literature, dependent pairs are often referred to as dependent sums or Σ-types.
3.6 Existential quantification 45
Hs : S a
Hst : ∀ x : A, S x → T x
============================
exists b : A, T b
Next, we apply the ex’s constructor by means of the exists tactic with an explicit
witness value a:
exists a.
We finish the proof by applying the weakening hypothesis Hst.
by apply: Hst.
Qed.
Exercise 3.2. Let us define our own version my ex of the existential quantifier using
the Ssreflect notation for constructors:
Inductive my ex A (S : A → Prop) : Prop := my ex intro x of S x.
The reader is invited to prove the following goal, establishing the equivalence of the
two propositions
Goal ∀ A (S : A → Prop), my ex A S <-> exists y: A, S y.
Hint: the propositional equivalence <-> is just a conjunction of two implications, so
proving it can be reduced to two separate goals by means of split tactics.
proposition P x holds. Continuing the same analogy, the disjunction in the assumption
of a goal usually leads to the proof by case analysis assuming that one of the disjuncts
holds at a time. Similarly, the way to destruct the existential quantification is by case-
analysing on its constructor, which results in acquiring the witness (i.e., the “tag”) and
the corresponding “disjunct”.
Finally, the folklore alias “dependent product type” for dependent function types (i.e.,
∀-quantified types) indicates its relation to products, which are Curry-Howard coun-
terparts of conjunctions. In the same spirit, the term “dependent sum type” for the
dependent types, of which existential quantification is a particular case, hints to the re-
lation to the usual sum types, and, in particular sum (discussed in Chapter 2), which is
a Curry-Howard dual of a disjunction.
End Connectives.
classic
: ∀ P : Prop, P ∨ ~P
Another axiom from the classical logic, which coincides with the type of Scheme’s
call/cc operator14 (pronounced as call with current continuation) modulo Curry-Howard
isomorphism is Peirce’s law:
Definition peirce law := ∀ P Q: Prop, ((P → Q) → P) → P.
In Scheme-like languages, the call/cc operator allows one to invoke the undelimited
continuation, which aborts the computation. Similarly to the fact that call/cc cannot be
14
http://community.schemewiki.org/?call-with-current-continuation
3.8 Universes and Prop impredicativity 47
NNPP
: ∀ P : Prop, ~~P → P
Finally, the classical formulation of the implication through the disjunction is again an
axiom in the constructive logic, as otherwise from the function of type P → Q one would
be able to construct the proof of ~P ∨ Q, which would make the law of excluded middle
trivial to derive.
Check imply to or.
imply to or
: ∀ P Q : Prop, (P → Q) → ~P ∨ Q
Curiously, none of these axioms, if added to Coq, makes its logic unsound: it has been
rigorously proven (although, not within Coq, due to Gödel’s incompleteness result) that
all classical logic axioms are consistent with CIC, and, therefore, don’t make it possible
to derive the falsehood [66].
The following exercise reconciles most of the familiar axioms of classical logic.
Exercise 3.3 (Equivalence of classical logic axioms (from § 5.2.4 of [3])). Prove that the
following five axioms of the classical are equivalent.
Definition peirce := peirce law.
Definition double neg := ∀ P: Prop, ~~P → P.
Definition excluded middle := ∀ P: Prop, P ∨ ~P.
Definition de morgan not and not := ∀ P Q: Prop, ~( ~P ∧ ~Q) → P ∨ Q.
Definition implies to or := ∀ P Q: Prop, (P → Q) → (˜P ∨ Q).
Hint: Use rewrite /d tactics to unfold the definition of a value d and replace its name
by its body. You can chain several unfoldings by writing rewrite /d1 /d2 ... etc.
Hint: To facilitate the forward reasoning by contradiction, you can use the Ssreflect
tactic suff: P, where P is an arbitrary proposition. The system will then require you to
prove that P implies the goal and P itself.
Hint: Stuck with a tricky proof? Use the Coq Admitted keyword as a “stub” for an
unfinished proof of a goal, which, nevertheless will be considered completed by Coq. You
can always get back to an admitted proof later.
over propositions still remain to be propositions, i.e., they still belong to the sort Prop.
This property of propositions in Coq (and, in general, the ability of entities of some class
to abstract over the entities of the same class) is called impredicativity. The opposite
characteristic (i.e., the inability to refer to the elements of the same class) is called
predicativity.
One of the main challenges when designing the Calculus of Constructions was to imple-
ment its logical component (i.e., the fragment responsible for constructing and operating
with elements of the Prop sort), so it would subsume the existing impredicative proposi-
tional calculi [12], and, in particular, System F (which is impredicative), allowing for the
expressive reasoning in higher-order propositional logic.
Impredicativity as a property of definitions allows one to define domains that are self-
recursive—a feature of Prop that we recently observed. Unfortunately, when restated
in the classical set theory, impredicativity immediately leads to the famous paradox by
Russell, which arises from the attempt to define the set of all sets that do not belong to
themselves. In terms of programming, Russell’s paradox provides a recipe to encode a
fixpoint combinator in the calculus itself and write generally-recursive programs.
System F is not a dependently-typed calculus and it has been proven to contain no
paradoxes [21], as it reasons only about types (or, propositions), which do not depend
on values. However, adding dependent types to the mix (which Coq requires to make
propositions quantify over arbitrary values, not just other propositions, serving as a
general-purpose logic) makes the design of a calculus more complicated, in order to avoid
paradoxes akin to the Russell’s, which arise from mixing values and sets of values. This
necessity to “cut the knot” inevitably requires to have a sort of a higher level, which
contains all sets and propositions (i.e., the whole sorts Set and Prop), but does not
contain itself. Let us call such sort Type. It turns out that the self-inclusion Type : Type
leads to another class of paradoxes [11], and in order to avoid them, the hierarchy of
higher-order sorts should be made infinite and stratified. Stratification means that each
sort has a level number, and is contained in a sort of a higher level but not in itself. The
described approach is suggested by Martin-Löf [38] and adopted literally, in particular, by
Agda [45]. The stratified type sorts, following Martin-Löf’s tradition, are usually referred
to as universes.
A similar stratification is also implemented in Coq, which has its own universe hier-
archy, although with an important twist. The two universes, Set and Prop cohabit at
the first level of the universe hierarchy with Prop being impredicative. The universe
containing both Set and Prop is called Type@{Set+1}, and it is predicative, as well as
all universes that are above it in the hierarchy. CIC therefore remains consistent as a
calculus, only because of the fact that all impredicativity in it is contained at the very
bottom of the hierarchy.
the explicit printing of the universe levels to see how they are assigned:
Set Printing Universes.
Check bool.
bool
: Set
Check Set.
Set
: Type@{Set+1}
Check Prop.
Prop
: Type@{Set+1}
The following type is polymorphic over the elements of the Set universe, and this is
why its own universe is “bumped up” by one, so it now belongs to Set+1.
Definition S := ∀ T : Set, list T.
Check S.
S
: Type@{Set+1}
Until version 8.5, Coq used to provide a very limited version of universe polymorphism.
To illustrate the idea, let us consider the next definition R, which is polymorphic with
respect to the universe of its parameter A, so its result is assumed to “live” in the universe,
whose level is taken to be the level of A.
Definition R (A: Type) (x: A): A := x.
Arguments R [A].
Check R tt.
R tt
: unit
(* |= Set <= Top.93 *)
The part in comments show the inequality, generated by the Coq unification algorithm
that had to be solved in order to determine the universe level of the value R tt with
Top.93 being the level, assigned to R itself.
If the argument of R is itself a universe, it means that A’s level is higher than x’s level,
and so is the level of R’s result.
Check R Type.
50 3 Propositional Logic
R Type@{Top.94}
: Type@{Top.95}
(* Top.94
Top.95 |= Top.94 < Top.95
Top.95 < Top.93 *)
The Coq’s unifier algorithm in this case looks for a universe levels Top.95, which can
be larger than the level of R’s argument level Top.94, but smaller than the one of R
itself (i.e., Top.93). In the absence of other constraints, such system of equalities is easily
satisfiable.
However, the attempt to apply R to itself immediately leads to an error reported, as
the system cannot infer the level of the result, by means of solving a system of universe
level inequations, therefore, preventing meta-circular paradoxes.
Check R R.
RPoly : ∀ A : Type@{Top.96}, A → A
(* Top.96 |= *)
selfRPoly is defined
15
More documentation on universe polymorphism is available at https://coq.inria.fr/distrib/V8.
5beta2/refman/Reference-Manual032.html.
3.8 Universes and Prop impredicativity 51
selfRPoly =
RPoly@{Top.97} (@RPoly@{Top.98})
: ∀ A : Type@{Top.98}, A → A
(* Top.97
Top.98 |= Top.98 < Top.97
*)
The display above demonstrates that the two occurrences of RPoly were assumed by
the typing algorithm to belong to different universes: Top.97 for the function and Top.98
for the argument, correspondingly. In the absence of additional additional constraints,
the inequality between them can be trivially satisfied by assuming Top.98 < Top.97.
4 Equality and Rewriting Principles
In the previous chapter we have seen how main connectives from propositional logic are
encoded in Coq. However, the mathematical reasoning only by means of propositional
logic is still quite limited. In particular, by this moment we are still unable to state what
does it mean for two objects to be equal. In this chapter we are going to see how equality
can be implemented in Coq. Moreover, the statement "x is equal to y" automatically
gives us a way to replace y by x and vice versa in the process of reasoning, therefore
implementing a discipline of rewriting—one of the key ingredients of the mathematical
proof.1 Later in the chapter, we will see how rewriting by equality is just a particular
case of a general proof pattern, which allows one to define arbitrary rewriting rules by
exploiting Coq’s mechanism of indexed type families.
From mathcomp
Require Import ssreflect ssrnat ssrbool eqtype.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Print eq.
in contrast to just Prop. In the Coq terminology, it means that eq is not just inductively-
defined datatype, but is an indexed type family. In this particular case, it is indexed by
elements of type A, which appears at the left of the arrow.
It is common to think of indexed type families in Coq as of generalized algebraic
datatypes (GADTs) [50, 69], familiar from Haskell, and allowing one to refine the process
pattern matching basing on the type index of the scrutinee. However, another analogy
turns out to be much more useful in the Coq setting: indexed type families in fact allow
one to encode rewriting principles. To understand, what the indexed datatype definition
has to do with rewriting, let us take a close look at the definition of eq. The type of its
only constructor eq refl is a bit misleading, as it looks like it is applied to two arguments:
x and ... x. To disambiguate it, we shall put some parentheses, so, in fact, it should
read as
2
The Coq’s command Lemma is identical to Theorem.
4.1 Propositional equality in Coq 55
A : Type
x : A
y: A
============================
x === x
This leads to the goal, being switched from y === x to x === x, as all occurrences of
y are now replaced by x, exactly as advertised. We can now finish the proof by applying
the constructor (apply: my refl eq) or simply by done, which is powerful enough to
figure out what to apply.
done.
Qed.
Our next exercise will be to show that the predicate we have just defined implies Leibniz
equality. The proof is accomplished in one line by case-analysing on the equality, which
leads to the automatic replacements of y by x.
Lemma my eq Leibniz A (x y: A) (P: A → Prop) : x === y → P x → P y.
Proof. by case. Qed.
H : 2 === 1
============================
False
As it is already hinted by the name of the method, the key insight in the proofs
by discrimination is to construct a function that can distinguish between values of the
type with an implicit definitional equality, which relates two values if they have identical
structure.3 In particular, natural numbers can be compared against each other by means
of direct pattern matching, which is decidable for them, thanks to the inductive definition.
Using this insight we define a local “discriminating” function D using the Ssreflect’s
enhanced pose tactic:
pose D x := if x is 2 then False else True.
3
It is not trivial to establish computable definitional equality on any values, as the values might be of
an infinite nature. For instance, stating the equality of two functions would require checking their
results on all elements of the common domain, which might be infinite. in this respect, propositional
equality acts like it “compares the references”, whereas definitional equality “compares the structure”
of two elements.
56 4 Equality and Rewriting Principles
H : 2 === 1
D := fun x : nat ⇒
match x with
| 0 ⇒ True
| 1 ⇒ True
| 2 ⇒ False
| S (S (S )) ⇒ True
end : nat → Prop
============================
False
Now, proving D 1 is True can be accomplished by simple executing D with appropriate
arguments (recall that D is an always-terminating function, whose result is a computable
value). That Ssreflect’s tactic have allows to declare the local fact, which can be then
proved in-place by simple computation (which is performed via by []).
have D1 : D 1.
by [].
H : 2 === 1
D := ...
D1 : D 1
============================
False
Next we “push” D1 and H back to the goal (using the : tactical), and case-analyse
on the top assumption H. Notice that the semantics of : is such that it first performs a
series of “pushings” and then runs the tactic on the left of itself (i.e., case).
case: H D1.
D := ...
============================
D 2 → False
Now, we got what we have needed: the proof of the falsehood! Thanks to the equality-
provided substitution, D 1 turned into D 2, and the only thing that remains now is to
evaluate it.
move=>/=.
The tactical /=, coming after ⇒ runs all possible simplifications on the result obtained
by the tactics, preceding ⇒, finishing the proof.
done.
Qed.
Let us provide a bit more explanation how did it happen that we managed to derive the
falsehood in the process of the proof. The discrimination function D is a function from
nat to Prop, and, indeed, it can return True and False, so it contains no contradictions
4.2 Proofs by rewriting 57
by itself. We also managed to prove easily a trivial proposition D 1, which is just True,
so it’s derivable. The genuine twist happened when we managed to turn the assumption
D 1 (which was True) to D 2 (which is False). This was only possible because of the
assumed equality 2 === 1, which contained the “falsehood” from the very beginning
and forced Coq to substitute the occurrence of 1 in the goal by 2, so the discrimination
function in the assumption finished the job.
Exercise 4.1. Let us change the statement of a previous lemma for a little bit:
Lemma disaster2 : 1 === 2 → False.
Now, try to prove it using the same scheme. What goes wrong and how to fix it?
A : Type
x : A
f: A→A
t: A
Et : t = double f x
============================
double f (double f x) = nat iter 4 f x
Even though the remaining goal is simple enough to be completed by done, let us
unfold both definition to make sure that the two terms are indeed equal structurally.
Such unfoldings can be chained, just as any other rewritings.
rewrite /double /nat iter.
x : A
f: A→A
============================
f (f (f (f x))) = f (f (f (f x)))
An alternative way to prove the same statement would be to use the -> tactical, which
is usually combined with move or case, but instead of moving the assumption to the top,
it makes sure that the assumption is an equality and rewrites by it.
Restart.
by move=>->; rewrite /double.
Qed.
Notice that the tactical has a companion one <-, which performs the rewriting by an
equality assumption from right to left, in contrast to ->, which rewrites left to right.
Folding, the reverse operation to unfolding, is done by using rewrite -/... instead of
rewrite /...4
Proof.
move⇒ x y.
First, let us unfold only all occurrences of f in the goal.
rewrite /f.
x : nat
y : nat
============================
x + y + (y + x) = y + x + (y + x)
We can now reduce the goal by appealing to Ssreflect’s congr tactics, which takes
advantage of the fact that equality implies Leibniz’ equality, in particular, with respect
to the addition taken as a function, so the external addition of equal elements can be
“stripped off”.
congr ( + ).
x : nat
y : nat
============================
x +y=y+x
Now, the only thing left to prove is that the addition is commutative, so at this point
we will just make use of Ssreflect’s ssrnat library lemma for integer addition.
Check addnC.
addnC
: ssrfun.commutative addn
At this point such signature might seem a bit cryptic, but worry not: this is just a
way to express in a generic way that the addition over natural numbers is commutative,
which can be witnessed by checking the definition of ssrfun.commutative predicate:
Print ssrfun.commutative.
ssrfun.commutative =
fun (S T : Type) (op : S → S → T ) ⇒ ∀ x y : S, op x y = op y x
: ∀ S T : Type, (S → S → T ) → Prop
As we can see, the definition of the commutative predicate ensures the equality of the
operation’s result with its arguments, permuted, hence op x y = op y x. The type of
the lemma addnC therefore refines op to be “ + ”, so, after specializing the definition
appropriately, the type of addnC should be read as:
addnC
: ∀ n m: nat, n + m = m + n
60 4 Equality and Rewriting Principles
Now, we can take advantage of this equality and rewrite by it a part of the goal. Notice
that Coq will figure out how the universally-quantified variables should be instantiated
(i.e., with y and x, respectively):
by rewrite [y + ]addnC.
Qed.
The r-pattern (regex pattern) [y + ], preceding the lemma to be used for rewriting,
specifies, which subexpression of the goal should be a subject of rewriting. When non-
ambiguous, some parts of the expressions can be replaced by wildcard underscores . In
this particular case, it does not matter that much, since any single rewriting by com-
mutativity in any of the sums, on the left or on the right, would make the proof to go
through. However, in a more sophisticated goal it makes sense to specify explicitly, what
should be rewritten:
Goal ∀ x y z, (x + (y + z)) = (z + y + x).
Proof.
by move⇒x y z; rewrite [y + ]addnC ; rewrite [z + + ]addnC.
Qed.
Proofs of “obvious” equalities that hold modulo, e.g., commutativity and subjectivity,
usually require several rewriting to be established, which might be tedious. There are
ways to automate such proofs by means of overloaded lemmas via canonical structures.
These techniques, hinted briefly in Chapter 7, are mostly outside of the scope of this
course, so we address the reader to a number of papers, presenting the state of the art in
this direction [25, 37].
m : nat
n : nat
============================
∀ p : nat, m + (n + p) = n + (m + p)
The proof will proceed by induction on m. We have already seen the use of the case
tactics, which just performs the case analysis. Another Ssreflect tactic elim generalizes
case by applying the default induction principle (nat ind in this case) with the respect
to the remaining goal (that is, the predicate [∀ p : nat, m + (n + p) = n + (m + p)]) is
to be proven by induction. The following sequence of tactics proceeds by induction on m
with the default induction principle. It also names some of the generated assumptions.
elim: m=>[ | m Hm ] p.
4.2 Proofs by rewriting 61
The first goal can now be proved by multiple rewritings via the lemma add0n, stating
that 0 is the left unit with respect to the addition:
by rewrite !add0n.
The second goal can be proved by a series of rewritings using the fact about the ( +
1) function:
by rewrite !addSnnS -addnS.
Notice that the conclusion of the addnS lemma is rewritten right-to-left.
The whole proof could be, however, accomplished in one line using the optional rewrit-
ings. The intuitions is to chain the rewritings in the goals, generated by elim in a way
that the unsuccessful rewriting would not fail the whole proof construction, as they are
irrelevant for some goals anyway. This is how it can be done:
Restart.
by move⇒m n; elim: m=>[ | m Hm ] p; rewrite ?add0n ?addSnnS -?addnS.
Qed.
Notice that the optional rewritings (e.g., ?addSnnS) are performed as many times as
they can be.
The first rewriting with addn0 “adds” 0 to the first occurrence of addn0, so the left-
hand side of the equality becomes m + (n + 0). The next rewriting employs the lemma
addnCA, so we get n + (m + 0) = n + m as the goal, and the last one “removes” zero,
so the result trivially follows.
We conclude this section by noticing that the same rewriting machinery is applicable
not only to the goal, but also to hypotheses in the assumption context using the rewrite
H1 in H2 syntax (where H1 is the rewriting hypothesis and H2 is a hypothesis, where the
rewriting should happen). There are many more tricks that can be done with rewritings,
and we address the reader to Chapter 7 of Ssreflect manual [23].
The stated lemma max is max can be, indeed, proved by induction on m and n, which
is a rather tedious exercise, so we will not be following this path.
| C1 | C2
-------------------------
m <= n | true | false
-------------------------
n < m | false | true
The boolean values in the cells specify what the values of C1 and C2 will be substituted
with in each of the two cases. However, the table does not capture, what to substitute
them for. Therefore, our next task is to provide suitable variants for C1 and C2, so the ta-
ble would describe a real situation and capture exactly the “case analysis” intuition. This
values of the columns are captured by the following lemma, which, informally speaking,
states that the table with this particular values of C1 and C2 “makes sense”.
n : nat
m : nat
============================
m ≤ n < m → False
The top assumption m ≤ n < m of the goal is just a syntactic sugar for (m ≤ n) &&
(n < m). It is time now to make use of our rewriting rule/truth table, constructed by
means of leqP.
case:leqP.
n : nat
m : nat
============================
m ≤ n → true && false → False
m : nat
n : nat
============================
n ≤ (if m < n then n else m) ∧ m ≤ (if m < n then n else m)
We are now in the position to unleash our rewriting rule, which, together with simpli-
fications by means of the // tactical does most of the job.
case: leqP=>//.
m : nat
n : nat
============================
m<n→n≤n∧m≤n
The rest of the proof employs rewriting by some trivial lemmas from ssrnat, but con-
ceptually is very easy.
move⇒H ; split.
by apply: leqnn.
by rewrite ltn neqAle in H ; case/andP: H.
Qed.
The key advantage we got out of using the custom rewriting rule, defined as an indexed
datatype family is lifting the need to prove by induction a statement, which one would
intuitively prove by means of case analysis. In fact, all inductive reasoning was conve-
niently “sealed” by the proof of leqP and the lemmas it made use of, so just the tailored
“truth table”-like interface for case analysis was given to the client.
We invite the reader to exercise in using the custom rewriting rules by proving a series
of properties of maxn.
Hint: It might be useful to employ the lemmas ltnNge, leqNgt, ltnS and similar from
Ssreflect’s ssrnat module. Use the Search command to find propositions that might help
you to deal with the goal.
Hint: Forward-style reasoning via suff and have might be more intuitive.
Hint: A hypothesis of the shape H : n < m is a syntactic sugar for H : n < m = true,
since n < m in fact has type bool, as will be explained in Chapter 5.
66 4 Equality and Rewriting Principles
We conclude this section and the chapter by showing an instance of a more sophisticated
custom rewriting rule, which now encodes a three-variant truth table for the ordering
relations on natural numbers.
Inductive nat rels m n : bool → bool → bool → Set :=
| CompareNatLt of m < n : nat rels m n true false false
| CompareNatGt of m > n : nat rels m n false true false
| CompareNatEq of m = n : nat rels m n false false true.
Exercise 4.3 (Comparing natural numbers as a rewriting rule). Prove the following
rewriting lemma for nat rels:
Lemma natrelP m n : nat rels m n (m < n) (n < m) (m == n).
Exercise 4.4. Let us define the minimum function minn on natural numbers as follows:
Definition minn m n := if m < n then m else n.
Prove the following lemma about minm and maxn:
Lemma addn min max m n : minn m n + maxn m n = m + n.
5 Views and Boolean Reflection
In Chapter 4, we have seen how custom rewriting rules and truth tables can be encoded
in Coq using its support for indexed datatype families, so they are of great help for
constructing the proofs by case analysis and rewriting. In this chapter, we will show
how the custom rewriting machinery can be taken to the whole new level and be used
to facilitate the reasoning about computable properties and predicates. We will consider
a series of insights that lead to the idea of the small-scale reflection, the heart of the
Ssreflect framework, which blurs the boundaries between computable predicates defined
in the sort Prop (see Chapter 3) and Coq’s recursive functions returning a result of type
bool (in the spirit of the definitions that we have seen in Chapter 2). That said, in the
vast number of cases these two are just the sides of the same coin and, hence, should be
treated uniformly, serving to facilitate the reasoning in two different directions:
• employing brute-force computations for quantifier-free goals within the Coq frame-
work itself, taken as a programming language, in order to reduce the goals to be
proved by means of simply computing them.
We will elaborate more on the differences between predicates stated by means of Prop
and bool in Section 5.2. The term small-scale reflection, which gives the name to the
whole framework of Ssreflect, emphasizes the two complementary ways of building proofs:
by means of intuitionistic inference (i.e., using the constructors of datatypes defined in
Prop) and by means of mere computation (i.e., with bool-returning function). These two
ways, therefore, serve as each other’s “reflections” and, moreover, both are implemented
within the same system, without the need to appeal to Coq’s meta-object protocol,1
which makes this reflection small-scale.
Unfortunately, the proper explanation of the implementation of the reflection mecha-
nism between Prop and bool in Ssreflect strongly relies on the views machinery, so let us
begin by describing it first.
1
In contrast, reflection mechanism in Java, Python or Ruby actually does appeal to the meta-object
protocol, e.g., the structure of the classes, which lies beyond the formally defined semantics of the
language itself and, hence, allows one to modify the program’s behaviour at runtime.
68 5 Views and Boolean Reflection
P : Type
Q : Type
R : Type
S : Type
H1 : P → Q
H2 : R → S
H3 : Q → R
============================
P →S
Since we are proficient in the proofs via implications, it is not difficult to construct the
explicit proof term by a series of apply: tactic calls or via the exact: tactic, as it has
been show in Chapter 3. Let us do something different, though, namely weaken the top
assumption of the goal by means of applying the hypothesis H1 to it, so the overall goal
will become Q → S.
move⇒p; move: (H1 p).
This proof pattern of “switching the view” turns out to be so frequent that Ssreflect
introduces a special view tactical / for it, which is typically combined with the standard
move or case tactics. In particular, the last proof line could be replaced by the following:
Undo.
move/H1.
...
H1 : P → Q
H2 : R → S
H3 : Q → R
============================
Q→S
The assumption H1 used for weakening is usually referred to as a view lemma. The
spaces before and after / are optional. One can also chain the views into one series, so
the current proof can be completed as follows:
by move/H3 /H2.
Qed.
5.1 Proving with views in Ssreflect 69
by move⇒H /STequiv.
Qed.
iffRL
: ∀ P Q : Prop, (P ↔ Q) → Q → P
The type of iffRL reveals that what it does is simply switching the equivalence to the
implication, which works right-to-left, as captured by the name. Let us now redo the
proof of the ST False lemma to see what is happening under the hood:
Lemma ST False’ a b: (T a → False) → S (a || b) → False.
Proof.
move⇒ H.
move/(iffRL (STequiv a b)).
done.
Qed.
The view switch on the second line of the proof is what has been done implicitly in
the previous case: the implicit view iffRL has been applied to the call of STequiv, which
was in its turn supplied the necessary arguments a and b, inferred by the system from
the goal, so the type of (STequiv a b) would match the parameter type of iffRL, and the
whole application would allow to make a view switch in the goal. What is left behind
the scenes is the rest of the attempts made by Coq/Ssreflect in its search for a suitable
implicit view, which ended when the system has finally picked iffRL.
In general, the design of powerful view hints is non-trivial, as they should capture
precisely the situation when the “view switch” is absolutely necessary and the implicit
views will not “fire” spuriously. In the same time, implicit view hints is what allows for
the smooth implementation of the boolean reflection, as we will discuss in Section 5.3.
TS neg =
fun (a : bool) (H : T (negb a)) ⇒
(fun F : T (negb a) ⇒
iffLR (Q:=S (negb a || a)) (STequiv (negb a) a) F ) H
: ∀ a : bool, T (negb a) → S (negb a || a)
i.e., such that contain quantifiers. For instance, it is not possible to implement a higher-
order function, which would take two arbitrary functions f1 and f2 of type nat → nat
and return a boolean answer, which would indicate whether these two functions are equal
(point-wise) or not, as it would amount to checking the result of the both function on each
natural number, which, clearly, wouldn’t terminate. Therefore, propositional equality of
functions is a good example of a proposition, which is undecidable in general, so we
cannot provide a terminating procedure for any values of its arguments (i.e., f1 and f2 ).
However, the undecidability of higher-order propositions (like the propositional equality
of functions) does not make them non-provable for particular cases, as we have clearly
observed thorough the past few chapters. It usually takes a human intuition, though,
to construct a proof of an undecidable proposition by means of combining a number of
hypotheses (i.e., constructing a proof term), which is what one does when building a
proof using tactics in Coq. For instance, if we have some extra insight about the two
functions f1 and f2 , which are checked for equality, we might be able to construct the
proof of them being equal or not, in the similar ways as we have carried the proofs so far.
Again, even if the functions are unknown upfront, it does not seem possible to implement
an always-terminating procedure that would automatically decide whether they are equal
or not.
The above said does not mean that all possible propositions should be implemented
as instances of Prop, making their clients to always construct their proofs, when it is
necessary, since, fortunately, some propositions are decidable, so it is possible to construct
a decision procedure for them. A good example of such proposition is a predicate, which
ensures that a number n is prime. Of course, in Coq one can easily encode primality of
a natural number by means of the following inductive predicate, which ensures that n is
prime if it is 1 or has no other natural divisors but 1 and n itself.
Definition isPrime n : Prop :=
∀ n1 n2, n = n1 × n2 → (n1 = 1 ∧ n2 = n) ∨ (n1 = n ∧ n2 = 1).
Such definition, although correct, is quite inconvenient to use, as it does not provide a
direct way to check whether some particular number (e.g., 239) is prime or not. Instead,
it requires one to construct a proof of primality for each particular case using the con-
structors (or the contradiction, which would imply that the number is not prime). As it’s
well known, there is a terminating procedure to compute whether the number is prime
or not by means of enumerating all potential divisors of n from 1 to the square root of
n. Such procedure is actually implemented in the Ssreflect’s prime module and proved
correct with respect to the definition similar to the one above,4 so now one can test the
numbers by equality by simply executing the appropriate function and getting a boolean
answer:
Eval compute in prime 239.
= true
: bool
Therefore, we can summarize that the decidability is what draws the line between
propositions encoded by means of Coq’s Prop datatypes and procedures, returning a bool
4
Although the implementation and the proof are somewhat non-trivial, as they require to build a
primitively-recursive function, which performs the enumeration, so we do not consider them here.
5.2 Prop versus bool 73
result. Prop provides a way to encode a larger class of logical statements, in particular,
thanks to the fact that it allows one to use quantifiers and, therefore, encode higher-
order propositions. The price to pay for the expressivity is the necessity to explicitly
construct the proofs of the encoded statements, which might lead to series of tedious and
repetitive scripts. bool-returning functions, when implemented in Coq, are decidable by
construction (as Coq enforces termination), and, therefore, provide a way to compute
the propositions they implement. Of course, in order to be reduced to true or false,
all quantifiers should be removed by means of instantiated the corresponding bound
variables, after which the computation becomes possible.
For instance, while the expression (prime 239) || (prime 42) can be evaluated to true
right away, whereas the expression
∀ n, (prime n) || prime (n + 1)
is not even well-typed. The reason for this is that polymorphic ∀-quantification in
Coq does not admit values to come after the comma (so the dependent function type
“Πn : nat, n” is malformed), similarly to how one cannot write a type Int → 3 in Haskell,
as it does not make sense. This expression can be, however, coerced into Prop by means
of comparing the boolean expression with true using propositional equality
computational approach to proofs is what has been taken by Ssreflect to the extreme,
making the proofs about common mathematical constructions to be very short, as most
of the proof obligations simply do not appear, as the system is possible to reduce them
by means of performing the computations on the fly. Even though, as discussed, some
propositions can be only encoded as elements of Prop, our general advice is to rely on
the computations whenever it is possible.
In the following subsections we will elaborate on some additional specifications and
proof patterns, which are enabled by using boolean values instead of full-fledged propo-
sitions from Prop.
Definition prime spec bad n m : Prop := m = (if isPrime n then 1 else 2).
Error: In environment
m : nat
n : nat
The term "isPrime n" has type "Prop" while it is expected to have type "bool".
Fortunately, the computable predicates are free from this problem, so on can freely use
them in the conditionals:
Definition prime spec n m : Prop := m = (if prime n then 1 else 2).
Proof.
move⇒n. rewrite /prime spec /discr prime.
n : nat
============================
(if prime n then 0 else 1) + 1 = (if prime n then 1 else 2)
The proof of the specification is totally in the spirit of what one would have done when
proving it manually: we just case-analyse on the value of prime n, which is either true or
false. Similarly to the way the rewritings are handled by means of unification, in both
cases the system substitutes prime n with its boolean value in the specification as well.
The evaluation completes the proof.
by case: (prime n).
Qed.
Another common use case of boolean predicates comes from the possibility to perform
a case analysis on the boolean computable equality, which can be employed in the proof
proceeding by an argument “let us assume a to be equal to b (or not)”. As already hinted
by the example with the function equality earlier in this section, the computable equality
is not always possible to implement. Fortunately, it can be implemented for a large
class of datatypes, such as booleans, natural numbers, lists and sets (of elements with
computable equality), and it was implemented in Ssreflect, so one can take an advantage
of it in the proofs.6
(see Section 4.3 of Chapter 4) and introducing the inductive predicate family reflect,
which connects propositions and booleans:
Print Bool.reflect.
n : nat
============================
do check1 n ∧ do check2 n → true → prime n
Case analysis on the rewriting rule andP generates two goals, and the second one has
false as an assumption, so it is discharged immediately by using //. The remaining goal
5.3 The reflect type family 77
has a shape that we can work with, so we conclude the proof by applying the hypothesis
H declared above.
by case⇒ /H.
Qed.
Although the example above is a valid usage of the reflected propositions, Ssreflect
leverages the rewriting with respect to boolean predicates even more by defining a number
of hint views for the rewriting lemmas that make use of the reflect predicates. This allows
one to use the rewriting rules (e.g., andP) in the form of views , which can be applied
directly to an assumption or a goal, as demonstrated by the next definition.
Definition andb orb b1 b2 : b1 && b2 → b1 || b2.
Proof.
case/andP⇒H1 H2.
by apply/orP; left.
Qed.
The first line of the proof switched the top assumption from the boolean conjunction to
the propositional one by means of andP used as a view. The second line applied the orP
view, doing the similar switch in the goal, completing the proof by using a constructor
of the propositional disjunction.
Print andb orb.
Let us take a brief look to the obtained proof term for andb orb.
andb orb =
fun (b1 b2 : bool) (goal : b1 && b2 ) ⇒
(fun F : ∀ (a : b1 ) (b : b2 ),
(fun : b1 ∧ b2 ⇒ is true (b1 || b2 )) (conj a b) ⇒
match
elimTF (andP b1 b2 ) goal as a return ((fun : b1 ∧ b2 ⇒ is true (b1 || b2 )) a)
with
| conj x x0 ⇒ F x x0
end)
(fun (H1 : b1 ) ( : b2 ) ⇒
(fun F : if true then b1 ∨ b2 else ~(b1 ∨ b2 ) ⇒
introTF (c:=true) orP F ) (or introl H1 ))
: ∀ b1 b2 : bool, b1 && b2 → b1 || b2
As we can see, the calls to the rewriting lemmas andP and orP were implicitly “wrapped”
into the call of hints elimTF and introTF, correspondingly. Defined via the conditional
operator, both these view hints allowed us to avoid the second redundant goal, which we
would be be forced to deal with, had we simply gone with case analysis on andP and orP
as rewriting rules.
Check elimTF.
elimTF
: ∀ (P : Prop) (b c : bool),
78 5 Views and Boolean Reflection
Unsurprisingly, every statement about exclusive or, e.g., its commutativity and asso-
ciativity, is extremely easy to prove when it is considered as a boolean function.
Lemma xorbC (b1 b2 : bool) : (xorb b1 b2 ) = (xorb b2 b1 ).
Proof. by case: b1 ; case: b2. Qed.
Lemma xorbA (b1 b2 b3 : bool) : (xorb (xorb b1 b2 ) b3 ) = (xorb b1 (xorb b2 b3 )).
Proof. by case: b1 ; case: b2 ; case: b3 =>//. Qed.
It is also not difficult to prove the propositional counterparts of the above lemmas for
decidable propositions, reflected by them, hence the following exercise.
Exercise 5.3. Prove the following specialized lemmas for decidable propositions repre-
sented by booleans (without using the intuition tactic):
Lemma xorCb (b1 b2 : bool) : (XOR b1 b2 ) ↔ (XOR b2 b1 ).
Lemma xorAb (b1 b2 b3 : bool) : (XOR (XOR b1 b2 ) b3 ) ↔ (XOR b1 (XOR b2 b3 )).
Hint: In the proof of xorAb the generalized reflection lemma xorP gen might come in
handy.
5.3 The reflect type family 79
x : nat
y : nat
============================
x = y → (if x == y then 1 else 0) = 1
The rewriting rule/view lemma eqP, imported from eqtype allows us to switch from
propositional to boolean equality, which makes the assumption to be x == y. Next, we
combine the implicit fact that x == y in the assumption of a proposition is in fact (x ==
y) = true to perform in-place rewriting (see Section 4.2.1) by means of the -> tactical,
so the rest of the proof is simply by computation.
by move/eqP=>->.
Qed.
Exercise 5.4. Sometimes, the statement “there exists unique x and y, such that P (x, y)
holds” is mistakingly formalized as ∃!x ∃!y P (x, y). In fact, the latter assertion is much
weaker than the previous one. The goal of this exercise is to demonstrate this formally.7
First, prove the following lemma, stating that the first assertion can be weakened from
the second one.
Lemma ExistsUnique1 A (P : A → A → Prop):
(∃ !x, ∃ y, P x y) →
(∃ !x, ∃ y, P y x) →
7
I am grateful to Vladimir Reshetnikov (@vreshetnikov) for making this observation on Twitter.
80 5 Views and Boolean Reflection
unique =
fun (A : Type) (P : A → Prop) (x : A) ⇒
P x ∧ (∀ x’ : A, P x’ → x = x’)
: ∀ A : Type, (A → Prop) → A → Prop
As we can see, the definition unique not just ensures that P x holds (the left conjunct),
but also that any x’ satisfying P is, in fact, equal to x. As on the top level unique is
merely a conjunction, it can be decomposed by case and proved using the split tactics.
Next, let us make sure that the statement in the conclusion of lemma ExistsUnique1, in
fact, admits predicates, satisfied by non-uniquely defined pair (x, y). You goal is to prove
that the following predicate Q, which obviously satisfied by (true, true), (false, true) and
(false, false) is nevertheless a subject of the second statement.
Definition Q x y : Prop :=
(x == true) && (y == true) || (x == false).
Lemma qlm : (∃ !x, ∃ !y, Q x y).
Hint: The following lemma eqxx, stating that the boolean equality x == x always holds,
might be useful for instantiating arguments for hypotheses you will get during the proof.
Check eqxx.
eqxx
: ∀ (T : eqType) (x : T ), x == x
Finally, you are invited to prove that the second statement is strictly weaker than the
first one by proving the following lemma, which states that the reversed implication of
the two statements for an arbitrary predicate P implies falsehood.
Lemma ExistsUnique2 :
(∀ A (P : A → A → Prop),
(∃ !x, ∃ !y, P x y) →
(∃ !x, ∃ y, P x y) ∧ (∃ !x, ∃ y, P y x)) →
False.
6 Inductive Reasoning in Ssreflect
In the previous chapters of this course, we have become acquainted with the main concepts
of constructive logic, Coq and Ssreflect. However, the proofs we have seen so far are mostly
done by case analysis, application of hypotheses and various forms of rewriting. In this
chapter we will consider in more detail the proofs that employ inductive reasoning as
their main component. We will see how such proofs are typically structured in Ssreflect,
making the corresponding scripts very concise, yet readable and maintainable. We will
also learn a few common techniques that will help to adapt an induction hypothesis to
become more suitable for a goal.
In the rest of the chapter we will be constantly relying on a series of standard Ssreflect
modules, such as ssrbool, ssrnat and eqtype, which we import right away.
From mathcomp
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
true = true
b : bool
============================
b && false → false = true
Now, right after case-analysing on c, the proof script specifies that the first of the
generated subgoals should be solved using by []. In this case first is called selector, and
its counterpart last would specify that the last goal should be taken care of instead,
before proceeding.
Finally, if several simple goals can be foreseen as a result of case analysis, Coq provides
a convenient way to discharge them in a structured way using the [|...|] tactical:
Restart.
case:c; [by [] | by case: b].
The script above solves the first generated goal using by [], and then solves the second
one via by case: b.
to prove.1 The do-tactical can be also combined with the [|...|] tactical, so it will try to
apply all of the enumerated tactics as alternatives. The following script finishes the proof
of the whole lemma.
Restart.
by do ![done | apply: eqxx | case: b | case: c].
Notice that we have added two tactics into the alternative list, done and apply: eqxx,
which were doomed to fail. The script, nevertheless, has succeeded, as the remaining
two tactics, case: b and case: c, did all the job. Lastly, notice that the do-tactical can
be specified how many times it should try to run each tactic from the list by using the
restricted form do n!tac, where n is the number of attempts (similarly to iterating the
rewrite tactics). The lemma above could be completed by the script of the form by do
2![...] with the same list of alternatives.
Qed.
That is, instead of the unavoidable case-analysis with the first Prop-based definition,
the functional definition made Coq compute the result for us, deriving the falsehood
automatically.
The benefits of the computable definitions become even more obvious when considering
the next example, the predicate defining whether a natural number is even or odd. Again,
we define two versions, the inductive predicate and a boolean function.
Inductive evenP n : Prop :=
Even0 of n = 0 | EvenSS m of n = m.+2 & evenP m.
Fixpoint evenb n := if n is n’.+2 then evenb n’ else n == 0.
Let us now prove a simple property: that fact that (n + 1 + n) is even leads to a
paradox. We first prove it for the version defined in Prop.
Lemma evenP contra n : evenP (n + 1 + n) → False.
Proof.
elim: n=>//[| n Hn]; first by rewrite addn0 add0n; case=>//.
We start the proof by induction on n, which is triggered by elim: n.2 The subsequent
two goals (for the zero and the successor cases) are then simplified via // and the induction
variable and hypothesis are given the names n and Hn, respectively, in the second goal (as
described in Section 4.2.3). Then, the first goal (the 0-case) is discharged by simplifying
the sum via two rewritings by addn0 and add0n lemmas from the ssrnat module and
case-analysis on the assumption of the form evenP 1, which delivers the contradiction.
The second goal is annoyingly trickier.
n : nat
Hn : evenP (n + 1 + n) → False
============================
evenP (n.+1 + 1 + n.+1) → False
First, let us do some rewritings that make the hypothesis and the goal look alike.3
rewrite addn1 addnS addnC !addnS.
rewrite addnC addn1 addnS in Hn.
n : nat
Hn : evenP (n + n).+1 → False
============================
evenP (n + n).+3 → False
Now, even though the hypothesis Hn and the goal are almost the same (modulo the
natural “(.+2)-orbit” of the evenP predicate and some rewritings), we cannot take an
advantage of it right away, and instead are required to case-analysed on the assumption
of the form evenP (n + n).+3:
case=>// m /eqP.
2
Remember that the elim, as most of other Ssreflect’s tactics operates on the top assumption.
3
Recall that n.+1 stands for the value of the successor of n, whereas n + 1 is a function call, so the
whole expression in the goal cannot be just trivially simplified by Coq’s computation and requires
some rewritings to take the convenient form.
6.2 Inductive predicates that should be functions 85
n : nat
Hn : evenP (n + n).+1 → False
m : nat
============================
(n + n).+3 = m.+2 → evenP m → False
Only now we can make use of the rewriting lemma to “strip off” the constant summands
from the equality in the assumption, so it could be employed for brushing the goal, which
would then match the hypothesis exactly.
by rewrite !eqSS ; move/eqP=><-.
Qed.
Now, let us take a look at the proof of the same fact, but with the computable version
of the predicate evenb.
Lemma evenb contra n: evenb (n + 1 + n) → False.
Proof.
elim: n=>[|n IH ] //.
n : nat
IH : evenb (n + 1 + n) → False
============================
evenb (n.+1 + 1 + n.+1) → False
In the case of zero, the proof by induction on n is automatically carried out by com-
putation, since evenb 1 = false. The inductive step is not significantly more complicated,
and it takes only two rewriting to get it into the shape, so the computation of evenb could
finish the proof.
by rewrite addSn addnS.
Qed.
Sometimes, though, the value “orbits”, which can be advantageous for the proofs in-
volving bool-returning predicates, might require a bit trickier induction hypotheses than
just the statement required to be proved. Let us compare the two proofs of the same
fact, formulated with evenP and evenb.
Lemma evenP plus n m : evenP n → evenP m → evenP (n + m).
Proof.
elim=>//n’; first by move=>->; rewrite add0n.
n : nat
m : nat
n’ : nat
============================
∀ m0 : nat,
n’ = m0.+2 →
evenP m0 → (evenP m → evenP (m0 + m)) → evenP m → evenP (n’ + m)
86 6 Inductive Reasoning in Ssreflect
The induction here is on the predicate evenP, so the first case is discharged by rewrit-
ing.
move⇒ m’->{n’} H1 H2 H3 ; rewrite addnC !addnS addnC.
n : nat
m : nat
m’ : nat
H1 : evenP m’
H2 : evenP m → evenP (m’ + m)
H3 : evenP m
============================
evenP (m’ + m).+2
In order to proceed with the inductive case, again a few rewritings are required.
apply: (EvenSS )=>//.
n : nat
m : nat
m’ : nat
H1 : evenP m’
H2 : evenP m → evenP (m’ + m)
H3 : evenP m
============================
evenP (m’ + m)
The proof script is continued by explicitly applying the constructor EvenSS of the evenP
datatype. Notice the use of the wildcard underscores in the application of EvenSS. Let
us check its type:
Check EvenSS.
EvenSS
: ∀ n m : nat, n = m.+2 → evenP m → evenP n
By using the underscores, we allowed Coq to infer the two necessary arguments for the
EvenSS constructor, namely, the values of n and m. The system was able to do it basing
on the goal, which was reduced by applying it. After the simplification and automatic
discharging the of the trivial subgoals (e.g., (m’ + m)+.2 = (m’ + m)+.2) via the //
tactical, the only left obligation can be proved by applying the hypothesis H2.
by apply: H2.
Qed.
In this particular case, the resulting proof was quite straightforward, thanks to the
explicit equality n = m.+2 in the definition of the EvenSS constructor.
In the case of the boolean specification, though, the induction should be done on the
natural argument itself, which makes the first attempt of the proof to be not entirely
trivial.
6.2 Inductive predicates that should be functions 87
m : nat
n : nat
Hn : evenb n → evenb m → evenb (n + m)
============================
evenb n.+1 → evenb m → evenb (n.+1 + m)
The problem now is that, if we keep building the proof by induction on n or m, the
induction hypothesis and the goal will be always “mismatched” by one, which will prevent
us finishing the proof using the hypothesis.
There are multiple ways to escape this vicious circle, and one of them is to generalize
the induction hypothesis. To do so, let us restart the proof.
Restart.
move: (leqnn n).
n : nat
m : nat
============================
n ≤ n → evenb n → evenb m → evenb (n + m)
Now, we are going to proceed with the proof by selective induction on n, such that
some of its occurrences in the goal will be a subject of inductive reasoning (namely, the
second one), and some others will be left generalized (that is, bound by a forall-quantified
variable). We do so by using Ssreflect’s tactics elim with explicit occurrence selectors.
elim: n {-2}n.
m : nat
============================
∀ n : nat, n ≤ 0 → evenb n → evenb m → evenb (n + m)
m : nat
n : nat
Hn : ∀ n0 : nat, n0 ≤ n → evenb n0 → evenb m → evenb (n0 + m)
============================
∀ n0 : nat, n0 ≤ n.+1 → evenb n0 → evenb m → evenb (n0 + m)
We then perform the case-analysis on n0 in the goal, which results in two goals, one
of which is automatically discharged.
case=>//.
m : nat
n : nat
Hn : ∀ n0 : nat, n0 ≤ n → evenb n0 → evenb m → evenb (n0 + m)
============================
∀ n0 : nat, n0 < n.+1 → evenb n0.+1 → evenb m → evenb (n0.+1 + m)
Doing one more case analysis will add one more 1 to the induction variable n0, which
will bring us to the desired (.+2)-orbit.
case=>// n0.
m : nat
n : nat
Hn : ∀ n0 : nat, n0 ≤ n → evenb n0 → evenb m → evenb (n0 + m)
n0 : nat
============================
n0.+1 < n.+1 → evenb n0.+2 → evenb m → evenb (n0.+2 + m)
The only thing left to do is to tweak the top assumption (by relaxing the inequality
via the ltnW lemma), so we could apply the induction hypothesis Hn.
by move/ltnW /Hn=>//.
Qed.
It is fair to notice that this proof was far less direct that one could expect, but it taught
us an important trick—selective generalization of the induction hypothesis. In particular,
by introducing an extra assumption n ≤ n in the beginning, we later exploited it, so we
could apply the induction hypothesis, which was otherwise general enough to match the
ultimate goal at the last step of the proof.
P 0 → P 1 → (∀ n, P n → P (n.+2)) → ∀ n, P n.
Proof.
move⇒ H0 H1 H n.
P : nat → Prop
H0 : P 0
H1 : P 1
H : ∀ n : nat, P n → P n.+2
n : nat
============================
P n
Unsurprisingly, the proof of this induction principle follows the same pattern as the
proof of evenb plus—generalizing the hypothesis. In this particular case, we generalize it
in the way that it would provide an “impedance matcher” between the 1-step “default”
induction principle on natural numbers and the 2-step induction in the hypothesis H. We
show that for the proof it is sufficient to establish (P n ∧ P (n.+1)):
suff: (P n ∧ P (n.+1)) by case.
The rest of the proof proceeds by the standard induction on n.
by elim: n=>//n; case⇒ H2 H3 ; split=>//; last by apply: H.
Qed.
Now, since the new induction principle nat2 ind exactly matches the 2-orbit, we can
directly employ it for the proof of the previous result.
Lemma evenb plus’ n m : evenb n → evenb m → evenb (n + m).
Proof.
by elim/nat2 ind : n.
Qed.
Notice that we used the version of the elim tactics with specific elimination view
nat2 ind, different from the default one, which is possible using the view tactical /. In
this sense, the “standard induction” elim: n would be equivalent to elim/nat ind: n.
Exercise 6.1. Let us define the binary division function div2 as follows.
Fixpoint div2 (n: nat) := if n is p.+2 then (div2 p).+1 else 0.
Prove the following lemma directly, without using the nat2 ind induction principle.
Lemma div2 le n: div2 n ≤ n.
n : nat
E :n=1
H : beautiful n
============================
False
The way to infer the falsehood will be to proceed by induction on the hypothesis H :
elim: H E⇒n’; do?[by move=>->].
move⇒ n1 m’ H2 H4 → {n’ n}.
Notice how the assumptions n’ and n are removed from the context (since we don’t
need them any more) by enumerating them using {n’ n} notation.
case: n1 H2 =>// n’⇒ H3.
by case: n’ H3 =>//; case.
Qed.
Exercise 6.2. Prove the following theorem about beautiful numbers.
4
In fact, the solution of this simple Diophantine equation are all natural numbers, greater than 7.
6.3 Inductive predicates that are hard to avoid 91
To practice with proofs by induction, let us consider yet another inductive predicate,
borrowed from Pierce et al.’s course and defining which of natural numbers are gorgeous.
Exercise 6.3. Prove by induction the following statements about gorgeous numbers:
Lemma gorgeous plus13 n: gorgeous n → gorgeous (n + 13).
Lemma beautiful gorgeous (n: nat) : beautiful n → gorgeous n.
Lemma g times2 (n: nat): gorgeous n → gorgeous (n × 2).
Lemma gorgeous beautiful (n: nat) : gorgeous n → beautiful n.
As usual, do not hesitate to use the Search utility for finding the necessary rewriting
lemmas from the ssrnat module.
Exercise 6.4 (Gorgeous reflection). Gorgeous and beautiful numbers, defining, in fact,
exactly the same subset of nat are a particular case of Frobenius coin problem, which
asks for the largest integer amount of money, that cannot be obtained using only coins
of specified denominations.5 In the case of beautiful and gorgeous numbers we have
two denominations available, namely 3 and 5. An explicit formula exists for the case of
only two denominations n1 and n2 , which allows one to compute the Frobenius number
as g(n1 , n2 ) = n1 × n2 − n1 − n2 . That said, for the case n1 = 3 and n2 = 5 the Frobenius
number is 7, which means that all numbers greater or equal than 8 are in fact beautiful
and gorgeous (since the two are equivalent, as was established by Exercise 6.3).
In this exercise, we suggest the reader to prove that the efficient procedure of “checking”
for gorgeousness is in fact correct. First, let us defined the following candidate function.
Fixpoint gorgeous b n : bool := match n with
| 1 | 2 | 4 | 7 ⇒ false
| ⇒ true
end.
The ultimate goal of this exercise is to prove the statement reflect (gorgeous n) (gorgeous b
n), which would mean that the two representations are equivalent. Let us divide the proof
into two stages:
• The first stage is proving that all numbers greater or equal than 8 are gorgeous. To
prove this it might be useful to have the following two facts established:
Hint: Use the tactic constructor i to prove a goal, which is an n-ary disjunction, which
is satisfied if its ith disjunct is true.
5
http://en.wikipedia.org/wiki/Frobenius_problem
92 6 Inductive Reasoning in Ssreflect
Lemma repr3 n : n ≥ 8 →
∃ k, [\/ n = 3 × k + 8, n = 3 × k + 9 | n = 3 × k + 10].
Lemma gorg3 n : gorgeous (3 × n).
Next, we can establish by induction the following criteria using the lemmas repr3 and
gorg3 in the subgoals of the proof.
Lemma gorg criteria n : n ≥ 8 → gorgeous n.
This makes the proof of the following lemma trivial.
Lemma gorg refl’ n: n ≥ 8 → reflect (gorgeous n) true.
• In the second stage of the proof of reflection, we will need to prove four totally
boring but unavoidable lemmas.
Hint: The rewriting lemmas addnC and eqSS from the ssrnat module might be particu-
larly useful here.
Lemma not g1 : ˜(gorgeous 1).
Lemma not g2 : ˜(gorgeous 2).
Lemma not g4 : ˜(gorgeous 4).
Lemma not g7 : ˜(gorgeous 7).
We can finally provide prove the ultimate reflection predicate, relating gorgeous and
gorgeous b.
Lemma gorg refl n : reflect (gorgeous n) (gorgeous b n).
Exercise 6.5 (Complete trees). In this exercise, we will consider a binary tree datatype
and several functions on such trees.
Inductive tree : Set :=
| leaf
| node of tree & tree.
A tree is either a leaf or a node with two branches. The height of a leaf is zero, and
height of a node is the maximum height of its branches plus one.
Fixpoint height t :=
if t is node t1 t2 then (maxn (height t1 ) (height t2 )).+1 else 0.
The number of leaves in a node is the total number of leaves in both its branches.
Fixpoint leaves t :=
if t is node t1 t2 then leaves t1 + leaves t2 else 1.
A node is deemed a complete tree if both its branches are complete and have the same
height; a leaf is considered a complete tree.
Fixpoint complete t :=
if t is node t1 t2 then complete t1 && complete t2 && (height t1 == height t2 )
else true.
We can now prove by induction that in a complete tree, the number of leaves is two to
the power of the tree’s height.
Theorem complete leaves height t : complete t → leaves t = 2 ˆ height t.
6.4 Working with Ssreflect libraries 93
mapˆ˜ [:: 1; 2; 3]
: (nat → ?2919) → seq ?2919
6
The same introduction pattern works in fact for any product type with one constructor, e.g., the
existential quantification (see Chapter 3).
94 6 Inductive Reasoning in Ssreflect
last ind
: ∀ (T : Type) (P : seq T → Type),
P [::] →
(∀ (s : seq T ) (x : T ), P s → P (rcons s x)) →
∀ s : seq T, P s
That is, last ind is very similar to the standard list induction principle list ind, except
for the fact that its “induction step” is defined with respect to the rcons function, rather
than the list’s constructor cons. We encourage the reader to check the proof of the list
function properties, such as nth rev or foldl rev to see the reasoning by the last ind
induction principle.
To demonstrate the power of the library for reasoning with lists, let us prove the follow-
ing property, known as Dirichlet’s box principle (sometimes also referred to as pigeonhole
principle), the formulation of which we have borrowed from Chapter MoreLogic of
Pierce et al.’s course [53].
6.4 Working with Ssreflect libraries 95
Variable A : eqType.
Fixpoint has repeats (xs : seq A) :=
if xs is x :: xs’ then (x \in xs’) || has repeats xs’ else false.
The property has repeats is stated over the lists with elements that have decidable
equality, which we have considered in Section 5.3.2. Following the computational ap-
proach, it is a boolean function, which makes use of the boolean disjunction || and Ssre-
flect’s element inclusion predicate \in, which is defined in the module seq.
The following lemma states that for two lists xs1 and xs2, is the size xs2 is strictly
smaller than the size of xs1, but nevertheless xs1 as a set is a subset of xs2 then there
ought to be repetitions in xs1.
Theorem dirichlet xs1 xs2 :
size xs2 < size xs1 → {subset xs1 ≤ xs2 } → has repeats xs1.
Let us go through the proof of this statement, as it is interesting by itself in its intensive
use of Ssreflect’s library lemmas from the seq module.
Proof.
First, the proof scripts initiates the induction on the structure of the first, “longer”,
list xs1, simplifying and moving to the context some hypotheses in the “step” case (as
the nil-case is proved automatically).
elim: xs1 xs2 =>[|x xs1 IH ] xs2 //= H1 H2.
x : A
xs1 : seq A
IH : ∀ xs2 : seq A,
size xs2 < size xs1 → {subset xs1 ≤ xs2 } → has repeats xs1
xs2 : seq A
H1 : size xs2 < (size xs1 ).+1
H2 : {subset x :: xs1 ≤ xs2 }
============================
(x \in xs1 ) || has repeats xs1
Next, exactly in the case of a paper-and-pencil proof, we perform the case-analysis on
the fact (x \in xs1 ), i.e., whether the “head” element x occurs in the remainder of the
list xs1. If it is, the proof is trivial and automatically discharged.
case H3 : (x \in xs1 ) ⇒ //=.
...
H3 : (x \in xs1 ) = false
============================
has repeats xs1
Therefore, we are considering now the situation when x was the only representative of
its class in the original “long” list. For the further inductive reasoning, we will have to
remove the same element from the “shorter” list xs2, which is done using the following
filtering operation (pred1 x checks every element for equality to x and predC constructs
96 6 Inductive Reasoning in Ssreflect
the negation of the passed predicate), resulting in the list xs2’, to which the induction
hypothesis is applied, resulting in two goals
pose xs2’ := filter (predC (pred1 x)) xs2.
apply: (IH xs2’); last first.
...
H2 : {subset x :: xs1 ≤ xs2 }
H3 : (x \in xs1 ) = false
xs2’ := [seq x ← xs2 | (predC (pred1 x)) x0 ] : seq A
============================
{subset xs1 ≤ xs2’}
...
H2 : {subset x :: xs1 ≤ xs2 }
H3 : (x \in xs1 ) = false
xs2’ := [seq x ← xs2 | (predC (pred1 x)) x0 ] : seq A
============================
has (pred1 x) xs2
The remaining goal can be proved by reflecting the boolean proposition has into its
Prop-counterpart exists2 from Ssreflect library. The switch is done using the view hasP,
and the proof is completed by supplying explicitly the existential witness x.
by apply/hasP; ∃ x=>//=; apply: H2 ; rewrite inE eq refl.
Qed.
7 Encoding Mathematical Structures
Long before programming has been established as a discipline, mathematics came to be
perceived as a science of building abstractions and summarizing important properties of
various entities necessary for describing nature’s phenomenons.1 From the basic course
of algebra, we are familiar with a number of mathematical structures, such as monoids,
groups, rings, fields etc., which couple a carrier set (or a number of sets), a number of
operations on it (them), and a collection of properties of the set itself and operations on
them.
From a working programmer’s perspective, a notion of a mathematical abstract struc-
ture is reminiscent to a notion of a class from object-oriented programming, modules
from Standard ML and type classes [64] from Haskell: all these mechanisms are targeted
to solve the same goal: package a number of operations manipulating with some data,
while abstracting of a particular implementation of this data itself. What neither of these
programming mechanisms is capable of doing, comparing to mathematics, is enforcing
the requirement for one to provide the proofs of properties, which restrict the operations
on the data structure. For instance, one can implement a type class for a lattice in Haskell
as follows:
class Lattice a where
bot :: a
top :: a
pre :: a -> a -> Bool
lub :: a -> a -> a
glb :: a -> a -> a
That is, the class Lattice is parametrized by a carrier type a, and provides the
abstract interfaces for top and bottom elements of the lattice, as well as for the order-
ing predicate pre and the binary least-upper-bound and greatest-lower-bound operations.
What this class cannot capture is a number of restrictions, for instance, that the pre
relation should be transitive, reflexive and antisymmetric. That said, one can instantiate
the Lattice class, e.g., for integers, providing an implementation of pre, which is not a
partial order (e.g., just constant true). While this relaxed approach is supposedly fine
for the programming needs, as the type classes are used solely for computing, not the
reasoning about the correctness of the computations, this is certainly unsatisfactory from
the mathematical perspective. Without the possibility to establish and enforce the nec-
essary properties of a mathematical structure’s operations, we would not be able to carry
out any sort of sound formal reasoning, as we simply could not distinguish a “correct”
implementation from a flawed one.
Luckily, Coq’s ability to work with dependent types and combine programs and propo-
sitions about them in the same language, as we’ve already witnessed in the previous
1
In addition to being a science of rewriting, as we have already covered in Chapter 4.
98 7 Encoding Mathematical Structures
2
Sometimes also referred to as an identity or neutral element.
7.1 Encoding partial commutative monoids 99
mixin of is defined
mixin of rect is defined
mixin of ind is defined
mixin of rec is defined
valid op is defined
join op is defined
unit op is defined
The syntax of Coq’s dependent records is reminiscent to the one of records in C.
Following Ssreflect’s naming pattern [20], we call the record type (defined in a dedicated
module for the reasons explained further) mixin of and its only constructor Mixin. The
reasons for such naming convention will be explained soon, and for now let us discuss
the definition. The PCM record type is parametrized over the carrier type T, which
determines the carrier set of a PCM. It then lists three named fields: join op describes an
implementation of the PCM’s binary operation, unit op defines the unit element, finally,
100 7 Encoding Mathematical Structures
the valid op predicate determines whether a particular element of the carrier set T is
valid or not, and, thus, serves as a way to express the partiality of the join op operation
(the result is undefined, whenever the corresponding value of T is non-valid). Next, the
PCM record lists five unnamed PCM properties, which should be satisfied whenever the
record is instantiated and are defined using the standard propositions from Ssreflect’s
ssrfun module (see Section 6.4.1). In particular, the PCM type definition requires the
operation to be commutative and associative. It also states that if a • b 6= ⊥ then a 6= ⊥
(the same statement about b can be proved by commutativity), and that the unit element
is a valid one.
Notice that in the definition of the mixin of record type, the types of some of the later
fields (e.g., any of the properties) depend on the values of fields declared earlier (e.g.,
unit op and join op), which makes mixin of to be a truly dependent type.
Upon describing the record, a number of auxiliary definitions have been generated by
Coq automatically. Along with the usual recursion and induction principles, the system
also generated three getters, valid op, join op and unit op for the record’s named fields.
That is, similarly to Haskell’s syntax, given an instance of a PCM, one can extract, for
example, its operation, via the following getter function.
Check valid op.
valid op
: ∀ T : Type, mixin of T → T → bool
Coq supports the syntax for anonymous record fields (via the underscore ), so getters
for them are not generated. We have decided to make the property fields of mixin of to
be anonymous, since they will usually appear only in the proofs, where the structure is
going to be decomposed by case analysis anyway, as we will soon see.
We can now prove a number of facts about the structure, very much in the spirit of
the facts that are being proven in the algebra course. For instance, the following lemma
states that unit op is also the right unit, in addition to it being the left unit, as encoded
by the structure’s definition.
Lemma r unit T (pcm: mixin of T ) (t: T ) : (join op pcm t (unit op pcm)) = t.
Proof.
case: pcm⇒ join unit Hc Hlu /=.
T : Type
t: T
join : T → T → T
unit : T
Hc : commutative join
Hlu : left id unit join
============================
join t unit = t
The first line of the proof demonstrates that dependent records in Coq are actually just
product types in disguise, so the proofs about them should be done by case analysis. In
this particular case, we decompose the pcm argument of the lemma into its components,
7.1 Encoding partial commutative monoids 101
replacing those of no interest with wildcards . The join and unit, therefore, bind the
operation and the identity element, whereas Hc and Hlu are the commutativity and
left-unit properties, named explicitly in the scope of the proof. The trailing Ssreflect’s
simplification tactical /= replaces the calls to the getters in the goal (e.g., join op pcm)
by the bound identifiers. The proof can be now accomplished by a series of rewritings by
the Hc and Hlu hypotheses.
by rewrite Hc Hlu.
Qed.
a “wrapper” record type, which would “pack” several mix-ins together, similar to how it
is done in object-oriented languages with implicit trait composition, e.g., Scala [47].4
Structure pack type : Type := Pack {type : Type; : mixin of type}.
The dependent data structure pack type declares two fields: the field type of type
Type, which described the carrier type of the PCM instance, and the actual PCM struc-
ture (without an explicit name given) of type (mixin of type). That is, in order to
construct an instance of pack type, one will have to provide both arguments: the carrier
set and a PCM structure for it.
Next, we specify that the field type of the pack type should be also considered as a
coercion, that is, whenever we have a value of type pack type, whose field type is some
T, it can be implicitly seen as an element of type T. The coercion is specified locally,
so it will work only in the scope of the current section (i.e., Packing) by using Coq’s
Local Coercion command. We address the reader to Chapter 18 of the Coq Reference
Manual [10] for more details of the implicit coercions.
Local Coercion type : pack type >-> Sortclass.
The >-> simply specifies the fact of the coercion, whereas Sortclass is an abstract
class of sorts, so the whole command postulates that whenever an instance of pack type
should be coerced into an element of an arbitrary sort, it should be done via referring to
is type field.
Next, in the same section, we provide a number of abbreviations to simplify the work
with the PCM packed structure and prepare it to be exported by clients.
Variable cT : pack type.
Definition pcm struct : mixin of cT :=
let: Pack c := cT return mixin of cT in c.
The function pcm struct extracts the PCM structure from the “packed” instance. No-
tice the use of dependent pattern matching in the let:-statement with the explicit return-
statement, so Coq would be able to refine the result of the whole expression basing on
the dependent type of the c component of the data structure cT, which is being scruti-
nized. With the help of this definition, we can now define three aliases for the PCM’s
key components, “lifted” to the packed data structure.
Definition valid := valid op pcm struct.
Definition join := join op pcm struct.
Definition unit := unit op pcm struct.
End Packing.
Now, as the packaging mechanism and the aliases are properly defined, we come to the
last step of the PCM package description: preparing the batch of definitions, notations
and facts to be exported to the client. Following the pattern of nesting modules, presented
in Section 2.6, we put all the entities to be exported into the inner module Exports.
Module Exports.
Notation pcm := pack type.
4
Using this mechanism will, however, afford us a greater degree of flexibility, as it is up to the Coq
programmer to define the resolution policy of the combined record’s members, rather than to rely on
an implicit mechanism of field linearization.
7.2 Properties of partial commutative monoids 103
Exercise 7.1 (PCM laws). Prove the rest of the PCM laws.
Lemma joinAC (x y z : U ) : x \+ y \+ z = x \+ z \+ y.
Lemma joinCA (x y z : U ) : x \+ (y \+ z) = y \+ (x \+ z).
Lemma validL (x y : U ) : valid (x \+ y) → valid x.
Lemma validR (x y : U ) : valid (x \+ y) → valid y.
Lemma unitL (x : U ) : (@Unit U ) \+ x = x.
Lemma unitR (x : U ) : x \+ (@Unit U ) = x.
Lemma valid unit : valid (@Unit U ).
End PCMLemmas.
End Exports.
End PCMDef.
Export PCMDef.Exports.
can be seen as an instance of the underlying PCM. The coercions are transitive, which
means that the same instance can be coerced even further to U ’s carrier type T.
Coercion pcmT : pack type >-> pcm.
We finish the definition of the cancellative PCM by providing its only important law,
which is a direct consequence of the newly added property.
Lemma cancel (U : cancel pcm) (x y z: U ):
valid (x \+ y) → x \+ y = x \+ z → y = z.
Proof.
by case: U x y z⇒Up [Hc] x y z; apply: Hc.
Qed.
End Exports.
End CancelPCM.
Export CancelPCM.Exports.
The proof of the following lemma, combining commutativity and cancellativity, demon-
strates how the properties of a cancellative PCM work in combination with the properties
of its base PCM structure.
Lemma cancelC (U : cancel pcm) (x y z : U ) :
valid (y \+ x \+ z) → y \+ x = x \+ z → y = z.
Proof.
by move/validL; rewrite ![y \+ ]joinC ; apply: cancel.
Qed.
addition. In the same spirit, the third argument, add0n makes it unambiguous that the
unit element is zero.
After defining the PCM mixin, we can instantiate the PCM packed class for nat by
the following definition:
Definition NatPCM := PCM nat natPCMMixin.
This definition will indeed work, although, being somewhat unsatisfactory. For ex-
ample, assume we want to prove the following lemma for natural numbers treated as
elements of a PCM, which should trivially follow from the PCM properties of nat with
addition and zero:
The term "a" has type "nat" while it is expected to have type "PCMDef.type ?135".
This error is due to the fact that Coq is unable to recognize natural numbers to be
elements of the corresponding PCM, and one possible way to fix it is to declare the
parameters of the lemma add perm, a, b and c to be of type NatPCM rather than nat.
This is still awkward: it means that the lemmas cannot be just applied to mere natural
numbers, instead they need to be coerced to the NatPCM type explicitly whenever we
need to apply this lemma. Coq suggests a better solution to this problem by providing a
mechanism of canonical structures as a flexible way to specify how exactly each concrete
datatype should be embedded into an abstract mathematical structure [57].
The Vernacular syntax for defining canonical structures is similar to the one of def-
initions and makes use of the Canonical command.5 The following definition defines
natPCM to be a canonical instance of the PCM structure for natural numbers.
Canonical natPCM := PCM nat natPCMMixin.
To see what kind of effect it takes, we will print all canonical projections, currently
available in the context of the module.
Print Canonical Projections.
...
nat ← PCMDef.type ( natPCM )
pred of mem ← topred ( memPredType )
pred of simpl ← topred ( simplPredType )
sig ← sub sort ( sig subType )
number ← sub sort ( number subType )
...
The displayed list enumerates all canonical projections that specify, which implicit
canonical instances are currently available and will be picked implicitly for appropriate
types (on the left of the arrow ←). That is, for example, whenever an instance of nat is
available, but in fact it should be treated as the type field of the PCM structure (with all
getters typed properly), the canonical instance natPCM will be automatically picked by
5
The command Canonical Structure serves the same purpose.
7.4 Instantiation and canonical structures 107
Coq for such embedding. In other words, the machinery of canonical structures allows us
to define the policy for finding an appropriate dictionary of functions and propositions
for an arbitrary concrete datatype, whenever it is supposed to have them. In fact, upon
declaring the canonical structure natPCM, the canonical projections are registered by Coq
for all named fields of the record PCM, which is precisely just the type field, since PCM’s
second component of type (mixin of type) was left unnamed (see the definition of the
record pack type on page 102).
The mechanism of defining canonical structures for concrete data types is reminiscent
of the resolution of type class constraints in Haskell [64]. However, unlike Haskell, where
the resolution algorithm for type class instances is hard-coded, in the case of Coq one
can actually program the way the canonical instances are resolved.6 This leads to a
very powerful technique to automate the process of theorem proving by encoding the
way to find and apply necessary lemmas, whenever it is required. These techniques
are, however, outside of the scope of this course, so we direct the interested reader to
the relevant research papers that describe the patterns of programming with canonical
structures [19, 25, 37].
Similarly to the way we have defined a canonical instance of PCM for nat, we can
define a canonical instance of a PCM with cancellativity. In order to instantiate it, we
will, however, need to prove the following lemma, which states that the addition on
natural numbers is indeed cancellative, so this fact will be used as an argument for the
CancelPCMMixin constructor.
Lemma cancelNat : ∀ a b c: nat, true → a + b = a + c → b = c.
Proof.
move⇒ a b c; elim: a=>// n /( is true true) Hn H.
by apply: Hn; rewrite !addSn in H ; move/eq add S : H.
Qed.
Notice the first assumption true of the lemma. Here it serves as a placeholder for the
general validity hypothesis valid (a \+ b), which is always true in the case of natural
numbers.
Definition cancelNatPCMMixin := CancelPCMMixin cancelNat.
Canonical cancelNatPCM := CancelPCM natPCM cancelNatPCMMixin.
Let us now see the canonical instances in action, so we can prove a number of lemmas
about natural numbers employing the general PCM machinery.
Section PCMExamples.
Variables a b c: nat.
Goal a \+ (b \+ c) = c \+ (b \+ a).
by rewrite joinA [c \+ ]joinC [b \+ ]joinC.
Qed.
The next goal is proved by using the combined machinery of PCM and CancelPCM.
Goal c \+ a = a \+ b → c = b.
6
In addition to canonical structures, Coq also provides mechanism of type classes, which are even more
reminiscent of the ones from Haskell, and, similar to the latter ones, do not provide a way to program
the resolution policy [59].
108 7 Encoding Mathematical Structures
Exercise 7.2 (Partially ordered sets). A partially ordered set order is a pair (T, v), such
that T is a set and v is a (propositional) relation on T , such that
1. ∀x ∈ T, x v x (reflexivity);
2. ∀x, y ∈ T, x v y ∧ y v x =⇒ x = y (antisymmetry);
3. ∀x, y, z ∈ T, x v y ∧ y v z =⇒ x v z (transitivity).
Implement a data structure for partially-ordered sets using mixins and packed classes.
Prove the following laws:
Exercise 7.3 (Canonical instances of partially ordered sets). Provide canonical instances
of partially ordered sets for the following types:
In order to provide a canonical instance for functions, you will need to assume and
make use of the following axiom of functional extensionality:
Axiom fext : ∀ A (B : A → Type) (f1 f2 : ∀ x, B x),
(∀ x, f1 x = f2 x) → f1 = f2.
7.4 Instantiation and canonical structures 109
Module Equality.
...
End Equality.
That is, the mixin for equality is a dependent record, whose first field is a relation
op on a particular carrier type T (defined internally as a function T × T → bool),
and the second argument is a proof of the definition axiom, which postulates that the
relation is in fact equivalent to propositional equality (which is established by means of
inhabiting the reflect predicate instance). Therefore, in order to make a relation op to
be a decidable equality on T, one needs to prove that, in fact, it is equivalent to the
standard, propositional equality.
Subsequently, Ssreflect libraries deliver the canonical instances of the decidable equality
structure to all commonly used concrete datatypes. For example, the decidable equal-
ity for natural numbers is implemented in the ssrnat module by the following recursive
function:7
end.
The following lemma ensures that eqn correctly reflects the propositional equality.
In this chapter, we will consider a fairly large case study that makes use of most of Coq’s
features as a programming language with dependent types and as a framework to build
proofs and reason about mathematical theories.
Programming language practitioners usually elaborate on the dichotomy between declar-
ative and imperative languages, emphasizing the fact that a program written in a declar-
ative language is pretty much documenting itself, as it already specifies the result of a
computation. Therefore, logic and constraint programming languages (such as Prolog [36]
or Ciao [28]) as well as data definition/manipulation languages (e.g., SQL), whose pro-
grams are just sets of constraints/logical clauses or queries describing the desired result,
are naturally considered to be declarative. Very often, pure functional programming
languages (e.g., Haskell) are considered as declarative as well. The reason for this is
the referential transparency property, which ensures that programs in such languages are
in fact effect-free expressions, evaluating to some result (similar to mathematical func-
tions) or diverging. Therefore, such programs, whose outcome is only a value, but not
some side effect (e.g., output to a file), can be replaced safely by their result, if it is
computable. This possibility provides a convenient way of reasoning algebraically about
such programs by means of equality rewritings—precisely what we were observing and
leveraging in Chapters 4 and 6 of this course in the context of Coq taken as a functional
programming language.
That said, pure functional programs tend to be considered to be good specifications for
themselves. Of course, the term “specification” (or simply, “spec”) is overloaded and in
some context it might mean the result of the program, its effect or some of the program’s
algebraic properties. While a functional program is already a good description of its result
(due to referential transparency), its algebraic properties (e.g., some equalities that hold
over it) are usually a subject of separate statements, which should be proved [4]. Good
examples of such properties are the commutativity and cancellation properties, which we
proved for natural numbers with addition, considered as an instance of PCM on page 107
of Chapter 7. Another classical series of examples, which we did not focus on in this
course, are properties of list functions, such as appending and reversal (e.g., that the list
112 8 Case Study: Program Verification in Hoare Type Theory
The reservation on termination of the program c is important. In fact, while the Hoare
triples in their simple form make sense only for terminating programs, it is possible to
specify non-terminating programs as well. This is due to the fact that the semantics of
a Hoare triple implies that a non-terminating program can be given any postcondition,
as one won’t be able to check it anyway, because the program will never reach the final
state.3 Such interpretation of a Hoare triple “modulo termination” is referred to as partial
correctness, and in this chapter we will focus on it. It is possible to give to a Hoare
triple {P } c {Q} a different interpretation, which would deliver a stronger property: “if
right before the program c is executed the state of mutable variables is described by
a proposition P , then c terminates and the resulting state satisfies the proposition Q”.
Such property is called total correctness and requires tracking some sort of “fuel” for the
program in the assertions, so it could run further. We do not consider total correctness
in this course and instead refer the reader to the relevant research results on Hoare-style
specifications with resource bounds [16].
{true} x := 3 {x = 3}
That is, the program’s precondition doesn’t make any specific assumptions, which is
expressed by the proposition true; the postcondition ensures that the value of a mutable
variable x is equal to three.
The formalism, which allows us to validate particular Hoare triples for specific programs
is called program logic (or, equivalently, Hoare logic).
Intuitively, logic in general is a formal system, which consists of axioms (propositions,
whose inhabitance is postulated) and inference rules, which allow one to construct proofs
of larger propositions out of proofs of small ones. This is very much of the spirit of
Chapter 3, where we were focusing on a particular formalism—propositional logic. Its
inference rules were encoded by means of Coq’s datatype constructors. For instance, in
order to construct a proof of conjunction (i.e., inhabit a proposition of type A ∧ B), one
should have provided a proof of a proposition A and a proposition B and then apply the
only conjunction’s constructor conj, as described in Section 3.4. The logicians, however,
prefer to write inference rules as “something with a bar”, rather than as constructors.
Therefore, an inference rule for conjunction introduction in the constructive logic looks
as follows:
A B
(∧-Intro)
A∧B
3
This intuition is consistent with the one, enforced by Coq’s termination checker, which allows only
terminating programs to be written, since non-terminating program can be given any type and
therefore compromise the consistency of the whole underlying logical framework of CIC.
114 8 Case Study: Program Verification in Hoare Type Theory
That is, the rule (∧-Intro) is just a paraphrase of the conj constructor, which speci-
fies how an instance of conjunction can be created. Similarly, the disjunction or has two
inference rules, for each of its constructors. The elimination rules are converses of the
introduction rules and formalize the intuition behind the case analysis. An alternative
example of an inference rule for a proposition encoded by means of Coq’s datatype con-
structor is the definition of the predicate for beautiful numbers beautiful from Section 6.3.
There, the constructor b sum serves as an inference rule that, given the proofs that n’ is
beautiful and m’ is beautiful, constructs the proof of the fact that their sum is beautiful.4
Hoare logic also suggests a number of axioms and inference rules that specify which
Hoare triple can in fact be inferred. We postpone the description of their encoding by
means of Coq’s datatypes till Section 8.4 of this chapter and so far demonstrate some of
them in the logical notation “with a bar”. For example, the Hoare triple for a variable
assignment is formed by the following rule:
The rule (Assign) is in fact an axiom (since it does not assume anything, i.e., does not
take any arguments), which states that if a proposition Q is valid after substituting all
occurrences of x in it with e (which is denoted by [e/x]), then it is a valid postcondition
for the assignment x := e.
The inference rule for sequential composition is actually a constructor, which takes the
proofs of Hoare triples for c1 and c2 and then delivers a composed program c1 ; c2 as well
as the proof for the corresponding Hoare triple, ensuring that the postcondition of c1
matches the precondition of c2 .
The rule (Seq) is in fact too “tight”, as it requires the two composed program agree
exactly on their post-/preconditions. In order to relax this restriction, on can use the rule
of consequence, which makes it possible to strengthen the precondition and weaken the
postcondition of a program. Intuitively, such rule is adequate, since the program that is
fine to be run in a precondition P 0 , can be equivalently run in a stronger precondition P
(i.e., the one that implies P 0 ). Conversely, if the program terminates in a postcondition
Q0 , it would not hurt to weaken this postcondition to Q, such that Q0 implies Q.
P =⇒ P 0 {P 0 } c {Q0 } Q0 =⇒ Q
(Conseq)
{P } c {Q}
4
Actually, some courses on Coq introduce datatype constructors exactly from this perspective—as a
programming counterpart of the introduction rules for particular kinds of logical propositions [53].
We came to the same analogy by starting from an opposite side and exploring the datatypes in the
programming perspective first.
8.1 Imperative programs and their specifications 115
With this respect, we can make the analogy between Hoare triples and function types
of the form A → B, such that the rule of consequence of a Hoare triple corresponds to
subtyping of function types, where the precondition P is analogous to an argument type
A and the postcondition Q is analogous to a result type B. Similarly to the functions with
subtyping, Hoare triples are covariant with respect to consequence in their postcondition
and contravariant in the precondition [52, Chapter 15]. This is the reason why, when
establishing a specification, one should strive to infer the weakest precondition and the
strongest postcondition to get the tightest possible (i.e., the most precise) spec, which can
be later weakened using the (Conseq) rule.
The observed similarity between functions and commands in a Hoare logic should serve
as an indicator that, perhaps, it would be a good idea to implement the Hoare logic in a
form of a type system. Getting a bit ahead of ourselves, this is exactly what is going to
happen soon in this chapter (as the title of the chapter suggests).
At this point, we can already see a simple paper-and-pencil proof of a program that
manipulates mutable variables. In the Hoare logic tradition, since most of the programs
are typically compositions of small programs, the proofs of specifications are written
to follow the structure of the program, so the first assertion corresponds to the overall
precondition, the last one is the overall postcondition, and the intermediate assertions
correspond to R from the rule (Seq) modulo weakening via the rule of consequence
(Conseq). Let us prove the following Hoare-style specification for a program that swaps
the values of two variables x and y.
{x = a ∧ y = b} t := x; x := y; y := t {x = b ∧ y = a}
The variables a and b are called logical and are used in order to name unspecified
values, which are a subject of manipulation in the program, and their identity should be
preserved. The logical variables are implicitly universally quantified over in the scope of
the whole Hoare triple they appear, but usually the quantifiers are omitted, so, in fact,
the specification above should have been read as follows.
∀ a b, {x = a ∧ y = b} t := x; x := y; y := t {x = b ∧ y = a}
This universal quantification should give some hints that converting Hoare triples into
types will, presumably, require to make some use of dependent types in order to express
value-polymorphism, similarly to how the universal quantification has been previously
used in Coq. Let us see a proof sketch of the above stated specification with explanations
of the rules applied after each assertion.
{x = a ∧ y = b} The precondition
t := x;
{x = a ∧ y = b ∧ t = a} by (Assign) and equality
x := y;
{x = b ∧ y = b ∧ t = a} by (Assign) and equality
y := t
{x = b ∧ y = a} by (Assign) equality and weakening via (Conseq)
The list of program constructs and inference rules for them would be incomplete without
conditional operators and loops.
116 8 Case Study: Program Verification in Hoare Type Theory
{I ∧ e} c {I}
(While)
{I} while e do c {I ∧ ¬e}
The inference rule for a conditional statement should be intuitively clear and reminds
of a typing rule for conditional expressions in Haskell or OCaml, which requires both
branches of the statement to have the same type (and here, equivalently, to satisfy the
same postcondition). The rule (While) for the loops is more interesting, as it makes use
of the proposition I, which is called loop invariant. Whenever the body of the cycle is
entered, the invariant should hold (as well as the condition e, since the iteration has just
started). Upon finishing, the body c should restore the invariant, so the next iteration
would start in a consistent state again. Generally, it takes a human prover’s intuition to
come up with a non-trivial resource invariant for a loop, so it can be used in the rest of the
program. Inference of the best loop invariant is an undecidable problem in general and it
has a deep relation to type inference with polymorphically-recursive functions [27]. This
should not be very surprising, since every loop can be encoded as a recursive function,
and, since, as we have already started guessing, Hoare triples are reminiscent of types,
automatic inferring of loop invariants would correspond to type inference for recursive
functions. In the subsequent sections we will see examples of looping/recursive programs
with loop invariants and exercise in establishing some of them.
different ways, and the nature of the proof usually depends on the underlying opera-
tional/denotational semantics, which is typically not questioned, being self-obvious, and
defines precisely what does it mean for a program to be executed. Traditional ways of
proving soundness of a program logic are reminiscent to the approaches for establishing
soundness of type systems [52, 68]. Of course, all program logics discussed in this chapter
have been proven to be sound with respect to some reasonable operational/denotational
semantics.
{x 7→ − ∧ y 7→ Y } x ::= 5 {x 7→ 5 ∧ y 7→ Y }
The logical variable Y is of importance, as it is used to state that the value of the
118 8 Case Study: Program Verification in Hoare Type Theory
pointer y remains unchanged after the program has terminated.5 Alas, this specification
is not correct, as the conjunction of the two does not distinguish between the case when
x and y are the same pointer and when they are not, which is precisely the aliasing
problem. It is not difficult to fix the specification for this particular example by adding a
conditional statement (or, equivalently, a disjunction) into the postcondition that would
describe two different outcomes of the execution with respect to the value of y, depending
on the fact whether x and y are aliases or not. However, if a program manipulates with
a large number of pointers, or, even worse, with an array (which is obviously just a
sequential batch of pointers), things will soon go wild, and the conditionals with respect
to equality or non-equality of certain pointers will pollute all the specifications, rendering
them unreadable and eventually useless. This was precisely the reason, why after being
discovered in late ’60s and investigated for a decade, Hoare-style logics were soon almost
dismissed as a specification and verification method, due to the immense complexity of the
reasoning process and overwhelming proof obligations. The situation has changed when in
2002 John C. Reynolds, Peter O’Hearn, Samin Ishtiaq and Hongseok Yang suggested an
alternative way to state Hoare-style assertions about heap-manipulating programs with
pointers [55]. The key idea was to make explicit the fact of disjointness (or, separation)
between different parts of a heap in the pre- and postconditions. This insight made it
possible to reason about disjointness of heaps and absence of aliasing without the need to
emit side conditions about equality of pointers. The resulting formal system received the
name separation logic, and below we consider a number of examples to specify and verify
programs in it. For instance, the program, shown above, which assigns 5 to a pointer x
can now be given the following specification in the separation logic:
{h | h = x 7→ − • y 7→ Y } x ::= 5 {res, h | h = x 7→ 5 • y 7→ Y }
We emphasize the fact that the heaps, being just partial maps from natural numbers
to arbitrary values, are elements of a PCM (Section 7.1) with the operation • taken to be
a disjoint union and the unit element to be an empty heap (denoted empty). The above
assertions therefore ensure that, before the program starts, it operates in a heap h, such
that h is a partial map, consisting of two different pointers, x and y, such that y points
to some universally-quantified value Y , and the content of x is of no importance (which
is denoted by -). The postcondition makes it explicit that only the value of the pointer
x has changed, and the value of y remained the same. The postcondition also mentions
the result res of the whole operations, which is, however, not constrained anyhow, since,
as it has been stated, it is just a value of type unit.6
5
We will abuse the terminology and refer to the values and immutable local variables uniformly, as,
unlike the setting of Section 8.1, the latter ones are assumed to be substituted by the former ones
during the evaluation anyway.
6
The classical formulation of Separation Logic [55] introduces the logical connective ∗, dubbed separating
conjunction, which allows to describe the split of a heap h into two disjoint parts without mentioning
h explicitly. That is, the assertion P ∗ Q holds for a heap h, if there exist heaps h1 and h2 , such that
h = h1 • h2 , P is satisfied by h1 and Q is satisfied by h2 . We will stick to the “explicit” notation,
though, as it allows for greater flexibility when stating the assertions, mixing both heaps and values.
8.2 Basics of Separation Logic 119
Notice, though, that, unlike the original Hoare logic for mutable variables, the rule
for writing explicitly requires the pointer x to be present in the heap. In other words,
the corresponding memory cell should be already allocated. This is why the traditional
separation logic assumes presence of an allocator, which can allocate new memory cells
and dispose them via the effectful functions alloc() and dealloc(), correspondingly.
For the sake of demonstration, the rules for alloc() and dealloc() are given in a
large footprint that, in contrast with small footprint-like specifications, mentions the
“additional” heap h0 in the pre- and post-conditions, which can be arbitrarily instan-
tiated, emphasizing that it remains unchanged (recall that h0 is implicitly universally-
quantified over, and its scope is the whole triple), so the resulting heap is just being
“increased”/“decreased” by a memory entry that has been allocated/deallocated.7 The
rule for binding is similar to the rule for sequential composition of programs c1 and c2
from the standard Hoare logic, although it specifies that the immutable variables can be
substituted in c2 .
The predicates P , Q and R in the rule (Bind) are considered to be functions of the
heap and result, correspondingly. This is why for the second program, c2 , the predicate
Q in a precondition is instantiated with x, which can occur as a free variable in c2 . The
rule of weakening (Conseq) is similar to the one from Hoare logic modulo the technical
details on how to weaken heap/result parametrized functions, so we omit it here as an
intuitive one. The rule for conditional operator is the same one as in Section 8.1.1, and,
hence, is omitted as well. In order to support procedures in separation logic, we need to
consider two additional rules—for function invocation and returning a value.
7
The classical separation logic provides a so-called frame rule, which allows for the switch between the
two flavours of footprint by attaching/removing the additional heap h0 . In our reasoning we will be
assuming it implicitly.
120 8 Case Study: Program Verification in Hoare Type Theory
The rule for returning simply constraints the dedicated variable res to be equal to
the expression e. The rule (Hyp) (for “hypothesis”) introduces the assumption context
Γ that contains specifications of available “library” functions (bearing the reminiscence
with the typing context in typing relations [52, Chapter 9]) and until now was assumed
to be empty. Notice that, similarly to dependently-typed functions, in the rule (Hyp)
the pre- and postcondition in the spec of the assumed function can depend on the value
of its argument x. The rule (App) accounts for the function application and instantiates
all occurrences of x with the argument expression e. Finally, sometimes we might be able
to infer two different specifications about the same program. In this case we should be
able to combine them into one, which is stronger, and this is what the rule of conjunction
(Conj) serves for:
while (e) do c
can be rewritten using a recursive function, defined via the in-place fixpoint operator as
That is, the function f is defined with an argument of the bool type and is immediately
invoked. If the condition argument x is satisfied, the body c is executed and the function
calls itself recursively with a new argument e0 ; otherwise the function just returns a unit
8
Although, such programs can be made tail-recursive via the continuation-passing style transformation
(CPS) [15]. They can be also converted into imperative loops via the subsequent transformation,
known as defunctionalization [54].
8.2 Basics of Separation Logic 121
result. For the first time, the function is invoked with some initial argument e. Given this
relation between imperative loops and effectful recursive functions, we won’t be providing
a rule for loops in separation logic at all, and rather provide one for recursive definitions.
Γ, ∀x, {h | P (x, h)} f (x) {res, h | Q(x, res, h)} ` {h | P (x, h)} c {res, h | Q(x, res, h)}
(Fix)
Γ ` ∀y, {h | P (y, h)} (fix f (x).c)(y) {res, h | Q(y, res, h)}
The premise of the rule (Fix) already assumes the specification of a function f (i.e.,
its loop invariant) in the context Γ and requires one to verify its body c for the same
specification, similarly to how recursive functions in some programming languages (e.g.,
Scala [46, § 4.1]) require explicit type annotations to be type-checked. In the remainder
of this chapter we will be always implementing imperative loops via effectful recursive
functions, whose specifications are stated explicitly, so the rule above would be directly
applicable.
The function fact first allocates two pointers, n and acc for the iteration variable
and the accumulator, correspondingly. It will then initiate the loop, implemented by
the recursive function loop, that reads the values of n and acc into local immutable
variables n’ and a’, correspondingly and then checks whether n’ is zero, in which case
it returns the value of the accumulator. Otherwise it stores into the accumulator the old
122 8 Case Study: Program Verification in Hoare Type Theory
value multiplied by n’, decrements n and re-iterates. After the loop terminates, the two
pointers are deallocated and the main function returns the result. Our goal for the rest
of this section will be to verify this program semi-formally, using the rules for separation
logic presented above, against its functional specification. In other words, we will have to
check that the program fact returns precisely the factorial of its argument value N . To
give such specification to fact, we define two auxiliary mathematical functions, f and
Finv :
f (N ) =
b if N = N 0 + 1 then N × f (N 0 ) else 1
Finv (n, acc, N, h) =
b ∃n0 , a0 , (h = n 7→ n0 • acc 7→ a0 ) ∧ (f (n0 ) × a0 = f (N ))
It is not difficult to see that f defines exactly the factorial function as one would define
it in a pure functional language (not very efficiently, though, but in the most declarative
form). The second function Finv is in fact a predicate, which we will use to give the loop
invariant to the loop function loop. Now, the function fact can be given the following
specification in separation logic, stating that it does not leak memory and its result is
the factorial of its argument N .
{h | Finv (n, acc, N, h)} loop(tt) {res, h | Finv (n, acc, N, h) ∧ res = f (N )}
Below, we demonstrate a proof sketch of verification of the body of fact against its
specification by systematically applying all of the presented logic rules.
Probably, the most tricky parts of the proof, which indeed require a human prover’s
insight, are (a) “decomposition” of the loop invariant Finv at the beginning of the loop,
when it falls into the components, constraining the values of n and acc in the heap
and (b) the “re-composition” of the same invariant immediately before the recursive call
of loop in order to ensure its precondition. The latter is possible because of algebraic
properties of the factorial function f , namely the fact that for any n, if n > 0 then
f (n) × a = f (n − 1) × n × a, the insight we have used in order to “re-distribute” the
values between the two pointers, n and acc so the invariant Finv could be restored.
It should be clear by this moment, that, even though the proof is proportional to the
size of the program, it has combined some mathematical reasoning with a machinery of
consistent rule application, until the postcondition has been reached, which, when done
by a human solely, might be an error-prone procedure. Nevertheless, this proof process is
very reminiscent to the proofs that we have seen so far in Coq, when one gradually applies
the lemmas, assumptions and performs rewritings until the final goal is proved. This is
why using Coq seems like a good idea to mechanize the process of proofs in separation
logic, so one can be sure that there is nothing missed during the reasoning process and the
specification is certainly correct. Employing Coq for this purpose is indeed our ultimate
goal and the topic of this chapter. However, before we reach that point, let us recall that
in a nutshell Coq is in fact a functional programming language and make yet another
short detour to the world of pure functional programming, to see how effects might be
specified by means of types.
result and the ultimate outcome may produce some irreversible effect (e.g., mutating
references, throwing exceptions, performing output or reading from input), which one
should account for. Hoare logics, and, in particular, separation logic focus on specifying
effectful programs taking expressions for granted and assuming their referential trans-
parency, which makes it not entirely straightforward to embed such reasoning into the
purely functional setting of the Coq framework. It has been a long-standing problem
for the functional programming community to reconcile the pure expressions, enjoying
referential transparency, with effectful computations, until Eugenio Moggi suggested to
use the mechanism of monads to separate the results of computations from the possible
effects they can produce [40], and Philip Wadler popularized this idea with a large num-
ber of examples [63], as it was adopted in the same time by the Haskell programming
language. There is a countless number of tutorials written and available on the Web that
are targeted to help building the intuition about the “monad magic”. Although grasping
some essence of monadic computations is desirable for understanding how verification of
the imperative programs can be structured in Coq, providing the reader with yet another
“monad tutorial” is not the task of this course. Luckily, in order to proceed to the ver-
ification in separation logic, which is the topic of this chapter, we need only very basic
intuition on what monads are, and how they are typically used to capture the essence of
computations and their effects.
• Binding (i.e., a program of the form x ← c1 ; c2 ) is a way to specify that the effect
of the computation c1 takes place strictly before the computation c2 is executed.
Following its name this program constructor also performs binding of the (pure)
result of the first computation, so it can be substituted to all occurrences of x in
the second command, c2 . In this sense, binding is different from expressions of the
form let x = e1 in e2, omnipresent in functional programs, as the latter ones
might allow for both strict and lazy evaluation of the right-hand side expression
e1 depending on a semantics of the language (e.g., call-by-value in Standard ML
vs. call-by-need in Haskell). This flexibility does not affect the result of a pure
program (modulo divergence), since e1 and e2 are expressions, and, hence, are
pure. However, in the case of computations, the order should be fixed and this is
what the binding construct serves for.
• Returning a value is a command constructor (which we typeset as ret), which allows
one to embed a pure expression into the realm of computations. Again, intuitively,
this is explained by the fact that expressions and commands should be distinguished
semantically,9 but sometimes an expression should be treated as a command (with
9
Although some mainstream languages prefer to blur the distinction between commands and expressions
in order to save on syntax [46], at the price of losing the ability to differentiate statically between the
effectful and pure code.
8.3 Specifying effectful computations using types 125
a trivial effect or none of it at all), whose result is the very same expression.
These two connectives, allowing one to construct the programs by means of binding and
embedding expressions into them are captured precisely by the Monad interface, expressed,
for instance, in Haskell via the following type class:
The signature specifies that each instance of Monad m is parametrized by one type
and requires two functions to be implemented. The »= function is pronounced as bind
and describes how a particular monad instance combines two computations, such that
the second one, whose type is m b, may depend on the value of result of the first one,
whose type is m a. The result of the overall computation is then the one of the second
component, namely, m b. The function return specifies how to provide a “default” value
for an effectful computation, i.e., how to “pair” a value of type a with an “effect” entity
in order to receive an element of m a. In this specification, the type m serves as a generic
placeholder of the effect, whose nature is captured by the monad. As it has been already
pointed out, such effect might be a mutable state, exceptions, explicit control, concurrency
or input/output (all captured by specific instances of monads in Haskell [48]), as well as
the fact of program non-termination (i.e., divergence), which Haskell deliberately does
not capture. In a more informal language, the monadic type m indicates that in the
program “something fishy is going on, besides the result being computed”, so this type
serves as a mechanism, which is used by the type checker to make sure that only programs
with the same effect are composed together by means of binding (hence the type of the
bind operator in the Monad type class). This is an important insight, which will be
directly used in the design of the verification methodology of imperative programs using
dependent types, as we will see in Section 8.4.
The computations involved in the program, are represented, in particular, by the Haskell
commands (i.e., monadically-typed function call) putStrLn "Enter a character", which
prints a string to the output stream, and the call to getChar, which reads a caracter from
the input stream. All these computations are bound using the <- syntax and do-notation,
and the last one returns an embedded unit value (), so the type of the whole program
main is inferred to be IO ().
• Hoare specifications in separation logic behave like types of the computations they
specify, which is witnessed by the rules of weakening (Conseq), function and
application specification inference (Hyp) and (App) and recursive functions (Fix)
(Section 8.2.1). Moreover, since pre- and postconditions can depend on the values
of logical universally-quantified variables as well as on the values of the command’s
arguments, Hoare-style specs are in fact instances of dependent types.
• Hoare triples in separation logic specify effectful computations that are composed
using the binding mechanism, with pure expressions being injected into them by
means of “wrapping” them with a ret operator. This makes Hoare triples behave
exactly like instances of monads from functional programming, whose composition
is described by, e.g., the Monad type class from Haskell.
• Effectful computations can take effects, which should be accounted for in their
specifications. The effects (or observation of an effectful state) are due to some
dedicated operations, such as pointer assignment, pointer reading, allocation or
deallocation. These operations come with dedicated specifications, similarly to how
operations putStrLn and getChar in Haskell are typed with respect to the IO
monad, whose state they modify.
• Another important effect, which has no explicit handling in the mainstream pro-
gramming languages like Haskell, but should be dealt with in the context of pure,
strongly-normalizing language of Coq, is divergence. We cannot allow one to have
potentially non-terminating computations as expressions in Coq (i.e., those imple-
mented by means of the general recursion operator fix from Section 8.2.2), but we
can afford having a monadic type of computations such that they might possibly
diverge if they are executed (and, even though, they will not be executed within
Coq, they can still be type-checked, and, hence, verified). Therefore, monadic en-
coding of the fixpoint operator provides a way to escape the termination-checking
conundrum and encode nonterminating programs in Coq.
8.4 Elements of Hoare Type Theory 127
All these observation resulted in a series of works on Hoare Type Theory (or just HTT),
which defines a notion of an indexed Hoare monad (or, Hoare type) as a mechanism
to encode Hoare-style specifications as dependent types and reduce the verification of
effectful progress to proving propositions in Coq [41–43]. In the rest of this chapter we
will consider a number of important concepts of HTT, so the necessary modules should be
imported from the library folder htt, which contains the compiled files (see Section 1.3.3
for the instructions on obtaining and building HTT from the sources).
From mathcomp
Require Import ssreflect ssrbool ssrnat eqtype seq ssrfun.
From fcsl
Require Import prelude pred pcm unionmap heap.
From HTT
Require Import stmod stsep stlog stlogR.
Module HTT.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
10
A curious reader can take a look at the definitions in the module stmod of the HTT library.
128 8 Case Study: Program Verification in Hoare Type Theory
tations used and essentially postulates that from the proposition, corresponding to the
specification inferred by Coq from the program definition, we should be able to prove the
specification that we have declared explicitly. Instead of explaining each component of
the goal, we will proceed directly to the proof and will build the necessary intuition as we
go. The proof mode for each of the remaining obligations is activated by the Vernacular
command Next Obligation, which automatically moves some of the assumptions to the
context.
Next Obligation.
A : Type
x : ptr
v: A
============================
conseq (x ::= v)
(logvar
(fun y : ptr ⇒
logvar
(fun Y : nat ⇒
binarify
(fun h : heap ⇒
exists (B : Type) (w : B), h = x :-> w \+ y :-> Y )
[vfun h ⇒ h = x :-> v \+ y :-> Y ])))
A usual first step in every HTT proof, which deals with a spec with logical variables is
to “pull them out”, so they would just become simple assumptions in the goal, allowing
one to get rid of the logvar and binarify calls in the goal.11 This is what is done by
applying the lemma ghR to the goal.
apply: ghR.
A : Type
x : ptr
v: A
============================
∀ (i : heap) (x0 : ptr × nat),
(exists (B : Type) (w : B), i = x :-> w \+ x0.1 :-> x0.2) →
valid i → verify i (x ::= v) [vfun h ⇒ h = x :-> v \+ x0.1 :-> x0.2]
We can now move a number of assumptions, arising from the “brushed” specification,
to the context, along with some rewriting by equality and simplifications.
11
In fact, the proper handling of the logical variables is surprisingly tricky in a type-based encoding,
which is what HTT delivers. It is due to the fact that the same variables can appear in both pre- and
postconditions. Earlier implementations of HTT used binary postconditions for this purpose [42, 43],
which was a cause of some code duplication in specifications and made the spec look differently from
those that someone familiar with the standard Hoare logic would expect. Current implementation
uses an encoding with recursive notations to circumvent the code duplication problem. This encoding
is a source of the observed occurrences of logvar and binarify definitions in the goal.
130 8 Case Study: Program Verification in Hoare Type Theory
...
B : Type
w: B
============================
verify (x :-> w \+ y :-> Y ) (x ::= v) [vfun h ⇒ h = x :-> v \+ y :-> Y ]
The resulting goal is stated using the verify-notation, which means that in this partic-
ular case, in the heap of the shape x :-> w \+ y :-> Y we need to be able to prove that
the result and the produced heap of the command x ::= v satisfy the predicate [vfun
h ⇒ h = x :-> v \+ y :-> Y ]. This goal can be proved using one of the numerous ver-
ify-lemmas that HTT provides (try executing Search (verify ) to see the full list),
however in this particular case the program and the goal are so simple and are obviously
correct that the statement can be proved by means of proof automation, implemented in
HTT by a brute-force tactic heval, which just tries a number of verify-lemmas applicable
in this case modulo the shape of the heap.
by heval.
Qed.
[vfun (res : nat) h ⇒ fact inv n acc N h ∧ res = fact pure N ]).
The type fact tp ensures additionally that the resulting value is in fact a factorial of
N, which is expressed by the conjunct res = fact pure N. The definition of the factorial
“accumulator” loop is then represented as a recursive function, taking as arguments the
two pointers, n and acc, and also a unit value. The body of the function is defined
using the monadic fixpoint operator Fix, whose semantics is similar to the semantics of
the classical Y-combinator, defined usually by the equation Y f = f (Y f ), where f is
a fixpoint operator argument that should be thought of as a recursive function being
defined. Similarly, the fixpoint operator Fix, provided by HTT, takes as arguments a
function, which is going to be called recursively (loop, in this case), its argument and
body. The named function (i.e., loop) can be then called from the body recursively. In
the similar spirit, one can define nested loops in HTT as nested calls of the fixpoint
operator.
Program Definition fact acc (n acc : ptr): fact tp n acc :=
Fix (fun (loop : fact tp n acc) ( : unit) ⇒
Do (a1 < −− read nat acc;
n’ < −− read nat n;
if n’ == 0 then ret a1
else acc ::= a1 × n’;;
n ::= n’ - 1;;
loop tt)).
The body of the accumulator loop function reproduces precisely the factorial imple-
mentation in pseudocode from page 121. It first reads the values of the pointers acc and
n into the local variables a1 and n’. Notice that the binding of the local immutable
variables is represented by the < −− notation, which corresponds to the bind operation
of the Hoare monad STsep. The function then uses Coq’s standard conditional operator
and returns a value of a1 if n’ is zero using the monadic ret operator. In the case of else-
branch, the new values are written to the pointers acc and n, after which the function
recurs. Stating the looping function like this leaves us with one obligation to prove.
Next Obligation.
As in the previous example, we start by transforming the goal, so the logical variable
N, coming from the specification of fact tp would be exposed as an assumption. We
immediately move it to the context along with the initial heap i.
apply: ghR⇒i N.
...
i : heap
N : nat
============================
fact inv n acc N i →
valid i →
verify i
(a1 < −− ! acc;
n’ < −− ! n;
132 8 Case Study: Program Verification in Hoare Type Theory
(if n’ == 0 then ret a1 else acc ::= a1 × n’;; n ::= n’ - 1;; loop tt))
[vfun res h ⇒ fact inv n acc N h ∧ res = fact pure N ]
We next case-analyse on the top assumption with the invariant fact inv to acquire the
equality describing the shape of the heap i. We then rewrite i in place and move a number
of hypotheses to the context.
case⇒n’ [a’][->{i}] Hi .
Now the goal has the shape verify (n :-> n’ \+ acc :-> a’) ..., which is suitable to be
hit with the automation by means of the heval tactic, progressing the goal to the state
when we should reason about the conditional operator.
heval.
...
n’ : nat
a’ : nat
Hi : fact pure n’ × a’ = fact pure N
============================
verify (n :-> n’ \+ acc :-> a’)
(if n’ == 0 then ret a’ else acc ::= a’ × n’;; n ::= n’ - 1;; loop tt)
[vfun res h ⇒ fact inv n acc N h ∧ res = fact pure N ]
The goal, containing a use of the conditional operator, is natural to be proved on case
analysis on the condition n’ == 0.
case X : (n’ == 0).
Now, the first goal has the form
...
Hi : fact pure n’ × a’ = fact pure N
X : (n’ == 0) = true
============================
verify (n :-> n’ \+ acc :-> a’) (ret a’)
[vfun res h ⇒ fact inv n acc N h ∧ res = fact pure N ]
To prove it, we will need one of the numerous val-lemmas, delivered as a part of HTT
libraries and directly corresponding to the rules of separation logic (Section 8.2.1). The
general recipe on acquiring intuition for the lemmas applicable for each particular verify-
goal is to make use of Ssreflect’s Search machinery. For instance, in this particular case,
given that the command to be verified (i.e., the second argument of verify) is ret a’, let
us try the following query.
Search (verify ) (ret ).
The request results report, in particular, on the following lemma found:
val ret
∀ (A : Type) (v : A) (i : heapPCM ) (r : cont A),
(valid i → r (Val v) i) → verify i (ret v) r
The lemma has a statement in its conclusion, which seems like it can be unified with
our goal, so we proceed by applying it.
8.4 Elements of Hoare Type Theory 133
...
Hi : fact pure n’ × a’ = fact pure N
X : (n’ == 0) = false
============================
fact inv n acc N (n :-> (n’ - 1) \+ acc :-> (a’ × n’))
12
In a case of several logical variables, the lemma should have been applied the corresponding number
of times with appropriate arguments.
134 8 Case Study: Program Verification in Hoare Type Theory
As in the case of the previous goal, the remaining proof is focused on proving a state-
ment about a heap and natural numbers, so we just present its proof below without
elaborating on the details, as they are standard and mostly appeal to propositional rea-
soning (Chapter 3) and rewriting by lemmas from Ssreflect’s ssrnat module.
exists (n’-1), (a’ × n’); split=>//=.
rewrite -Hi=>{Hi}; rewrite [a’ × ]mulnC mulnA [ × n’]mulnC.
by case: n’ X =>//= n’ ; rewrite subn1 -pred Sn.
Qed.
We can now implement the main body of the factorial function, which allocates the
necessary pointers, calls the accumulator loop and then frees the memory.
Program Definition fact (N : nat) :
STsep ([Pred h | h = Unit],
[vfun res h ⇒ res = fact pure N ∧ h = Unit]) :=
Do (n < −− alloc N ;
acc < −− alloc 1;
res < −− fact acc n acc tt;
dealloc n;;
dealloc acc;;
ret res).
The specification of fact explicitly states that its execution starts and terminates in
the empty heap; it also constraints its result to be a factorial of N.
Next Obligation.
Since the spec of fact does not have any logical variables (its postcondition only men-
tions its argument N ), there is no need to make use of the ghR lemma. However, the
current goal is somewhat obscure, so to clarify it let us unfold the definition of conseq
(which simply states that the consequence between the inferred type of the program and
the stated spec should be proved) and simplify the goal.
rewrite /conseq =>/=.
N : nat
============================
∀ i : heap,
i = Unit →
verify i
(n < −− alloc N ;
acc < −− alloc 1;
res < −− fact acc n acc tt; dealloc n;; dealloc acc;; ret res)
(fun (y : ans nat) (m : heap) ⇒
i = Unit → [vfun res h ⇒ res = fact pure N ∧ h = Unit] y m)
Next, we can rewrite the equality on the heap (which is Unit) and proceed by two runs
of the heval tactic, which will take care of the allocated pointers yielding new assumptions
n and acc, arising from the implicit application of the (Bind) rule.
move⇒ →.
8.4 Elements of Hoare Type Theory 135
Exercise 8.1 (Swapping two values). Implement in HTT a function that takes as argu-
ments two pointers, x and y, which point to natural numbers, and swaps their values.
Reflect this effect in the function’s specification and verify it.
Hint: Instead of reading the value of a pointer into a variable t using the t < −− !p
notation, you might need to specify the type of the expected value explicitly by using the
“de-sugared” version of the command t < −− read T p, where T is the expected type.
This way, the proof will be more straightforward.
Exercise 8.2. Try to redo the exercise 8.1 without using the automation provided by the
heval tactic. The goal of this exercise is to explore the library of HTT lemmas, mimicking
the rules of the separation logic. You can always display the whole list of the available
lemmas by running the command Search (verify ) and then refine the query for
specific programs (e.g., read or write).
Exercise 8.3 (Fibonacci numbers). Figure 8.1 presents the pseudocode listing of an
efficient imperative implementation of the function fib that computes the N th Fibonacci
number. Your task will be to prove its correctness with respect to the “pure” function
fib pure (which you should define in plain Coq) as well as the fact that it starts and ends
in an empty heap.
Hint: What is the loop invariant of the recursive computation defined by means of the
loop function?
Hint: Try to decompose the reasoning into verification of several code pieces as in the
factorial example and then composing them together in the “main” function.
136 8 Case Study: Program Verification in Hoare Type Theory
language”, which makes shallow embedding more preferable in this case—a reason why
this way has been chosen by HTT.
...
r : ptr
h’ : heap
============================
valid (null :-> x \+ (null.+1 :-> r \+ h’)) →
[/\ q = null, x :: xs = [::] & null :-> x \+ (null.+1 :-> r \+ h’) = Unit]
In the process of the proof we are forced to use the validity of a heap in order to derive a
contradiction. In the case of heap’s validity, one of the requirements is that every pointer
in it is not null. We can make it explicit by rewriting the top assumption with one of
the numerous HTT lemmas about heap validity (use the Search machinery to find the
others).
rewrite validPtUn.
...
============================
[&& null != null, valid (null.+1 :-> r \+ h’)
140 8 Case Study: Program Verification in Hoare Type Theory
Exercise 8.4. Define and verify function remove val which is similar to remove, but also
returns the value of the last “head” of the list before removal, in addition to the “next”
pointer. Use Coq’s option type to account for the possibility of an empty list in the
result.
End LList.
Exercise 8.5 (Imperative in-place map). Define, specify and verify the imperative higher-
order function list map that takes as arguments two types, S and T, a function f : T →
S and a head p of a single-linked list, described by a predicate lseq, and changes the list
in place by applying f to each of its elements, while preserving the list’s structure. The
specification should reflect the fact that the new “logical” contents of the single-linked
list are an f map-image of the old content.
Hint: The lemmas lseq null and lseq pos, proved previously, might be useful in the proof
of the established specification.
Hint: A tail-recursive call can be verified via HTT’s val do lemma, reminiscent to the
rule (App). However, the heap it operates with should be “massaged” appropriately via
PCM’s lemmas joinC and joinA.
Exercise 8.6 (In-place list reversal). Let us define the following auxiliary predicates,
where shape rev splits the heap into two disjoint linked lists (by means of the separating
conjunction #).
Definition shape rev T p s := [Pred h | h \In @lseq T p.1 s.1 # @lseq T p.2 s.2].
Then the in-place list reversal is implemented by means of the recursive function reverse
with a loop invariant expressed using the type revT.
Definition revT T : Type :=
∀ p, {ps}, STsep (@shape rev T p ps, [vfun y ⇒ lseq y (rev ps.1 ++ ps.2)]).
Program Definition
reverse T p : {xs}, STsep (@lseq T p xs, [vfun y ⇒ lseq y (rev xs)]) :=
142 8 Case Study: Program Verification in Hoare Type Theory
The goal of this course was to introduce a reader with a background in programming and
abstract algebra to interactive theorem proving in the Coq proof assistant.
Starting from the concepts, familiar from the world of functional programming, such as
higher-order functions, algebraic datatypes and recursion, we have first considered Coq
as a programming language in Chapter 2. The programming language intuition helped
us to move further into the realm of propositional logic and comprehend the way of en-
coding and proving propositions constructively in Chapter 3. At that point a number of
familiar logical connectives came in the new light of Curry-Howard correspondence with
respect to the familiar datatypes. Introducing universal and existential quantification,
though, required to appeal to the dependently-typed part of Coq as a programming lan-
guage, which moved us beyond a simple propositional logic, so we could make statements
over arbitrary entities, not just propositions. At the same point we had the first encounter
with Coq’s proof construction machinery. To unleash the full power of the mathematical
reasoning, in Chapter 4 we learned about the way equality is defined in Coq and how
it is used for proofs by rewriting. In the process we have learned that equality is just
one way to encode a rewriting principle and seen how custom rewriting principles can be
encoded in Coq. It turned out that one of the most useful rewriting principles is the abil-
ity to “switch” in the reasoning between the constructive and computable formulation of
decidable propositions—a trick that working mathematicians perform on the fly in their
minds. In Chapter 5, we have seen how the same switch can be implemented seam-
lessly in Coq using the boolean reflection machinery. With the introduction of boolean
reflection, our journey in the world of interactive theorem proving took a path, paved by
Gonthier’s et al.’s Ssreflect extension, embracing and leveraging the computational power
of Coq as a programming language to the extreme. The motto “let Coq compute a part of
the proof for you, since it’s a programming language after all!”, witnessed by formulation
of boolean functions instead of decidable inductive predicates, has been supplied by a
number of examples in Chapter 6, in which we have also exercised in proofs by induc-
tion of different flavours. Mathematics is a science of abstract structures and facts, and
formalizing such structures and facts is an important component of rigorous reasoning.
In Chapter 7 we have learned how the concepts of records and type classes, familiar
from languages like C and Haskell, can be directly employed, powered by Coq’s depen-
dent types, to encode a variety of mathematical structures from the course of abstract
algebra. Chapter 8 brought all of the presented programming and proving concepts
together and made them to work in concert to tackle a large case study—specifying and
verifying imperative programs in the framework of Hoare Type Theory.
144 9 Conclusion
Future directions
I hope that this short and by all means not exhaustive course on mechanized mathematics
in Coq was helpful in reconciling the reader’s programming expertise and mathematical
background in one solid picture. So, what now?
In the author’s personal experience, fluency in Coq and the ability to operate with a
large vocabulary of facts, lemmas and tactics is a volatile skill, which fades out at an
alarming rate without regular practice in proving and mechanized reasoning. On the
bright side, this is also a skill, which can fill one with a feeling of excitement from a
progressive reasoning process and the rewarding sense of achievement that few human
activities bring.
With this respect, it seems natural to advise the reader to pick a project on her own
and put it to the rails of machine-assisted proving. Sadly, formalizing things just for the
sake of formalization is rarely a pleasant experience, and re-doing someone’s results in
Coq just to “have them in Coq at any price” is not a glorious goal by itself. What is
less obvious is that setting up mathematical reasoning in Coq usually brings some brand
new insights that usually come from directions no one expected. Such insights might be
due to exploding proofs, which are repetitive and full of boilerplate code (seems like a
refactoring opportunity in someone’s math?) or because of the lack of abstraction in a
supposedly abstract concept, which overwhelms its clients with proof obligations, once
being applied to something its designer mathematician didn’t foresee (a case of leaky
abstraction?). Coq combines programming and mathematics in a single framework. I
believe, this must be the point, at which several decades of mastering the humanity’s
programming expertise should pay back and start being useful for producing the genuine
understanding of formally stated facts and proofs about them.
Bibliography
[1] Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah
Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for
Certified Compilers. Cambridge University Press, 2014 (cit. on pp. 7, 137).
[2] Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and
Stephanie Weirich. “Engineering formal metatheory”. In: Proceedings of the 35th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(POPL ’08). San Francisco, California, USA: ACM, 2008, pp. 3–15 (cit. on pp. 7,
137).
[3] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program De-
velopment. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical
Computer Science. Springer Verlag, 2004 (cit. on pp. 5, 17, 21, 29, 32, 44, 47).
[4] Richard Bird. Pearls of Functional Algorithm Design. Cambridge University Press,
2010 (cit. on p. 111).
[5] Hongxu Cai, Zhong Shao, and Alexander Vaynberg. “Certified self-modifying code”.
In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language
Design and Implementation (PLDI ’07). San Diego, California, USA: ACM, 2007,
pp. 66–77 (cit. on p. 7).
[6] Arthur Charguéraud. “The Locally Nameless Representation”. In: Journal of Au-
tomated Reasoning 49.3 (2012), pp. 363–408 (cit. on p. 137).
[7] Adam Chlipala. Certified Programming with Dependent Types. The MIT Press, 2013
(cit. on pp. 6–7, 17, 20, 46, 138).
[8] Adam Chlipala. “Mostly-automated verification of low-level programs in computa-
tional separation logic”. In: Proceedings of the 32nd ACM SIGPLAN Conference
on Programming Language Design and Implementation (PLDI ’11). San Jose, Cal-
ifornia, USA: ACM, 2011, pp. 234–245 (cit. on p. 7).
[9] Alonzo Church. “A Formulation of the Simple Theory of Types”. In: The Journal
of Symbolic Logic 5.2 (1940), pp. 56–68 (cit. on p. 30).
[10] The Coq Development Team. The Coq Proof Assistant – Reference Manual, Version
8.4pl4. Available at http://coq.inria.fr/refman/. 2015 (cit. on pp. 5, 8, 26,
102).
[11] Thierry Coquand. “An Analysis of Girard’s Paradox”. In: Proceedings of the Sympo-
sium on Logic in Computer Science. Cambridge, Massachusetts, USA: IEEE Com-
puter Society, 1986, pp. 227–236 (cit. on p. 48).
146 Bibliography
[12] Thierry Coquand and Gérard P. Huet. “Constructions: A Higher Order Proof Sys-
tem for Mechanizing Mathematics”. In: Proceedings of European Conference on
Computer Algebra (EUROCAL ’85), Volume 1: Invited Lectures. Vol. 203. Lecture
Notes in Computer Science. Linz, Austria: Springer, 1985, pp. 151–184 (cit. on
p. 48).
[13] Thierry Coquand and Gérard P. Huet. “The Calculus of Constructions”. In: Infor-
mation and Computation 76.2/3 (1988), pp. 95–120 (cit. on p. 29).
[14] Haskell B. Curry. “Functionality in combinatory logic”. In: Proceedings of the Na-
tional Academy of Sciences of the United States of America 20.11 (1934), pp. 584–
590 (cit. on p. 29).
[15] Olivier Danvy. Three Steps for the CPS Transformation. Tech. rep. CIS-92-2. Man-
hattan, Kansas, USA: Kansas State University, 1992 (cit. on p. 120).
[16] Robert Dockins and Aquinas Hobor. “A theory of termination via indirection”.
In: Proceedings of the Dagstuhl Seminar on Modelling, Controlling and Reasoning
about State. Vol. 10351. Dagstuhl, Germany, 2010, pp. 166–177 (cit. on p. 113).
[17] Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni.
“Modular verification of assembly code with stack-based control abstractions”. In:
Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language
Design and Implementation (PLDI ’06). Ottawa, Ontario, Canada: ACM, 2006,
pp. 401–414 (cit. on p. 7).
[18] Robert W. Floyd. “Assigning meanings to programs”. In: Proceedings of the Sym-
posium on Applied Mathematics. Vol. 19. 1967, pp. 19–31 (cit. on p. 112).
[19] François Garillot. “Generic Proof Tools and Finite Group Theory”. PhD thesis.
Palaiseau, France: École Polytechnique, 2011 (cit. on p. 107).
[20] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. “Pack-
aging Mathematical Structures”. In: Proceedings of the 22nd International Con-
ference on Theorem Proving in Higher Order Logics (TPHOLs 2009). Vol. 5674.
Munich, Germany: Springer, 2009, pp. 327–342 (cit. on pp. 99, 101).
[21] Jean-Yves Girard. “Interprétation fonctionnelle et élimination des coupures de l’arith-
métique d’ordre supérieur”. PhD thesis. Université Paris 7, 1972 (cit. on pp. 20, 30,
48).
[22] Georges Gonthier. “Formal Proof — The Four-Color Theorem”. In: Notices of the
American Mathematical Society 55.11 (Dec. 2008), pp. 1382–1393 (cit. on p. 8).
[23] Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection
Extension for the Coq system. Tech. rep. 6455. Microsoft Research – Inria Joint
Centre, 2009 (cit. on pp. 6–8, 24, 43, 62, 70, 81).
[24] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François
Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha,
Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry.
“A Machine-Checked Proof of the Odd Order Theorem”. In: Proceedings of the 4th
International Conference on Interactive Theorem Proving (ITP 2013). Vol. 7998.
Lecture Notes in Computer Science. Rennes, France: Springer, 2013, pp. 163–179
(cit. on p. 8).
Bibliography 147
[25] Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. “How
to make ad hoc proof automation less ad hoc”. In: Proceeding of the 16th ACM
SIGPLAN international conference on Functional Programming (ICFP ’11). Tokyo,
Japan: ACM, 2011, pp. 163–175 (cit. on pp. 7, 60, 107).
[26] Paul Graham. ANSI Common Lisp. Prentice Hall Press, 1996 (cit. on p. 137).
[27] Fritz Henglein. “Type Inference with Polymorphic Recursion”. In: ACM Transac-
tions on Programming Languages and Systems 15.2 (1993), pp. 253–289 (cit. on
p. 116).
[28] Manuel V. Hermenegildo, Francisco Bueno, Manuel Carro, Pedro López-García,
Edison Mera, José F. Morales, and Germán Puebla. “An overview of Ciao and its
design philosophy”. In: Theory and Practice of Logic Programming 12.1-2 (2012),
pp. 219–252 (cit. on p. 111).
[29] C. A. R. Hoare. “An Axiomatic Basis for Computer Programming”. In: Communi-
cations of the ACM 12.10 (1969), pp. 576–580 (cit. on p. 112).
[30] William A. Howard. “The formulae-as-types notion of construction”. In: To H.B.
Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Ed. by
Jonathan P. Seldin and J. Roger Hindley. Original paper manuscript from 1969.
Academic Press, 1980, pp. 479–490 (cit. on p. 29).
[31] Paul Hudak, Simon L. Peyton Jones, Philip Wadler, Brian Boutel, Jon Fairbairn,
Joseph H. Fasel, María M. Guzmán, Kevin Hammond, John Hughes, Thomas Johns-
son, Richard B. Kieburtz, Rishiyur S. Nikhil, Will Partain, and John Peterson.
“Report on the Programming Language Haskell, A Non-strict, Purely Functional
Language”. In: SIGPLAN Notices 27.5 (1992), pp. 1– (cit. on p. 8).
[32] Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. “The power of
parameterization in coinductive proof”. In: Proceedings of the 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13).
Rome, Italy: ACM, 2013, pp. 193–206 (cit. on p. 7).
[33] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. “Featherweight Java: a
minimal core calculus for Java and GJ”. In: ACM Trans. Program. Lang. Syst. 23.3
(2001), pp. 396–450 (cit. on p. 137).
[34] Xavier Leroy and Hervé Grall. “Coinductive big-step operational semantics”. In:
Information and Computation 207.2 (2009), pp. 284–304 (cit. on p. 7).
[35] Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and
Jérôme Vouillon. The OCaml system, release 4.01. Documentation and user’s man-
ual. Tech. rep. Available at http://caml.inria.fr/pub/docs/manual-ocaml/.
INRIA, 2013 (cit. on p. 8).
[36] John W. Lloyd. Foundations of Logic Programming, 2nd Edition. Springer, 1987
(cit. on p. 111).
[37] Assia Mahboubi and Enrico Tassi. “Canonical Structures for the Working Coq
User”. In: Proceedings of the 4th International Conference on Interactive Theorem
Proving (ITP 2013). Vol. 7998. Lecture Notes in Computer Science. Rennes, France:
Springer, 2013, pp. 19–34 (cit. on pp. 60, 107).
148 Bibliography
[38] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984 (cit. on pp. 29, 48).
[39] Robin Milner, Mads Tofte, and David Macqueen. The Definition of Standard ML.
Cambridge, MA, USA: MIT Press, 1997 (cit. on p. 8).
[40] Eugenio Moggi. “Notions of Computation and Monads”. In: Information and Com-
putation 93.1 (1991), pp. 55–92 (cit. on p. 124).
[41] Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. “Polymorphism and sep-
aration in Hoare Type Theory”. In: Proceedings of the 11th ACM SIGPLAN In-
ternational Conference on Functional Programming (ICFP ’06). Portland, Oregon,
USA: ACM, 2006, pp. 62–73 (cit. on pp. 7, 127).
[42] Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. “Hoare type the-
ory, polymorphism and separation”. In: Journal of Functional Programming 18.5-6
(2008), pp. 865–911 (cit. on pp. 7, 127, 129, 138).
[43] Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. “Structuring the verifica-
tion of heap-manipulating programs”. In: Proceedings of the 37th ACM SIGPLAN-
SIGACT Symposium on Principles of Programming Languages (POPL ’10). Madrid,
Spain: ACM, 2010, pp. 261–274 (cit. on pp. 98, 127, 129).
[44] Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco.
“Communicating State Transition Systems for Fine-Grained Concurrent Resources”.
In: Proceedings of the 23rd European Symposium on Programming (ESOP 2014).
Vol. 8410. Lecture Notes in Computer Science. Grenoble, France: Springer, 2014,
pp. 290–310 (cit. on pp. 7, 98).
[45] Ulf Norell. “Towards a practical programming language based on dependent type
theory”. PhD thesis. SE-412 96 Göteborg, Sweden: Department of Computer Sci-
ence and Engineering, Chalmers University of Technology, 2007 (cit. on p. 48).
[46] Martin Odersky. The Scala Language Specification, version 2.9. Tech. rep. Lau-
sanne, Switzerland: Programming Methods Laboratory, EPFL, 2014 (cit. on pp. 8,
121, 124).
[47] Martin Odersky and Matthias Zenger. “Scalable Component Abstractions”. In:
Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented
Programming, Systems, Languages, and Applications (OOPSLA ’05). San Diego,
California, USA: ACM, 2005, pp. 41–57 (cit. on p. 102).
[48] Simon L. Peyton Jones. “Tackling the awkward squad: monadic input/output, con-
currency, exceptions, and foreign-language calls in Haskell”. In: Proceedings of the
2000 Marktoberdorf Summer School on Engineering theories of software construc-
tion. Marktoberdorf, Germany: IOS Press, 2001, pp. 47–96 (cit. on p. 125).
[49] Simon L. Peyton Jones and Philip Wadler. “Imperative Functional Programming”.
In: Proceedings of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL ’93). Charleston, South Carolina,
USA: ACM Press, 1993, pp. 71–84 (cit. on pp. 112, 125).
[50] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn. “Simple unification-based type inference for GADTs”. In: Proceedings
of the 11th ACM SIGPLAN International Conference on Functional Programming
(ICFP ’06). Portland, Oregon, USA: ACM, 2006, pp. 50–61 (cit. on p. 54).
Bibliography 149
[51] Frank Pfenning and Conal Elliott. “Higher-Order Abstract Syntax”. In: Proceedings
of the ACM SIGPLAN’88 Conference on Programming Language Design and Im-
plementation (PLDI ’88). Atlanta, Georgia, USA: ACM, 1988, pp. 199–208 (cit. on
p. 136).
[52] Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002 (cit.
on pp. 20, 30, 44, 50, 115, 117, 120).
[53] Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin
Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Available at
http://www.cis.upenn.edu/~bcpierce/sf. Electronic textbook, 2014 (cit. on
pp. 6–7, 89, 94, 114, 137).
[54] John C. Reynolds. “Definitional Interpreters for Higher-Order Programming Lan-
guages”. In: Proceedings of 25th ACM National Conference. Reprinted in Higher-
Order and Symbolic Computation 11(4):363–397, 1998. Boston, Massachusetts,
USA: ACM, 1972, pp. 717–740 (cit. on p. 120).
[55] John C. Reynolds. “Separation Logic: A Logic for Shared Mutable Data Struc-
tures”. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science
(LICS 2002). Copenhagen, Denmark: IEEE Computer Society, 2002, pp. 55–74 (cit.
on p. 118).
[56] John C. Reynolds. “Towards a theory of type structure”. In: Symposium on Pro-
gramming. Vol. 19. LNCS. Paris, France: Springer, 1974, pp. 408–423 (cit. on pp. 20,
30).
[57] Amokrane Saïbi. “Outils Génériques de Modélisation et de Démonstration pour la
Formalisation des Mathématiques en Théorie des Types: application à la Théorie
des Catégories”. PhD thesis. Paris, France: Université Paris VI, 1999 (cit. on p. 106).
[58] Matthieu Sozeau. “Subset Coercions in Coq”. In: Proceedings of the International
Workshop on Types for Proofs and Programs. Vol. 4502. Lecture Notes in Computer
Science. Nottingham, United Kingdom: Springer, 2007, pp. 237–252 (cit. on p. 128).
[59] Matthieu Sozeau and Nicolas Oury. “First-Class Type Classes”. In: Proceedings
of the 21st International Conference on Theorem Proving in Higher Order Logics
(TPHOLs 2008). Vol. 5170. Lecture Notes in Computer Science. Montreal, Canada:
Springer, 2008, pp. 278–293 (cit. on p. 107).
[60] Matthieu Sozeau and Nicolas Tabareau. “Universe Polymorphism in Coq”. In: Pro-
ceedings of the 5th International Conference on Interactive Theorem Proving (ITP
2014). Vol. 8558. Lecture Notes in Computer Science. Vienna, Austria: Springer,
2014, pp. 499–514 (cit. on p. 50).
[61] Antonis Stampoulis and Zhong Shao. “Static and user-extensible proof checking”.
In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages (POPL ’12). Philadelphia, Pennsylvania, USA: ACM,
2012, pp. 273–284 (cit. on p. 7).
[62] Antonis Stampoulis and Zhong Shao. “VeriML: typed computation of logical terms
inside a language with effects”. In: Proceeding of the 15th ACM SIGPLAN inter-
national conference on Functional programming (ICFP ’10). Baltimore, Maryland,
USA: ACM, 2010, pp. 333–344 (cit. on pp. 7, 83).
150 Bibliography
[63] Philip Wadler. “The Essence of Functional Programming”. In: Proceedings of the
Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Pro-
gramming Languages (POPL ’92). Albuquerque, New Mexico, USA: ACM Press,
1992, pp. 1–14 (cit. on p. 124).
[64] Philip Wadler and Stephen Blott. “How to Make ad-hoc Polymorphism Less ad-
hoc”. In: Proceedings of the Sixteenth Annual ACM Symposium on Principles of Pro-
gramming Languages (POPL ’89). Austin, Texas, USA: ACM Press, 1989, pp. 60–
76 (cit. on pp. 97, 107).
[65] Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. “Binders unbound”. In: Pro-
ceeding of the 16th ACM SIGPLAN international conference on Functional Pro-
gramming (ICFP ’11). Tokyo, Japan: ACM, 2011, pp. 333–345 (cit. on p. 137).
[66] Benjamin Werner. “Sets in Types, Types in Sets”. In: Proceedings of the Third In-
ternational Symposium on Theoretical Aspects of Computer Software (TACS ’97).
Vol. 1281. Lecture Notes in Computer Science. Sendai, Japan: Springer, 1997,
pp. 530–346 (cit. on p. 47).
[67] Glynn Winskel. The formal semantics of programming languages — an introduction.
Foundation of computing series. MIT Press, 1993 (cit. on pp. 116, 138).
[68] Andrew K. Wright and Matthias Felleisen. “A Syntactic Approach to Type Sound-
ness”. In: Information and Computation 115.1 (1994), pp. 38–94 (cit. on p. 117).
[69] Hongwei Xi, Chiyan Chen, and Gang Chen. “Guarded recursive datatype construc-
tors”. In: Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL ’03). New Orleans, Louisisana, USA: ACM, 2003,
pp. 224–235 (cit. on p. 54).
[70] Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski,
and Viktor Vafeiadis. “Mtac: a monad for typed tactic programming in Coq”. In:
Proceedings of the 18th ACM SIGPLAN International Conference on Functional
Programming (ICFP ’13). Boston, Massachusetts, USA: ACM, 2013, pp. 87–100
(cit. on pp. 7, 83).
151
Index
;, 39 list, 23
<-, 58 nat rels, 66
=>, 35 nat, 15
by, 41, 82 option, 141
do, 82 or, 41
first, 82 prod, 22
last, 82 reflect, 76, 109
try, 39 sum, 23
Coq/Ssreflect tactics, 32 decidability, 71
apply:, 34 decidable equality, 109
case, 34 declarative programming, 111
clear, 79 definitional equality, 55
constructor, 40 dependent function type, 20, 35
done, 37, 82 dependent pair, 99
elim, 60, 62, 84, 89 dependent pattern matching, 18, 102
exact:, 31 dependent records, 99
exists, 45 dependent sum, 44
have, 56 Dirichlet’s box principle, 94
intuition, 79 discrimination, 55
left, 41 divergence, 125
move, 35 do-notation, 125
pose, 55 domain-specific language, 136
rewrite, 47, 57 DSL, see domain-specific language
right, 41
effects, see computational effects
split, 40
elimination view, 89
subst, 133
Emacs, 9
suff:, 47, 62
embedded DSL, 136
covariance, 115
encapsulation, 103
Curry-Howard correspondence, 29, 33
eta-expansion, 37
currying, 93
exclusive disjunction, 78
datatype indices, 54 extensionality, 108
datatype parameters, 53 extraction, 138
datatypes Feit-Thompson theorem, 8
False, 33 Fibonacci numbers, 135
True, 31 fixed-point combinator, 131
and, 40 forward proof style, 37
beautiful, 89 four color theorem, 8
bool, 14 frame rule, 119
eq, 53 Frobenius problem, 91
evenP, 84
ex, 44 GADT, see generalized algebraic datatypes
gorgeous, 91 Gallina, 10
isPrime, 72 generalized algebraic datatypes, 54
isZero, 83 getters, 100
leq xor gtn, 63 goal, 31
Index 153