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}
Theory Lunch 