Grace/Cumulus/Nat/ParityLemmas.g17

Open in Workbench Download source

Imports

Parity · PowLemmas · Division

Declarations

Source

1-- Parity of products, powers, and remainders modulo two2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Nat.ParityLemmas8import Parity9import PowLemmas10import Division1112theorem Even.two_mul (k : Nat)13  shows Even(2 * k)14proof15  have doubled := mul.two_left at k16  rw doubled17  exact Even.double with *1819theorem Even.mul_two (k : Nat)20  shows Even(k * 2)21proof22  have swap := mul.commutative at 2, k with *23  rw swap24  exact Even.two_mul with *2526theorem Even.iff_two_mul (n : Nat)27  shows Even(n) ↔ ∃ k, Nat(k) ∧ n = 2 * k28proof29  constructor30  . intro even31    obtain ⟨k, kMember, equation⟩ := even32    have kNat := nat.omega.backward with kMember33    witness k34    rw equation35    ring36  . intro shape37    obtain ⟨k, kNat, equation⟩ := shape38    rw equation39    exact Even.two_mul with *4041theorem Odd.iff_two_mul_add_one (n : Nat)42  shows Odd(n) ↔ ∃ k, Nat(k) ∧ n = 2 * k + 143proof44  constructor45  . intro odd46    obtain ⟨k, kMember, equation⟩ := odd47    have kNat := nat.omega.backward with kMember48    witness k49    rw equation50    ring51  . intro shape52    obtain ⟨k, kNat, equation⟩ := shape53    have doubled := mul.two_left at k54    have step : 2 * k + 1 = succ(k + k) by ring55    rw [equation, step]56    exact Odd.double_successor with *5758theorem Odd.one59  shows Odd(1)60proof61  have doubled := Odd.double_successor at 062  simpa [add] using doubled6364theorem Even.not_one65  shows ¬Even(1)66proof67  have one := Odd.one68  exact Odd.not_even with one6970theorem Odd.add_one_iff (n : Nat)71  shows Odd(n + 1) ↔ Even(n)72proof73  have shape := add.right_one at n74  rw shape75  exact Odd.succ_iff with *7677theorem Odd.positive (n : Nat)78  requires odd : Odd(n)79  shows 0 < n80proof81  obtain ⟨k, kMember, equation⟩ := odd82  have kNat := nat.omega.backward with kMember83  rw equation84  have step : succ(k + k) = k + k + 1 by ring85  rw step86  linarith8788theorem Even.mul_left (a b : Nat)89  requires even : Even(a)90  shows Even(a * b)91proof92  obtain ⟨k, kNat, equation⟩ := Even.iff_two_mul.forward with even93  apply Even.iff_two_mul.backward94  witness k * b95  rw equation96  ring9798theorem Even.mul_right (a b : Nat)99  requires even : Even(b)100  shows Even(a * b)101proof102  have swap := mul.commutative at b, a with *103  rw swap104  exact Even.mul_left with even105106theorem Odd.mul (a b : Nat)107  requires first : Odd(a)108  requires second : Odd(b)109  shows Odd(a * b)110proof111  obtain ⟨k, kNat, aShape⟩ := Odd.iff_two_mul_add_one.forward with first112  obtain ⟨m, mNat, bShape⟩ := Odd.iff_two_mul_add_one.forward with second113  apply Odd.iff_two_mul_add_one.backward114  witness 2 * k * m + k + m115  rw [aShape, bShape]116  ring117118theorem Even.of_mul (a b : Nat)119  requires even : Even(a * b)120  shows Even(a) ∨ Even(b)121proof122  have aSplit := parity.exhaustive at a123  cases aSplit with aEven | aOdd124  . left125    exact aEven126  . have bSplit := parity.exhaustive at b127    cases bSplit with bEven | bOdd128    . right129      exact bEven130    . have odd := Odd.mul with aOdd, bOdd131      exfalso132      exact Odd.not_even with odd, even133134theorem Odd.of_mul (a b : Nat)135  requires odd : Odd(a * b)136  shows Odd(a) ∧ Odd(b)137proof138  have aSplit := parity.exhaustive at a139  have bSplit := parity.exhaustive at b140  constructor141  . cases aSplit with aEven | aOdd142    . have even := Even.mul_left at a, b with aEven143      exfalso144      exact Even.not_odd with even, odd145    . exact aOdd146  . cases bSplit with bEven | bOdd147    . have even := Even.mul_right at a, b with bEven148      exfalso149      exact Even.not_odd with even, odd150    . exact bOdd151152theorem Even.mul_self_iff (n : Nat)153  shows Even(n * n) ↔ Even(n)154proof155  constructor156  . intro even157    have split := Even.of_mul with even158    cases split with first | second159    . exact first160    . exact second161  . intro even162    exact Even.mul_left with even163164theorem Odd.mul_self_iff (n : Nat)165  shows Odd(n * n) ↔ Odd(n)166proof167  constructor168  . intro odd169    have both := Odd.of_mul with odd170    exact both.left171  . intro odd172    exact Odd.mul with odd, odd173174theorem Even.pow (a n : Nat)175  requires even : Even(a)176  shows Even(a ^ (n + 1))177proof178  have powNat := pow.closed at a, n179  rw pow.add_one180  exact Even.mul_left with even181182theorem Odd.pow (a n : Nat)183  requires odd : Odd(a)184  shows Odd(a ^ n)185proof186  induction n187  | zero =>188    rw pow.zero189    exact Odd.one190  | succ(k) using ih =>191    have powNat := pow.closed at a, k192    rw pow.succ193    exact Odd.mul with odd, ih194195theorem Even.of_pow (a n : Nat)196  requires even : Even(a ^ n)197  shows Even(a)198proof199  have split := parity.exhaustive at a200  cases split with aEven | aOdd201  . exact aEven202  . have odd := Odd.pow at a, n with aOdd203    exfalso204    exact Odd.not_even with odd, even205206theorem Even.of_add_even (a b : Nat)207  requires sum : Even(a + b)208  requires even : Even(a)209  shows Even(b)210proof211  have split := parity.exhaustive at b212  cases split with bEven | bOdd213  . exact bEven214  . have odd := Odd.even_add at a, b with even, bOdd215    exfalso216    exact Odd.not_even with odd, sum217218theorem Odd.of_add_even_odd (a b : Nat)219  requires sum : Even(a + b)220  requires odd : Odd(a)221  shows Odd(b)222proof223  have split := parity.exhaustive at b224  cases split with bEven | bOdd225  . have sumOdd := Odd.add_even at a, b with odd, bEven226    exfalso227    exact Odd.not_even with sumOdd, sum228  . exact bOdd229230theorem Odd.of_add_odd_even (a b : Nat)231  requires sum : Odd(a + b)232  requires even : Even(a)233  shows Odd(b)234proof235  have split := parity.exhaustive at b236  cases split with bEven | bOdd237  . have sumEven := Even.add at a, b with even, bEven238    exfalso239    exact Even.not_odd with sumEven, sum240  . exact bOdd241242theorem Even.of_add_odd_odd (a b : Nat)243  requires sum : Odd(a + b)244  requires odd : Odd(a)245  shows Even(b)246proof247  have split := parity.exhaustive at b248  cases split with bEven | bOdd249  . exact bEven250  . have sumEven := Odd.add_odd at a, b with odd, bOdd251    exfalso252    exact Even.not_odd with sumEven, sum253254theorem Even.add_iff (a b : Nat)255  shows Even(a + b) ↔ (Even(a) ↔ Even(b))256proof257  have aSplit := parity.exhaustive at a258  constructor259  . intro sum260    constructor261    . intro aEven262      exact Even.of_add_even with sum, aEven263    . intro bEven264      have swap := add.commutative at b, a with *265      rw swap at sum266      exact Even.of_add_even at b, a with sum, bEven267  . intro same268    cases aSplit with aEven | aOdd269    . have bEven := same.forward with aEven270      exact Even.add with aEven, bEven271    . have bOdd : Odd(b)272        have split := parity.exhaustive at b273        cases split with bEven | odd274        . have aEven := same.backward with bEven275          exfalso276          exact Odd.not_even with aOdd, aEven277        . exact odd278      exact Odd.add_odd with aOdd, bOdd279280theorem Even.mod_two (n : Nat)281  shows Even(n) ↔ n % 2 = 0282proof283  have two : 2 ≠ 0284    intro zero285    have impossible : 0 < 2 by linarith286    rw zero at impossible287    exact Less.irreflexive with impossible288  have division := mod.division at 2, n with two289  rcases division with ⟨equation, bound⟩290  obtain ⟨q, qNat, shape⟩ := equation291  have modNat := mod.natural at 2, n292  have remainder : n % 2 = 0 ∨ n % 2 = 1293    have small : n % 2 ≤ 1 by linarith294    have split := LessEqual.cases with small295    cases split with strict | one296    . left297      have zero : n % 2 ≤ 0 by linarith298      exact LessEqual.eq_zero with zero299    . right300      exact one301  constructor302  . intro even303    cases remainder with zero | one304    . exact zero305    . rw one at shape306      have odd : Odd(n)307        apply Odd.iff_two_mul_add_one.backward308        witness q309        exact shape310      exfalso311      exact Odd.not_even with odd, even312  . intro zero313    rw zero at shape314    apply Even.iff_two_mul.backward315    witness q316    have unit := add.right_unit at 2 * q317    rw unit at shape318    exact shape319320theorem Odd.mod_two (n : Nat)321  shows Odd(n) ↔ n % 2 = 1322proof323  have two : 2 ≠ 0324    intro zero325    have impossible : 0 < 2 by linarith326    rw zero at impossible327    exact Less.irreflexive with impossible328  have modNat := mod.natural at 2, n329  have bound := mod.less at n, 2 with two330  constructor331  . intro odd332    have notEven := Odd.not_even with odd333    have nonzero : n % 2 ≠ 0334      intro zero335      have even := Even.mod_two.backward with zero336      exact notEven with even337    have positive := Less.positive_of_ne_zero with nonzero338    have upper : n % 2 ≤ 1 by linarith339    have lower : 1 ≤ n % 2 by linarith340    exact LessEqual.antisymmetric with upper, lower341  . intro one342    have split := parity.exhaustive at n343    cases split with even | odd344    . have zero := Even.mod_two.forward with even345      rw zero at one346      have impossible : 0 < 1 by linarith347      rw ← one at impossible348      exfalso349      exact Less.irreflexive with impossible350    . exact odd351