Grace/Cumulus/NumberTheory/Factorization.g17

Open in Workbench Download source

Imports

Prime · Coprime · Core.List

Declarations

Source

1-- The fundamental theorem of arithmetic: prime factorizations exist and are unique2-- 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.NumberTheory.Factorization8import Prime9import Coprime10import Core.List1112-- A factorization is a list of natural numbers; its value is their product,13-- written ∏ xs.14def listProduct (xs : List(ℕ)) → Nat15  | [] => 116  | x :: rest => mul(x, listProduct(rest))1718notation prefix 80 "∏" => listProduct1920-- The number of times a natural number occurs in a list.  Two lists with the21-- same multiplicities are the same multiset.22def multiplicity (p : Nat, xs : List(ℕ)) → Nat23  | p, [] => 024  | p, x :: rest => add(chooseNat(equalNat(p, x), 1, 0), multiplicity(p, rest))2526theorem listProduct.nil27  shows ∏ [] = 128proof29  simp3031theorem listProduct.cons (x : Nat) (rest : List(ℕ))32  shows ∏ (x :: rest) = x * ∏ rest33proof34  unfold listProduct35  rfl3637theorem multiplicity.nil (p : Nat)38  shows multiplicity(p, []) = 039proof40  unfold multiplicity41  rfl4243theorem multiplicity.cons (p x : Nat) (rest : List(ℕ))44  shows multiplicity(p, x :: rest) = chooseNat(equalNat(p, x), 1, 0) + multiplicity(p, rest)45proof46  unfold multiplicity47  rfl4849theorem multiplicity.cons_self (p : Nat) (rest : List(ℕ))50  shows multiplicity(p, p :: rest) = 1 + multiplicity(p, rest)51proof52  have same := equalNat.reflexive with *53  unfold multiplicity54  simp [chooseNat]5556theorem multiplicity.cons_other (p x : Nat) (rest : List(ℕ))57  requires different : p ≠ x58  shows multiplicity(p, x :: rest) = multiplicity(p, rest)59proof60  have test := equalNat.false_iff.backward with *61  unfold multiplicity62  simp [chooseNat, add]6364theorem multiplicity.positive_cons (p x : Nat) (rest : List(ℕ))65  requires positive : 0 < multiplicity(p, rest)66  shows 0 < multiplicity(p, x :: rest)67proof68  have equation := multiplicity.cons at p, x, rest with *69  rw equation70  arith7172-- A list of primes.  Membership is positive multiplicity, so two lists of73-- primes with the same counts describe the same multiset of primes.74predicate PrimeList (xs : List(ℕ)) :=75  ∀ q, Nat(q) → 0 < multiplicity(q, xs) → Prime(q)7677theorem PrimeList.nil78  shows PrimeList([])79proof80  intros q qNat positive81  rw multiplicity.nil at positive82  exfalso83  exact Less.irreflexive at 0 with *, positive8485theorem PrimeList.cons (x : Nat) (rest : List(ℕ))86  requires prime : Prime(x)87  requires primes : PrimeList(rest)88  shows PrimeList(x :: rest)89proof90  intros q qNat positive91  have split : q = x ∨ ¬(q = x) by tauto92  cases split with equal | different93  . rw equal94    exact prime95  . have equation := multiplicity.cons_other with *96    rw equation at positive97    exact primes with q, qNat, positive9899theorem PrimeList.head (x : Nat) (rest : List(ℕ))100  requires primes : PrimeList(x :: rest)101  shows Prime(x)102proof103  have equation := multiplicity.cons_self with *104  have positive : 0 < multiplicity(x, x :: rest)105    rw equation106    arith107  exact primes with x, positive108109theorem PrimeList.tail (x : Nat) (rest : List(ℕ))110  requires primes : PrimeList(x :: rest)111  shows PrimeList(rest)112proof113  intros q qNat positive114  have lifted := multiplicity.positive_cons at q, x, rest with *115  exact primes with q, qNat, lifted116117theorem Prime.nonzero (p : Nat)118  requires prime : Prime(p)119  shows p ≠ 0120proof121  have above := Prime.greater_than_one with prime122  intro zero123  rw zero at above124  have bad : 0 < 0 by arith125  exact Less.irreflexive at 0 with *, bad126127theorem Prime.divides_prime (p q : Nat)128  requires primeP : Prime(p)129  requires primeQ : Prime(q)130  requires divides : p ∣ q131  shows p = q132proof133  have qNonzero := Prime.nonzero with primeQ134  have bound := divides.le with *135  have shape := Less.trichotomy at p, q with *136  rcases shape with less | equal | greater137  . exfalso138    have member := membership.of_Less with *, less139    have one := Prime.divisor with primeQ, member, divides140    have above := Prime.greater_than_one with primeP141    rw one at above142    exact Less.irreflexive with *, above143  . exact equal144  . exfalso145    have bad : p < p by arith146    exact Less.irreflexive with *, bad147148-- A prime not dividing a is coprime to it: its only divisors are 1 and itself.149theorem Prime.coprime_of_not_divides (p a : Nat)150  requires prime : Prime(p)151  requires notDivides : ¬(p ∣ a)152  shows IsGCD(p, a, 1)153proof154  have left := one.divides at p with *155  have right := one.divides at a with *156  have greatest : ∀ d, Nat(d) → d ∣ p → d ∣ a → d ∣ 1157    intros d dNat dividesP dividesA158    have pNonzero := Prime.nonzero with *159    have bound := divides.le at d, p with *160    have shape := Less.trichotomy at d, p with *161    rcases shape with less | equal | greater162    . have member := membership.of_Less with *, less163      have one := Prime.divisor with prime, dNat, member, dividesP164      rw one165      exact divides.reflexive with *166    . exfalso167      rw equal at dividesA168      exact notDivides with dividesA169    . exfalso170      have bad : p < p by arith171      exact Less.irreflexive with *, bad172  exact IsGCD.intro with *173174-- Euclid's lemma, through the integer Bézout identity.175theorem Prime.divides_mul (p a b : Nat)176  requires prime : Prime(p)177  requires divides : p ∣ a * b178  shows p ∣ a ∨ p ∣ b179proof180  have split : p ∣ a ∨ ¬(p ∣ a) by tauto181  cases split with left | notLeft182  . left183    exact left184  . right185    have certificate := Prime.coprime_of_not_divides with *186    have unit := gcd.unique with *187    have ofNat := integerGCD.ofNat at p, a with *188    have coprime : IntegerCoprime(integerOfNat(p), integerOfNat(a))189      unfold IntegerCoprime190      rwa ofNat191    have absolute := integerNatAbs.ofNat at a * b with *192    have magnitude : p ∣ integerNatAbs(integerOfNat(a * b)) by rwa absolute193    have lifted := IntegerDivides.natural_left.backward with *194    have product := integerOfNat.mul at a, b with *195    rw product at lifted196    have cancelled := IntegerCoprime.cancel with *197    have back := IntegerDivides.natural_left.forward at p, integerOfNat(b) with *198    have absoluteB := integerNatAbs.ofNat at b with *199    rwa absoluteB at back200201theorem Prime.divides_listProduct (p : Nat) (xs : List(ℕ))202  requires prime : Prime(p)203  shows p ∣ ∏ xs → ∃ q, Nat(q) ∧ 0 < multiplicity(q, xs) ∧ p ∣ q204proof205  induction xs206  | List.nil =>207    intro divides208    rw listProduct.nil at divides209    exfalso210    have one := divides.one_only with *211    have above := Prime.greater_than_one with prime212    rw one at above213    exact Less.irreflexive at 1 with *, above214  | List.cons(x, rest) using ih =>215    intro divides216    have xNat : Nat(x) by typecheck217    have equation := listProduct.cons at x, rest with *218    rw equation at divides219    have split := Prime.divides_mul with *220    cases split with head | tail221    . have count := multiplicity.cons_self at x, rest with *222      have positive : 0 < multiplicity(x, x :: rest)223        rw count224        arith225      refine ⟨x, xNat, positive, head⟩226    . obtain ⟨q, qNat, positive, dividesQ⟩ := ih with tail227      have lifted := multiplicity.positive_cons at q, x, rest with *228      refine ⟨q, qNat, lifted, dividesQ⟩229230-- Removing one occurrence of y from a list leaves a list with the same product231-- after multiplying by y, and the same counts after putting y back.232theorem multiplicity.remove (y : Nat) (ys : List(ℕ))233  shows 0 < multiplicity(y, ys) →234    ∃ zs, List(ℕ, zs) ∧ ∏ ys = ∏ (y :: zs) ∧235      (∀ q, Nat(q) → multiplicity(q, ys) = multiplicity(q, y :: zs))236proof237  induction ys238  | List.nil =>239    intro positive240    have empty := multiplicity.nil with *241    rw empty at positive242    exfalso243    exact Less.irreflexive at 0 with *, positive244  | List.cons(x, rest) using ih =>245    intro positive246    have split : y = x ∨ ¬(y = x) by tauto247    cases split with equal | different248    . refine ⟨rest, h_rest, _, _⟩249      . rw equal250        rfl251      . intros q qNat252        rw equal253        rfl254    . have restPositive : 0 < multiplicity(y, rest)255        have equation := multiplicity.cons_other with different256        rwa equation at positive257      obtain ⟨zs, zsList, product, counts⟩ := ih with restPositive258      have consList : List(ℕ, x :: zs) by typecheck259      refine ⟨x :: zs, consList, _, _⟩260      . have e1 := listProduct.cons at x, rest with *261        have e2 := listProduct.cons at y, zs with *262        have e3 := listProduct.cons at y, x :: zs with *263        have e4 := listProduct.cons at x, zs with *264        rw e2 at product265        rw [e1, e3, e4, product]266        ring267      . intros q qNat268        have c1 := multiplicity.cons at q, x, rest with *269        have c2 := multiplicity.cons at q, y, x :: zs with *270        have c3 := multiplicity.cons at q, x, zs with *271        have c4 := multiplicity.cons at q, y, zs with *272        have count := counts with q, qNat273        rw c4 at count274        rw [c1, c2, c3, count]275        ring276277-- A list of primes with product one is empty.278theorem listProduct.one (xs : List(ℕ))279  requires primes : PrimeList(xs)280  requires unit : ∏ xs = 1281  shows ∀ q, Nat(q) → multiplicity(q, xs) = 0282proof283  have shape := List.cases with *284  cases shape with nil | cons285  . intros q qNat286    rw nil287    exact multiplicity.nil with *288  . exfalso289    obtain ⟨x, xMember, rest, restList, equal⟩ := cons290    rw equal at unit291    rw equal at primes292    have equation := listProduct.cons at x, rest with *293    rw equation at unit294    have one := mul.left_factor_one with *, unit295    have prime := PrimeList.head with *296    have above := Prime.greater_than_one with prime297    rw one at above298    exact Less.irreflexive with *, above299300-- Uniqueness: two lists of primes with the same product have the same counts.301theorem primeFactorization.unique (xs : List(ℕ))302  shows ∀ ys, List(ℕ, ys) → PrimeList(xs) → PrimeList(ys) →303    ∏ xs = ∏ ys →304    ∀ q, Nat(q) → multiplicity(q, xs) = multiplicity(q, ys)305proof306  induction xs307  | List.nil =>308    intros ys ysList primesXs primesYs equal309    rw listProduct.nil at equal310    symm at equal311    have zero := listProduct.one at ys with *312    intros q qNat313    have empty := multiplicity.nil at q with *314    have count := zero with q, qNat315    rw [empty, count]316    rfl317  | List.cons(x, rest) using ih =>318    intros ys ysList primesXs primesYs equal319    have primeX := PrimeList.head at x, rest with *320    have primesRest := PrimeList.tail at x, rest with *321    have e1 := listProduct.cons at x, rest with *322    rw e1 at equal323    have self := divides.reflexive at x with *324    have dividesYs : x ∣ ∏ ys325      rw ← equal326      exact divides.multiply_right at x, x, ∏ rest with *327    obtain ⟨y, yNat, yPositive, dividesY⟩ := Prime.divides_listProduct at x, ys with *, dividesYs328    have primeY : Prime(y) by exact primesYs with y, yNat, yPositive329    have same := Prime.divides_prime at x, y with *330    rw ← same at yPositive331    obtain ⟨zs, zsList, product, counts⟩ := multiplicity.remove at x, ys with *, yPositive332    have e2 := listProduct.cons at x, zs with *333    rw e2 at product334    rw product at equal335    have xNonzero := Prime.nonzero at x with *336    have restEqual := mul.left_cancel_positive at ∏ rest, ∏ zs, x with *337    have primesZs : PrimeList(zs)338      intros q qNat positive339      have count := counts with q, qNat340      have lifted := multiplicity.positive_cons at q, x, zs with *341      rw ← count at lifted342      exact primesYs with q, qNat, lifted343    have inner := ih with zs, zsList, primesRest, primesZs, restEqual344    intros q qNat345    have count := counts with q, qNat346    have c1 := multiplicity.cons at q, x, rest with *347    have c2 := multiplicity.cons at q, x, zs with *348    have innerCount := inner with q, qNat349    rw [count, c1, c2, innerCount]350    rfl351352-- Existence, by strong induction: a prime divisor splits off a smaller cofactor.353lemma primeFactorization.exists_membership (m : Set)354  shows Nat(m) → m ≠ 0 → ∃ xs, List(ℕ, xs) ∧ PrimeList(xs) ∧ ∏ xs = m355proof356  induction m using membership357  intros current ih currentNat nonzero358  have shape := natural.zero_one_or_above_one with *359  rcases shape with zero | one | above360  . exfalso361    exact nonzero with zero362  . have nilList : List(ℕ, [])363      typecheck364    refine ⟨[], nilList, PrimeList.nil, ?_⟩365    rw one366    exact listProduct.nil367  . have oneLess := Less.of_membership at 1, current with *, above368    obtain ⟨p, primeP, dividesP⟩ := natural.exists_prime_divisor at current with *369    obtain ⟨k, kNat, equation⟩ := dividesP370    have kNonzero : k ≠ 0371      intro kZero372      rw kZero at equation373      have annihilated := mul.right_zero at p with *374      rw annihilated at equation375      symm at equation376      exact nonzero with equation377    have aboveOne := Prime.greater_than_one with *378    have smaller : k < current379      have scaled := Less.mul_left at 1, p, k with *380      have unit := mul.right_unit at k with *381      have commuted := mul.commutative at p, k with *382      rwa [unit, commuted, equation] at scaled383    have member := membership.of_Less at k, current with *, smaller384    obtain ⟨xs, xsList, primes, product⟩ := ih with k, member, kNat, kNonzero385    have consList : List(ℕ, p :: xs) by typecheck386    have consPrimes := PrimeList.cons with *387    refine ⟨p :: xs, consList, consPrimes, ?_⟩388    have e := listProduct.cons at p, xs with *389    rwa [e, product]390391theorem primeFactorization.exists (n : Nat)392  requires nonzero : n ≠ 0393  shows ∃ xs, List(ℕ, xs) ∧ PrimeList(xs) ∧ ∏ xs = n394proof395  have natural : Nat(n) by assumption396  exact primeFactorization.exists_membership with natural, nonzero397398-- The fundamental theorem of arithmetic: every positive natural number is a399-- product of primes, and any two such products use each prime the same number400-- of times.401theorem primeFactorization.fundamental_theorem (n : Nat)402  requires nonzero : n ≠ 0403  shows (∃ xs, List(ℕ, xs) ∧ PrimeList(xs) ∧ ∏ xs = n) ∧404    (∀ xs, List(ℕ, xs) → ∀ ys, List(ℕ, ys) → PrimeList(xs) → PrimeList(ys) →405      ∏ xs = n → ∏ ys = n →406      ∀ q, Nat(q) → multiplicity(q, xs) = multiplicity(q, ys))407proof408  constructor409  . exact primeFactorization.exists with *410  . intros xs xsList ys ysList primesXs primesYs productXs productYs411    have equal : ∏ xs = ∏ ys412      rw [productXs, productYs]413      rfl414    have unique := primeFactorization.unique at xs with *415    exact unique with ys, ysList, primesXs, primesYs, equal416