91c9a50 · Idris-dev · git.iko.soy

6%default total

7%access public export

8

9−

10||| An integer is either a positive `Nat` or the negated successor of a `Nat`.

9||| An integer is either a positive `Nat` or the negated successor of a `Nat`.

11|||

10|||

12||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen

11||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen

51 (NegS n) == (NegS m) = n == m

50 (NegS n) == (NegS m) = n == m

52 _ == _ = False

51 _ == _ = False

53

52

54−

55implementation Ord ZZ where

53implementation Ord ZZ where

56 compare (Pos n) (Pos m) = compare n m

54 compare (Pos n) (Pos m) = compare n m

57 compare (NegS n) (NegS m) = compare m n

55 compare (NegS n) (NegS m) = compare m n

92 subZ : ZZ -> ZZ -> ZZ

90 subZ : ZZ -> ZZ -> ZZ

93 subZ n m = plusZ n (negate m)

91 subZ n m = plusZ n (negate m)

94

92

95−

96implementation Cast ZZ Integer where

93implementation Cast ZZ Integer where

97 cast (Pos n) = cast n

94 cast (Pos n) = cast n

98 cast (NegS n) = (-1) * (cast n + 1)

95 cast (NegS n) = (-1) * (cast n + 1)

100implementation Cast Integer ZZ where

97implementation Cast Integer ZZ where

101 cast = fromInteger

98 cast = fromInteger

102

99

103−

104--------------------------------------------------------------------------------

100--------------------------------------------------------------------------------

105-- Properties

101-- Properties

106--------------------------------------------------------------------------------

102--------------------------------------------------------------------------------

141 | No p = No $ \h => p $ negSInjective h

137 | No p = No $ \h => p $ negSInjective h

142

138

143-- Plus

139-- Plus

140+

144plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right

141plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right

145plusZeroLeftNeutralZ (Pos n) = Refl

142plusZeroLeftNeutralZ (Pos n) = Refl

146plusZeroLeftNeutralZ (NegS n) = Refl

143plusZeroLeftNeutralZ (NegS n) = Refl

213plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in

210plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in

214 rewrite sym $ doubleNegElim r in

211 rewrite sym $ doubleNegElim r in

215 lemmaAssocNegation k (negate c) (negate r) (lemmaAssocPos (S k) (negate c) (negate r))

212 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