---

Similar to my last post which gives some tips and reviews of The Little Typer, this post will do the same thing, but for The Little Prover.

Who is this book for?

This book teaches theorem proving over recursive functions using induction.

Suppose you want to prove a theorem related to a function. A sensible approach is to use a set of rules to rewrite the theorem until we are convinced that it’s true (i.e. it’s rewritten to 't).

The rules are either built-in (e.g. for all a, (equal a a) is true), or they are true by definition (e.g. replace a function application with its substituted body).

However, these are not enough if the function is recursive. This is because we want to prove that the theorem is true for every possible argument of that function. For recursive functions, the theorem’s form can be different for different arguments and the number of such forms can go to infinity. In such cases, we can instead prove by induction. This requires us to prove that:

1. The function is total.
2. The theorem is true for base cases.
3. The theorem is true for recursive cases, given the induction hypotheses.

This book will walk you through the whole process for several functions and theorems (literally step-by-step as we’ll see later). So I think it is especially useful for those who are already motivated for theorem proving, but would want to peek under the hood.

This will not necessarily help you understand the details of other proof assistants, but by going into the details of small examples, you will actually get the general idea. I think this will be the long lasting benefits you’ll get from reading the book.

Set up J-Bob

The book’s proof assistant, J-Bob, will check your proof as you follow the examples. Using J-Bob is quite different from using the Pie language from The Little Typer. The target language (i.e. the language used to define functions and theorems) is embedded in Scheme as atom lists. So there are no functionalities like going to the definition, finding all the references, checking the arity and so on. Instead we will use functions to rewrite the atom list and J-Bob will tell you the result.

To install J-Bob, clone the repository. Inside scheme/ you’ll find j-bob-lang.scm which defines the target language, j-bob.scm which is the complete implementation of the proof assistant, and little-prover.scm which contains all the examples from the book.

To use J-Bob in DrRacket, you need to set the language to Scheme following the repository’s README instruction. To check it’s working, use this example from the README:

;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")
;; Load the transcript of all proofs in the book:
(load "little-prover.scm")
;; Run every proof in the book, up to and including the proof of align/align:
(dethm.align/align)

When you run this file, J-Bob should run every proof in the book and output a list of definitions and theorems.

Use J-Bob

Most of the time, what you want is these two lines at the start.

;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")

Which will make the following functions available:

1. J-Bob/step
2. J-Bob/prove
3. J-Bob/define

And also prelude, which is a list of built-in definitions and theorems. To learn their usages, at one point in the book, you’ll be directed to the Recess chapter. However, J-Bob/prove is almost always what you want to use.

To add a definition or theorem, first we need to create a template:

(defun function-name ()
  (J-Bob/prove
   (proven-stuff)
   '(
     ((dethm theorem/name (args...)
             (theorem-body args))
      (induction-scheme) ; or just nil
      ... ; many lines of ((path) (rewritting-rule))
      )
     )))

proven-stuff is a list of definitions of functions that are proven to be total and theorems that are proven to be true. prelude is such an example. After you’ve proven the current theorem (running (function-name) yields 't), you can replace J-Bob/prove with J-Bob/define to add the function definitions and theorems to that list. After J-Bob/define, running (function-name) will print a new list of definitions and theorems, including those you just defined. Then when proving the next theorem, you can supply (function-name) as the first argument of J-Bob/prove and therefore grow your list step by step.

Defining a function is similar, but instead of an induction scheme, you’d supply a measure and the rewriting steps of its totality proof, if necessary.

Note that if you use J-Bob/define without finishing a proof (including the totality proof when defining a function), the new (function-name) will not error, but neither will it include anything that’s not proven. You need to be careful. It’s best to use J-Bob/define only after you’ve proven all theorems.

Take a look at little-prover.scm for some examples.

The next step is to write the proof. Running (function-name) (i.e. hit Run and type (function-name) and enter) should print out the current term. Then you’d extend the rewriting steps with a new step like ((E E) (size/cdr ys)), where the first component is the path to the term to rewrite, and the second component is the rewriting rule supplied with all arguments.

Note that to replace a function call with its definition, the rewriting rule is just the function’s name and arguments. For example, if we have (defun f (xs) (cons 'a xs)), then to rewrite (f '(b)) to (cons 'a '(b)), the rewriting rule should be (f '(b)).

Another important note on the output of J-Bob/prove: if a line of proof is wrong, it has two ways to inform you: either the term is not changed (usually due of a wrong path), or the output is 'nil (usually when some function is applied to a wrong number of arguments). So it’s best to compare the terms before and after each step to make sure that some progress is actually made.

Tips to streamline the proving process (a bit)

Apart from lacking many language features as mentioned above, J-Bob also has zero automation¹. Therefore, you need to tell it precisely which term to rewrite and how. This means to write out the complete path to the term all of the arguments of the rewriting rule, even those not present in the result (which are used internally for equality checking).

It’s the price to pay for an impressively small theorem prover, but these limitations at the same time make proof writing and debugging with J-Bob painful. Here are some tricks that I used to make the process a little bit easier.

File Organization

My file for each chapter is organized as follows:

(defun f1 ()
  (J-Bob/define
    (prelude)
    '(...)
  ))

(defun f8 ()
  (J-Bob/prove
    (f1)
    '(...)
  ))
(f8)

When proving the theorem from Frame 8 (thus the name f8), I would add a call of (f8) at the end of the definition. When running the definition, the state of the term is directly printed out.

Indent the definition and the output

Since the proof so often needs you to find the path to a term, it’s very important to indent the definitions and the output so that you can easily navigate around.

Use Racket - Indent all from the menu to indent your definitions (default keybinding Cmd+i).

The output style can be configured through Language - Choose language... and there you can see the language specific output configurations.

The default Output Syntax of write and Insert newlines in printed values are sane choices. However, I find that the pretty printing seems to assume that the font size is 12. Using a larger font size will cause the text to overflow to the next line instead of compressing the pretty printing box. At the time of writing, I didn’t find a bug report or a workaround for this issue, so I just accepted it as a fact of life. Luckily, the book is short enough such that I still got plenty of eyesight left after finishing it, which is more than what I could have hoped for.

Keybindings to the rescue

I adapted the keybinding snippet from the DrRacket reference to bind F4 to do three things: Reindent all, Run, and keep the focus at the definition editor.

#lang s-exp framework/keybinding-lang

(require drracket/tool-lib)
(require racket/gui/base)
(module test racket/base)

(define (call-menu menu-item)
  (λ (ed evt)
    (define canvas (send ed get-canvas))
    (when canvas
      (define menu-bar (find-menu-bar canvas))
      (when menu-bar
        (define item (find-item menu-bar menu-item))
        (when item
          (define menu-evt
            (new control-event%
                 [event-type 'menu]
                 [time-stamp
                  (send evt get-time-stamp)]))
          (send item command menu-evt))))))

(define/contract (find-menu-bar c)
  (-> (is-a?/c area<%>) (or/c #f (is-a?/c menu-bar%)))
  (let loop ([c c])
    (cond
      [(is-a? c frame%) (send c get-menu-bar)]
      [(is-a? c area<%>) (loop (send c get-parent))]
      [else #f])))

(define/contract (find-item menu-bar label)
  (-> (is-a?/c menu-bar%)
      string?
      (or/c (is-a?/c selectable-menu-item<%>) #f))
  (let loop ([o menu-bar])
    (cond
      [(is-a? o selectable-menu-item<%>)
       (and (equal? (send o get-plain-label) label)
            o)]
      [(is-a? o menu-item-container<%>)
       (for/or ([i (in-list (send o get-items))])
         (loop i))]
      [else #f])))

(keybinding "f4"
            (λ (ed evt)
              ((call-menu "Reindent All") ed evt)
              ((call-menu "Run") ed evt)
              (send (send ed get-canvas) focus)))

To use it, save the definition as a file and load it through the menu item Edit - Keybindings - Add User-defined Keybindings.... It’s also available as a gist.

With this keybinding, I can constantly edit my proof and hit F4 to see the effect, which almost gives an interactive theorem proving experience.

Final thoughts

I really appreciate the effort to keep the language and theorem prover as small as possible, but the lack of some common constructs makes the proving process not so intuitive. For example, A and B are encoded as (if A (if B 't 'nil) 'nil) which results in many routines to massage the term into the right shape. Maybe I’m not enlightened enough to see the value of “wax on wax off”, but these routines are more artifacts than practices for me and I think they are rare (or at least easily automated) in practice.

On the other hand, the price we paid gives us a really small language and theorem prover. After a proof is finished, you can confidently say that you know what’s happening at every single step and there’s literally no magic happening at all.

At the end of the day, being able to do inductive proofs with so little help is really something to be proud of. See how the confidence grows, when the mystery of theorem proving is unveiled. I think this book is a good example of going to the details but ended up grasping the general idea.

It’s hard work, but I enjoyed the journey. If only there were a follow-up of both The Little Typer and The Little Prover…or are you ready to dive in to the boundless space of real life dependant type theorem proving? Happy hacking and see you on the other side.

---

1. Boyer and J Moore, the namesakes of J-Bob, in contrast, are famous for their automated theorem proving systems.↩︎