Tuesday November 24 2020

Untangling Mechanized Proofs

Hacker News - Sat Nov 21 22:00

Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Coq code and prose, in a style sometimes called literate programming.

Coq proofs are hard to understand in isolation: unlike pen-and-paper proofs, proof scripts only record the steps to take (induct on x, apply a theorem, …), not the states (goals) that these steps lead to. As a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive interface like CoqIDE or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Coq is to manually copy Coq's output into source code comments — a tedious, error-prone, and brittle process. Any text that accompanies the proof is also embedded in comments, making for a painful editing experience.

Alectryon does better: it automatically captures Coq's output and interleaves it with proof scripts to produce interactive webpages, and it lets you toggle between prose- and code-oriented perspectives on the same document so that you can use your favorite text editing mode for writing prose and your favorite Coq IDE for writing proofs.

I have a talk about this at SLE2020 on November 16th; you should join!

Below, you can see three examples: in the first one I asked Alectryon to record the result of a single Check command. In the second, I recorded an error message printed by Coq. In the third, I recorded a simple proof script — try hovering or clicking on Coq sentences. In the last, I've used hidden Show Proof commands to show how each tactic participates in constructing a proof term.

By the way, I wrote an academic paper at SLE2020 (November 16) on Alectryon (preprint on my website since the DOI link doesn't resolve yet). It has plenty of cool visualizations and examples, it goes into much more depth than this intro, and importantly it has all the related work, including lots of stuff on procedural vs declarative proofs. This blog post, the paper, and the talk were all built with Alectryon.

If this is your first time on this blog, you might want to check the very short tutorial on navigating these visualizations before proceeding with the rest of this post.A quick tour of Alectryon

The library was written with two scenarios in mind:

Making it easier to browse Coq developments (even if these developments are not written in literate style) by turning Coq source files into webpages allowing readers to replay proofs in their browser (the “Proviola” style). As a demo, I recorded goals and responses for a complete build of the Flocq library.

Writing documents mixing Coq source code and explanatory prose, either starting from a text file containing special directives (the “coqtex” and “coqrst” style, used in Coq's reference manual), or starting from a Coq file containing special comments (the “coqdoc” style, used in CPDT, Software foundations, etc.).

The Alectryon paper, this blog post, and my SLE talk are examples of the former (they are written in reStructuredText, a Markdown-like markup language); as another example, here is a chapter from FRAP and one from CPDT, converted to reStructuredText by hand (change the URLs to .rst to see the sources).

As a demo of the latter here's a full build of Logical Foundations.

There's no support for attaching bits of documentation to specific bits of code, like definitions, axioms, variables, etc. As I've written in the past, I think this is a different job (“docstrings”), ideally to be handled by Coq itself (similar to how it tracks the body and location of definitions). Alectryon also doesn't support hyperlink Coq terms to their definitions like coqdoc can, but I plan to implement this eventually.Generating webpages

Alectryon's main purpose is to record Coq's outputs and interleave them with the corresponding inputs to create an interactive webpage:

: : list nat, length (rev l) = length l.

: list nat, length (rev l) = length l

: list nat, length (rev l) = length l

length (rev l) = length l

l [| n l' IHl'].

length (rev nil) = length nil

length (rev l') = length l'

length (rev (n :: l')) = length (n :: l')

length (rev nil) = length nil

length (rev l') = length l'

length (rev (n :: l')) = length (n :: l')

length (rev l') = length l'

length (rev l' ++ n :: nil) = S (length l')

length (rev l') = length l'

length (rev l') + length (n :: nil) = S (length l')

length (rev l') = length l'

length (n :: nil) + length (rev l') = S (length l')

length (rev l') = length l'

S (length (rev l')) = S (length l')

length (rev l') = length l'

S (length l') = S (length l')

rev_length : : list nat, length (rev l) = length l

Because this is an interactive webpage, we can apply all sorts of post-processing to the output, like using MathJax to make a math proof a bit more readable:

\(\newcommand{\ccQ}{\mathbb{Q}}\) \(\newcommand{\ccNat}{\mathbb{N}}\) \(\newcommand{\ccSucc}[1]{\mathrm{S}\:#1}\) \(\newcommand{\ccFrac}[2]{\frac{#1}{#2}}\) \(\newcommand{\ccPow}[2]{{#1}^{#2}}\) \(\newcommand{\ccNot}[1]{{\lnot #1}}\) \(\newcommand{\ccEvar}[1]{\textit{\texttt{#1}}}\) \(\newcommand{\ccForall}[2]{\forall \: #1. \; #2}\) \(\newcommand{\ccNsum}[3]{\sum_{#1 = 0}^{#2} #3}\)

: , * (nsum n ( => i)) = n * (n + ).

\ccForall{n : \ccNat{}}{ \times \ccNsum{i}{n}{i} = n \times (n + )}

\ccForall{n : \ccNat{}}{ \times \ccNsum{i}{n}{i} = n \times (n + )}

\times = \times ( + )

\times \ccNsum{i}{n}{i} = n \times (n + )

\times (\ccSucc{ n} + \ccNsum{i}{n}{i}) = \ccSucc{ n} \times (\ccSucc{ n} + )

\times = \times ( + )

\times \ccNsum{i}{n}{i} = n \times (n + )

\times (\ccSucc{ n} + \ccNsum{i}{n}{i}) = \ccSucc{ n} \times (\ccSucc{ n} + )


\times \ccSucc{ n} + \times \ccNsum{i}{n}{i} = \ccSucc{ n} \times (\ccSucc{ n} + )

\times \ccSucc{ n} + n \times (n + ) = \ccSucc{ n} \times (\ccSucc{ n} + )

… or using the browser's native support for vector graphics to render Game of Life boards encoded as lists of Booleans into small images:

:= [[;;;;]; [;;;;]; [;;;;]; [;;;;]; [;;;;]].

take (iter conway_life glider).

= [[[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]; [[; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]; [; ; ; ; ]]] : list (list (list bool))

… or using a graph library to draw visualizations that makes it clearer what happens when one builds a red-black tree with Coq.MSets.MSetRBT.

:= MSets.MSetRBT.Make Nat_as_OT.

(: list nat) := List.fold_left ( => RBT.add n (hd RBT.empty trs) :: trs) leaves [] |> List.rev.

build_trees [;;;;].

= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }}] : list RBT.t

build_trees [;;;;].

= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }}; { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': ''; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }}] : list RBT.t

Do these visualizations really help? You be the judge: here's how the red-black tree example looks with plain-text output:

build_trees [;;;;].

= [Node Black Leaf Leaf; Node Black Leaf (Node Red Leaf Leaf); Node Black (Node Black Leaf Leaf) (Node Black Leaf Leaf); Node Black (Node Black Leaf Leaf) (Node Black Leaf (Node Red Leaf Leaf)); Node Black (Node Black Leaf Leaf) (Node Red (Node Black Leaf Leaf) (Node Black Leaf Leaf))] : list t

build_trees [;;;;].

= [Node Black Leaf Leaf; Node Black (Node Red Leaf Leaf) Leaf; Node Black (Node Red Leaf Leaf) (Node Red Leaf Leaf); Node Black (Node Black (Node Red Leaf Leaf) Leaf) (Node Black Leaf Leaf); Node Black (Node Black (Node Red Leaf Leaf) Leaf) (Node Black Leaf (Node Red Leaf Leaf))] : list t

Even if you don't use Alectryon's literate programming features, these webpages have one additional advantage beyond convenient browsing: because they record both your code and Coq's responses, they can serve as a permanent record of your developments immune to bitrot and suitable for archival.Editing literate Coq documents

Besides generating webpages from standalone Coq files, Alectryon can help you write documentation, blog posts, and all sorts of other documents mixing proofs and prose. Alectryon's literate module implements translations from Coq to reStructuredText and from reStructuredText to Coq, which allow you to toggle between two independent views of the same document: one best for editing code, and one best for editing reST prose. Concretely, Alectryon knows how to convert between this:


Writing decision procedures

============================= Here's an inductive type: Inductive Even : nat -> Prop := EvenO : Even O EvenS : forall n, Even n -> Even (S (S n)). It has two constructors: unfold out Check EvenO. Check EvenS.


Writing decision procedures


Here's an inductive type:

It has two constructors:

Because the transformations are (essentially) inverses of each other, you don't have to pick one of these two styles and stick to it (or worse, to maintain two copies of the same document, copy-pasting snippets back and forth). Instead, you can freely switch between using your favorite Coq IDE to write code and proofs while editing bits of prose within comments, and using your favorite reStructuredText editor to write prose.

The reason for picking reStructuredText as the markup language for comments is that it's designed with extensibility in mind, which allows me to plug Alectryon into the standard Docutils and Sphinx compilation pipelines for reStructuredText (Sphinx is what the documentations of Haskell, Agda, Coq, and Python are written in). This is how this blog is written, and in fact you can download the sources if you're curious to see what it looks like. This is also how I made my SLE2020 slides (press p to see the presenter notes) and how I wrote my SLE2020 paper.

A small Emacs package (alectryon.el), allows you to toggle quickly between Coq and reST. The screenshot below demonstrates this feature: on the left is the Coq view of an edited excerpt of Software Foundations, in coq-mode; on the right is the reST view of the same excerpt, in a rst-mode buffer. The conversion is transparent, so editing either view updates the same .v file on disk. Notice the highlight indicating a reStructuredText warning on both sides:

Alectryon's syntax-highlighting is done with Pygments, but it uses an update Coq grammar with a database of keywords and commands extracted directly from the reference manual (ultimately, this part should be merged upstream, and the database-generation tool should be merged into the Coq reference manual; I'll write a separate blog post about it at some point).Recording Coq's output and caching it

Alectryon's design is pretty modular, so if you want to use it for other purposes it's easy to use just some parts of it. In particular, its core is a simple API that takes a list of code snippets, feeds them to Coq through SerAPI, and records goals and messages. This functionality is exposed on the command line (taking json as input and producing json as output) and also as a Python module:

"Example xyz (H: False): True. (* ... *) exact I. Qed."

'Example xyz (H: False): True.'

'xyz = fun _ : False => I

Alectryon uses JSON caches to speed up consecutive runs, but even when performance isn't a problem caches provide a very useful form of regression testing for embedded Coq snippets. Without such tests, it's easy for seemingly innocuous changes in a library to break its documentation in subtle ways. For example, you might have the following snippet:

The function plus is defined recursively:

plus = plus (n m : nat) { n} : nat := n | => m | S p => S (plus p m) : nat → nat → nat Argument scopes are [nat_scope nat_scope]

If you rename plus to Nat.add and add a compatibility notation, this is what your documentation will silently become, with no error or warning to let you realize that something went wrong:

:= Init.Nat.add

This was such a common problem in the reference manual that we implemented workarounds to catch the most egregious cases (where changes caused snippets to print errors instead of executing successfully). But if you check in Alectryon's caches into source control, then the following will show up pretty clearly: "contents": "Print plus.", "messages": [ { "_type": "message",

- "contents": "plus = \nfix plus (n m : nat) {struct n} : nat := …"

+ "contents": "Notation plus := Nat.add" }

All these features are exposed through a command line interface documented in Alectryon's README. This project has been in development for over a year, but there's still lots of rough bits, so expect bugs and please report them!Using AlectryonStandalone usage

The easiest way to get started Alectryon is to use it very much like coqdoc, but using reStructuredText syntax in special comments delimited with (*| and |*), like in this hypothetical even.v document:

Prose. *Emphasis*; **strong emphasis**; ``code``; `coq code`; `link <url>`__.

… which can then be compiled into a static webpage using ../ --frontend coq+rst --backend webpage even.v -o even.html.

This is what I did for FRAP and CPDT. For Software foundations and Flocq, I used a compatibility layer combining Alectryon to render the code and coqdoc to render the prose:find . -name *.v -exec --frontend coqdoc --backend webpage {} \;Authoring tips

There's a great reStructuredText primer on Sphinx's website, if you're new to this markup language (there's also an official quick-reference guide, which is as ugly as it is comprehensive). reStructuredText is no panacea, but it's a decent language with a good story about extensibility, and it's popular for writing documentation (Haskell, Agda, and Coq use it for their reference manuals).

If you use Emacs, you can install alectryon.el, a small Emacs library that makes it easy to toggle between reStructuredText and Coq:


With this, you'll get improved rendering of (*| … |*) comment markers, and you'll be able to toggle between reStructuredText and Coq with a simple press of C-c C-S-a. You probably also want to M-x package-install flycheck and pip3 install --user docutils, though neither of these are hard dependencies.

(Hi, reader! Are you thinking “why isn't this on MELPA?” Great question! It's because I haven't had the time to do it yet. But you can — yes, you! In exchange, I promise I'll sing your praises every time your name comes up in conversation — I might even refer to you as ‘writer-of-MELPA-recipes extraordinaire’.

Alternatively, if you're a member of this most distinguished category of people who write more grant proposals than Emacs Lisp programs, you should drop me a line: I'm on the academic job market this year, so we should chat!)Integrated into a blog or manual

Alectryon is very easy to integrate with platforms and tools that support Sphinx or Docutils, like Pelican, readthedocs, Nikola, etc. (In the long run, I hope to migrate Coq's reference manual to Alectryon. It currently uses coqrst, a previous iteration of Alectryon that I wrote a few years ago based on coqtop instead of SerAPI).

For this blog, for example, I just added the following snippet to our

# Register the ‘.. coq::’ directive

# Copy Alectryon's stylesheet

# Copy a custom Pygments theme with good contrast to theme/pygments \

Similar steps would be needed for Sphinx, though using alectryon.sphinx.register() instead. I hear that there's work in progress to integrate with other blog platforms.As a library

The choice of reStructuredText is a bit arbitrary, so it's not a hard dependency of Alectryon. It should be relatively straightforward to combine it with other input languages (like LaTeX, Markdown, etc.) — I just haven't found the time to do it. There's even an output mode that takes Coq fragments as input and produces individual HTML snippets for each, to make integration easier. See Alectryon's README for more info.

As an example, I made a compatibility shim for Coqdoc that uses Alectryon to render Coq code, responses, and goals, but calls to coqdoc to render the contents of (** … **) comments; look for coqdoc in file of the distribution to see how it works.Writing Coq proofs in Coq+reST

In reStructuredText documents, code in .. coq:: blocks is executed at compilation time; goals and responses are recorded and displayed along with the code. Here's an example:Display all goals and responses

: nat -> := | EvenO : Even O | EvenS : , Even n -> Even (S (S n)).

( : nat) : bool := n | => true | => false | S (S n) => even n .

: , even n = true -> Even n.

: nat, even n = true → Even n

: nat, even n = true → Even n

: nat, even n = true → Even n

n [ | [ | ] ].

: nat, even n = true → Even n

: nat, even n = true → Even n

: nat, even n0 = true → Even n0

even (S (S n)) = true → Even (S (S n))

: nat, even n = true → Even n

: nat, even n = true → Even n

: nat, even n0 = true → Even n0

even n = true → Even (S (S n))

: nat, even n = true → Even n

: nat, even n = true → Even n

: nat, even n0 = true → Even n0

: nat, even n = true → Even n

: nat, even n = true → Even n


(* Inductive case: [S (S _)] *)

: nat, even n0 = true → Even n0

: nat, even n0 = true → Even n0

Interacting with the proof

A small bubble (like this: ) next to a Coq fragment indicates that it produced output: you can either hover, click, or tap on the fragment to show the corresponding goals and messages.

A special ‘Display all goals and responses’ checkbox is added at the beginning of the document, as shown above; its position can be adjusted by adding an explicit .. alectryon-toggle:: directive.

These features do not require JavaScript (only a modern CSS implementation). Optionally, a small Javascript library can be used to enable keyboard navigation, which significantly improves accessibility. You can try it on this page by pressing Ctrl+↑ or Ctrl+↓.

Here is another example of highlighting:

: {: } (: A), Some a = None -> .

( : ) ( : A), Some a = None →

( Some a | Some _ => | None => ).

Some a | Some _ => | None =>

s | Some _ => | None =>

s | Some _ => | None =>

| [ H: = _ |- [] ] => H .

( ( : ) ( : A) ( : Some a = None), := Some a eq_ind_r ( : option A, s0 | Some _ => | None => ) I H)


= ( : ) ( : Some a = None), H (_ = y) (y = Some a) | eq_refl => eq_refl (_ = y) y | Some _ => | None => | eq_refl => I : : , Some a = None → Customizing the output

Directive arguments and special comments can be used to customize the display of Coq blocks. The documentation of Alectryon has details, but here are a few examples:

Run a piece of code silently: none Require Import Coq.Arith.Arith.

Start with all intermediate states shown, hide selectively: unfold Goal True /\ True. () split. () idtac "hello". () apply I. auto. Qed.

Show only a message, hiding the input: Compute (1 + 1). ()

Of course, if you're going to hide the input but show some output (as with .no-input, .messages, or .goals), you'll need to add .unfold, since the usual way to show the output (clicking on the input) won't be available.

The default alectryon.css stylesheet supports two display modes: the proviola style (two windows side by side, with code shown on one side and goals on the other), and this blog's style (with goals shown alongside each fragment when the window is wide enough and below the input line otherwise). Both modes support clicking on an input line to show the output right below it. You can pick a mode by placing theFuture work

There are a few things that would improve the quality of the documents produced by Alectryon, but I don't have immediate plans to tackle all of them, mostly for lack of time:

Adding a LaTeX backend. This is mostly done.

Working on other advanced visualizations, hopefully culminating in a Coq enhancement proposal to have a standardized way to do non-textual notations (you'd attach a function to a type that says how to render it as a graph, or a LaTeX formula, or an SVG picture, or any other form of rendering). I have early results on this for separation logic; please get in touch if you'd like to hear more.

Extending the system to other languages, probably starting with Lean, F*, easyCrypt, and possibly HOL4? It'd be interesting to see how well this generalizes.

Integrating with jsCoq, to allow users to interact with the code directly in the browser (most of the output would be precomputed, but users would also be able to edit the code and recompute the output). For a mock-up of the experience, see the related tools that I built for F*.

Highlighting differences between consecutive goals, possibly using the support that's now built-in in Coq, though see this issue.

Replacing the coqrst tool used by the Coq refman with a version based on Alectryon, which will likely require merging SerAPI into Coq (pretty please?). (This doesn't mean getting rid of or changing the syntax used in the manual, just changing the backend that's used to calculate Coq output). Most of the work is done: I built a prototype for SLE2020.

Ideally, we'd take this opportunity to generate not just highlighted snippets but also JSON output, as a giant regression test (we'd check in the generated JSON, so changes would be indicated by git diff and updating the file would just be a matter of committing it).

Porting Coq's box layout algorithm to JavaScript, or just compiling the existing implementation with js_of_ocaml, and using that to reflow code and messages when page dimensions change. I think CSS is close to being able to support this — I know how to do hov boxes (mostly), but I'm not sure whether hv boxes can be done (and in any case, it would likely be quite slow). It's funny that pretty-printing is a whole subfield of PL, but we've never managed to get implementers of web browsers interested.

Integrating Alectryon with CI to automatically produce annotated listings for all files in a repository.

Let me know if you're interested in tackling one of these. I'd love to work together or offer tips / pointers.