Update

The project that this blog talks about is finished! Here’s a video cast (it’s very fast, based on a terminal recorder):

Link.

Motivation

Recently, I watched the video The future of Mathematics, a mathematician talking about proof assistants (specifically, Lean (3)). When asked about Agda, the lecturer said he was told Agda is not for mathematician, but more of an experiment in type theory.

There is no tactic framework, is that right? Is it just all terms?

He asked. The answer he got is “Not that I just know”, while the fact is that there are more than one. It might be that Agda reflection is not enough documented, but I’d agree that Agda reflection (including the tactic keyword and macros) is just not good enough for writing tactics.

So, what’s wrong about Agda? Well, I split this big question into the following smaller ones:

Introspection

What is a tactic language? How does Coq support it?

A tactic language is an imperative language that interacts with the type checker and generates well-typed terms, which are mostly proofs.

In proof assistants with rich tactic support such as Coq or Lean, you write meta-level code that generates object-level code. You can use your IDE to run the tactics line by line and display the type checking state, so the way terms are generated and types are unified is crystal clear, because you can see how they are generated via the thing that is called “IDE” but actually a debugger that pretends to be an IDE.

With IDEs, your Coq code can’t be more readable. It’s an acceptable pity that Coq is (almost) completely unreadable without an IDE.

Conclusion: proofs in Coq, tactics, describe how the dev create the terms.

How are most proofs in Agda look like?

Agda on the other hand is somehow readable without IDE, because the proofs are presented as terms. The readability doesn’t improve (maybe it does, but very little) with IDEs, because you don’t get more information than more precise syntax highlighting and jump to library definition.

The proof terms are sometimes huge, which are way too unfriendly for a human being to read about.

So how do Agda people come up with proofs? Especially, those scary giant proofs?

Agda has a nice Emacs mode that offers a lot of actions (like IntelliJ quick-fixes) that somehow generate terms or provide information about the current context.

The process is that you write the theorem (aka the type signature), leave the body of the proof as a ?, load it in Emacs agda2-mode, invoke a bunch of actions (generate pattern matches, rewrites, etc.), manually write some function calls and leave the arguments as ?, try filling each of them with Agda’s proof term generator Agsy, if succeed, leave them; if not, hand-write a proof.

We can see that only some (small) parts of the proof terms are written by human. How can we let another human to read them? It’s the process that the proof is written that actually matters (and helps people to understand how things are proved), which is exactly what Coq’s/Lean’s tactic expresses.

Inspiration

In the video, the lecturer showed a webpage generated by a Python tool, which is like some literate programming but with more power – it shows the tactic state for each line of the tactic, with comments in LaTeX that helps people understand what’s going on in the proof. It’s in Lean and French, by the way.

How about putting this into Agda?

A year ago, I found Agda’s literate mode not good enough. It allows you to type-check the Agda code blocks in a markdown file, and compile (a better word will be “render”) it as HTML. Internally, Agda treats the non-code markdown texts as comments, so in the compiled HTML, these non-code things are put into code blocks and highlighted as comments. I want the code to be highlighted and clickable, so I added the flag --html-highlight to Agda, which tells Agda to preserve the non-code texts as-is. However, that’s all about prettifying the generated proof (you can find the documents in this style everywhere in my blog), which is still not good enough.

Implementation

This time, I decide to make a little REPL with few commands that are what one can do in Emacs agda2-mode. The REPL modifies a file while interacting with the user, like what we used to do in Emacs. These commands are “tactic” and can be saved in a file, so when one wanna read a proof, they open up the tactic file and load it in the REPL line by line, watching the REPL’s output and they understand how people prove something.

One thing about Agda’s existing tactic, or reflection system is that there is no tactic state displayed when working with tactics. The type-checker will show the goal type, but it’s still terms – even in tactics they are monadic do-notations – you cannot load the do-notation line by line, because Agda cannot load a program line by line.

Also, to undo one step in the proof, Agda people need to use the undo functionality provided by Emacs. If they closed their Emacs and reopen it later, they can no longer undo unless manually recovering the terms. With tactics, undo is deleting a line in the saved tactic file, which can be done anytime, anywhere.

I’m not sure how it’s gonna be, but I’d like to give it a try. This thing is my attempt, contribution is welcomed :).

P.S. GitHub Actions is awesome. Probably not gonna use Circle CI or AppVeyor anymore :)