@@ -6,7 +6,6 @@ import Data.Sign
66%default total
77%access public export
88
9−
109||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
1110|||
1211||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
@@ -51,7 +50,6 @@ implementation Eq ZZ where
5150 (NegS n) == (NegS m) = n == m
5251 _ == _ = False
5352
54−
5553implementation Ord ZZ where
5654 compare (Pos n) (Pos m) = compare n m
5755 compare (NegS n) (NegS m) = compare m n
@@ -92,7 +90,6 @@ mutual
9290 subZ : ZZ -> ZZ -> ZZ
9391 subZ n m = plusZ n (negate m)
9492
95−
9693implementation Cast ZZ Integer where
9794 cast (Pos n) = cast n
9895 cast (NegS n) = (-1) * (cast n + 1)
@@ -100,7 +97,6 @@ implementation Cast ZZ Integer where
10097implementation Cast Integer ZZ where
10198 cast = fromInteger
10299
103−
104100--------------------------------------------------------------------------------
105101-- Properties
106102--------------------------------------------------------------------------------
@@ -141,6 +137,7 @@ implementation DecEq ZZ where
141137 | No p = No $ \h => p $ negSInjective h
142138
143139-- Plus
140+
144141plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
145142plusZeroLeftNeutralZ (Pos n) = Refl
146143plusZeroLeftNeutralZ (NegS n) = Refl
@@ -213,3 +210,144 @@ plusAssociativeZ (Pos k) c r = lemmaAssocPos k c r
213210plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in
214211 rewrite sym $ doubleNegElim r in
215212 lemmaAssocNegation k (negate c) (negate r) (lemmaAssocPos (S k) (negate c) (negate r))
213+
214+lemmaMinusSymmZero : (k : Nat) -> minusNatZ k k = Pos 0
215+lemmaMinusSymmZero Z = Refl
216+lemmaMinusSymmZero (S k) = let ind = lemmaMinusSymmZero k in
217+ rewrite ind in Refl
218+
219+plusNegateInverseLZ : (a : ZZ) -> a + negate a = Pos Z
220+plusNegateInverseLZ (Pos Z) = Refl
221+plusNegateInverseLZ (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl
222+plusNegateInverseLZ (NegS k) = rewrite lemmaMinusSymmZero k in Refl
223+
224+plusNegateInverseRZ : (a : ZZ) -> negate a + a = Pos Z
225+plusNegateInverseRZ (Pos Z) = Refl
226+plusNegateInverseRZ (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl
227+plusNegateInverseRZ (NegS k) = rewrite lemmaMinusSymmZero k in Refl
228+
229+-- Mult
230+multZeroLeftZeroZ : (right : ZZ) -> (Pos Z) * right = (Pos Z)
231+multZeroLeftZeroZ (Pos k) = Refl
232+multZeroLeftZeroZ (NegS k) = Refl
233+
234+multZeroRightZeroZ : (left : ZZ) -> left * (Pos Z) = (Pos Z)
235+multZeroRightZeroZ (Pos k) = rewrite multZeroRightZero k in Refl
236+multZeroRightZeroZ (NegS k) = rewrite multZeroRightZero k in Refl
237+
238+multOneLeftNeutralZ : (right : ZZ) -> 1 * right = right
239+multOneLeftNeutralZ (Pos k) = rewrite plusZeroRightNeutral k in Refl
240+multOneLeftNeutralZ (NegS k) = rewrite plusZeroRightNeutral k in Refl
241+
242+multOneRightNeutralZ : (left : ZZ) -> left * 1 = left
243+multOneRightNeutralZ (Pos Z) = Refl
244+multOneRightNeutralZ (Pos (S k)) = cong $ multOneRightNeutral (S k)
245+multOneRightNeutralZ (NegS k) = cong $ multOneRightNeutral k
246+
247+multCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left * right = right * left)
248+multCommutativeZ (Pos k) (Pos j) = cong $ multCommutative k j
249+multCommutativeZ (Pos k) (NegS j) = rewrite multCommutative j k in
250+ cong $ multRightSuccPlus k j
251+multCommutativeZ (NegS k) (Pos j) = rewrite multCommutative j (S k) in Refl
252+multCommutativeZ (NegS k) (NegS j) = cong $ multCommutative (S k) (S j)
253+
254+lemmaPosMultNegNat : (k, j : Nat) -> multZ (Pos k) (negNat j) = negNat (mult k j)
255+lemmaPosMultNegNat k Z = rewrite multZeroRightZero k in Refl
256+lemmaPosMultNegNat k (S j) = Refl
257+
258+lemmaNegMultNegNat : (k, j : Nat) -> multZ (NegS k) (negNat j) = multZ (Pos (S k)) (Pos j)
259+lemmaNegMultNegNat k Z = rewrite multZeroRightZero k in Refl
260+lemmaNegMultNegNat k (S j) = Refl
261+
262+lemmaNegatePosNegNat : (k : Nat) -> negate (Pos k) = negNat k
263+lemmaNegatePosNegNat Z = Refl
264+lemmaNegatePosNegNat (S k) = Refl
265+
266+multNegLeftZ : (k : Nat) -> (j : ZZ) -> (NegS k) * j = negate (Pos (S k) * j)
267+multNegLeftZ k (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl
268+multNegLeftZ k (NegS j) = Refl
269+
270+multNegateLeftZ : (k, j : ZZ) -> (negate k) * j = negate (k * j)
271+multNegateLeftZ (Pos Z) j = rewrite multZeroLeftZeroZ j in Refl
272+multNegateLeftZ (Pos (S k)) (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl
273+multNegateLeftZ (Pos (S k)) (NegS j) = Refl
274+multNegateLeftZ (NegS k) j = rewrite sym $ doubleNegElim (multZ (Pos (S k)) j) in
275+ rewrite multNegLeftZ k j in Refl
276+
277+multAssociativeZPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c * r) = ((Pos k) * c) * r
278+multAssociativeZPos k (Pos j) (Pos i) = cong $ multAssociative k j i
279+multAssociativeZPos k (Pos j) (NegS i) = rewrite sym $ multAssociative k j (S i) in lemmaPosMultNegNat k (mult j (S i))
280+multAssociativeZPos k (NegS j) (Pos i) = rewrite multCommutative j i in
281+ rewrite sym $ multRightSuccPlus i j in
282+ rewrite lemmaPosMultNegNat k (mult i (S j)) in
283+ rewrite multCommutativeZ (negNat (mult k (S j))) (Pos i) in
284+ rewrite lemmaPosMultNegNat i (mult k (S j)) in
285+ rewrite multAssociative k i (S j) in
286+ rewrite multAssociative i k (S j) in
287+ rewrite multCommutative i k in Refl
288+multAssociativeZPos k (NegS j) (NegS i) = rewrite multCommutativeZ (negNat (mult k (S j))) (NegS i) in
289+ rewrite lemmaNegMultNegNat i (mult k (S j)) in
290+ rewrite multAssociative k (S j) (S i) in
291+ rewrite multCommutative (mult k (S j)) (S i) in Refl
292+
293+multAssociativeZ : (l, c, r : ZZ) -> l * (c * r) = (l * c) * r
294+multAssociativeZ (Pos k) c r = multAssociativeZPos k c r
295+multAssociativeZ (NegS k) c r = rewrite multNegLeftZ k (c * r) in
296+ rewrite multNegLeftZ k c in
297+ rewrite multNegateLeftZ (multZ (Pos (S k)) c) r in
298+ cong $ multAssociativeZPos (S k) c r
299+
300+lemmaPlusPosNegCancel : (k, j, i : Nat) -> plusZ (Pos (plus k j)) (negNat (plus k i)) = plusZ (Pos j) (negNat i)
301+lemmaPlusPosNegCancel Z j i = Refl
302+lemmaPlusPosNegCancel (S Z) j Z = rewrite plusZeroRightNeutral j in Refl
303+lemmaPlusPosNegCancel (S Z) j (S i) = Refl
304+lemmaPlusPosNegCancel (S (S k)) j i = lemmaPlusPosNegCancel (S k) j i
305+
306+lemmaPlusPosNegZero : (k : Nat) -> plusZ (Pos k) (negNat k) = Pos Z
307+lemmaPlusPosNegZero Z = Refl
308+lemmaPlusPosNegZero (S k) = rewrite lemmaMinusSymmZero k in Refl
309+
310+negNatDistributesPlus : (j, k : Nat) -> plusZ (negNat j) (negNat k) = negNat (plus j k)
311+negNatDistributesPlus Z k = rewrite plusZeroLeftNeutralZ (negNat k) in Refl
312+negNatDistributesPlus (S j) Z = rewrite plusZeroRightNeutral j in Refl
313+negNatDistributesPlus (S j) (S k) = rewrite plusSuccRightSucc j k in Refl
314+
315+-- Distributivity
316+
317+multDistributesOverPlusRightPosPosZ : (l, c : Nat) -> (r : ZZ) -> (Pos l) * ((Pos c) + r) = ((Pos l) * (Pos c)) + ((Pos l) * r)
318+multDistributesOverPlusRightPosPosZ l c (Pos i) = rewrite multDistributesOverPlusRight l c i in Refl
319+multDistributesOverPlusRightPosPosZ l Z (NegS i) = rewrite multZeroRightZero l in
320+ rewrite plusZeroLeftNeutralZ (negNat (mult l (S i))) in Refl
321+multDistributesOverPlusRightPosPosZ l (S c) (NegS Z) = rewrite multOneRightNeutral l in
322+ rewrite multRightSuccPlus l c in
323+ rewrite sym $ plusAssociativeZ (Pos l) (Pos (mult l c)) (negNat l) in
324+ rewrite plusCommutativeZ (Pos (mult l c)) (negNat l) in
325+ rewrite plusAssociativeZ (Pos l) (negNat l) (Pos (mult l c)) in
326+ rewrite lemmaPlusPosNegZero l in Refl
327+multDistributesOverPlusRightPosPosZ l (S c) (NegS (S i)) = let ind = multDistributesOverPlusRightPosPosZ l (assert_smaller (S c) c) (assert_smaller (NegS (S i)) (NegS i)) in
328+ rewrite ind in
329+ rewrite multRightSuccPlus l (S i) in
330+ rewrite multRightSuccPlus l c in
331+ rewrite lemmaPlusPosNegCancel l (mult l c) (mult l (S i)) in Refl
332+
333+multDistributesOverPlusRightPosZ : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c + r) = ((Pos k) * c) + ((Pos k) * r)
334+multDistributesOverPlusRightPosZ k (Pos j) r = multDistributesOverPlusRightPosPosZ k j r
335+multDistributesOverPlusRightPosZ k (NegS j) (Pos i) = rewrite plusCommutativeZ ((Pos k) * (NegS j)) ((Pos k) * (Pos i)) in
336+ rewrite multDistributesOverPlusRightPosPosZ k i (NegS j) in Refl
337+multDistributesOverPlusRightPosZ k (NegS j) (NegS i) = rewrite negNatDistributesPlus (mult k (S j)) (mult k (S i)) in
338+ rewrite sym $ multDistributesOverPlusRight k (S j) (S i) in
339+ rewrite plusSuccRightSucc j i in Refl
340+
341+multDistributesOverPlusRightZ : (l, c, r : ZZ) -> l * (c + r) = (l * c) + (l * r)
342+multDistributesOverPlusRightZ (Pos k) c r = multDistributesOverPlusRightPosZ k c r
343+multDistributesOverPlusRightZ (NegS k) c r = rewrite multNegLeftZ k (plusZ c r) in
344+ rewrite multNegLeftZ k c in
345+ rewrite multNegLeftZ k r in
346+ rewrite sym $ negateDistributesPlus (multZ (Pos (S k)) c) (multZ (Pos (S k)) r) in
347+ rewrite multDistributesOverPlusRightPosZ (S k) c r in Refl
348+
349+multDistributesOverPlusLeftZ : (l, c, r : ZZ) -> (l + c) * r = (l * r) + (c * r)
350+multDistributesOverPlusLeftZ l c r = rewrite multCommutativeZ (l + c) r in
351+ rewrite multDistributesOverPlusRightZ r l c in
352+ rewrite multCommutativeZ r l in
353+ rewrite multCommutativeZ r c in Refl