Odd Odd Even Agda Proof
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
n-1 + m-1 + 2 = n + mis 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.