I’m reading a book titled “The Haskell Road to Logic, Maths and Programming”, it teaches Haskell by using logic and logic by using Haskell. I’m using the book to get better at reading and writing proofs. I’m also trying to learn languages like Coq and Agda to solve exercises in the book.

One of the first exercises in Chapter 3 (The Use of Logic: Proof) is 3.4:

• Assume that n and m belong to the set of natural numbers
• Show that: if m is odd and n is odd then m + n is even

My proof involved:

• n-1 is even
• m-1 is even
• 2 is even
• Thus n-1 + m-1 + 2 = n + m is even

I decided to try Agda on this proof. First I needed to define a data type for even and odd numbers. I eventually came up with a mutually recursive definition:

mutual
  data Even : Set where
    zeroE : Even
    succE : Odd -> Even
  data Odd : Set where
    succO : Even -> Odd

The base case is even zero. Every number after is built like so:

succE (succO (succE (succO zeroE)))

This example represents 4 and belongs to the even set.

The above problem has this type signature:

_odd+_ : Odd -> Odd -> Even

That is, an odd plus an odd always equals an even.

The first two cases for this function are easy. If either side is one (succO zeroE), then we just increment the other side, which makes it even:

succO zeroE     odd+ n               = succE n
n               odd+ succO zeroE     = succE n

The last case is a bit confusing. We take 2 off each side to get to the previous odd number, recurse and then add back on the 4 that we subtracted:

succO (succE n) odd+ succO (succE m) = succE (succO (succE (succO (n odd+ m))))

I started writing the proof in Agda but didn’t end up using any dependent types - a unique feature to languages like Agda. My solution could have easily been made by using another language. For example, here is a direct Haskell translation:

data Even = ZeroE | SuccE Odd
data Odd  = SuccO Even

oddPlus :: Odd -> Odd -> Even
oddPlus (SuccO ZeroE) n = SuccE n
oddPlus n (SuccO ZeroE) = SuccE n
oddPlus (SuccO (SuccE n)) (SuccO (SuccE m)) = SuccE $ SuccO $ SuccE $ SuccO $ oddPlus n m

Maybe I’m not familiar enough with dependent types to use them in my solution. I imagine that a larger chunk of the problem could have been encoded into the type system. Hopefully I’ll figure out some tricks as I work through the book.