@@ -100,10 +100,9 @@ evenorodd (S k) = case evenorodd k of
100100
101101||| Every nat is either Even or Odd.
102102evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
103−evenOrOdd Z = Left (0 ** Refl)
104−evenOrOdd (S k) = case evenOrOdd k of
105− Left (half ** pf) => Right (half ** cong {f = S} pf)
106− 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
107106
108107||| No nat is both even and odd.
109108notevenandodd : even n = True -> odd n = True -> Void
@@ -112,11 +111,7 @@ notevenandodd {n = S _} en on = notevenandodd on en
112111
113112||| No nat is both Even and Odd.
114113notEvenAndOdd : Even n -> Odd n -> Void
115−notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd
116−notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =
117− notEvenAndOdd {n = k}
118− (haf ** cong {f = Nat.pred} odd)
119− (pred half ** succDoublePredPred even)
114+notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)
120115
121116||| Evenness is decidable.
122117evenDec : (n : Nat) -> Dec $ Even n
@@ -132,31 +127,44 @@ oddDec n = case evenOrOdd n of
132127
133128----------------------------------------
134129
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)))
133+
135134||| Even plus Even is Even.
136135evenPlusEven : Even j -> Even k -> Even (j + k)
137136evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =
138− rewrite pf_j in
139− rewrite pf_k in
140− (half_j + half_k **
137+ (half_j + half_k **
138+ rewrite pf_j in
139+ rewrite pf_k in
141140 sym $ multDistributesOverPlusLeft half_j half_k 2)
142141
143−||| Odd plus Odd is Even.
144−oddPlusOdd : Odd j -> Odd k -> Even (j + k)
145−oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =
146− rewrite pf_j in
147− rewrite pf_k in
148− rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in
149− rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in
150− (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)
151152
152153||| Even plus Odd is Odd.
153154evenPlusOdd : Even j -> Odd k -> Odd (j + k)
154−evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =
155− rewrite pf_j in
156− rewrite pf_k in
157− rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in
158− rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in
159− (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)
160168
161169||| A helper fact.
162170multShuffle : (a, b, c : Nat) ->
@@ -171,35 +179,39 @@ multShuffle a b c =
171179||| Even times Even is Even.
172180evenMultEven : Even j -> Even k -> Even (j * k)
173181evenMultEven (half_j ** pf_j) (half_k ** pf_k) =
174− rewrite pf_j in
175− rewrite pf_k in
176− (half_j * half_k * 2 **
182+ (half_j * half_k * 2 **
183+ rewrite pf_j in
184+ rewrite pf_k in
177185 multShuffle half_j half_k 2)
178186
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+
179201||| Even times Odd is Even.
180202evenMultOdd : Even j -> Odd k -> Even (j * k)
181−evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =
182− let half = half_j * haf_k * 2 in
183− rewrite pf_j in
184− rewrite pf_k in
185− rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in
186− rewrite multShuffle half_j haf_k 2 in
187− (half_j + half **
188− sym $ multDistributesOverPlusLeft half_j half 2)
203+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej
189204
190205||| Odd times Odd is Odd.
191206oddMultOdd : Odd j -> Odd k -> Odd (j * k)
192−oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =
207+oddMultOdd oj (haf_k ** pf_k) =
193208 let
194− haf = haf_j * haf_k * 2
195− rem = haf_j + haf_k
209+ (i ** (ipj, ei)) = oddSuccEven oj
210+ (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)
196211 in
197− rewrite pf_j in
198− rewrite pf_k in
199− rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in
200− rewrite multShuffle haf_j haf_k 2 in
201− rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in
202− rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in
203− rewrite plusCommutative haf_k haf_j in
204− rewrite sym $ multDistributesOverPlusLeft rem haf 2 in
205− (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)