Back

Formal Reasoning in Coq — a Beginner's Guide

09-25-2017 Formal Methods

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 company-coq and spacemacs-coq 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 company-coq commands with the Ctrl-C leader, and if you have spacemacs-coq, there’s some common commands under the , leader. Start the proof using proof-goto-point 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 company-coq-tutorial to learn about all the IDE-like helpers that the layer provides.

Coq objects

Here are some of the most important constructs in Coq:

Definition, Function, Fixpoint, and Inductive

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.

Built-in 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 and induction. 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 a fix expression that is harder to parse. Try simpl 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), spacemacs-coq 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:

(* A `nattree` is a tree of natural numbers, where every internal
   node has an associated number and leaves are empty. There are
   two constructors, L (empty leaf) and I (internal node).
   I's arguments are: left-subtree, number, right-subtree. *)
   
Inductive nattree : Set :=
  | L : nattree                                (* Leaf *)
  | I : nattree -> nat -> nattree -> nattree.  (* Internal nodes *)

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 saying b = true, which is of type Prop.

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.

match t with
           | L => false
           | I l n r => match beq_nat x n with
                       | true => true
                       | false =>  match Nat.ltb x n with
                                  | true => binsearch x l
                                  | false => binsearch x r
                                  end
                       end
           end
  end.

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!^{<span class=“hint–top hint–error hint–medium hint–rounded hint–bounce” aria-label=“<?, btw, is the notation for ltb, which you could have looked up with Locate "<?".”>[1]}

We need a lemma in Coq like

1	Lemma ltb_lt n m : (n <? m) = true <-> n < m.

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

1	rewrite <- Bool.not_true_iff_false, Nat.ltb_lt.

which changes the goal like:

__________________
(x <? n) = false

__________________
(x <? n) <> true

__________________
~ x < n

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

Function binsearch (x:nat) (t:nattree) : bool :=
match t with
| L =>  false
| I l n r => match x ?= n with
            | Eq => true
            | Lt => binsearch x l
            | Gt => binsearch x r
            end
  end.

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

Inductive comparison : Set :=
  | Eq : comparison
  | Lt : comparison
  | Gt : comparison.

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: Non-recursive definitions

Observe these two definitions of btree_sorted, which checks a tree is a valid BST.

Fixpoint isAscendingProp (t: list nat) : Prop :=
  match t with
  | nil => True
  | cons h tl => match tl with
                | nil => True
                | _ => and (Nat.le h (hd 0 tl)) (isAscendingProp tl)
                end
  end.

Function btree_sorted (t:nattree) : Prop :=
  isAscendingProp (flatten t).

Function btree_sorted (t:nattree) : Prop :=
 match t with
 | L => True
 | I l n r => btree_le l n /\ btree_ge r n /\ btree_sorted l /\ btree_sorted r
 end.

1 is flattening the tree via in-order 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 non-adjacent 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.

1 2	Function btree_in (x:nat) (t:nattree) : Prop := In x (flatten t).

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:

1	Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m.

to split up

1	H0: In x (flatten t1 ++ n :: flatten t2)

into

1	H0 : In x (flatten t1) \/ n = x \/ In x (flatten t2)

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 non-goal 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, beginner-oriented resources out there, so all of this post was constructed with trial and a lot of error.

Resources

1.<?, btw, is the notation for ltb, which you could have looked up with Locate "<?". ↩
2.simpl, like many other tactics, can be applied globally in context and goal with ___ in *, or to a specific hypothesis with ___ in H0. ↩