The other day I gave a very short introductory talk on formalising mathematics in Agda to a highly mathematically literate but otherwise quite general audience. I presented this example.

In Agda, proofs and programs are the same thing, types are sets are propositions. These sets contain values of that type, or equally they contain proofs of that proposition.

Agda is a very expressive language so very little is built in and most things can be defined in a library. We will define some of those things now to see how they work.

module talk where

Natural numbers (0,1,2,3,…) can be seen as being defined by either `zero`

or the successor (+1) `suc`

of another natural number.

data Nat : Set where
zero : Nat
suc : Nat → Nat

Addition `_+_`

takes two natural numbers and returns another. It can be defined by recursion (induction) on the first argument. If it is `zero`

we return `n`

and if it is successor we can make a recursive call to `(m + n)`

and apply the successor to the result. The recursive call (inductive hypothesis) is valid as `m`

is structurally smaller than `suc m`

.

_+_ : Nat → Nat → Nat
zero + n = n
suc m + n = suc (m + n)

Having defined one function we now want to prove something about it. One can think of this as an exercise in formal verification. I want to prove that `_+_`

satisfies some equations. There is an equals sign in the definition above but this is not the one I should use to state my equations. The `=`

is the definitional equality symbol and denotes equations that the computer can see are true. I want to *prove* some things that the computer isn’t able to see for itself.

The notion we need is propositional equality which is a relation we will define now. In another language one might expect a relation to have type like `Nat → Nat → Bool`

which might return true if the natural numbers were equal. In Agda we would use `Set`

instead of `Bool`

and the set would be inhabited if the relation holds. We can define propositional equality `_≅_`

once and for all for any set `A`

which we write as an implicit parameter `{A : Set}`

. Remarkably this set has only one canonical inhabitant `refl`

which is inhabits the type of equations between really identical (definitionally equal) values. This may seem strange but one can prove (derive) the other properties, such as symmetry and transitivity.

-- propositional equality
data _≅_ {A : Set} : A → A → Set where
refl : ∀{a} → a ≅ a

We could prove useful lemmas such as symmetry now but for this post I will only need `cong`

– that functions preserve equality. Given any function `f : A → B`

and two equal elements of `A`

the function should return equal results.

The lemma is very easy to prove as when we pattern match on the proof that the elements are equal then the only possible pattern is `refl`

which forces `a`

and `a'`

to be equal, replacing, say, `a'`

with `a`

which reduces our task to showing that `f a ≅ f a`

. This is easily proved using `refl`

.

-- lemma: functions preserve equality
cong : {A B : Set} → (f : A → B) → {a a' : A} → a ≅ a' → f a ≅ f a'
cong f refl = refl

The lemma is very useful for proving equations that have the same function (such as `suc`

) on both sides. We can use it to reduce our task to proving that what is underneath the function on both sides is equal.

One can define an algebraic structure like a monoid as a record (named tuple/struct/etc.) in Agda. It contains fields for the *data* and also for the laws. A monoid has a carrier set `M`

a distinguished unit element `e`

and a binary operation `op`

. The three laws state that `op`

has `e`

as its left and right unit and it is associative. The monoid record `Mon`

lives in `Set1`

as it contains a `Set`

(`0`

).

-- Monoid
record Mon : Set1 where
-- data
field M : Set
e : M
op : M → M → M
-- laws
lunit : ∀ m → op e m ≅ m
runit : ∀ m → op m e ≅ m
assoc : ∀ m n o → op (op m n) o ≅ op m (op n o)

The goal is to define a monoid where `M = Nat`

, `e = zero`

and `op = _+_`

. Let’s go ahead and prove the laws. The first law which would be `(zero + n) ≅ n`

doesn’t require proof as it holds definitionally (it is the first line of the definition of `_+_`

). The second law does require proof as here the `_+_`

doesn’t compute as the first argument is the variable `n`

.

+runit : ∀ n → (n + zero) ≅ n
+runit zero = refl
+runit (suc n) = cong suc (+runit n)

We prove the second law `+runit`

by induction on `n`

. When proving a property of a program as we are doing here it’s a good idea to follow the same pattern in the proof as in the program. Here `_+_`

is defined by recursion on its first argument so it makes sense to carry out the proof by induction on the first argument too. This makes things compute nicely. The first case is `zero + zero ≅ zero`

which Agda computes to `zero ≅ zero`

by applying the definition of `_+_`

. This is easily proved by `refl`

. The second case computes to `suc (n + zero) ≅ suc n`

. First we observe that there is a function `suc`

on both sides so we type `cong suc ?`

. This reduces our problem to proving that `n + zero ≅ n`

which follows from the inductive hypothesis `+runit n`

+assoc : ∀ m n o → ((m + n) + o) ≅ (m + (n + o))
+assoc zero n o = refl
+assoc (suc m) n o = cong suc (+assoc m n o)

The proof for associativity proceeds analogously. We pattern match on the first argument `m`

which gives two cases. The first case computes to `n + o ≅ n + o`

and the second computes to `suc ((m + n) + o) ≅ suc (m + (n + 0))`

. As before the first case follows by reflexivity and the second case by congruence of `suc`

and inductive hypothesis.

Having done all the hard work we can now define a monoid for `Nat`

, `_+_`

, and `zero`

:

-- natural numbers with addition form a monoid
NatMon : Mon
NatMon = record {
M = Nat;
e = zero;
op = _+_;
lunit = λ _ → refl; -- this one doesn't require proof
runit = +runit;
assoc = +assoc}