BAM Weblog

## Odd Odd Even Agda Proof, Take (suc (suc zero))

2013-08-03

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.