module HomeworkFive
import HomeworkFour
%default total

zeroEven : even Z = True
zeroEven = Refl

twoEven : even (S (S Z)) = True
twoEven = Refl

threeOdd : even (S (S (S Z))) = False
threeOdd = Refl

fourEven : even (S (S (S (S Z)))) = True
fourEven = Refl

xor : Bool -> Bool -> Bool
xor True p = not p
xor False p = p

xorNot : b1 = b2 -> xor (not b1) b2 = True
xorNot {b1=True} Refl = Refl
xorNot {b1=False} Refl = Refl

xorEq : xor (not b1) b2 = b1 == b2
xorEq {b1=True} {b2=True} = Refl
xorEq {b1=True} {b2=False} = Refl
xorEq {b1=False} {b2=True} = Refl
xorEq {b1=False} {b2=False} = Refl

plusE : even n = bn -> even m = bm -> even (n+m) = (xor (not bn) bm)
plusE {n=Z} Refl p = p
plusE {n=S Z} Refl p = evenFlip p
plusE {n=S (S m)} p1 p2 = plusE {n=m} p1 p2

plusEE : even n = True -> even m = True -> even (n+m) = True
plusEE = plusE

plusOE : even n = False -> even m = True  -> even (n+m) = False
plusOE = plusE

plusEO : even n = True  -> even m = False -> even (n+m) = False
plusEO = plusE

plusOO : even n = False -> even m = False -> even (n+m) = True
plusOO = plusE

plusEvenOdd : even n = even m -> even (n+m) = True
plusEvenOdd p = replace (xorNot (sym p)) $ plusE p (sym p)

plusEvenOdd' : even n = x -> even m = y -> even (n+m) = x==y
plusEvenOdd' p1 p2 = replace xorEq (plusE p1 p2)

plusEvenOdd'' : even n = x -> even m = y -> x = y -> even (n+m) = True
plusEvenOdd'' Refl Refl eq = plusEvenOdd eq