@@ -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,20 +45,73 @@ 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)
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)
103+evenOrOdd n = case evenorodd n of
104+ Left e => Left $ evenEvenConverse e
105+ Right o => Right $ oddOddConverse o
106+
107+||| No nat is both even and odd.
108+notevenandodd : even n = True -> odd n = True -> Void
109+notevenandodd {n = Z} en on = absurd on
110+notevenandodd {n = S _} en on = notevenandodd on en
61111
62112||| No nat is both Even and Odd.
63113notEvenAndOdd : 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)
114+notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)
69115
70116||| Evenness is decidable.
71117evenDec : (n : Nat) -> Dec $ Even n
@@ -79,42 +125,46 @@ oddDec n = case evenOrOdd n of
79125 Left even => No $ notEvenAndOdd even
80126 Right odd => Yes odd
81127
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
128+----------------------------------------
87129
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
130+||| An Odd is the successor of an Even.
131+oddSuccEven : Odd n -> (m : Nat ** (n = S m, Even m))
132+oddSuccEven (haf ** pf) = (haf * 2 ** (pf, (haf ** Refl)))
92133
93134||| Even plus Even is Even.
94135evenPlusEven : Even j -> Even k -> Even (j + k)
95136evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =
96− rewrite pf_j in
97− rewrite pf_k in
98− (half_j + half_k **
137+ (half_j + half_k **
138+ rewrite pf_j in
139+ rewrite pf_k in
99140 sym $ multDistributesOverPlusLeft half_j half_k 2)
100141
101−||| Odd plus Odd is Even.
102−oddPlusOdd : Odd j -> Odd k -> Even (j + k)
103−oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =
104− rewrite pf_j in
105− rewrite pf_k in
106− rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in
107− rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in
108− (S (haf_j + haf_k) ** Refl)
142+||| Odd plus Even is Odd.
143+oddPlusEven : Odd j -> Even k -> Odd (j + k)
144+oddPlusEven oj ek =
145+ let
146+ (i ** (ipj, ei)) = oddSuccEven oj
147+ (half_ik ** eik) = evenPlusEven ei ek
148+ in
149+ (half_ik **
150+ rewrite ipj in
151+ cong {f = S} eik)
109152
110153||| Even plus Odd is Odd.
111154evenPlusOdd : Even j -> Odd k -> Odd (j + k)
112−evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =
113− rewrite pf_j in
114− rewrite pf_k in
115− rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in
116− rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in
117− (half_j + haf_k ** Refl)
155+evenPlusOdd {j} {k} ej ok = rewrite plusCommutative j k in oddPlusEven ok ej
156+
157+||| Odd plus Odd is Even.
158+oddPlusOdd : Odd j -> Odd k -> Even (j + k)
159+oddPlusOdd oj ok =
160+ let
161+ (i ** (ipj, ei)) = oddSuccEven oj
162+ (haf_ik ** oik) = evenPlusOdd ei ok
163+ in
164+ (S haf_ik **
165+ rewrite ipj in
166+ rewrite oik in
167+ Refl)
118168
119169||| A helper fact.
120170multShuffle : (a, b, c : Nat) ->
@@ -129,35 +179,39 @@ multShuffle a b c =
129179||| Even times Even is Even.
130180evenMultEven : Even j -> Even k -> Even (j * k)
131181evenMultEven (half_j ** pf_j) (half_k ** pf_k) =
132− rewrite pf_j in
133− rewrite pf_k in
134− (half_j * half_k * 2 **
182+ (half_j * half_k * 2 **
183+ rewrite pf_j in
184+ rewrite pf_k in
135185 multShuffle half_j half_k 2)
136186
187+||| Odd times Even is Even.
188+oddMultEven : Odd j -> Even k -> Even (j * k)
189+oddMultEven oj (half_k ** pf_k) =
190+ let
191+ (i ** (ipj, ei)) = oddSuccEven oj
192+ (half_ik ** oik) = evenMultEven ei (half_k ** pf_k)
193+ in
194+ (half_k + half_ik **
195+ rewrite multDistributesOverPlusLeft half_k half_ik 2 in
196+ rewrite ipj in
197+ rewrite oik in
198+ rewrite pf_k in
199+ Refl)
200+
137201||| Even times Odd is Even.
138202evenMultOdd : Even j -> Odd k -> Even (j * k)
139−evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =
140− let half = half_j * haf_k * 2 in
141− rewrite pf_j in
142− rewrite pf_k in
143− rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in
144− rewrite multShuffle half_j haf_k 2 in
145− (half_j + half **
146− sym $ multDistributesOverPlusLeft half_j half 2)
203+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej
147204
148205||| Odd times Odd is Odd.
149206oddMultOdd : Odd j -> Odd k -> Odd (j * k)
150−oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =
207+oddMultOdd oj (haf_k ** pf_k) =
151208 let
152− haf = haf_j * haf_k * 2
153− rem = haf_j + haf_k
209+ (i ** (ipj, ei)) = oddSuccEven oj
210+ (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)
154211 in
155− rewrite pf_j in
156− rewrite pf_k in
157− rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in
158− rewrite multShuffle haf_j haf_k 2 in
159− rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in
160− rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in
161− rewrite plusCommutative haf_k haf_j in
162− rewrite sym $ multDistributesOverPlusLeft rem haf 2 in
163− (rem + haf ** Refl)
212+ (haf_k + half_ik **
213+ rewrite multDistributesOverPlusLeft haf_k half_ik 2 in
214+ rewrite ipj in
215+ rewrite eik in
216+ rewrite pf_k in
217+ Refl)