# An Agda eDSL for well-typed Hilbert style proofs

## Table of Contents

I present an Agda eDSL for writing Hilbert style proofs for logic $K$.

This blog consists of two main parts. The first part presents the language and some examples. The second offers some insight into the key parts of the implementation. The latter targets Agda beginner/intermediate users or any programmer interested in dependent types.

The code is available here. It has been implemented using Agda 2.6.0 with the standard library (at this specific commit).

## Some introductory concepts

**What is an eDSL?** The acronym eDSL stands for Embedded Domain Specific
Language. It refers to a small language (a set of functions and data types)
embedded in another language (in this case Agda) that has been designed to
solve a problem in a very specific domain, in this case, Hilbert style proofs.

**What is a Hilbert style proof?** First we need to know what a Hilbert calculus
is. A Hilbert calculus is a set of axioms plus a set of rules. The axioms are
formulas that we accept as primitive theorems and the rules allow us to
syntactically combine existing theorems to create new ones. Then, a Hilbert
style proof is a sequence of formulas where each formula is either an axiom of
the calculus or the result of applying a rule to previous formulas in the
sequence. The last formula in the sequence is the theorem of the proof. It is
best understood by seeing a concrete example, if you scroll down you will find
one.

## The eDSL and logic $K$

As a preface, let me remark that that the chosen logic, $π²$, is not of special importance here, it just lays the ground for some concrete examples. In fact, it would be interesting to implement a logic agnostic eDSL in the future.

Let's begin by defining the syntax of modal formulas:

\[ \begin{eqnarray} ModalFm β Var\ |\ ModalFm β ModalFm\ |\ β‘ ModalFm \ |\ β₯ \\ \end{eqnarray} \]

Of course, we are missing important logical connectives like $Β¬,β§,β¨$, but it is better to have a small core language and define the other connectives in terms of the primitive ones, for instance:

$$ \begin{align} Β¬Ο & β Οββ₯ \\ Οβ§Ο & β Β¬(ΟβΒ¬Ο) \\ Οβ¨Ο & β Β¬ΟβΟ \\ \end{align} $$

The axioms of $π²$ are the following:

$$ \begin{align} \text{(K1) } & Ο β (Ο β Ο) \\ \text{(K2) } & (Ο β (Ο β ΞΎ)) β ((Ο β Ο) β (Ο β ΞΎ)) \\ \text{(K3) } & (Β¬ Ο β Β¬ Ο) β (Ο β Ο) \\ \text{(Distribution) } & β‘ (Ο β Ο) β (β‘ Ο β β‘ Ο) \end{align} $$

Notice that these are actually axiom schemes (or templates), so $Ο,Ο,ΞΆ$ are formula metavariables which can be substituted for any modal formula.

And the rules are the following:

**Modus Ponens:**If $Ο$ is a theorem and $ΟβΟ$ is a theorem, then $Ο$ is a theorem.

\[\begin{array}{c} ΟβΟ \\ Ο \\ \hline Ο \end{array}\]

**Necessitation:**If $Ο$ is a theorem then $β‘Ο$ is a theorem.

\[\begin{array}{c} Ο \\ \hline β‘Ο \end{array}\]

**Identity:**If $ΟβΞ£$ then $Ξ£β’Ο$. Note that $Ο$ may not be a theorem. See clarification at the end of this section.

Finally! we can construct our first Hilbert style proof. Let's prove $β‘(ΟβΟ)$.

$$ \begin{align} & \text{[ 0 ] } (Ο β ((Ο β Ο) β Ο)) β ((Ο β (Ο β Ο)) β (Ο β Ο)) & \text{By K2} \\ & \text{[ 1 ] } Ο β ((Ο β Ο) β Ο) & \text{By K1} \\ & \text{[ 2 ] } Ο β (Ο β Ο) & \text{By K1} \\ & \text{[ 3 ] } (Ο β (Ο β Ο)) β (Ο β Ο) & \text{By MP 0, 1} \\ & \text{[ 4 ] } Ο β Ο & \text{By MP 3, 2} \\ & \text{[ 5 ] } β‘ (Ο β Ο) & \text{By Nec 4}\\ \end{align} $$

And nowβ¦ how does the same proof look in our eDSL as Agda code? Here it is:

```
β‘β¨ΟβΟβ© : β {Ξ£ Ο} β Ξ£ β’ β‘ (Ο β Ο)
β‘β¨ΟβΟβ© {Ξ£} {Ο} =
begin[ 0 ] (Ο β ((Ο β Ο) β Ο)) β ((Ο β (Ο β Ο)) β (Ο β Ο)) By K2
[ 1 ] Ο β ((Ο β Ο) β Ο) By K1
[ 2 ] Ο β (Ο β Ο) By K1
[ 3 ] (Ο β (Ο β Ο)) β (Ο β Ο) ByMP 0 , 1
[ 4 ] Ο β Ο ByMP 3 , 2
[ 5 ] β‘ (Ο β Ο) ByNec 4
β
```

Wow, they look really similar indeed! So what? Well, we can write Hilbert styles
proofs in a paper-like syntax with the key advantage that Agda's type
checker will make sure that the proof is constructed according to the rules,
that is, that there are **no mistakes** in it. For instance, proofs where an axiom
is instantiated incorrectly, or an application of modus ponens is incorrect will
fail to type check and we will get an error from the compiler telling us where
the misstep is. An additional free perk that we get is that we can easily export the proofs to
rich html or latex.

Let me underline that the code above is actual Agda code. This might be surprising for readers not accustomed to Agda's mixfix operators, which give great syntactical versatility.

It is worth noting that the `By`

step does not only accept axioms, but any
theorem previously proved. So, if we were to prove another theorem and we wanted
to use $β‘ (Ο β Ο)$ as an intermediate step we could do so. Also, since we proved
$β‘(ΟβΟ)$ for any $Ο$, we are free to substitute it for any formula. Example:

```
...
[ 1 ] β‘ (Ο β Ο) By β‘β¨ΟβΟβ©
[ 2 ] β‘ ((Ο β§ Ο) β (Ο β§ Ο)) By β‘β¨ΟβΟβ©
...
```

What about premises? Well, as you may have already noticed in the previous proof, we wrote $Ξ£ β’ β‘ (Ο β Ο)$, where $Ξ£$ is our set of premises, and we are free to use any formula in $Ξ£$ as if it was a theorem within the proof. As an example, let's prove $ΟβΟ,Ο,Ξ£β’Ο$.

```
ΟβΟβ·Οβ·Ξ£β’Ο : β {Ο Ο Ξ£} β Ο β Ο β· Ο β· Ξ£ β’ Ο
ΟβΟβ·Οβ·Ξ£β’Ο {Ο} {Ο} =
begin[ 0 ] Ο By premise 1
[ 1 ] Ο β Ο By premise 0
[ 2 ] Ο ByMP 0 , 1
β
```

**Clarification:** Notice that a formula $Ο$ is a *theorem* of the
logic $K$ if and only if $β
β’Ο$. So in case we have $Ξ£β’Ο$ with $Ξ£$ nonempty it
may be that $Ο$ is not a theorem of $K$. It is worth noting that when we
define `ΟβΟ : β {Ξ£ Ο} : Ξ£ β’ Ο β Ο`

, then the term `ΟβΟ`

is really a proof that
$Ο β Ο$ is a theorem of $K$ since $Ξ£$ is a parameter of the proof and in
particular it can be empty.

This concludes the overview of the language features.

## Implementation tour

We start by defining the syntax of formulas. We define variables to be natural numbers but this is not really relevant.

```
Var : Set
Var = Nat
infixr 20 _β_
data Fm : Set where
_! : Var β Fm
_β_ : Fm β Fm β Fm
β‘ : Fm β Fm
β₯ : Fm
```

Now, if we wanted, we could expand our language by defining more function symbols. For instance, we could define negation thus:

```
Β¬ : Fm β Fm
Β¬ Ο = Ο β β₯
```

We could do the same for $β§,β¨,β’,β€$ and any other operator.

Let's define a data type that represents a proof in Hilbert calculus. As expected, it will have a constructor for each axiom scheme and rule.

```
infix 0 _β’_
data _β’_ (Ξ£ : List Fm) : Fm β Set where
K1 : β {Ο Ο : Fm} β Ξ£ β’ Ο β (Ο β Ο)
K2 : β {Ο Ο ΞΎ : Fm} β Ξ£ β’ (Ο β (Ο β ΞΎ)) β ((Ο β Ο) β (Ο β ΞΎ))
K3 : β {Ο Ο : Fm} β Ξ£ β’ (Β¬ Ο β Β¬ Ο) β (Ο β Ο)
distribution : {Ο Ο : Fm} β Ξ£ β’ β‘ (Ο β Ο) β (β‘ Ο β β‘ Ο)
necessitation : β {Ο : Fm} β Ξ£ β’ Ο β Ξ£ β’ β‘ Ο
mp : β {Ο Ο : Fm} β Ξ£ β’ (Ο β Ο) β Ξ£ β’ Ο β Ξ£ β’ Ο
premise : β {Ο : Fm} β Member Ο Ξ£ β Ξ£ β’ Ο
```

We can now write our first proof. The following proof corresponds to the proof that $ΟβΟ$ is a theorem of $K$ shown above.

```
ΟβΟ : β {Ξ£ Ο} β Ξ£ β’ (Ο β Ο)
ΟβΟ {Ξ£} {Ο} = mp (mp (K2 {Ξ£} {Ο} {Ο β Ο} {Ο}) (K1 {Ξ£} {Ο} {Ο β Ο})) (K1 {Ξ£} {Ο} {Ο})
```

It is horrible to read and too verbose. We can make it a little more succinct by taking advantage of Agda's implicit argument inference:

```
ΟβΟ : β {Ξ£ Ο} β Ξ£ β’ Ο β Ο
ΟβΟ {Ξ£} {Ο} = mp (mp K2 K1) (K1 {Ο = Ο})
```

Much better but still hard for a human to visualize what are the intermediate
steps. Computer programmers could think of this as machine code; something
very useful for its simplicity but hard for humans to use. So, as we do in
programming, we will design a human-friendly language and a compiler that
translates nice looking proofs into (let's call them) *primitive Hilbert style
proofs*. Of course, everything will be guaranteed to work from the types, so
no need to execute any code, just type check it (as is always the case when
using Agda as a proof checker).

### A sketch of the eDSL

We want a language as close to the paper-like syntax showed above as
possible. We will refer to proofs in this language as *nice proofs* and
proofs of the type `_β’_`

as *primitive proofs*. We will refer to the
process of translating nice proofs to primitive proofs as *compilation*.

First we need to think about the type of a nice proof. Well, it needs to keep track of the set of premises, the formula that entails and the length of it, so the following type is what we want.

`data HilbertProof : List Fm β Fm β Nat β Set`

Then the compile function will be of the following type.

`compile : β {n Ξ£ Ο} β HilbertProof Ξ£ Ο n β Ξ£ β’ Ο`

We can now think about which constructors we need for a nice proof.

`By`

. To reference an axiom or another theorem.`MP`

. To apply modus ponens to previous formulas in the proof.`Nec`

. To apply necessitation to a previous formula in the proof.

We will refer to these constructors as *instructions*.

Instructions are numbered with consecutive naturals starting at 0. This
number is used to reference its corresponding formula in subsequent steps.
There must be a special instruction that does not expect instructions before
it. We call this instruction `Begin`

and it works the same as `By`

with the
exception that it can only be used as the first instruction.

### Highlights

We face the following challenges.

**Numbering**. We need to make sure that the user labels the instructions properly.**Proper references**. We need to make sure that the numbers referencing other instructions are in range of the size of the proof and that they reference the appropriate formulas.**Compilation**. We need to translate nice proofs into primitive proofs.

#### Numbering

The numbering certainly looks easier to tackle, so let's start by this one. Instead of trying to solve our problem directly, I propose an alternative problem that captures the same challenge but with no unnecessary noise around it.

Exercise: Boring list

Define a list type such that the first number must be a zero and each subsequent number must be equal to the head plus one.

## Solution

We do so with the help of singleton types.

```
data SingleNat : Nat β Set where
single : (n : Nat) β SingleNat n
data BoringList : Nat β Set where
[_] : SingleNat 0 β BoringList 0
_β·_ : β {n} β SingleNat (suc n) β BoringList n β BoringList (suc n)
example : BoringList 2
example = single 2 β· (single 1 β· [ single 0 ])
```

Well, yeah, this kind of works, but we still have to write `single`

before each
natural number, can't we do better? Yes, indeed! using literal overloading. If
we define a `Number`

instance for `SingleNat`

then we will be able to write
singleton naturals with plain natural numbers.

```
instance
NumNatSing : β {n} β Number (SingleNat n)
NumNatSing {n} .Number.Constraint m = n β‘ m
NumNatSing .Number.fromNat m β¦ refl β¦ = single m
```

Then the example becomes:

```
example : BoringList 2
example = 2 β· (1 β· [ 0 ])
```

Perfect! that's what we needed.

With the previous solution in hand, it is easy to imagine how we can incorporate the same idea into our language.

#### Proper references

Let's focus on the case of modus ponens (necessitation works analogously).
Assuming the modus ponens instruction entails $Ο$, it should receive one
reference to $ΟβΟ$ and another reference to $Ο$. As we mentioned, these
reference will be written as natural numbers by the user, but as we need to
make sure that they are in range and reference the correct formulas, we need
an extra proof object ensuring that. More precisely, assuming we defined the
function `lookup-maybe : β {Ξ£ ΞΆ Ο} β HilbertProof Ξ£ ΞΆ Ο β Nat β Maybe Fm`

with the
expected implementation we would require both proof objects
`lookup-maybe HP i β‘ just (Ο β Ο)`

and `lookup-maybe HP j β‘ just Ο`

.

But in the case that the references are correct, these proof objects will always be trivially solved by normalization and reflexivity, hence the code would look like this:

`[ 3 ] (Ο β (Ο β Ο)) β Ο β Ο ByMP 0 β¨ refl β© , 1 β¨ refl β©`

And we really want to avoid to have the explicit proof object as it makes the syntax unpleasant. Could we use literal overloading for references to previous formulas as well? Yes!

```
data HilbertRef {Ξ£ Ο n} (H : HilbertProof Ξ£ Ο n) (Ο : Fm) : Set where
ref : (i : Nat) β lookup-may H i β‘ just Ο β HilbertRef H Ο
instance
NumRef : β {Ο Ξ£ n} {H : HilbertProof Ξ£ Ο n} {Ο} β Number (HilbertRef H Ο)
NumRef {Ο} {Ξ£} {n} {H} {Ο} .Number.Constraint i = lookup-may H i β‘ just Ο
NumRef {Ο} {Ξ£} {n} {H} .Number.fromNat i β¦ x β¦ = ref i x
```

Now we can write:

` [ 3 ] (Ο β (Ο β Ο)) β Ο β Ο ByMP 0 , 1`

And then each proof object is implicitly embedded in the natural literal `0, 1`

.

#### Compilation

It is hard to highlight a specific part over the others for the compilation process. Compilation is mostly about fiddling with types and proof objects to get the desired translation. If you are interested in this part I suggest you look at the code directly.

### Conclusion

I hope that you enjoyed the reading. Any comments and suggestions are welcome.

I am not an expert Agda programmer, so in case you look at the full code, take it with a pinch of salt :)