Literate Theorem Proving with Org

home writeups

Introduction

Recently, I've been messing around with Coq. Despite having experience with similar dependently-typed languages/theorem-provers like Agda and Idris, I was intimidated by Coq's "weird" (read: not Haskell-like) syntax and pretty much paid it no attention for a few years. However, I've been increasingly frustrated with the tooling for those languages, which tends to be undocumented and buggy. The situation with Coq, which as far as I know is much more commonly used, seems to be better. Here, I won't focus so much on the language itself but rather on my editor configuration and workflow.

Tools Used

Goals

  • To write Coq easily and without much fussing with the environment.
  • For my Coq-related tooling to properly clean up after itself: as I spend all of my time in the same Emacs instance, I don't want cruft accumulating.
  • To easily consult documentation.
  • To embed Coq proofs within my Org blog posts/writeups/whatever else, and to check/edit them seamlessly. I want a literate style, but in Org, not Coq's comment syntax.
  • For everything to play nice with my heavily customized evil-mode setup.

Getting There

Without further ado, let's begin.

First, we load Proof General, which unfortunately is not on MELPA and does not play nice with use-package, and company-coq.

(load "~/.emacs.d/lisp/PG/generic/proof-site.el")
(use-package company-coq :ensure t)

Next, we establish some basic keybindings for coq-mode buffers using a Hydra:

(defhydra tonic/ide-coq (:color blue :hint nil)
  "Quinine > Coq IDE"
  ("i" proof-assert-next-command-interactive "next")
  ("u" proof-undo-last-successful-command "undo")
  ("Q" proof-shell-exit "quit"))

We store the body of the Hydra in a buffer-local variable that will be invoked when entering q i, a key sequence that is constant across all major modes. Also, we toggle some minor modes that won't be needed within Proof General, and set another buffer-local variable to the yet-to-be-defined function tonic/coq-man (effectively binding it to K, vi-style, in coq-mode). Finally, we call a bunch of company-coq internal functions (in summary, these just make sure some variables used for documentation lookup are initialized).

Note the manipulation of coq-compile-before-require: this is important to facilitate inter-sourceblock Require.

(defun tonic/coq-setup ()
  (company-quickhelp-mode -1)
  (flycheck-mode -1)
  (company-coq-mode)
  (setq coq-compile-before-require t)
  (company-coq--init-refman-vernac-abbrevs-cache)
  (company-coq--init-refman-tactic-abbrevs-cache)
  (company-coq--init-refman-scope-abbrevs-cache)
  (company-coq--init-refman-ltac-abbrevs-cache)
  (setq-local tonic/contextual-ide 'tonic/ide-coq/body)
  (setq-local tonic/contextual-lookup 'tonic/coq-man))
(add-hook 'coq-mode-hook 'tonic/coq-setup)

company-coq provides a function (company-coq-doc) for looking up the documentation of a symbol. It also provides documentation for Coq language features, but I couldn't find any way to request this on demand: it only appears during completion. Let's fix that by adding tonic/coq-man, a function that brings up Helm filled with every (non-symbol) item for which company-coq has documentation.

(defun tonic/coq-man-candidates (cache)
  "Produce an alist mapping Coq abbreviations to refman anchors using CACHE."
  (mapcar (lambda (x) (cons x (company-coq-get-prop 'anchor x))) cache))

(defvar tonic/coq-man-actions '(("Lookup" . company-coq-doc-buffer-refman)))

(defun tonic/coq-man (name)
  "Helm completion for Coq refman documentation lookup. Default input is NAME."
  (interactive (list (thing-at-point 'word t)))
  (helm :sources (list (helm-build-sync-source "Coq Vernacular"
                         :candidates (lambda () (tonic/coq-man-candidates company-coq--refman-vernac-abbrevs-cache))
                         :action tonic/coq-man-actions)
                       (helm-build-sync-source "Coq Tactic"
                         :candidates (lambda () (tonic/coq-man-candidates company-coq--refman-tactic-abbrevs-cache))
                         :action tonic/coq-man-actions)
                       (helm-build-sync-source "Coq Scope"
                         :candidates (lambda () (tonic/coq-man-candidates company-coq--refman-scope-abbrevs-cache))
                         :action tonic/coq-man-actions)
                       (helm-build-sync-source "Coq Ltac"
                         :candidates (lambda () (tonic/coq-man-candidates company-coq--refman-ltac-abbrevs-cache))
                         :action tonic/coq-man-actions))
        :buffer "*helm tonic/coq-man*"
        :input name))

That should be enough Proof General configuration for now: with the help of company-coq, we have great autocompletion, nice-looking symbols, and convenient documentation lookup. Onto Org (well, mostly org-babel) configuration!

First, we add a keybind for org-edit-special to our Org Hydra:

(defhydra tonic/ide-org (:color blue :hint nil)
  "Quinine > Org IDE"
  ; ... ;
  ("e" org-edit-special "edit")
  ; ... ;
  )

Next, we set tonic/contextual-write, which is invoked after evil-write if defined, to perform an automatic Babel tangle. In order to write Coq programs that span multiple source blocks, we'll make sure all of the blocks are properly tangled to different files with descriptive names, and then simply Require those names. Proof General will automatically compile the associated .v files.

(defun tonic/org-setup ()
  ; ... ;
  (setq-local tonic/contextual-ide 'tonic/ide-org/body)
  (setq-local tonic/contextual-write 'org-babel-tangle)
  ; ... ;
  )
(add-hook 'org-mode-hook 'tonic/org-setup)

Finally, we'll customize the source code editing environment. In order to prevent a Proof General session from staying open due to improperly closing the window, locally rebind the key sequences that close the window/kill the buffer to just call org-edit-src-exit, which will ensure that everything is closed and that we end up back in the Org buffer. Even if a Proof General session is open, it will be closed automatically when the org-src-mode buffer is killed, so we don't worry about it.

(defun tonic/org-src-setup ()
  (setq-local tonic/contextual-quit 'org-edit-src-exit)
  (setq-local tonic/contextual-kill 'org-edit-src-exit)
  (setq-local header-line-format (concat "Editing a source block:")))
(add-hook 'org-src-mode-hook 'tonic/org-src-setup)

That's all, so let's test it out! Here's a trivial Coq proposition:

Theorem id : forall A : Prop, A -> A.

Let's prove it: idproof.gif

Theorem id : forall A : Prop, A -> A.
Proof.
  intros A H.
  exact H.
Qed.

Done!

From here, it's also trivial to depend on code from a previous source block in the current source block: simply set that previous block to :tangle to a file, and then Require that file in the current block.

I'm pretty satisfied with this setup at the moment, and I'm going to be using it for most of my writeups from this point on. (If you didn't notice in the GIF above, this Expect to see many more Coq proofs!

If you have any feedback, please feel free to contact me via email at mailto:samuel@chame.co. Thanks!

Author: Samuel Breese

Created: 2018-06-15 Fri 00:51

Validate