Software Foundations, Volume 1: Logical Foundations

There is a certain amount of celebration going on at Maniagnosis’ underground lair at the moment. (Underground lair? There’s nothing underground or lair-ish about this place. It’s not even spectacularly office-like. –Ed) I have (Insert lame drum-roll here.) completed all of the exercises in Software Foundations, Vol. 1: Logical Foundations by Benjamin Pierce, et al. (Very much al.)

(Cue fireworks!) Pop!

The cover of Software Foundations, Vol. 1: Logical Foundations.

This is approximately my fourth pass at Coq, with my previous attempts including Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions and the previous version of Software Foundations. (Certified Programming with Dependent Types is still in the unread pile. I hope to get to it soon, now that I sort of know what I’m doing.)

I’ve previously described Coq as the best computer game ever invented, and I’ll pretty much stand by that. It’s fun. But it is also very, very frustrating. Consider doing a traditional proof, such as the following poor example of a proof sketch:

Theorem: addition is commutative. Prove n + m = m + n by induction on n.

• Assume n = 0. Then, 0 + m = m + 0 which can be simplified to m = m, which is a tautology.

• Assume n = n′+1 and that n′+m = m + n′. n + m is equal to n′+1 + m, which is equal to n′+m + 1, and likewise the right-hand side equals m + n′+1. Subtract one from both sides and the result is the induction hypothesis. QED.

(The first logic course I ever had was given by Daniel Bonevac from the UT Austin Department of Philosophy; at this point in the earliest proof lectures, he mentioned a textbook that he had, that completed the proofs with a small drawing of a pig. That’s how “QED” became associated with pigs in my mind. To be honest, I suspect I never really had a chance at normalcy.)

Anyway, the thing to notice is that the states of the proof are presented, with commentary describing the steps taken. That is how every published proof has been presented, ever.

Coq is different. Instead of showing the proof states, a Coq proof consists entirely of poorly-named, more-or-less obscure commands that alter the proof state. Here’s an example, a slightly obscured version of the same proof:

Definition p_comm (n m : nat) : Prop := n + m = m + n.

Theorem p_comm_def : forall n m, p_comm n m.
Proof.
  intros n m; unfold p_comm; induction m.
  - simpl. rewrite <- plus_n_O. reflexivity.
  - rewrite -> plus_Sn_m. rewrite <- IHm. rewrite -> plus_n_Sm. reflexivity.
Qed.

The only effective way to read this thing is by stepping through it in coqide or Emacs’ Proof General mode, both of which display the proof states between commands. But that is like understanding a program by stepping through it in a debugger. That is sub-optimal.

However, with the help of some changes in Coq’s language (in part, the bullet points in the proof above, for example) and Pierce, et al., I have finally made it through a reasonable introduction to Coq without too much cheating and with some semblance of understanding.

Let the corks fly! Pull those ferrets’ trousers down! We’re having a party!

Now, to decide which of the two other volumes to tackle next…