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

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.