I’m currently taking the Fall 2017 iteration of 6.826, Principles of Computer Systems. This class has been offered in various forms over the years, but this iteration is quite different. It focuses on formal verification of computer systems using Coq, a language for mechanical theorem proving.
The goal of this class is to write the spec, implementation, and proofs for a formally verified RAID filesystem in Coq, then generate Haskell code from it.
I’ve been quite curious about the field of formal verification since I first learned about it last semester. I couldn’t fit Adam Chlipala’s FRAP (Formal Reasoning About Programs) into my schedule, but I didn’t want to miss out on Zeldovich and Kaashoek’s PoCS class because it seemed more practical in nature.
This is the first in a series of posts on approaching Coq and formal verification as a complete beginner.
Environment Setup
I’d heard good things about using Emacs + Proof General for Coq, so I started using Spacemacs, which combines vim’s editing modes and keybindings with Emacs’.
I haven’t tried the default CoqIDE or Coquille in vim, but Emacs’ Coq support is pretty great. With companycoq and spacemacscoq layers, there’s not much more you could ask for.
If you’re coming from vim, Spacemacs is a little obnoxious to get set up, though. The Coq integration is a Spacemacs ‘layer’, which is a set of configurations for a specific task. Make sure that the Coq layer activates upon opening a .v
file.
Perhaps I’ll do another post about all the editors I use daily — Vim, Sublime, Atom, and Spacemacs — (I’m a mongrel, I know), but for now, I’ll just direct you to some Spacemacs resources.
Tactics, Datatypes, and Coq commands
Software Foundations is the best place to start getting your feet wet. The first three chapters — Basics, Induction, and Lists — will give you all you need to start being productive.
When you open a .v
Coq file in Spacemacs, Coq mode should be activated. You should now be able to access companycoq commands with the CtrlC
leader, and if you have spacemacscoq, there’s some common commands under the ,
leader. Start the proof using proofgotopoint
or an alias for it, and you’ll be able to see the goal you’re proving and the context, containing your variables and hypotheses, in a pane on the right. Note that the Coq process can only be active in one buffer at a time, so you can’t have proofs running simultaneously in several files.
Once you’ve learned the basic syntax, you should also do the Emacs companycoqtutorial
to learn about all the IDElike helpers that the layer provides.
Coq objects
Here are some of the most important constructs in Coq:
Definition
,Function
,Fixpoint
, andInductive
Inductive
defines inductive types. Function
and Fixpoint
are for recursively defined functions on inductive types. Note that Fixpoints
must be obviously decreasing on each recursive call, or else Coq will complain.
 Builtin datatypes such as
Nat
,List
,Prop
,Bool
. Theorem
,Lemma
,Proof
match
statements ( familiar from any other functional language )
Getting started with tactics
The first three chapters of SF will teach you a few basic tactics — namely, induction
, assert
, simpl
, reflexivity
, rewrite
, apply
, replace
. Nearly all the the exercises can be completed with just these.
Once you get sufficiently advanced, you’ll be able to identify when magic commands like auto
or omega
will just solve the rest of your proof for you. info_auto
will show you the tactics that auto
is using.
You’ll start to notice patterns in how to apply tactics.
For instance,
 If you see a recursive data structure, you should think about
destruct
andinduction
. Both are used to perform case analysis on a constructor of an inductively defined type; induction also generates an induction hypothesis, while destruct does not.  Sometimes,
unfold
will break a monolithic function into useful pieces. Other times, it will give you afix
expression that is harder to parse. Trysimpl
instead.^{2}
This cheatsheet is invaluable for most of the tactics you’ll ever need. I also found this site useful for the few most basic tactics.
When you first start out, it’s useful to be able to search for library lemmas, theorems, definitions, notation, etc. The Search ___
command will look for definitions and theorems. If you quote the search string like "eqb"
, it will look for all theorems with that as a substring.
Locate
can look up constants or notation, like "?="
. To insert the outputs of the last command as a comment (so you can refer to it without having to rerun it), spacemacscoq provides the key sequence , ;
.
Proving binary search trees (and pitfalls)
In the first lab of 6.826, we have to prove properties of trees. We are given a tree, defined as follows:


We have to define a binary search function and a function to test whether a tree is a BST, then write proofs about the correctness of our functions. We want to prove, among other things, that our BST tester does indeed enforce the sortedness of left and right subtrees, and that binsearch can indeed find every element in the tree.
My first attempt was a disaster, ending with convoluted proofs that would have gotten progressively harder had I not stopped and asked for help. I’ll talk about some of the pitfalls I made, and then discuss how everything went smoother on the second try.
Pitfall 1: The Bool and Prop worlds
Coq has two worlds: computational (Type
) and logical (Prop
). Booleans exist in the computational world, and can be either true
or false
. Props
, by distinction, are uppercased True
or False
.
As this answer explains,
Essentially, Coq has both because they are useful for different things: booleans correspond to facts that can be checked mechanically (i.e., with an algorithm), whereas propositions can express more concepts… If
b : bool
represents a statement, we can assert that this statement is true by sayingb = true
, which is of typeProp
.
Note that Props
can be used in proofs, but not in functions.
To relate the two, we need theorems that translate between Bool
and Prop
, as I quickly and painfully discovered.
Take a look at my initial definition of binsearch on a nattree
t.


This seems reasonable, right? However, the beq_nat
(an alias for Nat.eqb
) and Nat.ltb
return Bools
, not Props
!
So, when we want to use hypotheses like x < n
(a Prop
) to prove (x <? n) = true
, it’s not immediate because they’re in two different worlds!^{1}
We need a lemma in Coq like


This lemma says that the proposition n < m
is True
iff the proposition (n <? m) = true
is True
.
To illustrate this more, how about proving the proposition that (x <? n) = false
given x > n
?
First we have to do something ugly like


which changes the goal like:


and only then will an automagic command like omega
be able to solve it.
Second attempt
What’s a better way to define binsearch
, then? The cleanest is


The ?=
is Nat.compare
, which returns a comparison
type, defined below:


With this cleaner definition, we can now use the lab’s given destruct_compare
tactic to split our proof into three cases: x < n
, x = n
, x > n
.
Pitfall 2: Nonrecursive definitions
Observe these two definitions of btree_sorted
, which checks a tree is a valid BST.
1:


2:


1 is flattening the tree via inorder traversal, then checking that each element in the list is $\leq$ the next element. Algorithmically, this is efficient and correct, but it would lead to more work when writing proofs, since I would need more lemmas about isAscendingProp
that related nonadjacent elements.
Writing recursive definitions as in 2 makes the proof much easier. As my TA said, you want the definition to match how you’re writing the proof.
Aside: Using List
lemmas
In my final solution, all my functions were recursive except btree_in
, for determining membership in a list.


If you get comfortable with the List
library, then this shouldn’t be a problem. The In
function has some nice lemmas. I used this one a lot:


to split up


into


Identifying patterns
I found myself repeating the same tactic patterns in my proofs. For example, when I have a series of /\
like A /\ B /\ C
in my hypotheses, I can split them up using destruct_pairs
, allowing me to use each clause individually because I know each one must be true.
If there’s a series of \/
in a hypothesis, you need to use multiple destructs
.
For example, I often ended up having H0 : In x (flatten left_subtree) \/ n = x \/ In x (flatten right_subtree)
in my context, and my goal was to prove one of those clauses.
Well, I would use destruct
to consider each case individually, showing that the other two nongoal clauses resulted in contradictions. Therefore, my own goal must be true.
Conventions and sugar
In Basics.v
of SF, you’ll find best practices on organizing proofs. I like to use nested bullet points 
, +
, and *
, in that order, to focus subgoals whenever I am doing cases
, induction
, or destruct
. When I have an assert
, I wrap the proof of the assert in {}
.
Hopefully, you learned some pointers to get you more productive in Coq! There’s not many clear, beginneroriented resources out there, so all of this post was constructed with trial and a lot of error.