Grace/Cumulus/NumberTheory/ResidueLists.g17

Open in Workbench Download source

Imports

ModularInverse

Declarations

Source

1-- The residues coprime to n as a list, Euler's totient as its length, the2-- list scaled by a coprime factor, and what scaling does to products and to3-- multiplicities: it permutes the units4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.ResidueLists10import ModularInverse1112-- Prepend x exactly when the test holds.13def consIf (test : Bool, x : Nat, xs : List(ℕ)) → List(ℕ)14  | Bool.false, x, xs => xs15  | Bool.true, x, xs => x :: xs1617theorem consIf.false (x : Nat) (xs : List(ℕ))18  shows consIf(Bool.false, x, xs) = xs19proof20  simp [consIf]2122theorem consIf.true (x : Nat) (xs : List(ℕ))23  shows consIf(Bool.true, x, xs) = x :: xs24proof25  simp [consIf]2627-- The residues below m that are coprime to n.28def unitsBelow (n m : Nat) → List(ℕ)29  | n, zero => []30  | n, succ(m) => consIf(equalNat(gcd(m, n), 1), m, unitsBelow(n, m))31  descends m3233theorem unitsBelow.zero (n : Nat)34  shows unitsBelow(n, 0) = []35proof36  simp [unitsBelow]3738theorem unitsBelow.succ_unit (n m : Nat)39  requires coprime : gcd(m, n) = 140  shows unitsBelow(n, succ(m)) = m :: unitsBelow(n, m)41proof42  simp [unitsBelow, coprime, equalNat.reflexive, consIf]4344theorem unitsBelow.succ_other (n m : Nat)45  requires notCoprime : gcd(m, n) ≠ 146  shows unitsBelow(n, succ(m)) = unitsBelow(n, m)47proof48  have test := equalNat.false_iff.backward with notCoprime49  simp [unitsBelow, test, consIf]5051theorem unitsBelow.list (n m : Nat)52  shows List(ℕ, unitsBelow(n, m))53proof54  induction m55  | zero =>56    rw unitsBelow.zero57    typecheck58  | succ(j) using ih =>59    have alternatives : gcd(j, n) = 1 ∨ gcd(j, n) ≠ 1 by tauto60    cases alternatives with coprime | notCoprime61    . have step := unitsBelow.succ_unit at n, j with coprime62      rw step63      typecheck64    . have step := unitsBelow.succ_other at n, j with notCoprime65      rw step66      exact ih6768-- A residue that is not below m, or not coprime to n, does not occur.69theorem unitsBelow.multiplicity_other (n m : Nat)70  shows ∀ k, Nat(k) → ¬(k < m ∧ gcd(k, n) = 1) → multiplicity(k, unitsBelow(n, m)) = 071proof72  induction m73  | zero =>74    intros k kNat notBoth75    rw unitsBelow.zero76    exact multiplicity.nil at k77  | succ(j) using ih =>78    intros k kNat notBoth79    have restList := unitsBelow.list at n, j80    have smaller : ¬(k < j ∧ gcd(k, n) = 1)81      intro both82      obtain ⟨kBelow, kCoprime⟩ := both83      apply notBoth84      constructor85      . have below : k < succ(j) by arith86        exact below87      . exact kCoprime88    have previous := ih with k, kNat, smaller89    have alternatives : gcd(j, n) = 1 ∨ gcd(j, n) ≠ 1 by tauto90    cases alternatives with coprime | notCoprime91    . have step := unitsBelow.succ_unit at n, j with coprime92      rw step93      have different : k ≠ j94        intro same95        apply notBoth96        rw same97        constructor98        . arith99        . exact coprime100      have other := multiplicity.cons_other at k, j, unitsBelow(n, j) with different101      rw other102      exact previous103    . have step := unitsBelow.succ_other at n, j with notCoprime104      rw step105      exact previous106107-- A coprime residue below m occurs exactly once.108theorem unitsBelow.multiplicity_unit (n m : Nat)109  shows ∀ k, Nat(k) → k < m → gcd(k, n) = 1 → multiplicity(k, unitsBelow(n, m)) = 1110proof111  induction m112  | zero =>113    intros k kNat below coprime114    exfalso115    have impossible : ¬k < 0 by arith116    exact impossible with below117  | succ(j) using ih =>118    intros k kNat below coprime119    have restList := unitsBelow.list at n, j120    have trichotomy := Less.trichotomy at k, j121    rcases trichotomy with smaller | same | larger122    . have previous := ih with k, kNat, smaller, coprime123      have alternatives : gcd(j, n) = 1 ∨ gcd(j, n) ≠ 1 by tauto124      cases alternatives with coprimeJ | notCoprimeJ125      . have step := unitsBelow.succ_unit at n, j with coprimeJ126        rw step127        have different : k ≠ j128          intro equal129          rw equal at smaller130          exact Less.irreflexive at j with *, smaller131        have other := multiplicity.cons_other at k, j, unitsBelow(n, j) with different132        rw other133        exact previous134      . have step := unitsBelow.succ_other at n, j with notCoprimeJ135        rw step136        exact previous137    . rw same at coprime138      have step := unitsBelow.succ_unit at n, j with coprime139      rw [same, step]140      have self := multiplicity.cons_self at j, unitsBelow(n, j) with *141      rw self142      have notBoth : ¬(j < j ∧ gcd(j, n) = 1)143        intro both144        exact Less.irreflexive at j with *, both.left145      have others := unitsBelow.multiplicity_other at n, j146      have jNat : Nat(j) by typecheck147      have zero := others with j, jNat, notBoth148      rw zero149      ring150    . exfalso151      have impossible : ¬j < k by arith152      exact impossible with larger153154theorem unitsBelow.member (n m k : Nat)155  requires positive : 0 < multiplicity(k, unitsBelow(n, m))156  shows k < m ∧ gcd(k, n) = 1157proof158  by_contra none159  have others := unitsBelow.multiplicity_other at n, m160  have kNat : Nat(k) by typecheck161  have zero := others with k, none162  rw zero at positive163  exact Less.irreflexive with *, positive164165-- The units mod n and Euler's totient.166def units (n : Nat) : Set := unitsBelow(n, n)167168def totient (n : Nat) : Nat := length{ℕ}(unitsBelow(n, n))169170theorem units.definition (n : Nat)171  shows units(n) = unitsBelow(n, n)172proof173  unfold units174  rfl175176theorem totient.definition (n : Nat)177  shows totient(n) = length{ℕ}(units(n))178proof179  unfold totient180  rw units.definition181  rfl182183theorem units.list (n : Nat)184  shows List(ℕ, units(n))185proof186  rw units.definition187  exact unitsBelow.list188189theorem units.multiplicity (n k : Nat)190  requires below : k < n191  requires coprime : gcd(k, n) = 1192  shows multiplicity(k, units(n)) = 1193proof194  rw units.definition195  have all := unitsBelow.multiplicity_unit at n, n196  have kNat : Nat(k) by typecheck197  exact all with k, below, coprime198199theorem units.multiplicity_other (n k : Nat)200  requires notBoth : ¬(k < n ∧ gcd(k, n) = 1)201  shows multiplicity(k, units(n)) = 0202proof203  rw units.definition204  have all := unitsBelow.multiplicity_other at n, n205  have kNat : Nat(k) by typecheck206  exact all with k, notBoth207208theorem units.member (n k : Nat)209  requires positive : 0 < multiplicity(k, units(n))210  shows k < n ∧ gcd(k, n) = 1211proof212  rw units.definition at positive213  exact unitsBelow.member with positive214215-- Scaling every entry by a and reducing mod n.216def scaledList (a n : Nat, xs : List(ℕ)) → List(ℕ)217  | a, n, [] => []218  | a, n, x :: rest => mul(a, x) % n :: scaledList(a, n, rest)219220theorem scaledList.nil (a n : Nat)221  shows scaledList(a, n, []) = []222proof223  simp [scaledList]224225theorem scaledList.cons (a n x : Nat) (rest : List(ℕ))226  shows scaledList(a, n, x :: rest) = ((a * x) % n) :: scaledList(a, n, rest)227proof228  simp [scaledList]229230theorem scaledList.list (a n : Nat) (xs : List(ℕ))231  shows List(ℕ, scaledList(a, n, xs))232proof233  induction xs234  | List.nil =>235    rw scaledList.nil236    typecheck237  | List.cons(x, rest) using ih =>238    rw scaledList.cons239    typecheck240241theorem scaledList.length (a n : Nat) (xs : List(ℕ))242  shows length{ℕ}(scaledList(a, n, xs)) = length{ℕ}(xs)243proof244  induction xs245  | List.nil =>246    rw scaledList.nil247    rfl248  | List.cons(x, rest) using ih =>249    have scaledRest := scaledList.list at a, n, rest250    have step := scaledList.cons at a, n, x, rest251    have left := length.cons at ℕ, (a * x) % n, scaledList(a, n, rest) with *252    have right := length.cons at ℕ, x, rest with *253    rw step254    rw left255    rw right256    rw ih257    rfl258259-- The product of the scaled list is a^length times the product, mod n.260theorem scaledList.product (a n : Nat) (xs : List(ℕ))261  requires nonzero : n ≠ 0262  shows (∏ scaledList(a, n, xs)) % n = (a ^ length{ℕ}(xs) * ∏ xs) % n263proof264  induction xs265  | List.nil =>266    have one : 1 * 1 = 1 by ring267    rw [scaledList.nil, listProduct.nil, length.nil, pow.zero, one]268    rfl269  | List.cons(x, rest) using ih =>270    have scaledRest := scaledList.list at a, n, rest271    have expandScaled := listProduct.cons at (a * x) % n, scaledList(a, n, rest) with *272    have expandRest := listProduct.cons at x, rest with *273    have lengthRest := length.cons with *274    have scaledProduct : Nat(∏ scaledList(a, n, rest)) by typecheck275    have restProduct : Nat(∏ rest) by typecheck276    have powerNat := pow.closed at a, length{ℕ}(rest)277    have first := mod.mul_left at n, a * x, ∏ scaledList(a, n, rest) with nonzero278    have second := mod.mul_right at n, a * x, ∏ scaledList(a, n, rest) with nonzero279    have third := mod.mul_right at n, a * x, a ^ length{ℕ}(rest) * ∏ rest with nonzero280    have rearrange : a * x * (a ^ length{ℕ}(rest) * ∏ rest) = a * a ^ length{ℕ}(rest) * (x * ∏ rest) by ring281    rw [scaledList.cons, expandScaled, expandRest, lengthRest, pow.succ, first, ← second, ih, third, rearrange]282    rfl283284-- Every entry of the scaled list is a residue below n.285theorem scaledList.member (a n : Nat) (xs : List(ℕ))286  requires nonzero : n ≠ 0287  shows ∀ v, Nat(v) → 0 < multiplicity(v, scaledList(a, n, xs)) → v < n288proof289  induction xs290  | List.nil =>291    intros v vNat positive292    rw [scaledList.nil, multiplicity.nil] at positive293    exfalso294    exact Less.irreflexive at 0 with *, positive295  | List.cons(x, rest) using ih =>296    intros v vNat positive297    have scaledRest := scaledList.list at a, n, rest298    rw scaledList.cons at positive299    have alternatives : v = (a * x) % n ∨ v ≠ (a * x) % n by tauto300    cases alternatives with same | different301    . rw same302      exact mod.less at a * x, n with nonzero303    . have other := multiplicity.cons_other at v, (a * x) % n, scaledList(a, n, rest) with different304      rw other at positive305      exact ih with v, vNat, positive306307-- With b inverse to a, the entry v of the scaled list is counted as many308-- times as b·v is counted in the original list of residues.309theorem scaledList.multiplicity (a b n v : Nat) (xs : List(ℕ))310  requires nonzero : n ≠ 0311  requires inverse : (a * b) % n = 1312  requires vBelow : v < n313  shows (∀ x, Nat(x) → 0 < multiplicity(x, xs) → x < n) → multiplicity(v, scaledList(a, n, xs)) = multiplicity((b * v) % n, xs)314proof315  induction xs316  | List.nil =>317    intro residues318    rw [scaledList.nil, multiplicity.nil, multiplicity.nil]319    rfl320  | List.cons(x, rest) using ih =>321    intro residues322    have scaledRest := scaledList.list at a, n, rest323    have xPositive : 0 < multiplicity(x, x :: rest)324      have self := multiplicity.cons_self at x, rest with *325      rw self326      arith327    have xNat : Nat(x) by typecheck328    have xBelow := residues with x, xNat, xPositive329    have restResidues : ∀ y, Nat(y) → 0 < multiplicity(y, rest) → y < n330      intros y yNat positive331      have lifted := multiplicity.positive_cons at y, x, rest with positive332      exact residues with y, yNat, lifted333    have previous := ih with restResidues334    have bvNat : Nat((b * v) % n) by typecheck335    have cancelLeft : (b * ((a * x) % n)) % n = x336      have step1 := mod.mul_right at n, b, a * x with nonzero337      have rearrange : b * (a * x) = (a * b) * x by ring338      have step2 := mod.mul_left at n, a * b, x with nonzero339      have one : 1 * x = x by ring340      have self := mod.of_less at n, x with xBelow341      rw [step1, rearrange, ← step2, inverse, one, self]342      rfl343    have cancelRight : (a * ((b * v) % n)) % n = v344      have step1 := mod.mul_right at n, a, b * v with nonzero345      have rearrange : a * (b * v) = (a * b) * v by ring346      have step2 := mod.mul_left at n, a * b, v with nonzero347      have one : 1 * v = v by ring348      have self := mod.of_less at n, v with vBelow349      rw [step1, rearrange, ← step2, inverse, one, self]350      rfl351    rw scaledList.cons352    have alternatives : x = (b * v) % n ∨ x ≠ (b * v) % n by tauto353    cases alternatives with same | different354    . have hit : (a * x) % n = v355        rw same356        exact cancelRight357      rw hit358      have leftSelf := multiplicity.cons_self at v, scaledList(a, n, rest) with *359      rw ← same360      have rightSelf := multiplicity.cons_self at x, rest with *361      rw [leftSelf, rightSelf]362      rw same363      rw previous364      rfl365    . have miss : v ≠ (a * x) % n366        intro equal367        apply different368        rw [← cancelLeft, ← equal]369        rfl370      have leftOther := multiplicity.cons_other at v, (a * x) % n, scaledList(a, n, rest) with miss371      have differentReversed : (b * v) % n ≠ x372        intro equal373        apply different374        rw equal375        rfl376      have rightOther := multiplicity.cons_other at (b * v) % n, x, rest with differentReversed377      rw [leftOther, rightOther]378      exact previous379380-- Lists with the same multiplicities have the same product.381theorem listProduct.of_multiplicities (xs : List(ℕ))382  shows ∀ ys, List(ℕ, ys) → (∀ q, Nat(q) → multiplicity(q, xs) = multiplicity(q, ys)) → ∏ xs = ∏ ys383proof384  induction xs385  | List.nil =>386    intros ys ysList same387    have shape := List.cases with ysList388    cases shape with nil | cons389    . rw nil390      rfl391    . exfalso392      obtain ⟨y, yIn, rest, restList, equal⟩ := cons393      have yNat : Nat(y) by typecheck394      have count := same with y395      have self := multiplicity.cons_self at y, rest with *396      rw [multiplicity.nil, equal, self] at count397      have impossible : ¬(0:N) = 1 + multiplicity(y, rest) by arith398      exact impossible with count399  | List.cons(x, rest) using ih =>400    intros ys ysList same401    have positive : 0 < multiplicity(x, ys)402      have count := same with x, *403      have self := multiplicity.cons_self at x, rest with *404      rw self at count405      rw ← count406      arith407    have remove := multiplicity.remove at x, ys with *408    obtain ⟨zs, zsList, product, counts⟩ := remove with positive409    have restCounts : ∀ q, Nat(q) → multiplicity(q, rest) = multiplicity(q, zs)410      intros q qNat411      have count := same with q, qNat412      have shifted := counts with q, qNat413      have left := multiplicity.cons at q, x, rest with *414      have right := multiplicity.cons at q, x, zs with *415      rw [left, shifted, right] at count416      have cancel := add.left_cancel at multiplicity(q, rest), multiplicity(q, zs), chooseNat(equalNat(q, x), 1, 0)417      exact cancel with count418    have previous := ih with zs, zsList, restCounts419    have expandRest := listProduct.cons at x, rest with *420    have expandZs := listProduct.cons at x, zs with *421    rw [expandRest, previous, ← expandZs, product]422    rfl423424-- A product of residues coprime to n is coprime to n.425theorem listProduct.coprime (n : Nat) (xs : List(ℕ))426  requires nonzero : n ≠ 0427  shows (∀ x, Nat(x) → 0 < multiplicity(x, xs) → gcd(x, n) = 1) → gcd(∏ xs, n) = 1428proof429  induction xs430  | List.nil =>431    intro coprime432    rw listProduct.nil433    have divides := gcd.divides_left at 1, n434    have natural := gcd.natural at 1, n435    exact divides.one_only at gcd(1, n) with natural, divides436  | List.cons(x, rest) using ih =>437    intro coprime438    have xPositive : 0 < multiplicity(x, x :: rest)439      have self := multiplicity.cons_self at x, rest with *440      rw self441      arith442    have xNat : Nat(x) by typecheck443    have xCoprime := coprime with x, xNat, xPositive444    have restCoprime : ∀ y, Nat(y) → 0 < multiplicity(y, rest) → gcd(y, n) = 1445      intros y yNat positive446      have lifted := multiplicity.positive_cons at y, x, rest with positive447      exact coprime with y, yNat, lifted448    have previous := ih with restCoprime449    rw listProduct.cons450    exact coprime.mul at x, ∏ rest, n with nonzero, xCoprime, previous451