Grace/Cumulus/Int/Parity.g17
Open in Workbench Download source
Imports
OrderMul
Declarations
Source
1234567module Grace.Cumulus.Int.Parity8import OrderMul910predicate IntegerEven (z : Set) := ∃ k ∈ ℤ, z = k + k11predicate IntegerOdd (z : Set) := ∃ k ∈ ℤ, z = k + k + 11213theorem IntegerEven.double (k : Integer)14 shows IntegerEven(k + k)15proof16 have member : k ∈ ℤ by settle with Integer17 exact ⟨k, member, rfl⟩1819theorem IntegerOdd.double_add_one (k : Integer)20 shows IntegerOdd(k + k + 1)21proof22 have member : k ∈ ℤ by settle with Integer23 exact ⟨k, member, rfl⟩2425theorem IntegerEven.integer (z : Set)26 requires even : IntegerEven(z)27 shows Integer(z)28proof29 obtain ⟨k, kMember, shape⟩ := even30 have kInteger : Integer(k) by typecheck31 rw shape32 exact integerAddValue.integer with *3334theorem IntegerOdd.integer (z : Set)35 requires odd : IntegerOdd(z)36 shows Integer(z)37proof38 obtain ⟨k, kMember, shape⟩ := odd39 have kInteger : Integer(k) by typecheck40 have sum := integerAddValue.integer at k, k with *41 rw shape42 exact integerAddValue.integer at k + k, integerOne with *4344theorem IntegerEven.zero45 shows IntegerEven(integerZero)46proof47 have doubled := IntegerEven.double at integerZero48 have shape : integerZero + integerZero = integerZero by ring49 rw shape at doubled50 exact doubled5152theorem IntegerOdd.one53 shows IntegerOdd(integerOne)54proof55 have shaped := IntegerOdd.double_add_one at integerZero56 have shape : integerZero + integerZero + 1 = integerOne by ring57 rw shape at shaped58 exact shaped5960theorem IntegerEven.neg (z : Integer)61 requires even : IntegerEven(z)62 shows IntegerEven(-z)63proof64 obtain ⟨k, kMember, shape⟩ := even65 have kInteger : Integer(k) by typecheck66 have negated : -z = (-k) + (-k)67 rw shape68 ring69 rw negated70 exact IntegerEven.double with *7172theorem IntegerOdd.neg (z : Integer)73 requires odd : IntegerOdd(z)74 shows IntegerOdd(-z)75proof76 obtain ⟨k, kMember, shape⟩ := odd77 have kInteger : Integer(k) by typecheck78 have negated : -z = (-k - 1) + (-k - 1) + 179 rw shape80 ring81 rw negated82 exact IntegerOdd.double_add_one with *8384theorem IntegerEven.add (x y : Integer)85 requires first : IntegerEven(x)86 requires second : IntegerEven(y)87 shows IntegerEven(x + y)88proof89 obtain ⟨k, kMember, xShape⟩ := first90 obtain ⟨m, mMember, yShape⟩ := second91 have kInteger : Integer(k) by typecheck92 have mInteger : Integer(m) by typecheck93 have sum : x + y = (k + m) + (k + m)94 rw [xShape, yShape]95 ring96 rw sum97 exact IntegerEven.double with *9899theorem IntegerOdd.add_even (x y : Integer)100 requires first : IntegerOdd(x)101 requires second : IntegerEven(y)102 shows IntegerOdd(x + y)103proof104 obtain ⟨k, kMember, xShape⟩ := first105 obtain ⟨m, mMember, yShape⟩ := second106 have kInteger : Integer(k) by typecheck107 have mInteger : Integer(m) by typecheck108 have sum : x + y = (k + m) + (k + m) + 1109 rw [xShape, yShape]110 ring111 rw sum112 exact IntegerOdd.double_add_one with *113114theorem IntegerOdd.even_add (x y : Integer)115 requires first : IntegerEven(x)116 requires second : IntegerOdd(y)117 shows IntegerOdd(x + y)118proof119 have swapped := IntegerOdd.add_even with second, first120 have shape : y + x = x + y by ring121 rw shape at swapped122 exact swapped123124theorem IntegerEven.add_odd_odd (x y : Integer)125 requires first : IntegerOdd(x)126 requires second : IntegerOdd(y)127 shows IntegerEven(x + y)128proof129 obtain ⟨k, kMember, xShape⟩ := first130 obtain ⟨m, mMember, yShape⟩ := second131 have kInteger : Integer(k) by typecheck132 have mInteger : Integer(m) by typecheck133 have sum : x + y = (k + m + 1) + (k + m + 1)134 rw [xShape, yShape]135 ring136 rw sum137 exact IntegerEven.double with *138139theorem IntegerEven.sub (x y : Integer)140 requires first : IntegerEven(x)141 requires second : IntegerEven(y)142 shows IntegerEven(x - y)143proof144 have negated := IntegerEven.neg with second145 have sum := IntegerEven.add with first, negated146 have shape : x + (-y) = x - y by ring147 rw shape at sum148 exact sum149150theorem IntegerEven.sub_odd_odd (x y : Integer)151 requires first : IntegerOdd(x)152 requires second : IntegerOdd(y)153 shows IntegerEven(x - y)154proof155 have negated := IntegerOdd.neg with second156 have sum := IntegerEven.add_odd_odd with first, negated157 have shape : x + (-y) = x - y by ring158 rw shape at sum159 exact sum160161theorem IntegerEven.mul_left (x y : Integer)162 requires even : IntegerEven(x)163 shows IntegerEven(x * y)164proof165 obtain ⟨k, kMember, xShape⟩ := even166 have kInteger : Integer(k) by typecheck167 have product : x * y = (k * y) + (k * y)168 rw xShape169 ring170 rw product171 exact IntegerEven.double with *172173theorem IntegerEven.mul_right (x y : Integer)174 requires even : IntegerEven(y)175 shows IntegerEven(x * y)176proof177 have swapped := IntegerEven.mul_left at y, x with even178 have shape : y * x = x * y by ring179 rw shape at swapped180 exact swapped181182theorem IntegerOdd.mul (x y : Integer)183 requires first : IntegerOdd(x)184 requires second : IntegerOdd(y)185 shows IntegerOdd(x * y)186proof187 obtain ⟨k, kMember, xShape⟩ := first188 obtain ⟨m, mMember, yShape⟩ := second189 have kInteger : Integer(k) by typecheck190 have mInteger : Integer(m) by typecheck191 have product : x * y = (k * m + k * m + k + m) + (k * m + k * m + k + m) + 1192 rw [xShape, yShape]193 ring194 rw product195 exact IntegerOdd.double_add_one with *196197theorem integerAddValue.double_ne_one (j : Integer)198 shows j + j ≠ 1199proof200 intro same201 have split := integerLe.cases_sign at j202 cases split with nonnegative | nonpositive203 . have cases := integerLe.cases with nonnegative204 cases cases with positive | zero205 . have one := integerLess.one_le_of_positive with positive206 have doubled := integerLe.add with one, one207 rw same at doubled208 have strict := integerLess.add_one at integerOne209 exact integerLe.not_less with doubled, strict210 . rw ← zero at same211 have shape : integerZero + integerZero = integerZero by ring212 rw shape at same213 have strict := integerLess.zero_one214 rw same at strict215 exact integerLess.irreflexive with strict216 . have doubled := integerLe.add with nonpositive, nonpositive217 rw same at doubled218 have shape : integerZero + integerZero = integerZero by ring219 rw shape at doubled220 have strict := integerLess.zero_one221 exact integerLe.not_less with doubled, strict222223theorem IntegerOdd.not_even (z : Integer)224 requires odd : IntegerOdd(z)225 shows ¬IntegerEven(z)226proof227 intro even228 obtain ⟨k, kMember, oddShape⟩ := odd229 obtain ⟨m, mMember, evenShape⟩ := even230 have kInteger : Integer(k) by typecheck231 have mInteger : Integer(m) by typecheck232 have difference : (m - k) + (m - k) = 1233 linear_combination oddShape - evenShape234 have excluded := integerAddValue.double_ne_one at m - k235 exact excluded with difference236237theorem IntegerEven.not_odd (z : Integer)238 requires even : IntegerEven(z)239 shows ¬IntegerOdd(z)240proof241 intro odd242 exact IntegerOdd.not_even with odd, even243244theorem IntegerEven.ofNat (n : Nat)245 requires even : Even(n)246 shows IntegerEven(integerOfNat(n))247proof248 obtain ⟨k, kMember, shape⟩ := even249 have kNat := nat.omega.backward with kMember250 have sum := integerOfNat.add at k, k251 rw [shape, sum]252 exact IntegerEven.double with *253254theorem IntegerOdd.ofNat (n : Nat)255 requires odd : Odd(n)256 shows IntegerOdd(integerOfNat(n))257proof258 obtain ⟨k, kMember, shape⟩ := odd259 have kNat := nat.omega.backward with kMember260 have step : succ(k + k) = (k + k) + 1 by ring261 have inner := integerOfNat.add at k, k262 have outer := integerOfNat.add at k + k, 1263 have one : integerOfNat(1) = 1264 unfold integerOne265 rfl266 rw [shape, step, outer, inner, one]267 exact IntegerOdd.double_add_one with *268269theorem IntegerEven.negative_ofNat (n : Nat)270 requires even : Even(n)271 shows IntegerEven(integerNegativeOfNat(n))272proof273 have lifted := IntegerEven.ofNat with even274 have negated := IntegerEven.neg with lifted275 rw integerOfNat.neg at negated276 exact negated277278theorem IntegerOdd.negative_ofNat (n : Nat)279 requires odd : Odd(n)280 shows IntegerOdd(integerNegativeOfNat(n))281proof282 have lifted := IntegerOdd.ofNat with odd283 have negated := IntegerOdd.neg with lifted284 rw integerOfNat.neg at negated285 exact negated286287theorem IntegerParity.exhaustive (z : Integer)288 shows IntegerEven(z) ∨ IntegerOdd(z)289proof290 obtain ⟨n, nNat, sign⟩ := Integer.signed_natural at z with *291 have split := parity.exhaustive at n292 cases sign with positive | negative293 . rw positive294 cases split with even | odd295 . left296 exact IntegerEven.ofNat with even297 . right298 exact IntegerOdd.ofNat with odd299 . rw negative300 cases split with even | odd301 . left302 exact IntegerEven.negative_ofNat with even303 . right304 exact IntegerOdd.negative_ofNat with odd305306theorem IntegerEven.iff_not_odd (z : Integer)307 shows IntegerEven(z) ↔ ¬IntegerOdd(z)308proof309 constructor310 . intro even311 exact IntegerEven.not_odd with even312 . intro notOdd313 have split := IntegerParity.exhaustive at z314 cases split with even | odd315 . exact even316 . exfalso317 exact notOdd with odd318319theorem IntegerOdd.iff_not_even (z : Integer)320 shows IntegerOdd(z) ↔ ¬IntegerEven(z)321proof322 constructor323 . intro odd324 exact IntegerOdd.not_even with odd325 . intro notEven326 have split := IntegerParity.exhaustive at z327 cases split with even | odd328 . exfalso329 exact notEven with even330 . exact odd331332theorem IntegerEven.ofNat_iff (n : Nat)333 shows IntegerEven(integerOfNat(n)) ↔ Even(n)334proof335 constructor336 . intro even337 have split := parity.exhaustive at n338 cases split with natEven | natOdd339 . exact natEven340 . have odd := IntegerOdd.ofNat with natOdd341 exfalso342 exact IntegerOdd.not_even with odd, even343 . intro even344 exact IntegerEven.ofNat with even345346theorem IntegerOdd.ofNat_iff (n : Nat)347 shows IntegerOdd(integerOfNat(n)) ↔ Odd(n)348proof349 constructor350 . intro odd351 have split := parity.exhaustive at n352 cases split with natEven | natOdd353 . have even := IntegerEven.ofNat with natEven354 exfalso355 exact IntegerEven.not_odd with even, odd356 . exact natOdd357 . intro odd358 exact IntegerOdd.ofNat with odd359360theorem IntegerEven.add_one_iff (z : Integer)361 shows IntegerEven(z + 1) ↔ IntegerOdd(z)362proof363 constructor364 . intro even365 have split := IntegerParity.exhaustive at z366 cases split with zEven | zOdd367 . have one := IntegerOdd.one368 have odd := IntegerOdd.even_add with zEven, one369 exfalso370 exact IntegerOdd.not_even with odd, even371 . exact zOdd372 . intro odd373 have one := IntegerOdd.one374 exact IntegerEven.add_odd_odd with odd, one375376theorem IntegerOdd.add_one_iff (z : Integer)377 shows IntegerOdd(z + 1) ↔ IntegerEven(z)378proof379 constructor380 . intro odd381 have split := IntegerParity.exhaustive at z382 cases split with zEven | zOdd383 . exact zEven384 . have one := IntegerOdd.one385 have even := IntegerEven.add_odd_odd with zOdd, one386 exfalso387 exact IntegerEven.not_odd with even, odd388 . intro even389 have one := IntegerOdd.one390 exact IntegerOdd.even_add with even, one391392theorem IntegerEven.mul_self_iff (z : Integer)393 shows IntegerEven(z * z) ↔ IntegerEven(z)394proof395 constructor396 . intro even397 have split := IntegerParity.exhaustive at z398 cases split with zEven | zOdd399 . exact zEven400 . have odd := IntegerOdd.mul with zOdd, zOdd401 exfalso402 exact IntegerOdd.not_even with odd, even403 . intro even404 exact IntegerEven.mul_left with even405406theorem IntegerEven.neg_iff (z : Integer)407 shows IntegerEven(-z) ↔ IntegerEven(z)408proof409 constructor410 . intro even411 have negated := IntegerEven.neg with even412 have restore : -(-z) = z by ring413 rw restore at negated414 exact negated415 . intro even416 exact IntegerEven.neg with even417