Proving Parity in Idris

Posted on November 19, 2017 by Marko Dimjašević

Idris is a pure functional programming language with dependent types. In this post I am giving an example by David Christiansen on proving a parity theorem (or property) in Idris. The theorem states that every natural number is either even or odd. The example below demonstrates how to do theorem proving with a functional programming language such as Idris. It relies on equality expressed at the type level, which is possible thanks to dependent types. With that, Idris stands in stark contrast to languages such as Scala, where equality is broken. In the example, allEvenOrOdd k is a proof for every natural number k.

data Even : Nat -> Type where
  MkEven : (half : Nat) -> (k = half + half) -> Even k

zeroEven : Even 0
zeroEven = MkEven 0 Refl

data Odd : Nat -> Type where
  MkOdd : (half : Nat) -> (k = S (half + half)) -> Odd k

evenSOdd : Even k -> Odd (S k)
evenSOdd (MkEven half prf) = MkOdd half (cong prf)

oddSEven : Odd k -> Even (S k)
oddSEven (MkOdd half prf) = 
  MkEven (S half) (cong (trans prf $ plusSuccRightSucc half half))

allEvenOrOdd : (k : Nat) -> Either (Even k) (Odd k)
allEvenOrOdd Z = Left zeroEven
allEvenOrOdd (S k) = case allEvenOrOdd k of
                       Left l => Right $ evenSOdd l
                       Right r => Left $ oddSEven r