Getting started with 'The Little Prover'

So you are interested in proof assistants and you got your paws on the newly published The Little Prover, the latest book of the series you've heard much good about, which includes:

and more.

And maybe you've never really been into Scheme, and now you have to figure out which of the many Scheme implementation available is the one you want to get, in order to get the book examples running.
I'll save you that effort in this guide.

Get a scheme####

There many choices for a Scheme implementation, as you may have noticed.
They all have their merits, but if you're not completely against IDEs, probably the most convenient one is DrRacket.
DrRacket is an IDE geared geared towards people reading How to Design Programs, SICP and other famous books.
It's used in education, notably by Shriram Krishnamurthi at Brown, and it's very convenient to use, as it includes many different versions of Scheme in a neat package, with package management, many libraries and a lot of documentation.

Install DrRacket

Visit the DrRacket website and get the installer, run it, and you should be all set.

If you like to have command line control (like me) you'll want to get raco.
You have to run DrRacket and click Help -> Configure command line for Racket ...
That will ask for admin confirmation and install raco.
It points automatically /etc/paths.d/racket to /Applications/Racket v<version>/bin so you should have raco available if you restart your shell.

Dracula package

Dracula is a set of ACL2 theorem prover tools in DrRacket, which also includes J-Bob.

If you have raco you can install it with

raco pkg install dracula

or you can install through the UI, File -> Package Manager -> Available from Catalog -> search for Dracula, select it and press Install.

Now you should have Dracula and you'll be able to choose ACL2 as a language to use in DrRacket.

Get the book's code

The book's github repository contains all the code, it's best to have it as a reference, even if Dracula includes J-Bob.

Clone the repository to a directory on your machine:

git clone https://github.com/the-little-prover/j-bob ~/j-bob

That includes

j-bob-lang.scm the J-bob language
j-bob.scm J-bob itself
little-prover.scm the transcript of the book's proofs

in ACL2 and in Scheme R5S5 versions:

for ACL2 under /acl2/
for Scheme R5RS under /scheme/.

Load J-Bob

You can run any of them in DrRacket, by switching the current language, or as a third option just load the version of J-Bob already included in Dracula.

To switch to the ACL2 language/Dracula choose Language -> Choose Language Pack -> Other Languages -> Dracula -> ACL2.
To switch to Scheme R5RS choose Language -> Choose Language Pack -> Legacy Languages -> R5RS, you also have to press Show Details and make sure that Disallow redefinition of initial bindings is not checked.

Then you load the version of j-bob-lang.scm for the language you chose fist, then j-bob.scm and then little-pover.scm if you want to be able to access each proof from the start.

using Dracula

This will load all the files, including all the proofs

(include-book "j-bob-lang" :dir :teachpacks)
(include-book "j-bob" :dir :teachpacks)
(include-book "little-prover" :dir :teachpacks)

To run all the proofs up to align/align (might take a lot of cpu/RAM)

(dethm.align/align)

The equivalent commands in the other versions:

R5RS version

(load "j-bob-lang.scm")
(load "j-bob.scm")
(load "little-prover.scm")
(dethm.align/align)

ACL2 version

(include-book "j-bob-lang")
(include-book "j-bob")
(include-book "little-prover")
(dethm.align/align)

If you're opening them manually using a menu DrRacket will attempt to guess their language and you'll see a yellow message "Determine language from source", you'll have to force the language to be the one you chose again.

Follow the book

The Racket IDE is divided in two spaces, in the upper one you can write all the code you want and then press Run to execute. It's called the definitions area.
The interactions area is just below and works like a REPL, you can write the code and as soon as you press Return it will execute.

If you keep one of the little-prover.scm versions open while you read you'll be able to check the actual code needed to run the proofs one by one without typing them, though I do recommend typing, in order to learn better.

> (chapter1.example1)
'ham
> (chapter2.example1)
(if (if (equal a 't) 't (equal 'or '(black coffee))) c c)

You should be ready to get started now, have fun!

Comments? Give me a shout at @lambda_cat.
To get the latest post updates subscribe to the LambdaCat newsletter.
You can support my writing on LambdaCat's Patreon.