At OPLSS this year, I attended an awesome series of lectures by Ulf Norrell, in which he showed us the basics of dependently-typed wizardry in Agda. One of the coolest things about Agda is its Emacs mode, through which you communicate with Agda and do all kinds of crazy automatic code generation stuff. One of the things it can do is to automatically create well-typed helper functions while you’re in the middle of writing a program.
Inspired by this feature (and egged on by James), I wrote a much-hackier version for Coq proofs: it examines the current proof state and generates a helper lemma, generalizing over all of the context variables. For example, if your context looks like
A : Type
l : list A
a : A
H : In a l
========================
l <> []and you hit M-x extract-lemma <RET> in_not_empty <RET>, it’ll add
the following to your kill ring:
Lemma in_not_empty :
forall
(A : Type)
(l : list A)
(a : A)
(H : In a l),
l <> [].It does this in the absolute stupidest possible way: switching to the goals buffer and doing a bunch of crazy text munging. You’ll will probably want to clean up the output a bit, since it’ll generalize over the whole context and you probably don’t actually need/want that. Still, it’s a nice quick way to get a lemma of the correct type.
A quick note on why this is useful: separating large Coq proofs into self-contained, general lemmas is a good idea for the same reason that separating large programs into small functions is a good idea: it aids readability, maintainability, and durability. This bit of elisp should hopefully encourage this style of proof development.
Without further ado, here’s the code:
(defun chomp (str)
"Chomp leading and tailing whitespace from STR.
Stolen from http://www.emacswiki.org/emacs/ElispCookbook)"
(while (string-match "\\`\n+\\|^\\s-+\\|\\s-+$\\|\n+\\'"
str)
(setq str (replace-match "" t t str)))
str)
(defun extract-lemma (name)
"Extract a Coq lemma to the kill ring based on the current goal"
(interactive "sName of lemma: ")
(let ((conclusion) (antecedents '()))
(with-current-buffer "*goals*"
;; get to the beginning of the context
(goto-line 0)
(search-forward-regexp "^[[:space:]]*[^[:space:]]+ :")
(move-beginning-of-line nil)
;; find antecedents and add them to the list
(while (not (string-match " ======+$" (thing-at-point 'line)))
(let ((line (chomp (thing-at-point 'line))))
(if (string-match "^[^[:space:]]+ : .*" line) ;; new antecedent
(progn
(when antecedents ;; need to close the previous antecedent
(setcar antecedents (concat (car antecedents) ")")))
(push "(" antecedents))
(setcar antecedents (concat (car antecedents) "\n")))
(setcar antecedents (concat (car antecedents) line)))
(next-line))
(setcar antecedents (concat (car antecedents) ")"))
;; copy the conclusion
(next-line)
(move-beginning-of-line nil)
(let ((beg (point)))
(end-of-buffer)
(setq conclusion (chomp (buffer-substring beg (point))))))
(setq antecedents (reverse antecedents))
(kill-new "")
(kill-append (concat "Lemma " name " :\n") nil)
(when antecedents
(kill-append "forall" nil))
(dolist (antecedent antecedents)
(kill-append "\n" nil)
(kill-append antecedent nil))
(kill-append ",\n" nil)
(kill-append conclusion nil)
(kill-append ".\n" nil)))