Skip to content

Instantly share code, notes, and snippets.

@puffnfresh puffnfresh/EvenOdd.agda
Last active Dec 20, 2015

What would you like to do?
Proof that two even numbers or two odd numbers added always results in an even number.
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))
_e+e_ : {n m : ℕ} Even n Even m Even (n + m)
evenZero e+e b = b
evenSuc a e+e b = evenSuc (a e+e b)
_o+o_ : {n m : ℕ} Odd n Odd m Even (n + m)
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)
_o+e_ : {n m : ℕ} Odd n Even m Odd (n + m)
oddOne o+e evenZero = oddOne
oddOne o+e evenSuc b = oddSuc (oddOne o+e b)
oddSuc a o+e b = oddSuc (a o+e b)
_e+o_ : {n m : ℕ} Even n Odd m Odd (n + m)
evenZero e+o b = b
evenSuc a e+o b = oddSuc (a e+o b)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.