refactor(data/nat/factorization): Use factorization instead of factors.count (#11384)

Refactor to use `factorization` over `factors.count`, and adjust lemmas to be stated in terms of the former instead.



Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com>

Author: 3 people

src/algebra/is_prime_pow.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import algebra.associated
 import data.nat.factorization
+import number_theory.divisors
 
 /-!
 # Prime powers
@@ -104,7 +105,7 @@ lemma is_prime_pow_of_min_fac_pow_factorization_eq {n : ℕ}
   (h : n.min_fac ^ n.factorization n.min_fac = n) (hn : n ≠ 1) :
   is_prime_pow n :=
 begin
-  rcases n.eq_zero_or_pos with rfl | hn',
+  rcases eq_or_ne n 0 with rfl | hn',
   { simpa using h },
   refine ⟨_, _, nat.prime_iff.1 (nat.min_fac_prime hn), _, h⟩,
   rw [pos_iff_ne_zero, ←finsupp.mem_support_iff, nat.factor_iff_mem_factorization,
@@ -142,21 +143,19 @@ begin
     exact (nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq') },
   rintro ⟨p, ⟨hp, hn⟩, hq⟩,
   -- Take care of the n = 0 case
-  rcases n.eq_zero_or_pos with rfl | hn₀,
+  rcases eq_or_ne n 0 with rfl | hn₀,
   { obtain ⟨q, hq', hq''⟩ := nat.exists_infinite_primes (p + 1),
     cases hq q ⟨hq'', by simp⟩,
     simpa using hq' },
   -- So assume 0 < n
-  refine ⟨p, n.factors.count p, hp, _, _⟩,
-  { apply list.count_pos.2,
-    rwa nat.mem_factors_iff_dvd hn₀ hp },
+  refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, _⟩,
   simp only [and_imp] at hq,
-  apply nat.dvd_antisymm (nat.pow_factors_count_dvd _ _),
-  -- We need to show n ∣ p ^ n.factors.count p
-  apply nat.dvd_of_factors_subperm hn₀.ne',
+  apply nat.dvd_antisymm (nat.pow_factorization_dvd _ _),
+  -- We need to show n ∣ p ^ n.factorization p
+  apply nat.dvd_of_factors_subperm hn₀,
   rw [hp.factors_pow, list.subperm_ext_iff],
   intros q hq',
-  rw nat.mem_factors hn₀.ne' at hq',
+  rw nat.mem_factors hn₀ at hq',
   cases hq _ hq'.1 hq'.2,
   simp,
 end

src/data/nat/factorization.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stuart Presnell
 -/
 import data.nat.prime
-import data.nat.mul_ind
+import data.finsupp.multiset
 import algebra.big_operators.finsupp
 
 /-!
@@ -30,6 +30,8 @@ and (where appropriate) choose a uniform canonical way of expressing these ideas
 with a normalization function, and then deduplicated.  The basics of this have been started in
 `ring_theory/unique_factorization_domain`.
 
+* Extend the inductions to any `normalization_monoid` with unique factorization.
+
 -/
 
 open nat finset list finsupp
@@ -44,38 +46,38 @@ noncomputable def factorization (n : ℕ) : ℕ →₀ ℕ := (n.factors : multi
 @[simp] lemma factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : n.factorization.prod pow = n :=
 begin
   simp only [←prod_to_multiset, factorization, multiset.coe_prod, multiset.to_finsupp_to_multiset],
-  exact prod_factors hn.bot_lt,
+  exact prod_factors hn,
 end
 
-lemma factorization_eq_count {n p : ℕ} : n.factorization p = n.factors.count p :=
+@[simp] lemma factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p :=
 by simp [factorization]
--- TODO: As part of the unification mentioned in the TODO above,
--- consider making this a [simp] lemma from `n.factors.count` to `n.factorization`
+
+lemma eq_of_factorization_eq {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
+  (h : ∀ p : ℕ, a.factorization p = b.factorization p) : a = b :=
+eq_of_perm_factors ha hb (by simpa only [list.perm_iff_count, factors_count_eq] using h)
 
 /-- Every nonzero natural number has a unique prime factorization -/
 lemma factorization_inj : set.inj_on factorization { x : ℕ | x ≠ 0 } :=
-λ a ha b hb h, eq_of_count_factors_eq
-  (zero_lt_iff.mpr ha) (zero_lt_iff.mpr hb) (λ p, by simp [←factorization_eq_count, h])
+λ a ha b hb h, eq_of_factorization_eq ha hb (λ p, by simp [h])
 
-@[simp] lemma factorization_zero : factorization 0 = 0  :=
+@[simp] lemma factorization_zero : factorization 0 = 0 :=
 by simp [factorization]
 
 @[simp] lemma factorization_one : factorization 1 = 0 :=
 by simp [factorization]
 
 /-- The support of `n.factorization` is exactly `n.factors.to_finset` -/
-@[simp] lemma support_factorization {n : ℕ} :
-  n.factorization.support = n.factors.to_finset :=
+@[simp] lemma support_factorization {n : ℕ} : n.factorization.support = n.factors.to_finset :=
 by simpa [factorization, multiset.to_finsupp_support]
 
 lemma factor_iff_mem_factorization {n p : ℕ} : p ∈ n.factorization.support ↔ p ∈ n.factors :=
 by simp only [support_factorization, list.mem_to_finset]
 
 lemma prime_of_mem_factorization {n p : ℕ} : p ∈ n.factorization.support → p.prime :=
-(@prime_of_mem_factors n p) ∘ (@factor_iff_mem_factorization n p).mp
+prime_of_mem_factors ∘ (@factor_iff_mem_factorization n p).mp
 
 lemma pos_of_mem_factorization {n p : ℕ} : p ∈ n.factorization.support → 0 < p :=
-(@prime.pos p) ∘ (@prime_of_mem_factorization n p)
+prime.pos ∘ (@prime_of_mem_factorization n p)
 
 lemma factorization_eq_zero_of_non_prime (n p : ℕ) (hp : ¬p.prime) : n.factorization p = 0 :=
 not_mem_support_iff.1 (mt prime_of_mem_factorization hp)
@@ -87,27 +89,79 @@ by simp [factorization, add_equiv.map_eq_zero_iff, multiset.coe_eq_zero]
 /-- For nonzero `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
 @[simp] lemma factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
   (a * b).factorization = a.factorization + b.factorization :=
-by { ext p, simp only [add_apply, factorization_eq_count,
-  count_factors_mul_of_pos (zero_lt_iff.mpr ha) (zero_lt_iff.mpr hb)] }
+by { ext p, simp only [add_apply, ←factors_count_eq,
+                       perm_iff_count.mp (perm_factors_mul ha hb) p, count_append] }
 
 /-- For any `p`, the power of `p` in `n^k` is `k` times the power in `n` -/
-lemma factorization_pow {n k : ℕ} :
+@[simp] lemma factorization_pow (n k : ℕ) :
   factorization (n^k) = k • n.factorization :=
-by { ext p, simp [factorization_eq_count, factors_count_pow] }
+begin
+  induction k with k ih,
+  { simp },
+  rcases n.eq_zero_or_pos with rfl | hn,
+  { simp },
+  rw [pow_succ, factorization_mul hn.ne' (pow_ne_zero _ hn.ne'), ih, succ_eq_one_add, add_smul,
+    one_smul],
+end
+
+/-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
+lemma factorization_mul_apply_of_coprime {p a b : ℕ} (hab : coprime a b)  :
+  (a * b).factorization p = a.factorization p + b.factorization p :=
+by simp only [←factors_count_eq, perm_iff_count.mp (perm_factors_mul_of_coprime hab), count_append]
+
+/-- If `p` is a prime factor of `a` then the power of `p` in `a` is the same that in `a * b`,
+for any `b` coprime to `a`. -/
+lemma factorization_eq_of_coprime_left {p a b : ℕ} (hab : coprime a b) (hpa : p ∈ a.factors) :
+  (a * b).factorization p = a.factorization p :=
+begin
+  rw [factorization_mul_apply_of_coprime hab, ←factors_count_eq, ←factors_count_eq],
+  simpa only [count_eq_zero_of_not_mem (coprime_factors_disjoint hab hpa)],
+end
+
+/-- If `p` is a prime factor of `b` then the power of `p` in `b` is the same that in `a * b`,
+for any `a` coprime to `b`. -/
+lemma factorization_eq_of_coprime_right {p a b : ℕ} (hab : coprime a b) (hpb : p ∈ b.factors) :
+  (a * b).factorization p = b.factorization p :=
+by { rw mul_comm, exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb }
+
+lemma pow_factorization_dvd (n p : ℕ) : p ^ n.factorization p ∣ n :=
+begin
+  rw ←factors_count_eq,
+  by_cases hp : p.prime,
+  { apply dvd_of_factors_subperm (pow_ne_zero _ hp.ne_zero),
+    rw [hp.factors_pow, list.subperm_ext_iff],
+    intros q hq,
+    simp [list.eq_of_mem_repeat hq] },
+  { rw count_eq_zero_of_not_mem (mt prime_of_mem_factors hp),
+    simp },
+end
+
+lemma pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : p.prime) :
+  ¬ p ^ (n.factorization p + 1) ∣ n :=
+begin
+  intro h,
+  have := factors_sublist_of_dvd h hn,
+  rw [hp.factors_pow, ←le_count_iff_repeat_sublist, factors_count_eq] at this,
+  linarith
+end
+
+lemma prime.factorization_pos_of_dvd {n p : ℕ} (hp : p.prime) (hn : n ≠ 0) (h : p ∣ n) :
+  0 < n.factorization p :=
+by rwa [←factors_count_eq, count_pos, mem_factors_iff_dvd hn hp]
 
 /-- The only prime factor of prime `p` is `p` itself, with multiplicity `1` -/
 @[simp] lemma prime.factorization {p : ℕ} (hp : prime p) :
   p.factorization = single p 1 :=
 begin
   ext q,
-  rw [factorization_eq_count, factors_prime hp, single_apply, count_singleton', if_congr eq_comm];
+  rw [←factors_count_eq, factors_prime hp, single_apply, count_singleton', if_congr eq_comm];
   refl,
 end
 
 /-- For prime `p` the only prime factor of `p^k` is `p` with multiplicity `k` -/
-@[simp] lemma prime.factorization_pow {p k : ℕ} (hp : prime p) :
-  factorization (p^k) = single p k :=
-by simp [factorization_pow, hp.factorization]
+lemma prime.factorization_pow {p k : ℕ} (hp : prime p) :
+  factorization (p ^ k) = single p k :=
+by simp [hp]
 
 /-- For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : finset α`,
 the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`.
@@ -169,7 +223,7 @@ lemma factorization_mul_of_coprime {a b : ℕ} (hab : coprime a b) :
   (a * b).factorization = a.factorization + b.factorization :=
 begin
   ext q,
-  simp only [finsupp.coe_add, add_apply, factorization_eq_count, count_factors_mul_of_coprime hab],
+  simp only [finsupp.coe_add, add_apply, ←factors_count_eq, factorization_mul_apply_of_coprime hab],
 end
 
 /-- For coprime `a` and `b` the prime factorization `a * b` is the union of those of `a` and `b` -/
@@ -185,9 +239,72 @@ lemma factorization_mul_support {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
 begin
   ext q,
   simp only [finset.mem_union, factor_iff_mem_factorization],
-  rw mem_factors_mul ha hb,
+  exact mem_factors_mul ha hb
 end
 
+/-- Given `P 0, P 1` and a way to extend `P a` to `P (p ^ k * a)`,
+you can define `P` for all natural numbers. -/
+@[elab_as_eliminator]
+def rec_on_prime_pow {P : ℕ → Sort*} (h0 : P 0) (h1 : P 1)
+  (h : ∀ a p n : ℕ, p.prime → ¬ p ∣ a → P a → P (p ^ n * a)) : ∀ (a : ℕ), P a :=
+λ a, nat.strong_rec_on a $ λ n,
+  match n with
+  | 0     := λ _, h0
+  | 1     := λ _, h1
+  | (k+2) := λ hk, begin
+    let p := (k + 2).min_fac,
+    have hp : prime p := min_fac_prime (succ_succ_ne_one k),
+    -- the awkward `let` stuff here is because `factorization` is noncomputable (finsupp);
+    -- we get around this by using the computable `factors.count`, and rewriting when we want
+    -- to use the `factorization` API
+    let t := (k+2).factors.count p,
+    have ht : t = (k+2).factorization p := factors_count_eq,
+    have hpt : p ^ t ∣ k + 2 := by { rw ht, exact pow_factorization_dvd _ _ },
+    have htp : 0 < t :=
+    by { rw ht,
+         exact hp.factorization_pos_of_dvd (nat.succ_ne_zero (k + 1)) (min_fac_dvd _) },
+
+    convert h ((k + 2) / p ^ t) p t hp _ _,
+    { rw nat.mul_div_cancel' hpt },
+    { rw [nat.dvd_div_iff hpt, ←pow_succ', ht],
+      exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp },
+
+    apply hk _ (nat.div_lt_of_lt_mul _),
+    rw [lt_mul_iff_one_lt_left nat.succ_pos', one_lt_pow_iff htp.ne],
+    exact hp.one_lt
+    end
+  end
+
+/-- Given `P 0`, `P 1`, and `P (p ^ k)` for positive prime powers, and a way to extend `P a` and
+`P b` to `P (a * b)` when `a, b` are coprime, you can define `P` for all natural numbers. -/
+@[elab_as_eliminator]
+def rec_on_pos_prime_coprime {P : ℕ → Sort*} (hp : ∀ p n : ℕ, prime p → 0 < n → P (p ^ n))
+  (h0 : P 0) (h1 : P 1) (h : ∀ a b, 0 < a → 0 < b → coprime a b → P a → P b → P (a * b)) :
+  ∀ a, P a :=
+rec_on_prime_pow h0 h1 $ λ a p n hp' hpa ha,
+  (h (p ^ n) a (pow_pos hp'.pos _) (nat.pos_of_ne_zero (λ t, by simpa [t] using hpa))
+  (prime.coprime_pow_of_not_dvd hp' hpa).symm
+  (if h : n = 0 then eq.rec h1 h.symm else hp p n hp' $ nat.pos_of_ne_zero h) ha)
+
+/-- Given `P 0`, `P (p ^ k)` for all prime powers, and a way to extend `P a` and `P b` to
+`P (a * b)` when `a, b` are coprime, you can define `P` for all natural numbers. -/
+@[elab_as_eliminator]
+def rec_on_prime_coprime {P : ℕ → Sort*} (h0 : P 0) (hp : ∀ p n : ℕ, prime p → P (p ^ n))
+  (h : ∀ a b, 0 < a → 0 < b → coprime a b → P a → P b → P (a * b)) : ∀ a, P a :=
+rec_on_pos_prime_coprime (λ p n h _, hp p n h) h0 (hp 2 0 prime_two) h
+
+/-- Given `P 0`, `P 1`, `P p` for all primes, and a proof that you can extend
+`P a` and `P b` to `P (a * b)`, you can define `P` for all natural numbers. -/
+@[elab_as_eliminator]
+def rec_on_mul {P : ℕ → Sort*} (h0 : P 0) (h1 : P 1)
+  (hp : ∀ p, prime p → P p) (h : ∀ a b, P a → P b → P (a * b)) : ∀ a, P a :=
+let hp : ∀ p n : ℕ, prime p → P (p ^ n) :=
+  λ p n hp', match n with
+  | 0     := h1
+  | (n+1) := by exact h _ _ (hp p hp') (_match _)
+  end in
+rec_on_prime_coprime h0 hp $ λ a b _ _ _, h a b
+
 /-- For any multiplicative function `f` with `f 1 = 1` and any `n > 0`,
 we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n` -/
 lemma multiplicative_factorization {β : Type*} [comm_monoid β] (f : ℕ → β)
@@ -233,6 +350,29 @@ begin
   { rintro ⟨c, rfl⟩, rw factorization_mul hd (right_ne_zero_of_mul hn), simp },
 end
 
+lemma dvd_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) : p ∣ n :=
+begin
+  rcases eq_or_ne p 0 with rfl | hp,
+  { rw [nat.support_factorization, list.mem_to_finset] at h,
+    exact absurd (nat.prime_of_mem_factors h) (nat.not_prime_zero) },
+  apply nat.dvd_of_factors_subperm hp,
+  rw [nat.factors_prime $ nat.prime_of_mem_factorization h, list.subperm_singleton_iff],
+  rwa ←nat.factor_iff_mem_factorization,
+end
+
+lemma factorization_le_factorization_mul_left {a b : ℕ} (hb : b ≠ 0) :
+  a.factorization ≤ (a * b).factorization :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha,
+  { simp },
+  rw [factorization_le_iff_dvd ha $ mul_ne_zero ha hb],
+  exact dvd.intro b rfl
+end
+
+lemma factorization_le_factorization_mul_right {a b : ℕ} (ha : a ≠ 0) :
+  b.factorization ≤ (a * b).factorization :=
+by { rw mul_comm, apply factorization_le_factorization_mul_left ha }
+
 lemma prime.pow_dvd_iff_le_factorization {p k n : ℕ} (pp : prime p) (hn : n ≠ 0) :
   p ^ k ∣ n ↔ k ≤ n.factorization p :=
 by rw [←factorization_le_iff_dvd (pow_pos pp.pos k).ne' hn, pp.factorization_pow, single_le_iff]
@@ -250,51 +390,49 @@ begin
   exact le_of_dvd ha.bot_lt hab,
 end
 
-@[simp]
-lemma div_factorization_eq_tsub_of_dvd {d n : ℕ} (hn : n ≠ 0) (h : d ∣ n) :
+@[simp] lemma factorization_div {d n : ℕ} (h : d ∣ n) :
   (n / d).factorization = n.factorization - d.factorization :=
 begin
-  have hd : d ≠ 0 := ne_zero_of_dvd_ne_zero hn h,
-  cases dvd_iff_exists_eq_mul_left.mp h with c hc,
-  have hc_pos : c ≠ 0, { subst hc, exact left_ne_zero_of_mul hn },
-  rw [hc, nat.mul_div_cancel c hd.bot_lt, factorization_mul hc_pos hd, add_tsub_cancel_right],
+  rcases eq_or_ne d 0 with rfl | hd,
+  { rw zero_dvd_iff at h,
+    subst h,
+    simp },
+  rcases eq_or_ne n 0 with rfl | hn,
+  { simp },
+  apply add_left_injective d.factorization,
+  simp only,
+  symmetry,
+  rw [tsub_add_cancel_of_le $ (nat.factorization_le_iff_dvd hd hn).mpr h],
+  nth_rewrite 0 ←nat.div_mul_cancel h,
+  exact nat.factorization_mul (nat.div_pos (nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
 end
 
 lemma dvd_iff_div_factorization_eq_tsub (d n : ℕ) (hd : d ≠ 0) (hdn : d ≤ n) :
   d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization :=
 begin
-  have hn : n ≠ 0 := (lt_of_lt_of_le hd.bot_lt hdn).ne.symm,
-  refine ⟨div_factorization_eq_tsub_of_dvd hn, _⟩,
-  { rcases eq_or_lt_of_le hdn with rfl | hd_lt_n, { simp },
-    have h1 : n / d ≠ 0 := λ H, nat.lt_asymm hd_lt_n ((nat.div_eq_zero_iff hd.bot_lt).mp H),
-    intros h,
-    rw dvd_iff_le_div_mul n d,
-    by_contra h2,
-    cases (exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)) with p hp,
-    rwa [factorization_mul h1 hd, add_apply, ←lt_tsub_iff_right, h, tsub_apply,
-      lt_self_iff_false] at hp },
-end
-
-lemma pow_factorization_dvd (p d : ℕ) : p ^ d.factorization p ∣ d :=
-begin
-  rcases eq_or_ne d 0 with rfl | hd, { simp },
-  by_cases pp : prime p,
-  { rw pp.pow_dvd_iff_le_factorization hd },
-  { rw factorization_eq_zero_of_non_prime d p pp, simp },
+  refine ⟨factorization_div, _⟩,
+  rcases eq_or_lt_of_le hdn with rfl | hd_lt_n, { simp },
+  have h1 : n / d ≠ 0 := λ H, nat.lt_asymm hd_lt_n ((nat.div_eq_zero_iff hd.bot_lt).mp H),
+  intros h,
+  rw dvd_iff_le_div_mul n d,
+  by_contra h2,
+  cases (exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)) with p hp,
+  rwa [factorization_mul h1 hd, add_apply, ←lt_tsub_iff_right, h, tsub_apply,
+    lt_self_iff_false] at hp
 end
 
 lemma dvd_iff_prime_pow_dvd_dvd {n d : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
-  d ∣ n ↔ ∀ p k : ℕ, prime p → p^k ∣ d → p^k ∣ n :=
+  d ∣ n ↔ ∀ p k : ℕ, prime p → p ^ k ∣ d → p ^ k ∣ n :=
 begin
   split,
   { exact λ h p k pp hpkd, dvd_trans hpkd h },
   { intros h,
     rw [←factorization_le_iff_dvd hd hn, finsupp.le_def],
     intros p,
     by_cases pp : prime p, swap,
-    { rw factorization_eq_zero_of_non_prime d p pp, exact zero_le' },
+    { rw factorization_eq_zero_of_non_prime d p pp, exact nat.zero_le _ },
     rw ←pp.pow_dvd_iff_le_factorization hn,
-    exact h p _ pp (pow_factorization_dvd p _) },
+    exact h p _ pp (pow_factorization_dvd _ _) },
 end
 
 end nat