Idris code from Munich Lambda meetup, 2017-11-20

Proofs.idr

module Proofs

%default total

data Natural : Type where
    Zero : Natural
    Succ : Natural -> Natural

add : Natural -> Natural -> Natural
add Zero y = y
add (Succ x) y = Succ (add x y)

add_zero_right : (n : Natural) -> add n Zero = n
add_zero_right Zero = Refl
add_zero_right (Succ x) = rewrite add_zero_right x in Refl

succ_zero_right : (m, n : Natural) -> add m (Succ n) = Succ (add m n)
succ_zero_right Zero n = Refl
succ_zero_right (Succ m) n = rewrite succ_zero_right m n in Refl

add_comm : (m, n : Natural) -> add m n = add n m
add_comm Zero n = rewrite add_zero_right n in Refl
add_comm (Succ m) n =
    rewrite add_comm m n in
        rewrite succ_zero_right n m in
            Refl

add_assoc : (m, n, o: Natural) -> add (add m n) o = add m (add n o)
add_assoc Zero n o = Refl
add_assoc (Succ m) n o = rewrite add_assoc m n o in Refl


interface Mashable (a : Type) where
    mash : a -> a -> a
    mash_assoc : (x, y, z : a) -> mash (mash x y) z = mash x (mash y z)

interface Mashable a => Reducible a where
    nothing : a
    mash_nothing_left : (x : a) -> mash nothing x = x
    mash_nothing_right : (x : a) -> mash x nothing = x

implementation Mashable Natural where
    mash = add
    mash_assoc = add_assoc

implementation Reducible Natural where
    nothing = Zero
    mash_nothing_left = \x => Refl
    mash_nothing_right = add_zero_right

data Even : Natural -> Type where
    EvenZero : Even Zero
    EvenSucc : Even n -> Even (Succ (Succ n))

evenFour : Even (Succ (Succ (Succ (Succ Zero))))
evenFour = EvenSucc (EvenSucc EvenZero)

evenThree : Even (Succ (Succ (Succ Zero))) -> Void
evenThree (EvenSucc EvenZero) impossible
evenThree (EvenSucc (EvenSucc _)) impossible

data Odd : Natural -> Type where
    OddOne : Odd (Succ Zero)
    OddSucc : Odd n -> Odd (Succ (Succ n))

evenSuccOdd : {n : Natural} -> Even n -> Odd (Succ n)
evenSuccOdd EvenZero = OddOne
evenSuccOdd (EvenSucc y) = OddSucc (evenSuccOdd y)

oddSuccEven : {n : Natural} -> Odd n -> Even (Succ n)
oddSuccEven OddOne = EvenSucc EvenZero
oddSuccEven (OddSucc y) = EvenSucc (oddSuccEven y)

evenOrOdd : (n : Natural) -> Either (Even n) (Odd n)
evenOrOdd Zero = Left EvenZero
evenOrOdd (Succ x) =
    case evenOrOdd x of
        Left even => Right (evenSuccOdd even)
        Right odd => Left (oddSuccEven odd)

evenAndOdd : {n : Natural} -> Even n -> Odd n -> Void
evenAndOdd EvenZero OddOne impossible
evenAndOdd EvenZero (OddSucc _) impossible
evenAndOdd (EvenSucc y) (OddSucc z) = evenAndOdd y z

oddPlusOdd : {n, m : Natural} -> Odd n -> Odd m -> Even (add n m)
oddPlusOdd OddOne y = oddSuccEven y
oddPlusOdd (OddSucc x) y = EvenSucc (oddPlusOdd x y)