Working with data Parity - Agda

Parity.agda

module Parity where

-- Using Human lib
open import Nat
open import Vector
open import List

-- A vector containing n copies of an element x
vec : {n : Nat} {A : Set} -> A -> Vector A n
vec {zero}  x = end
vec {suc n} x = (n , x) (vec x)


data Parity : Nat -> Set where
  even : (k : Nat) -> Parity (k * 2)
  odd  : (k : Nat) -> Parity (1 + k * 2)


test-vec : Vector Nat 5
test-vec = vec 2


parity : (n : Nat) -> Parity n
parity zero = even zero
parity (suc n) with parity n
... | even k = odd k  -- a proof that n is even. Now I have to prove that it's successor is odd
... | odd  k = even (suc k)  -- a proof that n is odd

-- Parity works with proofs of half the number. Here we are using parity to get half of a number
half : Nat → Nat
half n with parity n
half .(k * 2)       | even k = k
half .(suc (k * 2)) | odd k  = k