56 lines
1.4 KiB
Idris
56 lines
1.4 KiB
Idris
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
|