Almost 2 years ago I attempted to write an Agda proof that two odd numbers added together always result in an even number.

I picked Agda up again yesterday to have a little play. I quickly wrote a HList, which used a list of types at the type level to represent the heterogeneity:

data HList : List Set → Set1 where
  HCons : forall {x xs} → x → HList xs → HList (x ∷ xs)
  HNil : HList []

Really interesting. I definitely attribute some of my understanding to working on shapeless.

I felt comfortable enough to be able to go back to my original “odd + odd = even” proof in Agda. I was so impressed by Agda that I’m writing this.

Here we create types for even and odd, each taking a natural number type:

module EvenOdd where

open import Data.Nat

data Even : ℕ → Set where
  evenZero : Even 0
  evenSuc : {n : ℕ} → Even n → Even (suc (suc n))

data Odd : ℕ → Set where
  oddOne : Odd 1
  oddSuc : {n : ℕ} → Odd n → Odd (suc (suc n))

Next, we just write a type signature like so:

_o+o_ : {n m : ℕ} → Odd n → Odd m → Even (n + m)

Agda has an interactive Emacs mode. We can write this:

a o+o b = ?

Then load it in Agda C-c C-l for it to find the ? as a goal:

a o+o b = {  }0

We can get Agda to expand the patterns by typing C-c C-c a RET (i.e. expand the a cases). It comes out like so:

oddOne o+o b = {  }0
oddSuc a o+o b = {  }1

We can expand the b side, similarly:

oddOne o+o oddOne = {  }0
oddOne o+o oddSuc b = {  }1
oddSuc a o+o b = {  }2

Looks like all the cases are covered. Now, here’s the coolest part. We just hit C-c C-a over each of the goals and Agda figures out the only possible solution:

oddOne o+o oddOne = evenSuc evenZero
oddOne o+o oddSuc b = evenSuc (oddOne o+o b)
oddSuc a o+o b = evenSuc (a o+o b)

Amazing.

With Agda’s huge help, we’ve proved that adding two odd numbers always results in an even number.

Try it for yourself with the following type signature:

_e+e_ : {n m : ℕ} → Even n → Even m → Even (n + m)

I’ve posted the answer if you can’t properly setup Agda or Emacs.