Assisted Theorem Proving with J-Bob

There is an excellent book floating around out there called The Little Prover by Daniel Friedman and Carl Eastlund. If you have an interest in approaching proof assistants like Coq or Isabelle, this is the book to start with. Aside from basic math and programming, the authors assume no other prior knowledge, and each chapter is written as a step-by-step dialogue in a style I find ideal for this type of learning.

My motivation for working through this particular book was to position myself to understand more advanced material on specific proof assistants, namely Coq, which is fairly prominent with some industrial uses, and TLAPS, which is used to prove properties of TLA+ specifications. I’m still a long way from being able to use either of those, but working with J-Bob, the minimal proof assistant introduced in The Little Prover, has given me a solid foundation on which to build.

The toughest part for me was getting a complete understanding of the first two chapters. After a few re-readings, I had a cursory understanding, but not an intuitive grasp. So I left the book alone for a few months, then came back to it and tried again. Everything clicked for me when I thought less like a programmer, surprisingly enough. To explain, here’s one of the intermediate axioms introduced by the authors:

(dethm equal-if (x y)
  (if (equal x y) (equal x y) 't))

Coming from a software background, I caught myself immediately trying to evaluate that “function”, in my mind, on various inputs to understand its purpose. With the book’s help, I eventually trained myself to see axioms and theorems like this as merely symbols, not as the functions they appear to be. These “functions” are merely rewriting rules that are “evaluated” by other functions: those of the proof assistant, in this case, J-Bob. For example, given the very simple, obviously true theorem:

(dethm example (a b)
  (if (equal a b)
     (equal a b)
     't))

We don’t have to “evaluate” it on any values of a or b to prove that it’s always true for all values; we simply cite axiom equal-if above, which allows us to rewrite (equal a b) to 't as long as there’s a conditional nested somewhere above it with the same expression:

(dethm example (a b)
  (if (equal a b)
     't
     't))

Once I started treating everything as mere symbols, the later chapters made complete sense and naturally flowed together. The authors advance to proving totality and induction claims for recursive functions, the proofs for which get lengthy, but are entirely understandable if you have an intuitive understanding of the first two chapters. To me, the coolest part about all of this is the immediate feedback of the proof assistant: you blow up a simple theorem body into a huge expression, then dance forward and backwards using only some rules and your gut in order to reduce everything to a simple 't value.

In fact, all of this reminded me of the first part of Gödel, Escher, Bach, where Douglas Hofstadter similarly demonstrates how mere symbol shunting is enough to prove attributes of a formal system, without any knowledge of what those symbols mean. Now that I think about it, given the whimsical writing style and the Jabberwocky example on page 20 of the The Little Prover, I’d bet the authors have waded through GEB themselves.

Since a lack of programming experience appears to be somewhat of an asset here, I think the progression of this book would fare positively in a high school or undergraduate setting. The Little Prover strikes me as the perfect blending of math and software, in that it gives one an appreciation for some of the strengths and limits of both. Add in the individual agency of conversing with the proof assistant, and it’s hard to believe at least a few students wouldn’t walk away excited (not sure if any US schools would even allow for such “experimentation,” but I won’t get into that here).

Anyway, if you have even the slightest interest in proof assistants and no foundation whatsoever, get a copy of this book and work through all the proofs. Your mind will be expanded.