[Agda] Writing a paper in Literate Agda

[Alan Jeffrey]

Hi everyone,

I've just been writing a paper using Agda as the mechanical proof 
assistant. Previously, I've just written an Agda file and then 
summarized its content in the paper. This time I decided to try an 
experiment of actually writing the paper in Literate Agda, so the 
mathematics in the paper is actually what has been validated. On the 
whole, the experiment was successful, and I thought I'd summarize some 
of the steps I used.

First of all, I defined some Agda functions such as:

&_ : ∀ {α} {A : Set α} → A → A
& x = x

_\\ : ∀ {α} {A : Set α} → A → A
x \\ = x

and a TeX function |...| which sets mathematics in sans serif so that I 
can control the layout and font of Agda code, for example:

\begin{code}
|idN|    : & |Nat| → |Nat| \\
|idN|(x) = & x
\end{code}

This works for definitions in a fixed universe, but not for universe 
polymorphic definitions, since Setω isn't allowed in user code, so I 
defined:

Member : ∀ {α} → (A : Set α) → A → Set
Member A x = ⊤
syntax Member A x = x ∶ A

which means you can write:

\begin{comment}
\begin{code}
|id| : ∀ {/α} → {/A : Set α} → /A → /A
\end{comment}
\end{code}
\begin{code}
%id-type : ∀ {α} → {A : Set α} →
   |id| ∶ & A → A \\
%id-type = tt
|id|(x) = & x
\end{code}

Why the weird variable names, /α and /A? Well, sometimes you need to 
give Agda hints about not-so-inferrable arguments, and you don't want 
them showing up in the paper, so you write:

\begin{code}
%id-defn : ∀ {α} → {A : Set α} {x} →
   |id|{/A = A}(x) ≡ x
%id-defn = refl
\end{code}

And then with the appropriate bit of LaTeX hackery we can make {/stuff} 
disappear (OK there's probably an easier way to do this then messing 
around with \futurelet, but hey, it works!):

{\global\futurelet\rbr\relax}
\def\gobbleRest{\futurelet\nextchar\gobbleRestOne}
\def\gobbleRestOne{\ifx\nextchar\rbr\else\expandafter\gobbleRestTwo\fi}
\def\gobbleRestTwo#1{\gobbleRest}
\catcode`\/=\active
\def/{\gobbleRest}

So in the paper, this just appears as "id(x) ≡ x" (with the "id" in sans 
serif).

Another trick was to define (as suggested by Martin Escardo):

★ : ∀ {/α} → Set (suc /α)
★ {/α} = Set /α

which means we can write:

\begin{code}
%type-in-type :
   ★ ∶ ★
%type-in-type = tt
\end{code}

and pretend that we're using type-in-type but actually have the real 
development use level polymorphism.

Er that was about it, hope this is useful to someone else writing a 
paper in Literate Agda!

A.