Proof that numbers go even-odd-even-odd...

EvenOdd.hs

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

data Nat = Zero | Succ Nat

data Even :: Nat -> * where
    Even_base :: Even Zero
    Even_induct :: Even k -> Even (Succ (Succ k))

data Odd :: Nat -> * where
    Odd_base :: Odd (Succ Zero)
    Odd_induct :: Odd k -> Odd (Succ (Succ k))


-- Proof that numbers go even-odd-even-odd...
evenOdd :: Even n -> Odd (Succ n)
evenOdd Even_base = Odd_base
evenOdd (Even_induct k) = let ih = evenOdd k -- inductive hypothesis
                            in Odd_induct ih

oddEven :: Odd n -> Even (Succ n)
oddEven Odd_base = Even_induct Even_base
oddEven (Odd_induct k) = let ih = oddEven k
                            in Even_induct ih