@@ -14,3 +14,78 @@ mutual
14 odd : Nat -> Bool
14 odd : Nat -> Bool
15 odd Z = False
15 odd Z = False
16 odd (S k) = even k
16 odd (S k) = even k
18+||| A nat is Even when it is twice some other nat.
20+Even n = (half : Nat ** n = half * 2)
22+||| A nat is Odd when it is one more than twice some other nat.
24+Odd n = (haf : Nat ** n = S $ haf * 2)
26+||| Two more than an Even is Even.
27+add2Even : Even n -> Even (2 + n)
28+add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)
30+||| Two more than an Odd is Odd.
31+add2Odd : Odd n -> Odd (2 + n)
32+add2Odd (haf ** pf) = (S haf ** cong {f = (+) 2} pf)
34+||| One more than an Even is Odd.
35+succEvenOdd : Even n -> Odd (S n)
36+succEvenOdd (half ** pf) = (half ** cong {f = S} pf)
38+||| One more than an Odd is Even.
39+succOddEven : Odd n -> Even (S n)
40+succOddEven (haf ** pf) = (S haf ** cong {f = S} pf)
42+||| One less than an Odd is Even.
43+predOddEven : Odd (S n) -> Even n
44+predOddEven (haf ** pf) = (haf ** cong {f = Nat.pred} pf)
47+succDoublePredPred : S n = k * 2 -> n = S $ (pred k) * 2
48+succDoublePredPred {k = Z} prf = absurd prf
49+succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf
51+||| One less than an Even is Odd.
52+predEvenOdd : Even (S n) -> Odd n
53+predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)
55+||| Every nat is either Even or Odd.
56+evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
57+evenOrOdd Z = Left (0 ** Refl)
58+evenOrOdd (S k) = case evenOrOdd k of
59+ Left (half ** pf) => Right (half ** cong {f = S} pf)
60+ Right (haf ** pf) => Left (S haf ** cong {f = S} pf)
62+||| No nat is both Even and Odd.
63+notEvenAndOdd : Even n -> Odd n -> Void
64+notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd
65+notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =
66+ notEvenAndOdd {n = k}
67+ (haf ** cong {f = Nat.pred} odd)
68+ (pred half ** succDoublePredPred even)
70+||| Evenness is decidable.
71+evenDec : (n : Nat) -> Dec $ Even n
72+evenDec n = case evenOrOdd n of
73+ Left even => Yes even
74+ Right odd => No $ \even => notEvenAndOdd even odd
76+||| Oddness is decidable.
77+oddDec : (n : Nat) -> Dec $ Odd n
78+oddDec n = case evenOrOdd n of
79+ Left even => No $ notEvenAndOdd even
84+ evenEven : Even n -> even n = True
85+ evenEven {n = Z} _ = Refl
86+ evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
89+ oddOdd : Odd n -> odd n = True
90+ oddOdd {n = Z} (_ ** pf) = absurd pf
91+ oddOdd {n = S _} pf = evenEven $ predOddEven pf