@@ -2,18 +2,9 @@ module Data.Nat.Parity
22
33%access public export
44
5−--------------------------------------------------------------------------------
6−-- Parity
7−--------------------------------------------------------------------------------
5+----------------------------------------
86
9−mutual
10− even : Nat -> Bool
11− even Z = True
12− even (S k) = odd k
13−
14− odd : Nat -> Bool
15− odd Z = False
16− odd (S k) = even k
7+-- Type-level, constructive definitions of parity.
178
189||| A nat is Even when it is twice some other nat.
1910Even : Nat -> Type
@@ -23,6 +14,8 @@ Even n = (half : Nat ** n = half * 2)
2314Odd : Nat -> Type
2415Odd n = (haf : Nat ** n = S $ haf * 2)
2516
17+----------------------------------------
18+
2619||| Two more than an Even is Even.
2720add2Even : Even n -> Even (2 + n)
2821add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)
@@ -52,6 +45,59 @@ succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf
5245predEvenOdd : Even (S n) -> Odd n
5346predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)
5447
48+----------------------------------------
49+
50+-- Boolean definitions of parity.
51+
52+mutual
53+ even : Nat -> Bool
54+ even Z = True
55+ even (S k) = odd k
56+
57+ odd : Nat -> Bool
58+ odd Z = False
59+ odd (S k) = even k
60+
61+----------------------------------------
62+
63+-- The boolean and type-level definitions are equivalent in the sense
64+-- that a proof of one can be gotten from a proof of the other.
65+
66+mutual
67+ ||| Evens are even.
68+ evenEven : Even n -> even n = True
69+ evenEven {n = Z} _ = Refl
70+ evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
71+
72+ ||| Odds are odd.
73+ oddOdd : Odd n -> odd n = True
74+ oddOdd {n = Z} (_ ** pf) = absurd pf
75+ oddOdd {n = S _} pf = evenEven $ predOddEven pf
76+
77+mutual
78+ ||| If it's even, it's Even.
79+ evenEvenConverse : even n = True -> Even n
80+ evenEvenConverse {n = Z} prf = (0 ** Refl)
81+ evenEvenConverse {n = S k} prf =
82+ let (haf ** pf) = oddOddConverse prf in
83+ (S haf ** cong pf)
84+
85+ ||| If it's odd, it's Odd
86+ oddOddConverse : odd n = True -> Odd n
87+ oddOddConverse {n = Z} prf = absurd prf
88+ oddOddConverse {n = S k} prf =
89+ let (half ** pf) = evenEvenConverse prf in
90+ (half ** cong pf)
91+
92+----------------------------------------
93+
94+||| Every nat is either even or odd.
95+evenorodd : (n : Nat) -> Either (even n = True) (odd n = True)
96+evenorodd Z = Left Refl
97+evenorodd (S k) = case evenorodd k of
98+ Left l => Right l
99+ Right r => Left r
100+
55101||| Every nat is either Even or Odd.
56102evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
57103evenOrOdd Z = Left (0 ** Refl)
@@ -59,6 +105,11 @@ evenOrOdd (S k) = case evenOrOdd k of
59105 Left (half ** pf) => Right (half ** cong {f = S} pf)
60106 Right (haf ** pf) => Left (S haf ** cong {f = S} pf)
61107
108+||| No nat is both even and odd.
109+notevenandodd : even n = True -> odd n = True -> Void
110+notevenandodd {n = Z} en on = absurd on
111+notevenandodd {n = S _} en on = notevenandodd on en
112+
62113||| No nat is both Even and Odd.
63114notEvenAndOdd : Even n -> Odd n -> Void
64115notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd
@@ -79,16 +130,7 @@ oddDec n = case evenOrOdd n of
79130 Left even => No $ notEvenAndOdd even
80131 Right odd => Yes odd
81132
82−mutual
83− ||| Evens are even.
84− evenEven : Even n -> even n = True
85− evenEven {n = Z} _ = Refl
86− evenEven {n = S _} pf = oddOdd $ predEvenOdd pf
87−
88− ||| Odds are odd.
89− oddOdd : Odd n -> odd n = True
90− oddOdd {n = Z} (_ ** pf) = absurd pf
91− oddOdd {n = S _} pf = evenEven $ predOddEven pf
133+----------------------------------------
92134
93135||| Even plus Even is Even.
94136evenPlusEven : Even j -> Even k -> Even (j + k)